Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
bb4e54da
Commit
bb4e54da
authored
Mar 14, 2016
by
MARCHE Claude
Browse files
driver Z3 4.3.2: should not use native BV theory at all
parent
e5a3c677
Changes
2
Hide whitespace changes
Inline
Side-by-side
drivers/z3_432.drv
View file @
bb4e54da
...
...
@@ -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
share/provers-detection-data.conf
View file @
bb4e54da
...
...
@@ -355,7 +355,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
=
"%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment