Commit 851f55d9 authored by MARCHE Claude's avatar MARCHE Claude

Support for Z3 4.3.[0-1] and Gappa 0.16.[2-4]

parent 1ae79454
* marks an incompatible change
o [prover] support for Z3 4.3.*
o [prover] fixed Coq 8.4 support for theory real.Trigonometry
o [prover] support for CVC4
o [prover] support for mathematica
......
......@@ -78,16 +78,19 @@ scheduled on ? 2012
== New Features to announce ==
o
o [why3ide] allow several files on the command-line
o [ocaml API] incompatible changes in Set/Map/Hashtbl modules
o [prover] fixed Coq 8.4 support for theory real.Trigonometry
o [prover] support for Z3 4.2
o [prover] support for Gappa 0.16.4
o [prover] support for Z3 4.2, 4.3.*
o [prover] support for Alt-Ergo 0.95
o [prover] support for CVC4
o [stdlib] fixed inconsistency in map.MapPermut theory
o [prover] support of PVS 6
o [prover] support for mathematica
o [prover] support for MathSAT5
o [prover] support for PVS 6
o [prover] experimental support for mathematica
o [prover] experimental support for MathSAT5
o [examples] several new examples, including solutions to the
VerifyThis@fm2012 challenges
== Final preparation ==
......
......@@ -146,48 +146,12 @@ name = "Gappa"
exec = "gappa"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "^0.16.[0-1]$"
version_ok = "^0\.16\.[0-4]$"
version_ok = "^0\.1[4-5]\..+$"
version_old = "^0\.1[1-2]\..+$"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa]
name = "Gappa+dev"
exec = "gappa-0.16.0+dev"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.16.0"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa]
name = "Gappa"
exec = "gappa-0.16.0"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.16.0"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa]
name = "Gappa"
exec = "gappa-0.15.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.15.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa]
name = "Gappa"
exec = "gappa-0.14.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.14.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
......@@ -243,12 +207,16 @@ driver = "drivers/verit.drv"
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.3.1"
exec = "z3-4.3.0"
exec = "z3-4.2"
exec = "z3-4.1.2"
exec = "z3-4.1.1"
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.3.1"
version_ok = "4.3.0"
version_ok = "4.2"
version_ok = "4.1.2"
version_ok = "4.1.1"
......
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