let constructInvariants () =
  let readAndAddInvariants filename =
    let doParse inchan =
      let _ = VampyreErrormsg.startFile filename in
      let lexbuf = Lexing.from_channel inchan in
      let _ = VampyreErrormsg.theLexbuf := lexbuf in
      Inputparse.main Inputflex.token lexbuf 
    in
    ignore (Message.msg_string Message.Normal "Reading in invariants...");
    try
      let inchan = open_in filename
      in
      let a = doParse inchan
      in
      ignore (Message.msg_string Message.Normal "Invariants read.\n") ;
      List.iter (fun a -> Message.msg_string Message.Normal (Predicate.toString a)) a ;
       a
    with
      Sys_error _ -> (Message.msg_string Message.Error ("Cannot find invariant information in "^filename^".\n"); [])
    | VampyreErrormsg.Error -> (Message.msg_string Message.Error ("Error raised in reading invariants.\n"); [])
  in
  let invFile = Options.getValueOfString "inv" in
  if (invFile = "") then
    (* Nothing to do *)
    []
  else
    readAndAddInvariants invFile