Support for Z3 4.7.1

CHANGES.md

@@ -36,6 +36,7 @@ Provers
   * support for Alt-Ergo 2.2.0 (released Apr 26, 2018)
   * support for Coq 8.8.1 (released Jun 29, 2018)
   * support for CVC4 1.6 (released Jun 25, 2018)
+  * support for Z3 4.7.1 (released May 23, 2018)
   * support for Isabelle 2018 (released Aug 2018)
     [Contribution Stefan Berghofer <stefan.berghofer@secunet.com>]
   * dropped support for Isabelle 2016 (2017 still supported) :x:

examples/logic/genealogy/why3session.xml

@@ -16,6 +16,7 @@
 <prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="0" memlimit="1000"/>
 <prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
+<prover id="14" name="Z3" version="4.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="18" name="PVS" version="6.0" timelimit="5" steplimit="0" memlimit="4000"/>
@@ -47,6 +48,7 @@
  <proof prover="9"><result status="valid" time="0.01"/></proof>
  <proof prover="11"><result status="valid" time="0.00"/></proof>
  <proof prover="13"><result status="valid" time="0.04"/></proof>
+ <proof prover="14"><result status="valid" time="0.02"/></proof>
  <proof prover="15"><result status="valid" time="0.02"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="18" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"><result status="valid" time="0.24"/></proof>
@@ -77,6 +79,7 @@
  <proof prover="10"><result status="valid" time="0.02"/></proof>
  <proof prover="11"><result status="valid" time="0.00"/></proof>
  <proof prover="12"><result status="valid" time="0.00"/></proof>
+ <proof prover="14"><result status="valid" time="0.02"/></proof>
  <proof prover="15"><result status="valid" time="0.12"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="19"><result status="valid" time="0.00"/></proof>
@@ -105,6 +108,7 @@
  <proof prover="9"><result status="valid" time="0.01"/></proof>
  <proof prover="11"><result status="valid" time="0.00"/></proof>
  <proof prover="13"><result status="valid" time="0.03"/></proof>
+ <proof prover="14"><result status="valid" time="0.02"/></proof>
  <proof prover="15"><result status="valid" time="0.04"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="19"><result status="valid" time="0.00"/></proof>
@@ -132,6 +136,7 @@
  <proof prover="10"><result status="valid" time="0.03"/></proof>
  <proof prover="11"><result status="valid" time="0.00"/></proof>
  <proof prover="12"><result status="valid" time="0.04"/></proof>
+ <proof prover="14"><result status="valid" time="0.02"/></proof>
  <proof prover="15"><result status="valid" time="0.07"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="19"><result status="valid" time="0.00"/></proof>
@@ -161,6 +166,7 @@
  <proof prover="10"><result status="valid" time="0.03"/></proof>
  <proof prover="11"><result status="valid" time="0.00"/></proof>
  <proof prover="12"><result status="valid" time="0.02"/></proof>
+ <proof prover="14"><result status="valid" time="0.02"/></proof>
  <proof prover="15"><result status="valid" time="0.03"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="19"><result status="valid" time="0.00"/></proof>
@@ -189,6 +195,7 @@
  <proof prover="10"><result status="valid" time="0.03"/></proof>
  <proof prover="11"><result status="valid" time="0.01"/></proof>
  <proof prover="12"><result status="valid" time="0.03"/></proof>
+ <proof prover="14"><result status="valid" time="0.01"/></proof>
  <proof prover="15"><result status="valid" time="0.03"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="19"><result status="valid" time="0.00"/></proof>
@@ -217,6 +224,7 @@
  <proof prover="10"><result status="valid" time="0.03"/></proof>
  <proof prover="11"><result status="valid" time="0.00"/></proof>
  <proof prover="12"><result status="valid" time="0.00"/></proof>
+ <proof prover="14"><result status="valid" time="0.01"/></proof>
  <proof prover="15"><result status="valid" time="0.05"/></proof>
  <proof prover="16"><result status="valid" time="0.01"/></proof>
  <proof prover="19"><result status="valid" time="0.00"/></proof>

share/provers-detection-data.conf

@@ -369,12 +369,14 @@ version_old = "201310"
 name = "Z3"
 alternative = "counterexamples"
 exec = "z3"
+exec = "z3-4.7.1"
 exec = "z3-4.6.0"
 exec = "z3-4.5.0"
 exec = "z3-4.4.1"
 exec = "z3-4.4.0"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok  = "4.7.1"
 version_ok  = "4.6.0"
 version_ok  = "4.5.0"
 version_old  = "4.4.1"
@@ -388,12 +390,14 @@ command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_se
 [ATP z3]
 name = "Z3"
 exec = "z3"
+exec = "z3-4.7.1"
 exec = "z3-4.6.0"
 exec = "z3-4.5.0"
 exec = "z3-4.4.1"
 exec = "z3-4.4.0"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok  = "4.7.1"
 version_ok  = "4.6.0"
 version_ok  = "4.5.0"
 version_old  = "4.4.1"
@@ -408,12 +412,14 @@ use_at_auto_level = 1
 name = "Z3"
 alternative = "noBV"
 exec = "z3"
+exec = "z3-4.7.1"
 exec = "z3-4.6.0"
 exec = "z3-4.5.0"
 exec = "z3-4.4.1"
 exec = "z3-4.4.0"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok  = "4.7.1"
 version_ok  = "4.6.0"
 version_ok  = "4.5.0"
 version_old  = "4.4.1"