Fix monomorpisation tests with typechecker changes

Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues

1 files changed, 23 insertions, 7 deletions

diff --git a/src/constraint.ml b/src/constraint.ml
index b00c0a4e..af024ce3 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -208,12 +208,21 @@ let call_z3' l vars constraints : smt_result =
   with
   | Not_found ->
     begin
-      let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
+      let (input_file, tmp_chan) =
+        try Filename.open_temp_file "constraint_" ".sat" with
+        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling Z3: " ^ msg))
+      in
       output_string tmp_chan z3_file;
       close_out tmp_chan;
-      let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-      let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
-      let _ = Unix.close_process_in z3_chan in
+      let z3_output =
+        try
+          let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+          let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
+          let _ = Unix.close_process_in z3_chan in
+          z3_output
+        with
+        | exn -> raise (Reporting.err_general l ("Error when calling z3: " ^ Printexc.to_string exn))
+      in
       Sys.remove input_file;
       try
         let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
@@ -250,9 +259,16 @@ let rec solve_z3 l vars constraints var =
   let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
   output_string tmp_chan z3_file;
   close_out tmp_chan;
-  let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-  let z3_output = String.concat " " (input_all z3_chan) in
-  let _ = Unix.close_process_in z3_chan in
+  let z3_output =
+    try
+      let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+      let z3_output = String.concat " " (input_all z3_chan) in
+      let _ = Unix.close_process_in z3_chan in
+      z3_output
+    with
+    | exn ->
+       raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn))
+  in
   Sys.remove input_file;
   let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in
   try