From d575a6a842dd8da923286afb5eff1ad66e8fe4ed Mon Sep 17 00:00:00 2001 From: Johannes Blaser Date: Wed, 29 Jan 2025 15:58:31 +0100 Subject: [PATCH 1/2] Reverted removal of Z3 version check fix which breaks when Z3 binaries output additional information after the version number when calling z3 --version --- src/smtencoding/FStarC.SMTEncoding.Z3.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index a20469feddb..4969be078c4 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -176,7 +176,7 @@ let check_z3version (p:proc) : unit = ); _already_warned_solver_mismatch := true ); - let ver_found : string = BU.trim_string (getinfo "version") in + 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 ( let open FStarC.Errors in From dde3d94ec632bed11bdaf74e3871a3cfbce04254 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 30 Jan 2025 08:56:27 -0800 Subject: [PATCH 2/2] Z3: add a comment about version checking --- src/smtencoding/FStarC.SMTEncoding.Z3.fst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index 4969be078c4..9652190e69b 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -176,6 +176,11 @@ let check_z3version (p:proc) : unit = ); _already_warned_solver_mismatch := true ); + (* Note: Z3 can either output a "clean" version like 4.13.4 or something like + "4.13.4 - build hashcode 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571" depending + on how it was built. Hence we split by "-" and take the first component to + ignore the hashcode. See https://github.com/FStarLang/FStar/pull/3700 for + more details. *) 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 (