Merge pull request #3067 from Johanmyst/z3_version_check_fix

Fixed Z3 version check crash
FStarLang · Oct 17, 2023 · f7c80bf · f7c80bf
2 parents e2a4de3 + 6746733
commit f7c80bf
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 14 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
@@ -209,14 +209,15 @@ let check_z3version (p:proc) : unit =
         );
     _already_warned_solver_mismatch := true
   );
-  let ver = getinfo "version" in
-  if ver <> Options.z3_version () && not (!_already_warned_version_mismatch) then (
+  let ver_found : string = BU.trim_string (List.hd (BU.split (getinfo "version") "-")) in
+  let ver_conf  : string = BU.trim_string (Options.z3_version ()) in
+  if ver_conf <> ver_found && not (!_already_warned_version_mismatch) then (
     Errors.log_issue Range.dummyRange (Errors.Warning_SolverMismatch,
-      BU.format5 "Unexpected Z3 version for `%s': expected %s, got %s.\n\
+      BU.format5 "Unexpected Z3 version for `%s': expected `%s', got `%s'.\n\
                   Please download the correct version of Z3 from %s\n\
                   and install it into your $PATH as `%s'."
         (proc_prog p)
-        (Options.z3_version()) ver
+        ver_conf ver_found
         z3url (Platform.exe ("z3-" ^ Options.z3_version  ()))
         );
     _already_warned_version_mismatch := true