Commit a8cfacb5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Support for Z3 4.4.0, released on Apr 29, 2015

See https://github.com/Z3Prover/z3/releases

Seems compatible with Z3 4.3.2
parent df70d354
......@@ -10,12 +10,13 @@ Encodings
format is direct
provers
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Isabelle 2015 (released May 25, 2015)
o support for Coq 8.4pl6 (released April 9, 2015)
o support for Gappa 1.2.0 (released May 19, 2015)
o discarded support for Alt-Ergo versions older than 0.95.2
o support for Coq 8.4pl6 (released Apr 9, 2015)
o support for Gappa 1.2.0 (released May 19, 2015)
o support for Isabelle 2015 (released May 25, 2015)
o support for Z3 4.4.0 (released Apr 29, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
Version 0.86.2, October 13, 2015
================================
......
......@@ -29,6 +29,7 @@
<prover id="24" name="veriT" version="201410" timelimit="5" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" memlimit="1000"/>
<prover id="27" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter" expanded="true">
......@@ -59,6 +60,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Sibling_sym" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -86,6 +88,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Sibling_is_brother_or_sister" expanded="true">
<proof prover="1"><result status="unknown" time="0.01"/></proof>
......@@ -113,6 +116,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.01"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -139,6 +143,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="38"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Grandfather_male" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -165,6 +170,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Grandmother_female" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -191,6 +197,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Only_two_grandfathers" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -217,6 +224,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -306,14 +306,15 @@ version_old = "201310"
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.3.3"
exec = "z3-4.4.0"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.3.3"
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"
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
[ATP z3]
name = "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