Commit 5fb8c95f authored by MARCHE Claude's avatar MARCHE Claude

update sessions and shapes after merge with master (improvements on shape computations)

parent 171085d9
......@@ -8,8 +8,8 @@
<file name="../formula.why" expanded="true">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="PropositionalCalculus" sum="110d0ad354ecb0d3c55eba1dce7aacda" expanded="true">
<goal name="Test1" expanded="true">
<theory name="PropositionalCalculus" sum="7f2804c705a099e7f5ba415139b5ad50" expanded="true">
<goal name="Test1" expl="" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="46"/></proof>
......
......@@ -6,63 +6,63 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" expanded="true">
<theory name="Imp" sum="812efe9f12d37d909cfb6fce353ea280" expanded="true">
<goal name="ident_eq_dec">
<theory name="Imp" sum="393416a5d93852e1dde31286bcba2c8e" expanded="true">
<goal name="ident_eq_dec" expl="">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="check_skip">
<goal name="check_skip" expl="">
<proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="Test13">
<goal name="Test13" expl="">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Test42">
<goal name="Test42" expl="">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Test55">
<goal name="Test55" expl="">
<proof prover="4"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
<goal name="Ass42">
<goal name="Ass42" expl="">
<proof prover="4"><result status="valid" time="0.04" steps="91"/></proof>
</goal>
<goal name="If42">
<goal name="If42" expl="">
<proof prover="4"><result status="valid" time="0.13" steps="485"/></proof>
</goal>
<goal name="progress">
<goal name="progress" expl="">
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="steps_non_neg">
<goal name="steps_non_neg" expl="">
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="many_steps_seq">
<goal name="many_steps_seq" expl="">
<proof prover="0" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="eval_subst_expr">
<goal name="eval_subst_expr" expl="">
<transf name="induction_ty_lex">
<goal name="eval_subst_expr.1" expl="1.">
<goal name="eval_subst_expr.1" expl="">
<proof prover="4"><result status="valid" time="0.02" steps="107"/></proof>
</goal>
</transf>
</goal>
<goal name="eval_subst">
<goal name="eval_subst" expl="">
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="skip_rule">
<goal name="skip_rule" expl="">
<proof prover="4"><result status="valid" time="0.04" steps="146"/></proof>
</goal>
<goal name="assign_rule">
<goal name="assign_rule" expl="">
<proof prover="4"><result status="valid" time="0.99" steps="1831"/></proof>
</goal>
<goal name="seq_rule">
<goal name="seq_rule" expl="">
<proof prover="4"><result status="valid" time="2.20" steps="6927"/></proof>
</goal>
<goal name="if_rule">
<goal name="if_rule" expl="">
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="while_rule">
<goal name="while_rule" expl="">
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="consequence_rule">
<goal name="consequence_rule" expl="">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
......
......@@ -7,7 +7,7 @@
<file name="../add_list.mlw">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AddListRec" sum="33def14244e48e7a03216981ac5000bf">
<theory name="AddListRec" sum="191e311078f6223c9af44eece1bb2a47">
<goal name="VC sum" expl="VC for sum">
<proof prover="1"><result status="valid" time="0.02" steps="93"/></proof>
</goal>
......@@ -15,7 +15,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="f7b23f93ac300ff2dca6f1bdf5f7fec6">
<theory name="AddListImp" sum="25869898cb7ed98962558d9845b87089">
<goal name="VC sum" expl="VC for sum">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="AddListRec" sum="33def14244e48e7a03216981ac5000bf" expanded="true">
<theory name="AddListRec" sum="191e311078f6223c9af44eece1bb2a47" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -14,7 +14,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="f7b23f93ac300ff2dca6f1bdf5f7fec6" expanded="true">
<theory name="AddListImp" sum="25869898cb7ed98962558d9845b87089" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......
This diff is collapsed.
This diff is collapsed.
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="c7d1e9748b365e541a36b248436a7eb0" expanded="true">
<theory name="Algo64" sum="97b944efcc8d08f1fdb866cadb4074fb" expanded="true">
<goal name="VC quicksort" expl="VC for quicksort" expanded="true">
<proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="875a99e8633733f0c2ca127e9f379e87" expanded="true">
<theory name="Algo65" sum="0343e5826de1d0b12c03d5cc1d6b9e90" expanded="true">
<goal name="VC find" expl="VC for find" expanded="true">
<proof prover="0"><result status="valid" time="0.52" steps="1682"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="fe8094ecb69ba53dfe8fe5ac8495503a" expanded="true">
<theory name="AllDistinct" sum="29d64b955c0ca1b6353b32886f2fa1d0" expanded="true">
<goal name="VC all_distinct" expl="VC for all_distinct" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="273"/></proof>
</goal>
......
......@@ -4,14 +4,14 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="0fb2021452931587ceb1d5ae93b96bbf" expanded="true">
<theory name="M" sum="3f4a7332fb862e7e78830642919cdaaf" expanded="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="156"/></proof>
</goal>
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="InsertionSortExample" sum="8a3d58ebfc4e621c805950d96e63138f" expanded="true">
<theory name="InsertionSortExample" sum="b0bf33c0b21cb5adba7e72e6f7e3acfd" expanded="true">
<goal name="VC path_init_l2" expl="VC for path_init_l2" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
......
......@@ -4,12 +4,12 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw" expanded="true">
<theory name="Sum" sum="873296719533457bc97e6577d5aaed17" expanded="true">
<theory name="Sum" sum="464fbc01e7969eb94479e6f6762a1672" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
</theory>
<theory name="Division" sum="3fe8cf0a6e9f26c89aa9adc5d5734b14" expanded="true">
<theory name="Division" sum="ce38e3995afc25e5981ed2086f16a1aa" expanded="true">
<goal name="VC division" expl="VC for division" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
......
This diff is collapsed.
......@@ -9,29 +9,29 @@
</theory>
<theory name="MonoidSum" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MonoidSumDef" sum="30a0bf1fbd21f9d9961d39b86bd816f7">
<theory name="MonoidSumDef" sum="ad359559eb9e4ed736b1bf8ae16b4f7e">
<goal name="VC agg" expl="VC for agg">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="agg_sing_core">
<goal name="agg_sing_core" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="VC agg_cat" expl="VC for agg_cat">
<proof prover="0"><result status="valid" time="0.07" steps="435"/></proof>
</goal>
<goal name="MS.M.assoc">
<goal name="MS.M.assoc" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="MS.M.neutral">
<goal name="MS.M.neutral" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="MS.agg_empty">
<goal name="MS.agg_empty" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="MS.agg_sing">
<goal name="MS.agg_sing" expl="">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="MS.agg_cat">
<goal name="MS.agg_cat" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
......
This diff is collapsed.
......@@ -4,20 +4,20 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="23b1953119a07d783af66468a25d4402">
<theory name="RAL" sum="681ef3c18575b4542ada144c31b48687">
<goal name="VC balancing" expl="VC for balancing">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="M.assoc">
<goal name="M.assoc" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="M.neutral">
<goal name="M.neutral" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="M.M.assoc">
<goal name="M.M.assoc" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="M.M.neutral">
<goal name="M.M.neutral" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="M.VC zero" expl="VC for zero">
......@@ -35,10 +35,10 @@
<goal name="VC selected_part" expl="VC for selected_part">
<proof prover="0"><result status="valid" time="0.26" steps="761"/></proof>
</goal>
<goal name="Sel.M.assoc">
<goal name="Sel.M.assoc" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Sel.M.neutral">
<goal name="Sel.M.neutral" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Sel.M.VC zero" expl="VC for zero">
......@@ -47,13 +47,13 @@
<goal name="Sel.M.VC op" expl="VC for op">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Sel.M.agg_empty">
<goal name="Sel.M.agg_empty" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="Sel.M.agg_sing">
<goal name="Sel.M.agg_sing" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="Sel.M.agg_cat">
<goal name="Sel.M.agg_cat" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="Sel.D.VC measure" expl="VC for measure">
......@@ -62,7 +62,7 @@
<goal name="Sel.VC balancing" expl="VC for balancing">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Sel.selection_empty">
<goal name="Sel.selection_empty" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="Sel.VC selected_part" expl="VC for selected_part">
......@@ -121,34 +121,34 @@
</goal>
<goal name="VC harness" expl="VC for harness">
<transf name="split_goal_wp">
<goal name="VC harness.1" expl="1. precondition">
<goal name="VC harness.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.03" steps="5"/></proof>
</goal>
<goal name="VC harness.2" expl="2. precondition">
<goal name="VC harness.2" expl="precondition">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="VC harness.3" expl="3. precondition">
<goal name="VC harness.3" expl="precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC harness.4" expl="4. precondition">
<goal name="VC harness.4" expl="precondition">
<proof prover="0"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC harness.5" expl="5. check">
<goal name="VC harness.5" expl="check">
<proof prover="0"><result status="valid" time="0.06" steps="142"/></proof>
</goal>
<goal name="VC harness.6" expl="6. check">
<goal name="VC harness.6" expl="check">
<proof prover="0"><result status="valid" time="0.07" steps="142"/></proof>
</goal>
<goal name="VC harness.7" expl="7. precondition">
<goal name="VC harness.7" expl="precondition">
<proof prover="0"><result status="valid" time="0.03" steps="17"/></proof>
</goal>
<goal name="VC harness.8" expl="8. precondition">
<goal name="VC harness.8" expl="precondition">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="VC harness.9" expl="9. check">
<goal name="VC harness.9" expl="check">
<proof prover="0"><result status="valid" time="0.58" steps="360"/></proof>
</goal>
<goal name="VC harness.10" expl="10. check">
<goal name="VC harness.10" expl="check">
<proof prover="0" timelimit="5"><result status="valid" time="1.81" steps="533"/></proof>
</goal>
</transf>
......
......@@ -6,7 +6,7 @@
<file name="../balance.mlw" expanded="true">
<theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Puzzle8" sum="acd846f51dd7305d4e569d48197b6c46">
<theory name="Puzzle8" sum="cd15b414a487f5dee1d992c22c5e3264">
<goal name="VC solve3" expl="VC for solve3">
<proof prover="0"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
......@@ -14,7 +14,7 @@
<proof prover="0"><result status="valid" time="0.13" steps="291"/></proof>
</goal>
</theory>
<theory name="Puzzle12" sum="3d382d4e673bb394fa271044f818889c" expanded="true">
<theory name="Puzzle12" sum="6ea315cb4493db13a7fa4541d6a0e474" expanded="true">
<goal name="VC solve12" expl="VC for solve12" expanded="true">
<proof prover="0"><result status="valid" time="0.53" steps="1379"/></proof>
</goal>
......
......@@ -7,110 +7,110 @@
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bignum.mlw" expanded="true">
<theory name="BigNum" sum="458e30d62c074211297da3625c3a7e6f" expanded="true">
<theory name="BigNum" sum="749b12ef40764483c15b39d2d67ddf50" expanded="true">
<goal name="VC base" expl="VC for base">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC nonneg" expl="VC for nonneg" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC nonneg.1" expl="1. variant decrease">
<goal name="VC nonneg.1" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC nonneg.2" expl="2. precondition">
<goal name="VC nonneg.2" expl="precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC nonneg.3" expl="3. postcondition" expanded="true">
<goal name="VC nonneg.3" expl="postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="VC msd" expl="VC for msd" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC msd.1" expl="1. variant decrease">
<goal name="VC msd.1" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC msd.2" expl="2. precondition">
<goal name="VC msd.2" expl="precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC msd.3" expl="3. postcondition" expanded="true">
<goal name="VC msd.3" expl="postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_digit" expl="VC for add_digit">
<transf name="split_goal_wp">
<goal name="VC add_digit.1" expl="1. variant decrease">
<goal name="VC add_digit.1" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC add_digit.2" expl="2. precondition">
<goal name="VC add_digit.2" expl="precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_digit.3" expl="3. precondition">
<goal name="VC add_digit.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_digit.4" expl="4. postcondition">
<goal name="VC add_digit.4" expl="postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_digit.5" expl="5. postcondition">
<goal name="VC add_digit.5" expl="postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_cin" expl="VC for add_cin">
<transf name="split_goal_wp">
<goal name="VC add_cin.1" expl="1. precondition">
<goal name="VC add_cin.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.2" expl="2. precondition">
<goal name="VC add_cin.2" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.3" expl="3. precondition">
<goal name="VC add_cin.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.4" expl="4. precondition">
<goal name="VC add_cin.4" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.5" expl="5. precondition">
<goal name="VC add_cin.5" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.6" expl="6. precondition">
<goal name="VC add_cin.6" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.7" expl="7. variant decrease">
<goal name="VC add_cin.7" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="VC add_cin.8" expl="8. precondition">
<goal name="VC add_cin.8" expl="precondition">
<proof prover="1" timelimit="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_cin.9" expl="9. variant decrease">
<goal name="VC add_cin.9" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="VC add_cin.10" expl="10. precondition">
<goal name="VC add_cin.10" expl="precondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC add_cin.11" expl="11. postcondition">
<goal name="VC add_cin.11" expl="postcondition">
<transf name="split_goal_wp">
<goal name="VC add_cin.11.1" expl="1. postcondition">
<goal name="VC add_cin.11.1" expl="postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.2" expl="2. postcondition">
<goal name="VC add_cin.11.2" expl="postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.3" expl="3. postcondition">
<goal name="VC add_cin.11.3" expl="postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.4" expl="4. postcondition">
<goal name="VC add_cin.11.4" expl="postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_cin.11.5" expl="5. postcondition">
<goal name="VC add_cin.11.5" expl="postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_cin.12" expl="12. postcondition">
<goal name="VC add_cin.12" expl="postcondition">
<proof prover="2"><result status="valid" time="0.31" steps="113"/></proof>
</goal>
</transf>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" expanded="true">
<theory name="BinaryMultiplication" sum="f1eebc593f40a0c87893ba3fd42ece8d" expanded="true">
<theory name="BinaryMultiplication" sum="6dfaeaf640fc19b709ad881e0f1b9b82" expanded="true">