Merge pull request #3517 from mtzguido/z3errfix

A better error when z3 cannot be started
FStarLang · Oct 3, 2024 · 57b25e6 · 57b25e6
2 parents 55e1119 + ecbbb22
commit 57b25e6
Show file tree

Hide file tree

Showing 2 changed files with 54 additions and 5 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml
diff --git a/src/smtencoding/FStar.SMTEncoding.Z3.fst b/src/smtencoding/FStar.SMTEncoding.Z3.fst
@@ -232,7 +232,21 @@ let check_z3version (p:proc) : unit =
   ()
 
 let new_z3proc (id:string) (cmd_and_args : string & list string) : BU.proc =
-    let proc = BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!") in
+    let proc =
+      try
+        BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!")
+      with
+      | e ->
+        let open FStar.Pprint in
+        let open FStar.Errors.Msg in
+        Errors.raise_error0 Errors.Error_Z3InvocationError [
+          text "Could not start SMT solver process.";
+          prefix 2 1 (text "Command:" )
+            (fst cmd_and_args |> arbitrary_string |> squotes);
+          prefix 2 1 (text "Exception:")
+            (BU.print_exn e |> arbitrary_string);
+        ]
+    in
     check_z3version proc;
     proc
 
@@ -804,4 +818,4 @@ let ask
         just_ask ()
   in
   // pop "query";
-  result
+  result