Commit 468ace60 authored by MARCHE Claude's avatar MARCHE Claude

update sessions: no more use of private versions of Alt-Ergo

parent 8c7aaafc
...@@ -4,14 +4,13 @@ ...@@ -4,14 +4,13 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.10.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="7" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="8" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.5.0" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="9" name="Z3" version="4.5.0" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" proved="true"> <file name="../bitwalker.mlw" proved="true">
<theory name="Bitwalker" proved="true"> <theory name="Bitwalker" proved="true">
<goal name="nth64" proved="true"> <goal name="nth64" proved="true">
...@@ -196,10 +195,10 @@ ...@@ -196,10 +195,10 @@
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="WP_parameter peek.6" expl="loop invariant init" proved="true"> <goal name="WP_parameter peek.6" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="92"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof> <proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof> <proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="93"/></proof>
</goal> </goal>
<goal name="WP_parameter peek.7" expl="loop invariant init" proved="true"> <goal name="WP_parameter peek.7" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="92"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="92"/></proof>
...@@ -239,7 +238,7 @@ ...@@ -239,7 +238,7 @@
<proof prover="3"><result status="valid" time="0.12"/></proof> <proof prover="3"><result status="valid" time="0.12"/></proof>
</goal> </goal>
<goal name="WP_parameter peek.16" expl="loop invariant preservation" proved="true"> <goal name="WP_parameter peek.16" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="3.08" steps="710"/></proof> <proof prover="10"><result status="valid" time="1.94" steps="1224"/></proof>
</goal> </goal>
<goal name="WP_parameter peek.17" expl="loop invariant preservation" proved="true"> <goal name="WP_parameter peek.17" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
...@@ -480,7 +479,7 @@ ...@@ -480,7 +479,7 @@
</goal> </goal>
<goal name="WP_parameter poke.20" expl="assertion" proved="true"> <goal name="WP_parameter poke.20" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof> <proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.82" steps="323"/></proof> <proof prover="10"><result status="valid" time="0.50" steps="500"/></proof>
</goal> </goal>
<goal name="WP_parameter poke.21" expl="assertion" proved="true"> <goal name="WP_parameter poke.21" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
......
...@@ -5,10 +5,10 @@ ...@@ -5,10 +5,10 @@
<prover id="0" name="CVC4" version="1.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/> <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/> <prover id="2" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="120" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="2.19" timelimit="10" steplimit="0" memlimit="0"/> <prover id="6" name="Z3" version="2.19" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="7" name="Alt-Ergo" version="1.00.prv" timelimit="120" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="8" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="9" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="10" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
...@@ -199,7 +199,7 @@ ...@@ -199,7 +199,7 @@
<proof prover="4"><result status="valid" time="0.18"/></proof> <proof prover="4"><result status="valid" time="0.18"/></proof>
</goal> </goal>
<goal name="WP_parameter prime_numbers.39.0.3" expl="VC for prime_numbers" proved="true"> <goal name="WP_parameter prime_numbers.39.0.3" expl="VC for prime_numbers" proved="true">
<proof prover="7"><result status="valid" time="36.74" steps="5240"/></proof> <proof prover="3"><result status="valid" time="6.14" steps="1699"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -14,10 +14,8 @@ ...@@ -14,10 +14,8 @@
<prover id="9" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="9" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="10" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="10" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="13" name="CVC4" version="1.3" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="13" name="CVC4" version="1.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="14" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="14" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="15" name="Alt-Ergo" version="1.00.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="16" name="veriT" version="201410" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="16" name="veriT" version="201410" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="17" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="17" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="18" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="18" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
...@@ -25,10 +23,6 @@ ...@@ -25,10 +23,6 @@
<prover id="20" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="20" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="21" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../einstein.why"> <file name="../einstein.why">
<theory name="Bijection" proved="true">
</theory>
<theory name="Einstein" proved="true">
</theory>
<theory name="Goals"> <theory name="Goals">
<goal name="G1" proved="true"> <goal name="G1" proved="true">
<proof prover="0"><result status="timeout" time="1.00"/></proof> <proof prover="0"><result status="timeout" time="1.00"/></proof>
...@@ -43,10 +37,8 @@ ...@@ -43,10 +37,8 @@
<proof prover="9"><result status="valid" time="0.26"/></proof> <proof prover="9"><result status="valid" time="0.26"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof> <proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="valid" time="12.98" steps="969"/></proof> <proof prover="11"><result status="valid" time="12.98" steps="969"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof> <proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.50"/></proof> <proof prover="14"><result status="valid" time="1.50"/></proof>
<proof prover="15"><result status="timeout" time="1.00"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof> <proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="1.17" steps="983"/></proof> <proof prover="17"><result status="valid" time="1.17" steps="983"/></proof>
<proof prover="18"><result status="valid" time="1.41" steps="989"/></proof> <proof prover="18"><result status="valid" time="1.41" steps="989"/></proof>
...@@ -67,10 +59,8 @@ ...@@ -67,10 +59,8 @@
<proof prover="9"><result status="timeout" time="1.00"/></proof> <proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof> <proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="unknown" time="9.26"/></proof> <proof prover="11"><result status="unknown" time="9.26"/></proof>
<proof prover="12"><result status="timeout" time="1.01"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof> <proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="unknown" time="2.00"/></proof> <proof prover="14"><result status="unknown" time="2.00"/></proof>
<proof prover="15"><result status="unknown" time="1.33"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof> <proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="unknown" time="0.57"/></proof> <proof prover="17"><result status="unknown" time="0.57"/></proof>
<proof prover="18"><result status="unknown" time="0.66"/></proof> <proof prover="18"><result status="unknown" time="0.66"/></proof>
...@@ -91,10 +81,8 @@ ...@@ -91,10 +81,8 @@
<proof prover="9"><result status="valid" time="0.62"/></proof> <proof prover="9"><result status="valid" time="0.62"/></proof>
<proof prover="10"><result status="valid" time="0.79"/></proof> <proof prover="10"><result status="valid" time="0.79"/></proof>
<proof prover="11"><result status="valid" time="7.72" steps="1007"/></proof> <proof prover="11"><result status="valid" time="7.72" steps="1007"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof> <proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.27"/></proof> <proof prover="14"><result status="valid" time="1.27"/></proof>
<proof prover="15"><result status="valid" time="1.82" steps="523"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof> <proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="0.78" steps="1152"/></proof> <proof prover="17"><result status="valid" time="0.78" steps="1152"/></proof>
<proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof> <proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof>
......
...@@ -27,7 +27,6 @@ ...@@ -27,7 +27,6 @@
<prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="1" memlimit="1000"/> <prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/> <prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/> <prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/> <prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="27" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="27" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/> <prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
...@@ -60,7 +59,6 @@ ...@@ -60,7 +59,6 @@
<proof prover="22"><result status="valid" time="0.00"/></proof> <proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof>
...@@ -93,7 +91,6 @@ ...@@ -93,7 +91,6 @@
<proof prover="22"><result status="valid" time="0.00"/></proof> <proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="2"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof> <proof prover="27"><result status="valid" time="0.00"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof> <proof prover="28"><result status="valid" time="0.00"/></proof>
...@@ -123,7 +120,6 @@ ...@@ -123,7 +120,6 @@
<proof prover="22"><result status="valid" time="0.00"/></proof> <proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.01"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof>
...@@ -154,7 +150,6 @@ ...@@ -154,7 +150,6 @@
<proof prover="22"><result status="valid" time="0.01"/></proof> <proof prover="22"><result status="valid" time="0.01"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="32"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="32"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof>
...@@ -186,7 +181,6 @@ ...@@ -186,7 +181,6 @@
<proof prover="22"><result status="valid" time="0.03"/></proof> <proof prover="22"><result status="valid" time="0.03"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof> <proof prover="28"><result status="valid" time="0.00"/></proof>
...@@ -217,7 +211,6 @@ ...@@ -217,7 +211,6 @@
<proof prover="22"><result status="valid" time="0.01"/></proof> <proof prover="22"><result status="valid" time="0.01"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof> <proof prover="27"><result status="valid" time="0.00"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof> <proof prover="28"><result status="valid" time="0.00"/></proof>
...@@ -248,7 +241,6 @@ ...@@ -248,7 +241,6 @@
<proof prover="22"><result status="valid" time="0.01"/></proof> <proof prover="22"><result status="valid" time="0.01"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <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="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof>
......
...@@ -6,12 +6,10 @@ ...@@ -6,12 +6,10 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.10.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../queens_bv.mlw" proved="true"> <file name="../queens_bv.mlw" proved="true">
<theory name="S" proved="true">
</theory>
<theory name="Solution" proved="true"> <theory name="Solution" proved="true">
<goal name="partial_solution_eq_prefix" proved="true"> <goal name="partial_solution_eq_prefix" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="44"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
...@@ -21,8 +19,6 @@ ...@@ -21,8 +19,6 @@
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="BitsSpec" proved="true">
</theory>
<theory name="Bits" proved="true"> <theory name="Bits" proved="true">
<goal name="WP_parameter empty" expl="VC for empty" proved="true"> <goal name="WP_parameter empty" expl="VC for empty" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
...@@ -50,8 +46,8 @@ ...@@ -50,8 +46,8 @@
<proof prover="3"><result status="valid" time="0.11"/></proof> <proof prover="3"><result status="valid" time="0.11"/></proof>
</goal> </goal>
<goal name="WP_parameter mul2.0.3" expl="type invariant" proved="true"> <goal name="WP_parameter mul2.0.3" expl="type invariant" proved="true">
<proof prover="4"><result status="valid" time="0.48" steps="537"/></proof>
<proof prover="6"><result status="valid" time="0.14"/></proof> <proof prover="6"><result status="valid" time="0.14"/></proof>
<proof prover="7"><result status="valid" time="0.21" steps="365"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -5,8 +5,8 @@ ...@@ -5,8 +5,8 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="3000"/> <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="3000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="60" steplimit="0" memlimit="3000"/> <prover id="2" name="CVC4" version="1.4" timelimit="60" steplimit="0" memlimit="3000"/>
<prover id="3" name="Alt-Ergo" version="1.00.prv" timelimit="10" steplimit="0" memlimit="4000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="3500"/> <prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="3500"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="4000"/>
<file name="../schorr_waite.mlw" proved="true"> <file name="../schorr_waite.mlw" proved="true">
<theory name="SchorrWaite" proved="true"> <theory name="SchorrWaite" proved="true">
<goal name="WP_parameter tl_stackNodes" expl="VC for tl_stackNodes" proved="true"> <goal name="WP_parameter tl_stackNodes" expl="VC for tl_stackNodes" proved="true">
...@@ -50,7 +50,7 @@ ...@@ -50,7 +50,7 @@
<goal name="WP_parameter trans_path.3" expl="postcondition" proved="true"> <goal name="WP_parameter trans_path.3" expl="postcondition" proved="true">
<proof prover="0" memlimit="4000"><result status="valid" time="0.61" steps="598"/></proof> <proof prover="0" memlimit="4000"><result status="valid" time="0.61" steps="598"/></proof>
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="0.51"/></proof> <proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="0.51"/></proof>
<proof prover="3"><result status="valid" time="0.07" steps="297"/></proof> <proof prover="5"><result status="valid" time="0.07" steps="393"/></proof>
</goal> </goal>
<goal name="WP_parameter trans_path.4" expl="postcondition" proved="true"> <goal name="WP_parameter trans_path.4" expl="postcondition" proved="true">
<proof prover="0" memlimit="4000"><result status="valid" time="0.66" steps="475"/></proof> <proof prover="0" memlimit="4000"><result status="valid" time="0.66" steps="475"/></proof>
......
This diff is collapsed.
...@@ -3,91 +3,84 @@ ...@@ -3,91 +3,84 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="30" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="30" steplimit="0" memlimit="1000"/> <prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="30" steplimit="0" memlimit="1000"/>
<file name="../vacid_0_build_maze.mlw"> <file name="../vacid_0_build_maze.mlw" proved="true">
<theory name="UnionFind_pure"> <theory name="BuildMaze" proved="true">
</theory> <goal name="Ineq1" proved="true">
<theory name="UnionFind_sig"> <transf name="split_goal_right" proved="true" >
</theory> <goal name="Ineq1.0" proved="true">
<theory name="Graph">
</theory>
<theory name="Graph_sig">
</theory>
<theory name="BuildMaze">
<goal name="Ineq1" expl="">
<transf name="split_goal_right">
<goal name="Ineq1.1" expl="">
<proof prover="6"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="6"><result status="valid" time="0.00" steps="5"/></proof>
</goal> </goal>
<goal name="Ineq1.2" expl=""> <goal name="Ineq1.1" proved="true">
<proof prover="0"><result status="valid" time="0.14"/></proof> <proof prover="0"><result status="valid" time="0.14"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter add_edge_and_union" expl="VC for add_edge_and_union"> <goal name="WP_parameter add_edge_and_union" expl="VC for add_edge_and_union" proved="true">
<transf name="split_goal_right"> <transf name="split_goal_right" proved="true" >
<goal name="WP_parameter add_edge_and_union.1" expl="precondition"> <goal name="WP_parameter add_edge_and_union.0" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="6"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter add_edge_and_union.2" expl="precondition"> <goal name="WP_parameter add_edge_and_union.1" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.00" steps="7"/></proof> <proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter add_edge_and_union.3" expl="postcondition"> <goal name="WP_parameter add_edge_and_union.2" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.29" steps="615"/></proof> <proof prover="6"><result status="valid" time="0.29" steps="615"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter build_maze" expl="VC for build_maze"> <goal name="WP_parameter build_maze" expl="VC for build_maze" proved="true">
<transf name="split_goal_right"> <transf name="split_goal_right" proved="true" >
<goal name="WP_parameter build_maze.1" expl="precondition"> <goal name="WP_parameter build_maze.0" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.00" steps="2"/></proof> <proof prover="6"><result status="valid" time="0.00" steps="2"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.2" expl="assertion"> <goal name="WP_parameter build_maze.1" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="17"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.3" expl="loop invariant init"> <goal name="WP_parameter build_maze.2" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="24"/></proof> <proof prover="6"><result status="valid" time="0.02" steps="24"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.4" expl="precondition"> <goal name="WP_parameter build_maze.3" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.5" expl="precondition"> <goal name="WP_parameter build_maze.4" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.00" steps="12"/></proof> <proof prover="6"><result status="valid" time="0.00" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.6" expl="precondition"> <goal name="WP_parameter build_maze.5" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="14"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.7" expl="assertion"> <goal name="WP_parameter build_maze.6" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="19"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.8" expl="assertion"> <goal name="WP_parameter build_maze.7" expl="assertion" proved="true">
<proof prover="5" timelimit="30"><result status="valid" time="0.01"/></proof> <proof prover="5" timelimit="30"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.9" expl="precondition"> <goal name="WP_parameter build_maze.8" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.13" steps="50"/></proof> <proof prover="6"><result status="valid" time="0.13" steps="50"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.10" expl="precondition"> <goal name="WP_parameter build_maze.9" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.06" steps="44"/></proof> <proof prover="6"><result status="valid" time="0.06" steps="44"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.11" expl="precondition"> <goal name="WP_parameter build_maze.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.24" steps="381"/></proof> <proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.12" expl="loop invariant preservation"> <goal name="WP_parameter build_maze.11" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.13" expl="loop invariant preservation"> <goal name="WP_parameter build_maze.12" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="197"/></proof>
<proof prover="3"><result status="valid" time="2.47"/></proof> <proof prover="3"><result status="valid" time="2.47"/></proof>
<proof prover="4"><result status="valid" time="0.18" steps="175"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.14" expl="loop invariant preservation"> <goal name="WP_parameter build_maze.13" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="33"/></proof> <proof prover="6"><result status="valid" time="0.02" steps="33"/></proof>
</goal> </goal>
<goal name="WP_parameter build_maze.15" expl="postcondition"> <goal name="WP_parameter build_maze.14" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.03" steps="21"/></proof> <proof prover="6"><result status="valid" time="0.03" steps="21"/></proof>
</goal> </goal>
</transf> </transf>
......
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