Commit 3327989e authored by MARCHE Claude's avatar MARCHE Claude

driver Z3 4.3.2: should not use native BV theory at all

parent 52d9e192
......@@ -77,6 +77,8 @@ end
*)
(* REMOVED: we do not use BV theory from Z3 in 4.3.2 but starting from 4.4.0
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
......@@ -98,3 +100,5 @@ theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
*)
\ No newline at end of file
......@@ -359,7 +359,6 @@ name = "Z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.4.0"
version_ok = "4.3.2"
driver = "drivers/z3_432.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment