Commit d7d97acc authored by MARCHE Claude's avatar MARCHE Claude

updated obsolete sessions

parent 008aef67
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -1196,10 +1196,10 @@
<goal name="WP_parameter bellman_ford.14.2.1.3" expl="3. VC for bellman_ford">
<transf name="eliminate_builtin">
<goal name="WP_parameter bellman_ford.14.2.1.3.1" expl="1. VC for bellman_ford">
<proof prover="2" obsolete="true"><result status="valid" time="0.45"/></proof>
<proof prover="8" obsolete="true"><result status="valid" time="1.44" steps="1775"/></proof>
<proof prover="9" obsolete="true"><result status="valid" time="0.29"/></proof>
<proof prover="10" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.45"/></proof>
<proof prover="8"><result status="valid" time="1.44" steps="1775"/></proof>
<proof prover="9"><result status="valid" time="0.29"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......@@ -2186,10 +2186,10 @@
<goal name="WP_parameter bellman_ford.14.2.1.5" expl="5. VC for bellman_ford">
<transf name="eliminate_builtin">
<goal name="WP_parameter bellman_ford.14.2.1.5.1" expl="1. VC for bellman_ford">
<proof prover="2" obsolete="true"><result status="valid" time="0.28"/></proof>
<proof prover="8" obsolete="true"><result status="valid" time="0.24" steps="547"/></proof>
<proof prover="9" obsolete="true"><result status="valid" time="0.29"/></proof>
<proof prover="10" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.28"/></proof>
<proof prover="8"><result status="valid" time="0.24" steps="547"/></proof>
<proof prover="9"><result status="valid" time="0.29"/></proof>
<proof prover="10"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -2207,7 +2207,7 @@
<goal name="WP_parameter bellman_ford.16" expl="16. assertion">
<transf name="inline_goal">
<goal name="WP_parameter bellman_ford.16.1" expl="1. assertion">
<proof prover="6" timelimit="54"><result status="valid" time="4.64" steps="752"/></proof>
<proof prover="6" timelimit="54"><result status="valid" time="4.08" steps="752"/></proof>
</goal>
</transf>
</goal>
......
......@@ -23,7 +23,7 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="a262c15cb4d2436b3ce5f5f23a0c4cc8" expanded="true">
<theory name="BinarySearchInt32" sum="1a20b53b88547b45b31a04796cdc6796" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
......
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="2f7ca04436adce0a2ff366b7c0732b04" expanded="true">
<theory name="Test_proofinuse" sum="28f69746dc8ff9c44df602d0c0d5d0b8" expanded="true">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter shift_is_div.1" expl="1. assertion" expanded="true">
......@@ -40,7 +40,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="4654c8ff303455bf7fa77e548ce32e29" expanded="true">
<theory name="Hackers_delight" sum="9705eaccc6076bac3885e79a54965be4" expanded="true">
<goal name="DM1" expanded="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -103,7 +103,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="9bd65287ded6227801e3938797884abf" expanded="true">
<theory name="Hackers_delight_mod" sum="d52e2c470f4cc499dd89711163d487dc" expanded="true">
<goal name="WP_parameter dm1" expl="VC for dm1" expanded="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -172,7 +172,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="b7325d5e488675e7561a07698251c8c7" expanded="true">
<theory name="Test_imperial_violet" sum="bcb782e1a7e132b2f42dad1f91362e75" expanded="true">
<goal name="bv32_bounds_bv" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="144"/></proof>
<proof prover="1"><result status="valid" time="0.25"/></proof>
......@@ -199,7 +199,7 @@
<proof prover="1"><result status="valid" time="0.95"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="10084efad7e8cec54eff063c84fbe1f6" expanded="true">
<theory name="Test_from_bitvector_example" sum="22d1d76b63ec655dcadb3387aad2a5b3" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="96"/></proof>
<proof prover="1"><result status="valid" time="0.22"/></proof>
......@@ -270,14 +270,14 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr20" expl="VC for lsr20" expanded="true">
<proof prover="0"><result status="valid" time="0.24" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="1"><result status="valid" time="0.41"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr13" expl="VC for lsr13" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="1"><result status="valid" time="0.56"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -12,7 +12,7 @@
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestDouble" sum="6f68b2bb458812f8dac7a682020945e6" expanded="true">
<theory name="TestDouble" sum="2dfd8f472574f55c4ed59e7a347e128e" expanded="true">
<goal name="nth_one1" expanded="true">
<proof prover="6" timelimit="3"><result status="valid" time="0.32" steps="107"/></proof>
</goal>
......
......@@ -11,14 +11,14 @@
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="6138fee1d9542841b21ad746cad9a930" expanded="true">
<theory name="TestNegAsXOR" sum="4b3f5b71a28db1ecea74d9fd0780e47d" expanded="true">
<goal name="Nth_j">
<proof prover="1"><result status="valid" time="0.56" steps="114"/></proof>
<proof prover="6" timelimit="3"><result status="valid" time="0.35" steps="107"/></proof>
</goal>
<goal name="sign_of_j">
<proof prover="1"><result status="valid" time="0.15" steps="108"/></proof>
<proof prover="3"><result status="valid" time="0.86"/></proof>
<proof prover="3"><result status="valid" time="0.65"/></proof>
<proof prover="6"><result status="valid" time="0.09" steps="100"/></proof>
</goal>
<goal name="mantissa_of_j">
......@@ -34,7 +34,7 @@
<proof prover="1"><result status="valid" time="0.17" steps="124"/></proof>
<proof prover="2"><result status="valid" time="0.62"/></proof>
<proof prover="3"><result status="valid" time="0.59"/></proof>
<proof prover="4"><result status="valid" time="0.92"/></proof>
<proof prover="4"><result status="valid" time="0.70"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.13"/></proof>
<proof prover="6"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
......@@ -51,7 +51,7 @@
<goal name="MainResultBits">
<proof prover="1"><result status="valid" time="0.15" steps="132"/></proof>
<proof prover="3"><result status="valid" time="0.55"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="128"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="127"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="MainResultSign">
......@@ -89,7 +89,7 @@
<proof prover="2"><result status="valid" time="1.36"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.94"/></proof>
<proof prover="5"><result status="valid" time="3.57"/></proof>
<proof prover="5"><result status="valid" time="3.08"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.20" steps="142"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
......@@ -100,8 +100,8 @@
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult">
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="2.42"/></proof>
<proof prover="1"><result status="valid" time="2.27" steps="326"/></proof>
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="1.86"/></proof>
<proof prover="1"><result status="valid" time="1.92" steps="326"/></proof>
</goal>
</theory>
</file>
......
......@@ -7,22 +7,22 @@
<prover id="2" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" memlimit="0"/>
<file name="../bool.why" expanded="true">
<theory name="Test" sum="abfec60b825ac36924745736298e461b" expanded="true">
<theory name="Test" sum="1df769008ab78b260468adc25cb91f79" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -10,7 +10,7 @@
<file name="../cursor.mlw">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestCursor" sum="b7657686cab5c94f3d90eee7eca8293b">
<theory name="TestCursor" sum="e56a5bf38578a0a432da76c0aaee8164">
<goal name="WP_parameter sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="WP_parameter sum.1" expl="1. loop invariant init">
......
This diff is collapsed.
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../imp.why" expanded="true">
<theory name="Imp" sum="5a89c7a4dcbf74c008d517cb12f85b7a">
<theory name="Imp" sum="3b90bd1ffd336bb62782238529a2e860">
<goal name="ceval_deterministic_aux">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="1.">
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<file name="../ewd673.mlw" expanded="true">
<theory name="EWD673" sum="89d52bfbe8b3834a651b9d1a7379cfc3" expanded="true">
<theory name="EWD673" sum="311658b97d5a6f9e4fc143d881b6e9c5" expanded="true">
<goal name="WP_parameter s" expl="VC for s" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
</theory>
</file>
......
......@@ -9,53 +9,53 @@
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Utils_Spec" sum="3967722ffb6389d883275ccf0879b34f" expanded="true">
<theory name="Utils_Spec" sum="847a297558090f626aad0b2d693c227e" expanded="true">
<goal name="countZero" expanded="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="numOfZero" expanded="true">
<proof prover="0"><result status="valid" time="0.87" steps="228"/></proof>
<proof prover="3"><result status="valid" time="0.78"/></proof>
<proof prover="0"><result status="valid" time="0.47" steps="228"/></proof>
<proof prover="3"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="countStep" expanded="true">
<proof prover="1" timelimit="30"><result status="valid" time="5.82"/></proof>
<proof prover="1" timelimit="30"><result status="valid" time="4.95"/></proof>
</goal>
<goal name="WP_parameter numof_shift" expl="VC for numof_shift" expanded="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.34"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux" expl="VC for countSpec_Aux" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter countSpec_Aux.1" expl="1. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.89" steps="265"/></proof>
<proof prover="0"><result status="valid" time="0.47" steps="265"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.61"/></proof>
<proof prover="3"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease" expanded="true">
<proof prover="1"><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.99"/></proof>
<proof prover="3"><result status="valid" time="0.41"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3" expl="3. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter countSpec_Aux.3.1" expl="1. assertion" expanded="true">
<proof prover="3"><result status="valid" time="1.86"/></proof>
<proof prover="3"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion" expanded="true">
<proof prover="3"><result status="valid" time="0.60"/></proof>
<proof prover="3"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion" expanded="true">
<proof prover="0"><result status="valid" time="0.90" steps="158"/></proof>
<proof prover="0"><result status="valid" time="0.51" steps="158"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion" expanded="true">
<proof prover="3" timelimit="15"><result status="valid" time="7.26"/></proof>
<proof prover="3" timelimit="15"><result status="valid" time="3.83"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter countSpec_Aux.4" expl="4. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.57"/></proof>
<proof prover="1"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
</goal>
......@@ -68,7 +68,7 @@
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter hamming_spec.1" expl="1. assertion" expanded="true">
<proof prover="0"><result status="valid" time="0.25" steps="216"/></proof>
<proof prover="0"><result status="valid" time="1.47" steps="592"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter hamming_spec.2" expl="2. postcondition" expanded="true">
......@@ -81,13 +81,13 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="separation" expanded="true">
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter numof_or" expl="VC for numof_or" expanded="true">
<proof prover="1"><result status="valid" time="0.53"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.30"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt" expanded="true">
<transf name="split_goal_wp" expanded="true">
......@@ -115,7 +115,7 @@
<proof prover="1" timelimit="15"><result status="valid" time="2.35"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="c8ec539e41c47d4d821a25e51a788371" expanded="true">
<theory name="Hackers_delight" sum="275dc4d80fc97952f381d86f9f73fc33" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii" expanded="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -132,14 +132,14 @@
</goal>
<goal name="nthGray" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="2.73"/></proof>
<proof prover="3"><result status="valid" time="1.46"/></proof>
</goal>
<goal name="lastNthGray" expanded="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="2.22"/></proof>
<proof prover="3"><result status="valid" time="1.02"/></proof>
</goal>
<goal name="nthBinary" expanded="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.38"/></proof>
<proof prover="1" timelimit="30"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="evenOdd" expanded="true">
<proof prover="1"><result status="valid" time="0.14"/></proof>
......
......@@ -14,7 +14,7 @@
<prover id="9" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="10" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<file name="../blocking_semantics5.mlw" expanded="true">
<theory name="Syntax" sum="8dc2e4bff12fd419e76529908b6eb472">
<theory name="Syntax" sum="2de9c4bb8601cb580add66a10580a6da">
<goal name="mident_decide">
<proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
......@@ -25,7 +25,7 @@
<proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
</theory>
<theory name="SemOp" sum="4e6742b97be7449b4cb5e8c610e0eedc">
<theory name="SemOp" sum="f781d1e1c0632bbfac9169ef1ac38b42">
<goal name="get_stack_eq">
<proof prover="3" timelimit="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="6"/></proof>
......@@ -44,7 +44,7 @@
<proof prover="1" memlimit="1000" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="1.02"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="4c73e3dbde7aba44cc38775168e54389">
<theory name="TestSemantics" sum="5386d426772b7907db51e574cfc3e48a">
<goal name="Test13">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="3"/></proof>
......@@ -68,7 +68,7 @@
</theory>
<theory name="Typing" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TypingAndSemantics" sum="ec272bc049f1d4b31d148d825ee7f14f">
<theory name="TypingAndSemantics" sum="8108b51d56192fd80d06ffc9907680cf">
<goal name="type_inversion">
<proof prover="1" timelimit="6" memlimit="1000" edited="blocking_semantics5_TypingAndSemantics_type_inversion_1.v"><result status="valid" time="1.65"/></proof>
<transf name="induction_ty_lex">
......@@ -111,7 +111,7 @@
<proof prover="1" memlimit="1000" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="2.62"/></proof>
</goal>
</theory>
<theory name="FreshVariables" sum="6d8e655a14f4bd0e9d9de6ddf748c00a">
<theory name="FreshVariables" sum="490368b5a16b190f6c29edfc9b0d5a6b">
<goal name="Cons_append">
<proof prover="4" memlimit="1000"><result status="valid" time="0.03" steps="7"/></proof>
</goal>
......@@ -279,7 +279,7 @@
<proof prover="4" timelimit="30"><result status="valid" time="0.15" steps="127"/></proof>
</goal>
<goal name="eval_swap_gen.1.11" expl="11.">
<proof prover="4" timelimit="30"><result status="valid" time="9.48" steps="4160"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="9.48" steps="3852"/></proof>
</goal>
<goal name="eval_swap_gen.1.12" expl="12.">
<proof prover="4" timelimit="30"><result status="valid" time="7.70" steps="3544"/></proof>
......@@ -383,7 +383,7 @@
</transf>
</goal>
</theory>
<theory name="HoareLogic" sum="f3463f6a9e5ddbe0700794e7bbb11178">
<theory name="HoareLogic" sum="06bb2600c8d8760878e05c429245d541">
<goal name="many_steps_seq">
<proof prover="1" memlimit="1000" edited="blocking_semantics5_HoareLogic_many_steps_seq_1.v"><result status="valid" time="1.73"/></proof>
</goal>
......@@ -414,7 +414,7 @@
<proof prover="1" memlimit="1000" edited="blocking_semantics5_HoareLogic_while_rule_1.v"><result status="valid" time="1.39"/></proof>
</goal>
</theory>
<theory name="WP" sum="88b824b8532e7039f8b2a59918544638">
<theory name="WP" sum="c3b1d24b21f6d88ab3dc3fc87a7ea92a">
<goal name="monotonicity">
<transf name="induction_ty_lex">
<goal name="monotonicity.1" expl="1.">
......@@ -442,7 +442,7 @@
<proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="monotonicity.1.6" expl="6.">
<proof prover="1" memlimit="1000" edited="blocking_semantics5_WP_monotonicity_3.v"><result status="valid" time="1.25"/></proof>
<proof prover="1" memlimit="1000" edited="blocking_semantics5_WP_monotonicity_3.v"><result status="valid" time="0.96"/></proof>
</goal>
</transf>
</goal>
......@@ -465,7 +465,7 @@
</goal>
<goal name="distrib_conj.1.4" expl="4.">
<proof prover="0"><result status="valid" time="0.08"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.70" steps="2685"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.89" steps="3316"/></proof>
<proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="distrib_conj.1.5" expl="5.">
......
......@@ -8,11 +8,11 @@
<file name="../formula.why">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="PropositionalCalculus" sum="301cb7a5ed4189e6ad27314d2bb7c0a4" expanded="true">
<theory name="PropositionalCalculus" sum="7ca365b7b7386e0bf1ce16a164074533" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="46"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
</theory>
</file>
......
......@@ -10,7 +10,7 @@
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
<file name="../wp2.mlw" expanded="true">
<theory name="Imp" sum="b532cee701e945a262f760dcdf2eb774">
<theory name="Imp" sum="128a05171862f85c119bf4cc4ff1493c">
<goal name="eval_subst_term">
<proof prover="0" timelimit="5" memlimit="0" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.88"/></proof>
</goal>
......@@ -25,7 +25,7 @@
<proof prover="4" timelimit="3" memlimit="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="eval_change_free">
<proof prover="0" timelimit="5" memlimit="0" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="1.15"/></proof>
<proof prover="0" timelimit="5" memlimit="0" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.91"/></proof>
</goal>
<goal name="check_skip">
<proof prover="1" timelimit="5" memlimit="0"><result status="valid" time="0.01" steps="2"/></proof>
......@@ -41,7 +41,7 @@
<proof prover="0" memlimit="0" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="1.04"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="c7994a3b47b5bcf2f9e9af33ab586107">
<theory name="TestSemantics" sum="43e242b3d12bc39d4b29f9b888732dc9">
<goal name="Test13">
<proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -69,7 +69,7 @@
<proof prover="0" timelimit="5" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="2.17"/></proof>
</goal>
</theory>
<theory name="HoareLogic" sum="bcb6cb9d4fd1ffebe18a70f2b461f2eb">
<theory name="HoareLogic" sum="82e50c9c6ac0f07e1bde1792daeea9d0">
<goal name="consequence_rule">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
......@@ -100,7 +100,7 @@
<proof prover="0" memlimit="0" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="1.17"/></proof>
</goal>
</theory>
<theory name="WP" sum="bf5656d59e0d8e42666645707fd25671" expanded="true">
<theory name="WP" sum="2eefef2d9f018c4c3ae47c2538543bed" expanded="true">
<goal name="assigns_refl">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
......
This diff is collapsed.
......@@ -7,13 +7,13 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="d35077f1ef4ed4360e683835f5410ec4" expanded="true">
<theory name="TestBV" sum="963c694e921f3386f04b0405c5dd8d3f" expanded="true">
<goal name="g1">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="f1">
<proof prover="0"><result status="timeout" time="3.02"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="2.62"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.97"/></proof>
......@@ -23,7 +23,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="f2">
<proof prover="0"><result status="timeout" time="2.88"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="2.62"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
......@@ -45,26 +45,26 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="f3c" expanded="true">
<proof prover="0"><result status="timeout" time="2.44"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g3aa">
<proof prover="0"><result status="timeout" time="2.41"/></proof>
<proof prover="1"><result status="unknown" time="2.86"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="1.32"/></proof>
<proof prover="2"><result status="unknown" time="0.02"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g3bb">
<proof prover="0"><result status="timeout" time="2.64"/></proof>
<proof prover="1"><result status="unknown" time="1.21"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.50"/></proof>
<proof prover="2"><result status="unknown" time="0.03"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="f3cc">
<proof prover="0"><result status="timeout" time="2.65"/></proof>
<proof prover="1"><result status="unknown" time="6.92"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="3.13"/></proof>
<proof prover="2"><result status="unknown" time="0.02"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
......@@ -79,12 +79,12 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g4aa" expanded="true">
<proof prover="0"><result status="timeout" time="2.53"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="2.75"/></proof>
</goal>
<goal name="g4bb">
<proof prover="0"><result status="timeout" time="2.54"/></proof>
<proof prover="1"><result status="unknown" time="1.48"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="0.63"/></proof>
</goal>
<goal name="g5a">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -95,14 +95,14 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g5aa">
<proof prover="0"><result status="timeout" time="2.65"/></proof>
<proof prover="1"><result status="unknown" time="2.79"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="1.36"/></proof>
<proof prover="2"><result status="unknown" time="0.02"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g5bb">
<proof prover="0"><result status="timeout" time="2.53"/></proof>
<proof prover="1"><result status="unknown" time="4.10"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="1.92"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
......@@ -117,14 +117,14 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g7a">
<proof prover="0"><result status="timeout" time="2.52"/></proof>
<proof prover="1"><result status="unknown" time="4.92"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="2.17"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.92"/></proof>
</goal>
<goal name="g7b">
<proof prover="0"><result status="timeout" time="2.55"/></proof>
<proof prover="1"><result status="unknown" time="4.04"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="1"><result status="unknown" time="1.89"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
......@@ -137,12 +137,12 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g8aa">
<proof prover="0"><result status="timeout" time="2.54"/></proof>
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="5.03"/></proof>
</goal>
<goal name="g8bb">
<proof prover="0"><result status="timeout" time="2.55"/></proof>
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
......@@ -152,8 +152,8 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="gttt">
<proof prover="0"><result status="timeout" time="4.05"/></proof>