Commit c4e4f9b7 authored by MARCHE Claude's avatar MARCHE Claude

fix sessions, remove usage of private versions of Alt-Ergo

parent 273f47ff
......@@ -4,16 +4,15 @@
<why3session shape_version="4">
<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="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="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="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="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"/>
<file name="../bitwalker.mlw" expanded="true">
<theory name="Bitwalker" sum="d3739287c7b8602c11979aa2d5921b7f" expanded="true">
<prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw">
<theory name="Bitwalker" sum="d3739287c7b8602c11979aa2d5921b7f">
<goal name="nth64" expl="">
<proof prover="0"><result status="valid" time="0.10" steps="93"/></proof>
</goal>
......@@ -165,8 +164,8 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter peek" expl="VC for peek" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter peek" expl="VC for peek">
<transf name="split_goal_wp">
<goal name="WP_parameter peek.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.11" steps="114"/></proof>
<proof prover="3"><result status="valid" time="0.13"/></proof>
......@@ -196,10 +195,10 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter peek.7" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.03" steps="92"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></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 name="WP_parameter peek.8" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.03" steps="92"/></proof>
......@@ -220,7 +219,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="116"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter peek.13" expl="precondition" expanded="true">
<goal name="WP_parameter peek.13" expl="precondition">
<proof prover="3"><result status="valid" time="2.14"/></proof>
<proof prover="6"><result status="valid" time="0.09"/></proof>
<proof prover="9"><result status="valid" time="0.12"/></proof>
......@@ -239,7 +238,7 @@
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter peek.17" expl="loop invariant preservation">
<proof prover="4"><result status="valid" time="3.08" steps="710"/></proof>
<proof prover="10"><result status="valid" time="1.92" steps="1224"/></proof>
</goal>
<goal name="WP_parameter peek.18" expl="loop invariant preservation">
<proof prover="5"><result status="valid" time="0.01"/></proof>
......@@ -383,9 +382,9 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter poke" expl="VC for poke" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter poke.1" expl="precondition" expanded="true">
<goal name="WP_parameter poke" expl="VC for poke">
<transf name="split_goal_wp">
<goal name="WP_parameter poke.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.05" steps="114"/></proof>
<proof prover="3"><result status="valid" time="0.15"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
......@@ -401,13 +400,13 @@
<proof prover="1"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter poke.4" expl="postcondition" expanded="true">
<goal name="WP_parameter poke.4" expl="postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.07"/></proof>
<proof prover="9"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter poke.5" expl="postcondition" expanded="true">
<goal name="WP_parameter poke.5" expl="postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
......@@ -456,7 +455,7 @@
<goal name="WP_parameter poke.15" expl="precondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter poke.16" expl="precondition" expanded="true">
<goal name="WP_parameter poke.16" expl="precondition">
<proof prover="3"><result status="valid" time="1.70"/></proof>
<proof prover="6"><result status="valid" time="0.09"/></proof>
<proof prover="9"><result status="valid" time="0.13"/></proof>
......@@ -480,7 +479,7 @@
</goal>
<goal name="WP_parameter poke.21" expl="assertion">
<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.49" steps="500"/></proof>
</goal>
<goal name="WP_parameter poke.22" expl="assertion">
<transf name="split_goal_wp">
......
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../dijkstra.mlw" expanded="true">
<theory name="DijkstraShortestPath" sum="20ec7a75a06b6a173b67eb381a54961e" expanded="true">
<goal name="WP_parameter relax" expl="VC for relax">
......@@ -42,9 +42,9 @@
<goal name="Path_shortest_path" expl="">
<proof prover="1" timelimit="5" edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="Main_lemma" expl="">
<goal name="Main_lemma" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="205"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.08"/></proof>
<proof prover="9"><result status="valid" time="0.38" steps="937"/></proof>
</goal>
<goal name="Completeness_lemma" expl="">
<transf name="induction_pr">
......
......@@ -7,8 +7,8 @@
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compiler.mlw" expanded="true">
<theory name="Compile_aexpr" sum="411273fbd1fd074bd85d168f5a46d8fc" expanded="true">
<goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr">
......@@ -682,14 +682,15 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter compile_bexpr_natural" expl="VC for compile_bexpr_natural">
<transf name="split_goal_wp">
<goal name="WP_parameter compile_bexpr_natural" expl="VC for compile_bexpr_natural" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter compile_bexpr_natural.1" expl="assertion">
<proof prover="2"><result status="valid" time="0.05" steps="11"/></proof>
</goal>
<goal name="WP_parameter compile_bexpr_natural.2" expl="postcondition">
<goal name="WP_parameter compile_bexpr_natural.2" expl="postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.13"/></proof>
<metas>
<metas
expanded="true">
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
......@@ -1727,13 +1728,13 @@
<meta name="remove_type">
<meta_arg_ts id="6652"/>
</meta>
<goal name="WP_parameter compile_bexpr_natural.2" expl="postcondition">
<transf name="eliminate_builtin">
<goal name="WP_parameter compile_bexpr_natural.2.1" expl="postcondition">
<goal name="WP_parameter compile_bexpr_natural.2" expl="postcondition" expanded="true">
<transf name="eliminate_builtin" expanded="true">
<goal name="WP_parameter compile_bexpr_natural.2.1" expl="postcondition" expanded="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="60"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.06" steps="67"/></proof>
</goal>
</transf>
</goal>
......
......@@ -17,7 +17,6 @@
<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="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="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"/>
......@@ -43,10 +42,8 @@
<proof prover="9"><result status="valid" time="0.26"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></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="17"><result status="valid" time="1.17" steps="983"/></proof>
<proof prover="18"><result status="valid" time="1.41" steps="989"/></proof>
......@@ -67,15 +64,13 @@
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="12"><result status="timeout" time="1.01"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="unknown" time="2.02"/></proof>
<proof prover="15"><result status="unknown" time="1.33"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="unknown" time="0.57"/></proof>
<proof prover="18"><result status="unknown" time="0.66"/></proof>
<proof prover="19"><result status="unknown" time="1.00"/></proof>
<proof prover="20"><result status="unknown" time="1.00"/></proof>
<proof prover="19"><result status="unknown" time="2.01"/></proof>
<proof prover="20"><result status="unknown" time="1.86"/></proof>
<proof prover="21"><result status="unknown" time="0.07"/></proof>
</goal>
<goal name="G2" expl="" expanded="true">
......@@ -91,10 +86,9 @@
<proof prover="9"><result status="valid" time="0.62"/></proof>
<proof prover="10"><result status="valid" time="0.79"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="12" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></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="17"><result status="valid" time="0.78" steps="1152"/></proof>
<proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof>
......
......@@ -27,7 +27,6 @@
<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="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="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"/>
......@@ -60,7 +59,6 @@
<proof prover="22"><result status="valid" time="0.00"/></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="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.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
......@@ -93,7 +91,6 @@
<proof prover="22"><result status="valid" time="0.00"/></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="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.00"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
......@@ -123,7 +120,6 @@
<proof prover="22"><result status="valid" time="0.00"/></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="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>
<proof prover="28"><result status="valid" time="0.01"/></proof>
......@@ -154,7 +150,6 @@
<proof prover="22"><result status="valid" time="0.01"/></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="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.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
......@@ -186,7 +181,6 @@
<proof prover="22"><result status="valid" time="0.03"/></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="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>
<proof prover="28"><result status="valid" time="0.00"/></proof>
......@@ -217,7 +211,6 @@
<proof prover="22"><result status="valid" time="0.01"/></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="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>
<proof prover="28"><result status="valid" time="0.00"/></proof>
......@@ -248,7 +241,6 @@
<proof prover="22"><result status="valid" time="0.01"/></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="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.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
......
......@@ -6,9 +6,9 @@
<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="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="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" expanded="true">
<theory name="S" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
......@@ -36,10 +36,10 @@
<goal name="WP_parameter add_singleton" expl="VC for add_singleton">
<proof prover="6"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter mul2" expl="VC for mul2" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter mul2.1" expl="type invariant" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter mul2" expl="VC for mul2">
<transf name="split_goal_wp">
<goal name="WP_parameter mul2.1" expl="type invariant">
<transf name="split_goal_wp">
<goal name="WP_parameter mul2.1.1" expl="type invariant">
<proof prover="0"><result status="valid" time="0.20" steps="196"/></proof>
</goal>
......@@ -49,9 +49,9 @@
<goal name="WP_parameter mul2.1.3" expl="type invariant">
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter mul2.1.4" expl="type invariant" expanded="true">
<proof prover="4"><result status="valid" time="0.48" steps="537"/></proof>
<goal name="WP_parameter mul2.1.4" expl="type invariant">
<proof prover="6"><result status="valid" time="0.14"/></proof>
<proof prover="7"><result status="valid" time="0.21" steps="365"/></proof>
</goal>
</transf>
</goal>
......
......@@ -5,8 +5,8 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="3000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="60" steplimit="1" memlimit="3000"/>
<prover id="3" name="Alt-Ergo" version="1.00.prv" timelimit="10" steplimit="1" memlimit="4000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="3500"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="1" memlimit="4000"/>
<file name="../schorr_waite.mlw" expanded="true">
<theory name="SchorrWaite" sum="56c2caccc11b30c12c93dbf0b4080bd6" expanded="true">
<goal name="WP_parameter tl_stackNodes" expl="VC for tl_stackNodes">
......@@ -36,8 +36,8 @@
<goal name="WP_parameter tl_cons" expl="VC for tl_cons">
<proof prover="0"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="WP_parameter trans_path" expl="VC for trans_path">
<transf name="split_goal_wp">
<goal name="WP_parameter trans_path" expl="VC for trans_path" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter trans_path.1" expl="variant decrease">
<proof prover="0" memlimit="4000"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
......@@ -47,10 +47,10 @@
<goal name="WP_parameter trans_path.3" expl="precondition">
<proof prover="0" memlimit="4000"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter trans_path.4" expl="postcondition">
<goal name="WP_parameter trans_path.4" expl="postcondition" expanded="true">
<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="3"><result status="valid" time="0.07" steps="297"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="393"/></proof>
</goal>
<goal name="WP_parameter trans_path.5" expl="postcondition">
<proof prover="0" memlimit="4000"><result status="valid" time="0.66" steps="475"/></proof>
......@@ -66,8 +66,8 @@
<goal name="path_edge_cons" expl="">
<proof prover="2" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter schorr_waite" expl="VC for schorr_waite" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter schorr_waite" expl="VC for schorr_waite">
<transf name="split_goal_wp">
<goal name="WP_parameter schorr_waite.1" expl="precondition">
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
......
This diff is collapsed.
......@@ -3,8 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<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="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="6" name="Alt-Ergo" version="0.99.1" timelimit="30" steplimit="0" memlimit="1000"/>
<file name="../vacid_0_build_maze.mlw" expanded="true">
......@@ -72,17 +73,17 @@
<goal name="WP_parameter build_maze.10" expl="precondition">
<proof prover="6"><result status="valid" time="0.06" steps="44"/></proof>
</goal>
<goal name="WP_parameter build_maze.11" expl="precondition">
<proof prover="4"><result status="valid" time="0.24" steps="381"/></proof>
<goal name="WP_parameter build_maze.11" expl="precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter build_maze.12" expl="loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter build_maze.13" expl="loop invariant preservation">
<goal name="WP_parameter build_maze.13" expl="loop invariant preservation" expanded="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="4"><result status="valid" time="0.18" steps="175"/></proof>
</goal>
<goal name="WP_parameter build_maze.14" expl="loop invariant preservation">
<proof prover="6"><result status="valid" time="0.02" steps="33"/></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