Commit 41bf52d7 authored by MARCHE Claude's avatar MARCHE Claude

Update the XML DTD

- metas not there anymore
- lot of other simplifications
- sessions files updated accordingly when needed
parent 345afb30
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
<prover id="10" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="10" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="11" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="12" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="12" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../blocking_semantics5.mlw" expanded="true"> <file name="../blocking_semantics5.mlw">
<theory name="Syntax" sum="f7cde33e5e26ee60d3da8eec7b217241"> <theory name="Syntax" sum="f7cde33e5e26ee60d3da8eec7b217241">
<goal name="mident_decide" expl=""> <goal name="mident_decide" expl="">
<proof prover="9"><result status="valid" time="0.01" steps="1"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="1"/></proof>
......
...@@ -6,10 +6,10 @@ ...@@ -6,10 +6,10 @@
<prover id="2" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/> <prover id="2" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/> <prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../formula.why"> <file name="../formula.why">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true"> <theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="PropositionalCalculus" sum="2197343d91936e442b6aeb7d3a3b50db" expanded="true"> <theory name="PropositionalCalculus" sum="2197343d91936e442b6aeb7d3a3b50db">
<goal name="Test1" expl="" expanded="true"> <goal name="Test1" expl="">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof> <proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="46"/></proof> <proof prover="3"><result status="valid" time="0.05" steps="46"/></proof>
......
...@@ -7,8 +7,8 @@ ...@@ -7,8 +7,8 @@
<prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/> <prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/> <prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" expanded="true"> <file name="../imp_n.why">
<theory name="Imp" sum="4edcb627e6f7cecac2b0d3f266958856" expanded="true"> <theory name="Imp" sum="4edcb627e6f7cecac2b0d3f266958856">
<goal name="ident_eq_dec" expl=""> <goal name="ident_eq_dec" expl="">
<proof prover="6"><result status="valid" time="0.00" steps="0"/></proof> <proof prover="6"><result status="valid" time="0.00" steps="0"/></proof>
</goal> </goal>
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/> <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/> <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/> <prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../wp2.mlw" expanded="true"> <file name="../wp2.mlw">
<theory name="Imp" sum="4d6ec4c3ea3a39365f84600c953b8179"> <theory name="Imp" sum="4d6ec4c3ea3a39365f84600c953b8179">
<goal name="eval_subst_term" expl=""> <goal name="eval_subst_term" expl="">
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof> <proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof>
......
...@@ -5,26 +5,26 @@ ...@@ -5,26 +5,26 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true"> <file name="../add_list.mlw">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="AddListRec" sum="ddf9071b1a9688fe9218a8b95f77634f" expanded="true"> <theory name="AddListRec" sum="ddf9071b1a9688fe9218a8b95f77634f">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true"> <goal name="WP_parameter sum" expl="VC for sum">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="49"/></proof> <proof prover="3"><result status="valid" time="0.02" steps="49"/></proof>
</goal> </goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true"> <goal name="WP_parameter main" expl="VC for main">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="AddListImp" sum="b8d9e3c0e71fb300ad846cc5060783ef" expanded="true"> <theory name="AddListImp" sum="b8d9e3c0e71fb300ad846cc5060783ef">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true"> <goal name="WP_parameter sum" expl="VC for sum">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true"> <goal name="WP_parameter main" expl="VC for main">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
......
This diff is collapsed.
...@@ -3,10 +3,10 @@ ...@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true"> <file name="../algo64.mlw">
<theory name="Algo64" sum="51d805a22bc2e9af151efc73086f3b23" expanded="true"> <theory name="Algo64" sum="51d805a22bc2e9af151efc73086f3b23">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true"> <goal name="WP_parameter quicksort" expl="VC for quicksort">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter quicksort.1" expl="precondition"> <goal name="WP_parameter quicksort.1" expl="precondition">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal> </goal>
......
...@@ -3,10 +3,10 @@ ...@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true"> <file name="../algo65.mlw">
<theory name="Algo65" sum="4ec16c9b9e583f9273e61e0b69664be0" expanded="true"> <theory name="Algo65" sum="4ec16c9b9e583f9273e61e0b69664be0">
<goal name="WP_parameter find" expl="VC for find" expanded="true"> <goal name="WP_parameter find" expl="VC for find">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter find.1" expl="precondition"> <goal name="WP_parameter find.1" expl="precondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
...@@ -22,9 +22,9 @@ ...@@ -22,9 +22,9 @@
<goal name="WP_parameter find.5" expl="assertion"> <goal name="WP_parameter find.5" expl="assertion">
<proof prover="1"><result status="valid" time="0.02" steps="96"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="96"/></proof>
</goal> </goal>
<goal name="WP_parameter find.6" expl="assertion" expanded="true"> <goal name="WP_parameter find.6" expl="assertion">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter find.6.1" expl="assertion" expanded="true"> <goal name="WP_parameter find.6.1" expl="assertion">
<proof prover="1" timelimit="6"><result status="valid" time="0.22" steps="248"/></proof> <proof prover="1" timelimit="6"><result status="valid" time="0.22" steps="248"/></proof>
</goal> </goal>
<goal name="WP_parameter find.6.2" expl="assertion"> <goal name="WP_parameter find.6.2" expl="assertion">
...@@ -89,9 +89,9 @@ ...@@ -89,9 +89,9 @@
<goal name="WP_parameter find.25" expl="assertion"> <goal name="WP_parameter find.25" expl="assertion">
<proof prover="1"><result status="valid" time="0.04" steps="163"/></proof> <proof prover="1"><result status="valid" time="0.04" steps="163"/></proof>
</goal> </goal>
<goal name="WP_parameter find.26" expl="assertion" expanded="true"> <goal name="WP_parameter find.26" expl="assertion">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter find.26.1" expl="assertion" expanded="true"> <goal name="WP_parameter find.26.1" expl="assertion">
<proof prover="1" timelimit="6"><result status="valid" time="0.30" steps="380"/></proof> <proof prover="1" timelimit="6"><result status="valid" time="0.30" steps="380"/></proof>
</goal> </goal>
<goal name="WP_parameter find.26.2" expl="assertion"> <goal name="WP_parameter find.26.2" expl="assertion">
......
...@@ -3,44 +3,44 @@ ...@@ -3,44 +3,44 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true"> <file name="../all_distinct.mlw">
<theory name="AllDistinct" sum="9890dccbada5eed3f27377796f4d13ec" expanded="true"> <theory name="AllDistinct" sum="9890dccbada5eed3f27377796f4d13ec">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true"> <goal name="WP_parameter all_distinct" expl="VC for all_distinct">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter all_distinct.1" expl="array creation size" expanded="true"> <goal name="WP_parameter all_distinct.1" expl="array creation size">
<proof prover="1"><result status="valid" time="0.02" steps="2"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.2" expl="postcondition" expanded="true"> <goal name="WP_parameter all_distinct.2" expl="postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.3" expl="loop invariant init" expanded="true"> <goal name="WP_parameter all_distinct.3" expl="loop invariant init">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.4" expl="loop invariant init" expanded="true"> <goal name="WP_parameter all_distinct.4" expl="loop invariant init">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.5" expl="index in array bounds" expanded="true"> <goal name="WP_parameter all_distinct.5" expl="index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.6" expl="type invariant" expanded="true"> <goal name="WP_parameter all_distinct.6" expl="type invariant">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.7" expl="index in array bounds" expanded="true"> <goal name="WP_parameter all_distinct.7" expl="index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.8" expl="postcondition" expanded="true"> <goal name="WP_parameter all_distinct.8" expl="postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.9" expl="index in array bounds" expanded="true"> <goal name="WP_parameter all_distinct.9" expl="index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.10" expl="loop invariant preservation" expanded="true"> <goal name="WP_parameter all_distinct.10" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="36"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="36"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.11" expl="loop invariant preservation" expanded="true"> <goal name="WP_parameter all_distinct.11" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="34"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.12" expl="postcondition" expanded="true"> <goal name="WP_parameter all_distinct.12" expl="postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="17"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="17"/></proof>
</goal> </goal>
</transf> </transf>
......
...@@ -4,8 +4,8 @@ ...@@ -4,8 +4,8 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" expanded="true"> <file name="../arm.mlw">
<theory name="M" sum="a8ed8ac125c36f5df5d21cfb0c45379b" expanded="true"> <theory name="M" sum="a8ed8ac125c36f5df5d21cfb0c45379b">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort"> <goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="loop invariant init"> <goal name="WP_parameter insertion_sort.1" expl="loop invariant init">
...@@ -56,9 +56,9 @@ ...@@ -56,9 +56,9 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true"> <theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="InsertionSortExample" sum="bb2596f60660accb63622e86fa9bb854" expanded="true"> <theory name="InsertionSortExample" sum="bb2596f60660accb63622e86fa9bb854">
<goal name="WP_parameter path_init_l2" expl="VC for path_init_l2"> <goal name="WP_parameter path_init_l2" expl="VC for path_init_l2">
<proof prover="1"><result status="valid" time="0.14"/></proof> <proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof> <proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
......
...@@ -5,13 +5,13 @@ ...@@ -5,13 +5,13 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/> <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../assigning_meanings_to_programs.mlw"> <file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="8f3c63959383424df2f105c6c6127ecf" expanded="true"> <theory name="Sum" sum="8f3c63959383424df2f105c6c6127ecf">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true"> <goal name="WP_parameter sum" expl="VC for sum">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof> <proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Division" sum="f62ea84f2ab94541b42c389bab1e7d0d" expanded="true"> <theory name="Division" sum="f62ea84f2ab94541b42c389bab1e7d0d">
<goal name="WP_parameter division" expl="VC for division" expanded="true"> <goal name="WP_parameter division" expl="VC for division">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</theory> </theory>
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
<prover id="3" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="3" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.4.1" timelimit="60" steplimit="0" memlimit="4000"/> <prover id="5" name="CVC3" version="2.4.1" timelimit="60" steplimit="0" memlimit="4000"/>
<prover id="9" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="4000"/> <prover id="9" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../bag.mlw" expanded="true"> <file name="../bag.mlw">
<theory name="Bag" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="Bag" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="BagSpec" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="BagSpec" sum="d41d8cd98f00b204e9800998ecf8427e">
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="2" name="CVC4" version="1.3" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../balance.mlw" expanded="true"> <file name="../balance.mlw">
<theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="Puzzle8" sum="d05576d2511803fe661e8d6a753674ed"> <theory name="Puzzle8" sum="d05576d2511803fe661e8d6a753674ed">
...@@ -80,8 +80,8 @@ ...@@ -80,8 +80,8 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Puzzle12" sum="bb7c05c9be8113b3274ffb728eacf65f" expanded="true"> <theory name="Puzzle12" sum="bb7c05c9be8113b3274ffb728eacf65f">
<goal name="WP_parameter solve12" expl="VC for solve12" expanded="true"> <goal name="WP_parameter solve12" expl="VC for solve12">
<proof prover="2"><result status="valid" time="0.31"/></proof> <proof prover="2"><result status="valid" time="0.31"/></proof>
</goal> </goal>
</theory> </theory>
......
This diff is collapsed.
...@@ -3,9 +3,9 @@ ...@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" expanded="true"> <file name="../binary_multiplication.mlw">
<theory name="BinaryMultiplication" sum="4449384b189c7319b8d5ae6a4c5370ae" expanded="true"> <theory name="BinaryMultiplication" sum="4449384b189c7319b8d5ae6a4c5370ae">
<goal name="WP_parameter binary_mult" expl="VC for binary_mult" expanded="true"> <goal name="WP_parameter binary_mult" expl="VC for binary_mult">
<proof prover="0"><result status="valid" time="0.50" steps="47"/></proof> <proof prover="0"><result status="valid" time="0.50" steps="47"/></proof>
</goal> </goal>
</theory> </theory>
......
...@@ -4,9 +4,9 @@ ...@@ -4,9 +4,9 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" expanded="true"> <file name="../binary_sort.mlw">
<theory name="BinarySort" sum="511f87d74df1b785aefbf2e7aac4ff00" expanded="true"> <theory name="BinarySort" sum="511f87d74df1b785aefbf2e7aac4ff00">
<goal name="WP_parameter occ_shift" expl="VC for occ_shift" expanded="true"> <goal name="WP_parameter occ_shift" expl="VC for occ_shift">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter occ_shift.1" expl="assertion"> <goal name="WP_parameter occ_shift.1" expl="assertion">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
......
...@@ -7,10 +7,10 @@ ...@@ -7,10 +7,10 @@
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_sqrt.mlw" expanded="true"> <file name="../binary_sqrt.mlw">
<theory name="BinarySqrt" sum="9ce354fc5ea5258e85043aee351a1947" expanded="true"> <theory name="BinarySqrt" sum="9ce354fc5ea5258e85043aee351a1947">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true"> <goal name="WP_parameter sqrt" expl="VC for sqrt">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter sqrt.1" expl="postcondition"> <goal name="WP_parameter sqrt.1" expl="postcondition">
<proof prover="7"><result status="valid" time="0.02"/></proof> <proof prover="7"><result status="valid" time="0.02"/></proof>
</goal> </goal>
...@@ -55,8 +55,8 @@ ...@@ -55,8 +55,8 @@
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter sqrt_main" expl="VC for sqrt_main" expanded="true"> <goal name="WP_parameter sqrt_main" expl="VC for sqrt_main">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp">
<goal name="WP_parameter sqrt_main.1" expl="precondition"> <goal name="WP_parameter sqrt_main.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
......
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/> <prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector.why" expanded="true"> <file name="../bitvector.why">
<theory name="BitVector" sum="5720c2b4494f4318602469524b5a7701"> <theory name="BitVector" sum="5720c2b4494f4318602469524b5a7701">
<goal name="Nth_bw_xor_v1true" expl=""> <goal name="Nth_bw_xor_v1true" expl="">
<proof prover="2"><result status="valid" time="0.08" steps="85"/></proof> <proof prover="2"><result status="valid" time="0.08" steps="85"/></proof>
......
...@@ -7,14 +7,14 @@ ...@@ -7,14 +7,14 @@
<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="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/> <prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double.why" expanded="true"> <file name="../double.why">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="TestDouble" sum="b7b2448ba36ad5c80868aff06a16bf4d" expanded="true"> <theory name="TestDouble" sum="b7b2448ba36ad5c80868aff06a16bf4d">
<goal name="nth_one1" expl="" expanded="true"> <goal name="nth_one1" expl="">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof> <proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal> </goal>
<goal name="nth_one2" expl="" expanded="true"> <goal name="nth_one2" expl="">
<proof prover="0" timelimit="3"><result status="valid" time="0.04" steps="77"/></proof> <proof prover="0" timelimit="3"><result status="valid" time="0.04" steps="77"/></proof>
</goal> </goal>
<goal name="nth_one3" expl=""> <goal name="nth_one3" expl="">
...@@ -26,7 +26,7 @@ ...@@ -26,7 +26,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof> <proof prover="5"><result status="valid" time="0.11"/></proof>
</goal> </goal>
<goal name="exp_one" expl="" expanded="true"> <goal name="exp_one" expl="">
<proof prover="0" timelimit="30"><result status="valid" time="2.23" steps="668"/></proof> <proof prover="0" timelimit="30"><result status="valid" time="2.23" steps="668"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof> <proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof>
</goal> </goal>
......
...@@ -9,8 +9,8 @@ ...@@ -9,8 +9,8 @@
<prover id="5" name="Coq" version="8.7.1" timelimit="60" steplimit="0" memlimit="1000"/>