Commit 42700759 authored by MARCHE Claude's avatar MARCHE Claude

removed usage of theory checksum (see issue #81)

updated the DTD accordingly, and all session files
parent e8e1db6b
......@@ -10,7 +10,7 @@
<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"/>
<file name="../blocking_semantics5.mlw">
<theory name="Syntax" sum="f7cde33e5e26ee60d3da8eec7b217241">
<theory name="Syntax">
<goal name="mident_decide" expl="">
<proof prover="9"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -21,7 +21,7 @@
<proof prover="9"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
</theory>
<theory name="SemOp" sum="60fbf73e1f7166ff30a0a13e124972f7">
<theory name="SemOp">
<goal name="get_stack_eq" expl="">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.04"/></proof>
......@@ -38,7 +38,7 @@
<proof prover="1" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.31"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="86970d496f2db125feae52276a283ee6">
<theory name="TestSemantics">
<goal name="Test13" expl="">
<proof prover="9"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="10"><result status="valid" time="0.03"/></proof>
......@@ -60,9 +60,9 @@
<proof prover="1" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="0.81"/></proof>
</goal>
</theory>
<theory name="Typing" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Typing">
</theory>
<theory name="TypingAndSemantics" sum="a93f17496bf551e48a79468a47f1668b">
<theory name="TypingAndSemantics">
<goal name="type_inversion" expl="">
<transf name="induction_ty_lex">
<goal name="type_inversion.1" expl="">
......@@ -100,7 +100,7 @@
<proof prover="1" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="1.52"/></proof>
</goal>
</theory>
<theory name="FreshVariables" sum="e8d942e6e9d0add73d0d37a3267da968">
<theory name="FreshVariables">
<goal name="Cons_append" expl="">
<proof prover="9"><result status="valid" time="0.03" steps="13"/></proof>
</goal>
......@@ -337,7 +337,7 @@
</transf>
</goal>
</theory>
<theory name="HoareLogic" sum="23cedd132ddce3b408fd64127096ec7a">
<theory name="HoareLogic">
<goal name="many_steps_seq" expl="">
<proof prover="1" edited="blocking_semantics5_HoareLogic_many_steps_seq_1.v"><result status="valid" time="0.92"/></proof>
</goal>
......@@ -367,7 +367,7 @@
<proof prover="1" edited="blocking_semantics5_HoareLogic_while_rule_1.v"><result status="valid" time="0.46"/></proof>
</goal>
</theory>
<theory name="WP" sum="5cc3a5597ba7d5d9898b25547d8addba">
<theory name="WP">
<goal name="monotonicity" expl="">
<transf name="induction_ty_lex">
<goal name="monotonicity.1" expl="">
......
......@@ -6,9 +6,9 @@
<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"/>
<file name="../formula.why">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Formula">
</theory>
<theory name="PropositionalCalculus" sum="2197343d91936e442b6aeb7d3a3b50db">
<theory name="PropositionalCalculus">
<goal name="Test1" expl="">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
......
......@@ -8,7 +8,7 @@
<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"/>
<file name="../imp_n.why">
<theory name="Imp" sum="4edcb627e6f7cecac2b0d3f266958856">
<theory name="Imp">
<goal name="ident_eq_dec" expl="">
<proof prover="6"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
......
......@@ -7,7 +7,7 @@
<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"/>
<file name="../wp2.mlw">
<theory name="Imp" sum="4d6ec4c3ea3a39365f84600c953b8179">
<theory name="Imp">
<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>
</goal>
......@@ -35,7 +35,7 @@
<proof prover="0" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="ea9fb18b1935c25df0ce7f228aabf76f">
<theory name="TestSemantics">
<goal name="Test13" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="2"/></proof>
......@@ -59,7 +59,7 @@
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.00"/></proof>
</goal>
</theory>
<theory name="HoareLogic" sum="ac7395abbc54f2eaf2a4731bbadf3a7c">
<theory name="HoareLogic">
<goal name="consequence_rule" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.32"/></proof>
</goal>
......@@ -88,7 +88,7 @@
<proof prover="0" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
</goal>
</theory>
<theory name="WP" sum="ac7e95b3f1136de0ba1a9054f4091dbf">
<theory name="WP">
<goal name="assigns_refl" expl="">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
......
......@@ -6,9 +6,9 @@
<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"/>
<file name="../add_list.mlw">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="SumList">
</theory>
<theory name="AddListRec" sum="ddf9071b1a9688fe9218a8b95f77634f">
<theory name="AddListRec">
<goal name="WP_parameter sum" expl="VC for sum">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -19,7 +19,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="b8d9e3c0e71fb300ad846cc5060783ef">
<theory name="AddListImp">
<goal name="WP_parameter sum" expl="VC for sum">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......
......@@ -5,7 +5,7 @@
<prover id="1" name="Eprover" version="1.8-001" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true" sum="24fc90fcff68609a56b7e8b043f981e2">
<theory name="Algo63" proved="true">
<goal name="WP_parameter exchange" expl="VC for exchange" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="29"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw">
<theory name="Algo64" sum="51d805a22bc2e9af151efc73086f3b23">
<theory name="Algo64">
<goal name="WP_parameter quicksort" expl="VC for quicksort">
<transf name="split_goal_wp">
<goal name="WP_parameter quicksort.1" expl="precondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw">
<theory name="Algo65" sum="4ec16c9b9e583f9273e61e0b69664be0">
<theory name="Algo65">
<goal name="WP_parameter find" expl="VC for find">
<transf name="split_goal_wp">
<goal name="WP_parameter find.1" expl="precondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw">
<theory name="AllDistinct" sum="9890dccbada5eed3f27377796f4d13ec">
<theory name="AllDistinct">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct">
<transf name="split_goal_wp">
<goal name="WP_parameter all_distinct.1" expl="array creation size">
......
......@@ -5,7 +5,7 @@
<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"/>
<file name="../arm.mlw">
<theory name="M" sum="a8ed8ac125c36f5df5d21cfb0c45379b">
<theory name="M">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="loop invariant init">
......@@ -56,9 +56,9 @@
</transf>
</goal>
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="ARM">
</theory>
<theory name="InsertionSortExample" sum="bb2596f60660accb63622e86fa9bb854">
<theory name="InsertionSortExample">
<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="3"><result status="valid" time="0.02" steps="17"/></proof>
......
......@@ -5,12 +5,12 @@
<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"/>
<file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="8f3c63959383424df2f105c6c6127ecf">
<theory name="Sum">
<goal name="WP_parameter sum" expl="VC for sum">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
</theory>
<theory name="Division" sum="f62ea84f2ab94541b42c389bab1e7d0d">
<theory name="Division">
<goal name="WP_parameter division" expl="VC for division">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -5,7 +5,7 @@
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../association_list.mlw">
<theory name="Assoc" sum="f1eec4bdbae0cd684ad7ea962bb9e8e4">
<theory name="Assoc">
<goal name="appear_append" expl="">
<proof prover="4"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
......@@ -72,7 +72,7 @@
</transf>
</goal>
</theory>
<theory name="AssocSorted" sum="2c15cf21cebb766828cb0ce1bbb7c823">
<theory name="AssocSorted">
<goal name="Eq.Refl" expl="">
<proof prover="4"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......
......@@ -5,12 +5,12 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="2" steplimit="0" memlimit="0"/>
<file name="../avl.mlw">
<theory name="SelectionTypes" sum="524429d11c4ad874e40c019262594465">
<theory name="SelectionTypes">
<goal name="rebuild_aternative_def" expl="">
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.07" steps="88"/></proof>
</goal>
</theory>
<theory name="AVL" sum="b73997428ccb586bd42fd89fda00c186">
<theory name="AVL">
<goal name="M.M.assoc" expl="">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
......
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../key_type.mlw">
<theory name="KeyType" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="KeyType">
</theory>
<theory name="ProgramKeyType" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="ProgramKeyType">
</theory>
</file>
</why3session>
......@@ -4,14 +4,14 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../monoid.mlw">
<theory name="Monoid" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Monoid">
</theory>
<theory name="MonoidSum" sum="6dbf81b70f8a683573bb1e9010f902f0">
<theory name="MonoidSum">
<goal name="WP_parameter sum_append" expl="VC for sum_append">
<proof prover="1"><result status="valid" time="0.03" steps="27"/></proof>
</goal>
</theory>
<theory name="MonoidSumDef" sum="d6f1521e70c50941e7b758c2b840b19e">
<theory name="MonoidSumDef">
<goal name="sum_def_nil" expl="">
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -19,7 +19,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
</theory>
<theory name="ComputableMonoid" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="ComputableMonoid">
</theory>
</file>
</why3session>
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="3" steplimit="0" memlimit="1000"/>
<file name="../preorder.mlw">
<theory name="Full" sum="41eddb6a5f9e7172479be99f6dc563ca">
<theory name="Full">
<goal name="Eq.Refl">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
......@@ -21,7 +21,7 @@
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
<theory name="TotalFull" sum="b7a34af67ae9cf9bf55e6d6a58a0f423">
<theory name="TotalFull">
<goal name="Lt.Total">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
......@@ -29,7 +29,7 @@
<proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
</theory>
<theory name="Computable" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Computable">
</theory>
</file>
</why3session>
......@@ -7,7 +7,7 @@
<prover id="2" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../priority_queue.mlw" proved="true">
<theory name="PQueue" proved="true" sum="2a7bb7c7183fdccd6de1df98e72a50bc">
<theory name="PQueue" proved="true">
<goal name="Trans" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="19714b392bd8e5e1cf08fdb09f06643c">
<theory name="RAL">
<goal name="M.assoc" expl="">
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../sorted.mlw">
<theory name="Increasing" sum="baae8633e3006c26787a2ff04fe40ed5">
<theory name="Increasing">
<goal name="smaller_lower_bound" expl="">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tables.mlw" proved="true">
<theory name="MapBase" proved="true" sum="ed1f23290df416ffeff89b8c527f1571">
<theory name="MapBase" proved="true">
<goal name="WP_parameter measure" expl="VC for measure" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
......@@ -780,7 +780,7 @@
</transf>
</goal>
</theory>
<theory name="Map" proved="true" sum="3b0dc7ad12f01af75afa6c2569cb19c4">
<theory name="Map" proved="true">
<goal name="WP_parameter get_key" expl="VC for get_key" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -851,7 +851,7 @@
<proof prover="1"><result status="valid" time="0.28" steps="715"/></proof>
</goal>
</theory>
<theory name="Set" proved="true" sum="4136cf7c473e4c0ea62656646bfba52b">
<theory name="Set" proved="true">
<goal name="WP_parameter get_key" expl="VC for get_key" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -947,7 +947,7 @@
<proof prover="1" timelimit="1"><result status="valid" time="0.06" steps="222"/></proof>
</goal>
</theory>
<theory name="IMapAndSet" proved="true" sum="ff61b4113e7742621c274153ebf13364">
<theory name="IMapAndSet" proved="true">
<goal name="WP_parameter compare" expl="VC for compare" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.01" steps="0"/></proof>
</goal>
......
......@@ -8,13 +8,13 @@
<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"/>
<file name="../bag.mlw">
<theory name="Bag" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Bag">
</theory>
<theory name="BagSpec" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="BagSpec">
</theory>
<theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="ResizableArraySpec">
</theory>
<theory name="BagImpl" sum="04f2593d97604dbae67eb342f4687d32">
<theory name="BagImpl">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
......@@ -110,7 +110,7 @@
</transf>
</goal>
</theory>
<theory name="Harness" sum="54e66c5ddd34c1e0113aa1b612b77112">
<theory name="Harness">
<goal name="WP_parameter test1" expl="VC for test1">
<transf name="split_goal_wp">
<goal name="WP_parameter test1.1" expl="assertion">
......
......@@ -6,9 +6,9 @@
<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"/>
<file name="../balance.mlw">
<theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Roberval">
</theory>
<theory name="Puzzle8" sum="d05576d2511803fe661e8d6a753674ed">
<theory name="Puzzle8">
<goal name="WP_parameter solve3" expl="VC for solve3">
<proof prover="1"><result status="valid" time="0.01" steps="41"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="52"/></proof>
......@@ -80,7 +80,7 @@
</transf>
</goal>
</theory>
<theory name="Puzzle12" sum="bb7c05c9be8113b3274ffb728eacf65f">
<theory name="Puzzle12">
<goal name="WP_parameter solve12" expl="VC for solve12">
<proof prover="2"><result status="valid" time="0.31"/></proof>
</goal>
......
......@@ -11,7 +11,7 @@
<prover id="10" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bellman_ford.mlw" proved="true">
<theory name="Graph" proved="true" sum="49cc8e4186915b1ef6dd771303cc5760">
<theory name="Graph" proved="true">
<goal name="vertices_cardinal_pos" proved="true">
<proof prover="8" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
......@@ -37,7 +37,7 @@
<proof prover="0" timelimit="10" memlimit="0" edited="bf_Graph_key_lemma_1_1.v"><result status="valid" time="1.69"/></proof>
</goal>
</theory>
<theory name="BellmanFord" proved="true" sum="d0c03acce6765f1070ef467f5c54f705">
<theory name="BellmanFord" proved="true">
<goal name="key_lemma_2" proved="true">
<proof prover="0" memlimit="4000" edited="bf_WP_BellmanFord_key_lemma_2_1.v"><result status="valid" time="2.76"/></proof>
</goal>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../bignum.mlw">
<theory name="BigNum" sum="1fae80aec7dd5e698e2707bddfd6c28b">
<theory name="BigNum">
<goal name="WP_parameter nonneg" expl="VC for nonneg">
<transf name="split_goal_wp">
<goal name="WP_parameter nonneg.1" expl="postcondition">
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw">
<theory name="BinaryMultiplication" sum="4449384b189c7319b8d5ae6a4c5370ae">
<theory name="BinaryMultiplication">
<goal name="WP_parameter binary_mult" expl="VC for binary_mult">
<proof prover="0"><result status="valid" time="0.50" steps="47"/></proof>
</goal>
......
......@@ -7,21 +7,21 @@
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_search.mlw" proved="true">
<theory name="BinarySearch" proved="true" sum="7bf7883d6e8fde9d87f261fd912923e0">
<theory name="BinarySearch" proved="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.17" steps="59"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" proved="true" sum="617e28329136ba275ecf8ba02bcc2957">
<theory name="BinarySearchAnyMidPoint" proved="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true" sum="bf7b08f3631f7a99219dd72d9ff9e24f">
<theory name="BinarySearchInt32" proved="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter binary_search.0" expl="integer overflow" proved="true">
......@@ -106,7 +106,7 @@
</transf>
</goal>
</theory>
<theory name="BinarySearchBoolean" proved="true" sum="665a5152cccd5f2361968000d62eb210">
<theory name="BinarySearchBoolean" proved="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="118"/></proof>
</goal>
......
......@@ -5,7 +5,7 @@
<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"/>
<file name="../binary_sort.mlw">
<theory name="BinarySort" sum="511f87d74df1b785aefbf2e7aac4ff00">
<theory name="BinarySort">
<goal name="WP_parameter occ_shift" expl="VC for occ_shift">
<transf name="split_goal_wp">
<goal name="WP_parameter occ_shift.1" expl="assertion">
......
......@@ -8,7 +8,7 @@
<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"/>
<file name="../binary_sqrt.mlw">
<theory name="BinarySqrt" sum="9ce354fc5ea5258e85043aee351a1947">
<theory name="BinarySqrt">
<goal name="WP_parameter sqrt" expl="VC for sqrt">
<transf name="split_goal_wp">
<goal name="WP_parameter sqrt.1" expl="postcondition">
......
......@@ -7,7 +7,7 @@
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binomial_heap.mlw" proved="true">
<theory name="BinomialHeap" proved="true" sum="c73423ae83bf256f76beff55439dbfd7">
<theory name="BinomialHeap" proved="true">
<goal name="WP_parameter size_nonnneg" expl="VC for size_nonnneg" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
......
......@@ -11,7 +11,7 @@
<prover id="6" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitcount.mlw" proved="true">
<theory name="BitCount8bit_fact" proved="true" sum="b2c587134cc06bcdceac094cd6c17750">
<theory name="BitCount8bit_fact" proved="true">
<goal name="nth_as_bv_is_int" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.16" steps="166"/></proof>
......@@ -219,7 +219,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" proved="true" sum="9e4d0d1cd977ec3554c7002f08c5c385">
<theory name="BitCounting32" proved="true">
<goal name="WP_parameter proof0" expl="VC for proof0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter proof0.0"