Commit 93650c62 authored by MARCHE Claude's avatar MARCHE Claude

update sessions affected by the add of a soft limit for Z3

parent 3b2e76db
......@@ -11,7 +11,7 @@
<prover id="6" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bv.why" expanded="true">
<theory name="CheckBV64" sum="02fb170f5e5286c25ede13463f9bf5ab" expanded="true">
<theory name="CheckBV64" sum="02fb170f5e5286c25ede13463f9bf5ab">
<goal name="ok_zero" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -232,19 +232,19 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="f1" expl="" expanded="true">
<goal name="f1" expl="">
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="6"><result status="timeout" time="1.01"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="1.00"/></proof>
</goal>
<goal name="g2" expl="">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="f2" expl="" expanded="true">
<goal name="f2" expl="">
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="1.00"/></proof>
</goal>
<goal name="g3" expl="">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -268,10 +268,10 @@
</goal>
</transf>
</goal>
<goal name="f3" expl="" expanded="true">
<goal name="f3" expl="">
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="1.00"/></proof>
</goal>
<goal name="g4a" expl="">
<proof prover="0"><result status="valid" time="0.06" steps="100"/></proof>
......@@ -300,10 +300,10 @@
<proof prover="3" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="f7" expl="" expanded="true">
<goal name="f7" expl="">
<proof prover="2" timelimit="1"><result status="unknown" time="0.02"/></proof>
<proof prover="6"><result status="timeout" time="0.99"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="1.00"/></proof>
</goal>
<goal name="g8a" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......
......@@ -186,17 +186,17 @@
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="unknown" time="0.25"/></proof>
<proof prover="11"><result status="unknown" time="0.25"/></proof>
<proof prover="11"><result status="unknown" time="0.12"/></proof>
<proof prover="12"><result status="unknown" time="0.01"/></proof>
<proof prover="13"><result status="timeout" time="1.00"/></proof>
<proof prover="14"><result status="unknown" time="1.65"/></proof>
<proof prover="14"><result status="unknown" time="2.03"/></proof>
<proof prover="15"><result status="unknown" time="0.00"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="19"><result status="unknown" time="0.00"/></proof>
<proof prover="20"><result status="unknown" time="0.02"/></proof>
<proof prover="21"><result status="unknown" time="2.05"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.13"/></proof>
<proof prover="25"><result status="unknown" time="0.14"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -212,7 +212,7 @@
<proof prover="7"><result status="unknown" time="0.01"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="timeout" time="1.01"/></proof>
<proof prover="10"><result status="unknown" time="0.30"/></proof>
<proof prover="10"><result status="unknown" time="0.16"/></proof>
<proof prover="11"><result status="unknown" time="0.28"/></proof>
<proof prover="12"><result status="unknown" time="0.01"/></proof>
<proof prover="13"><result status="timeout" time="1.00"/></proof>
......@@ -223,7 +223,7 @@
<proof prover="20"><result status="unknown" time="0.01"/></proof>
<proof prover="21"><result status="unknown" time="1.80"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.31"/></proof>
<proof prover="25"><result status="unknown" time="0.12"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -251,7 +251,7 @@
<proof prover="20"><result status="unknown" time="0.01"/></proof>
<proof prover="21"><result status="unknown" time="1.82"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.11"/></proof>
<proof prover="25"><result status="unknown" time="0.13"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -278,7 +278,7 @@
<proof prover="20" timelimit="1"><result status="unknown" time="0.03"/></proof>
<proof prover="21"><result status="unknown" time="1.79"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24" timelimit="1"><result status="unknown" time="0.11"/></proof>
<proof prover="25"><result status="unknown" time="0.14"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -295,7 +295,7 @@
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="timeout" time="1.09"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.01"/></proof>
<proof prover="11"><result status="timeout" time="0.70"/></proof>
<proof prover="12"><result status="unknown" time="0.01"/></proof>
<proof prover="13"><result status="timeout" time="1.00"/></proof>
<proof prover="14"><result status="unknown" time="2.13"/></proof>
......@@ -305,7 +305,7 @@
<proof prover="20"><result status="unknown" time="0.02"/></proof>
<proof prover="21"><result status="unknown" time="2.07"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.12"/></proof>
<proof prover="25"><result status="unknown" time="0.12"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -332,7 +332,7 @@
<proof prover="20"><result status="unknown" time="0.06"/></proof>
<proof prover="21"><result status="unknown" time="1.92"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.12"/></proof>
<proof prover="25"><result status="unknown" time="0.11"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -505,7 +505,7 @@
<proof prover="20"><result status="unknown" time="0.02"/></proof>
<proof prover="21"><result status="unknown" time="2.06"/></proof>
<proof prover="22"><result status="unknown" time="0.01"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.02"/></proof>
<proof prover="25"><result status="unknown" time="0.13"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -530,9 +530,9 @@
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="19"><result status="unknown" time="0.02"/></proof>
<proof prover="20"><result status="unknown" time="0.02"/></proof>
<proof prover="21"><result status="unknown" time="1.27"/></proof>
<proof prover="21"><result status="unknown" time="2.06"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.05"/></proof>
<proof prover="25"><result status="unknown" time="0.12"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -561,7 +561,7 @@
<proof prover="20"><result status="unknown" time="0.06"/></proof>
<proof prover="21"><result status="unknown" time="1.98"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.01"/></proof>
<proof prover="25"><result status="unknown" time="0.10"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -588,7 +588,7 @@
<proof prover="20" timelimit="1"><result status="unknown" time="0.02"/></proof>
<proof prover="21"><result status="unknown" time="1.93"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24" timelimit="1"><result status="unknown" time="0.02"/></proof>
<proof prover="25"><result status="unknown" time="0.13"/></proof>
<proof prover="26" timelimit="2"><result status="timeout" time="2.00"/></proof>
......@@ -615,7 +615,7 @@
<proof prover="20"><result status="unknown" time="0.05"/></proof>
<proof prover="21"><result status="unknown" time="2.07"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.02"/></proof>
<proof prover="25"><result status="unknown" time="0.14"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......@@ -642,7 +642,7 @@
<proof prover="20"><result status="unknown" time="0.02"/></proof>
<proof prover="21"><result status="unknown" time="2.07"/></proof>
<proof prover="22"><result status="unknown" time="0.00"/></proof>
<proof prover="23"><result status="timeout" time="1.00"/></proof>
<proof prover="23"><result status="unknown" time="1.00"/></proof>
<proof prover="24"><result status="unknown" time="0.04"/></proof>
<proof prover="25"><result status="unknown" time="0.14"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
......
......@@ -35,7 +35,7 @@
</goal>
<goal name="WP_parameter triplet.2" expl="assertion">
<proof prover="2"><result status="valid" time="4.30" steps="10733"/></proof>
<proof prover="3"><result status="valid" time="1.86"/></proof>
<proof prover="3"><result status="valid" time="1.52"/></proof>
<proof prover="4"><result status="valid" time="0.79"/></proof>
</goal>
<goal name="WP_parameter triplet.3" expl="assertion">
......@@ -46,11 +46,11 @@
<proof prover="5"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter triplet.4" expl="assertion">
<proof prover="0"><result status="outofmemory" time="4.61"/></proof>
<proof prover="0"><result status="outofmemory" time="3.93"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="5.00"/></proof>
<proof prover="4"><result status="unknown" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter triplet.5" expl="assertion">
......@@ -75,8 +75,8 @@
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="5.00"/></proof>
<proof prover="4"><result status="unknown" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter triplet.9" expl="assertion">
......@@ -91,8 +91,8 @@
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="valid" time="4.89"/></proof>
<proof prover="4"><result status="unknown" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
......@@ -153,7 +153,7 @@
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter test.2" expl="assertion">
......@@ -190,14 +190,14 @@
<proof prover="3"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="WP_parameter test.7" expl="assertion">
<proof prover="0"><result status="outofmemory" time="4.57"/></proof>
<proof prover="0"><result status="outofmemory" time="3.96"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="5.00"/></proof>
</goal>
<goal name="WP_parameter test.8" expl="assertion">
<proof prover="0"><result status="outofmemory" time="4.43"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="5.00"/></proof>
</goal>
<goal name="WP_parameter test.9" expl="assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......
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