Commit e2c84cad authored by MARCHE Claude's avatar MARCHE Claude

Support for Z3 4.3.2

parent 04dc9c43
* marks an incompatible change
library
* renamed library int.NumOfParam into int.NumOf; the predicate numof
now takes some higher-order predicate as argument (no more need
for cloning). Similar change in modules array.NumOf...
provers
o support for Z3 4.3.2 (released Oct 25, 2014)
version 0.85, September 17, 2014
================================
......
This diff is collapsed.
......@@ -294,6 +294,18 @@ command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \
driver = "drivers/verit.drv"
version_ok = "201310"
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.3.2"
driver = "drivers/z3.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
[ATP z3]
name = "Z3"
exec = "z3"
......
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