Commit c687def9 authored by Andrei Paskevich's avatar Andrei Paskevich

upgrade Alt-Ergo to 2.0.0 where possible

parent 5c35938d
......@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" 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"/>
<file name="../formula.why" proved="true">
<theory name="PropositionalCalculus" proved="true">
<goal name="Test1" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="38"/></proof>
<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>
</goal>
</theory>
</file>
......
......@@ -4,29 +4,29 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="3" steplimit="0" memlimit="0"/>
<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"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" proved="true">
<theory name="Imp" proved="true">
<goal name="ident_eq_dec" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="check_skip" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="Test13" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Test42" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Test55" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="16"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
<goal name="Ass42" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="91"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="91"/></proof>
</goal>
<goal name="If42" proved="true">
<proof prover="4"><result status="valid" time="0.13" steps="485"/></proof>
<proof prover="2"><result status="valid" time="0.13" steps="328"/></proof>
</goal>
<goal name="progress" proved="true">
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
......@@ -40,7 +40,7 @@
<goal name="eval_subst_expr" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_subst_expr.0" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="107"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="107"/></proof>
</goal>
</transf>
</goal>
......@@ -48,13 +48,13 @@
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="skip_rule" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="146"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="149"/></proof>
</goal>
<goal name="assign_rule" proved="true">
<proof prover="4"><result status="valid" time="0.99" steps="1831"/></proof>
<proof prover="2"><result status="valid" time="0.70" steps="1641"/></proof>
</goal>
<goal name="seq_rule" proved="true">
<proof prover="4"><result status="valid" time="2.20" steps="6935"/></proof>
<proof prover="2"><result status="valid" time="0.84" steps="3015"/></proof>
</goal>
<goal name="if_rule" proved="true">
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
......
This diff is collapsed.
This diff is collapsed.
......@@ -4,119 +4,119 @@
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.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="749b12ef40764483c15b39d2d67ddf50" expanded="true">
<goal name="VC base" expl="VC for base">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bignum.mlw" proved="true">
<theory name="BigNum" proved="true">
<goal name="VC base" expl="VC for base" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC nonneg" expl="VC for nonneg" expanded="true">
<transf name="split_goal_right" expanded="true">
<goal name="VC nonneg.1" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
<goal name="VC nonneg" expl="VC for nonneg" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC nonneg.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC nonneg.2" expl="precondition">
<goal name="VC nonneg.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC nonneg.3" expl="postcondition" expanded="true">
<goal name="VC nonneg.2" expl="postcondition" proved="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_right" expanded="true">
<goal name="VC msd.1" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
<goal name="VC msd" expl="VC for msd" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC msd.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC msd.2" expl="precondition">
<goal name="VC msd.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC msd.3" expl="postcondition" expanded="true">
<goal name="VC msd.2" expl="postcondition" proved="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_right">
<goal name="VC add_digit.1" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
<goal name="VC add_digit" expl="VC for add_digit" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC add_digit.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC add_digit.2" expl="precondition">
<goal name="VC add_digit.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_digit.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_digit.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_digit.4" expl="postcondition">
<goal name="VC add_digit.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_digit.5" expl="postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="82"/></proof>
<goal name="VC add_digit.4" expl="postcondition" proved="true">
<proof prover="4"><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_right">
<goal name="VC add_cin.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_cin" expl="VC for add_cin" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC add_cin.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.2" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_cin.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_cin.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.4" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_cin.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.5" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_cin.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.6" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add_cin.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.7" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
<goal name="VC add_cin.6" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC add_cin.8" expl="precondition">
<goal name="VC add_cin.7" expl="precondition" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_cin.9" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
<goal name="VC add_cin.8" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC add_cin.10" expl="precondition">
<goal name="VC add_cin.9" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC add_cin.11" expl="postcondition">
<transf name="split_goal_right">
<goal name="VC add_cin.11.1" expl="postcondition">
<goal name="VC add_cin.10" expl="postcondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC add_cin.10.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.2" expl="postcondition">
<goal name="VC add_cin.10.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.3" expl="postcondition">
<goal name="VC add_cin.10.2" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.4" expl="postcondition">
<goal name="VC add_cin.10.3" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_cin.11.5" expl="postcondition">
<goal name="VC add_cin.10.4" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_cin.12" expl="postcondition">
<proof prover="2"><result status="valid" time="0.31" steps="113"/></proof>
<goal name="VC add_cin.11" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.31" steps="113"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add" expl="VC for add" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
<goal name="VC add" expl="VC for add" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,10 +4,10 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw">
<theory name="BinarySort">
<goal name="VC occ_shift" expl="VC for occ_shift">
<proof prover="0" obsolete="true"><result status="valid" time="0.54"/></proof>
<file name="../binary_sort.mlw" proved="true">
<theory name="BinarySort" proved="true">
<goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
<proof prover="0"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC binary_sort" expl="VC for binary_sort" proved="true">
<transf name="split_vc" proved="true" >
......
This diff is collapsed.
This diff is collapsed.
......@@ -2,40 +2,40 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" 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="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double.why" proved="true">
<theory name="TestDouble" proved="true">
<goal name="nth_one1" proved="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.05" steps="79"/></proof>
</goal>
<goal name="nth_one2" proved="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.04" steps="77"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.04" steps="79"/></proof>
</goal>
<goal name="nth_one3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="77"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="sign_one" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="75"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="exp_one" proved="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.21" steps="668"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="0.16" steps="210"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="mantissa_one" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
<proof prover="2"><result status="valid" time="0.09" steps="88"/></proof>
<proof prover="3"><result status="valid" time="1.04"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.72"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.11"/></proof>
</goal>
<goal name="double_value_of_1" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="94"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="95"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,53 +2,53 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../neg_as_xor.why" proved="true">
<theory name="TestNegAsXOR" proved="true">
<goal name="Nth_j" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
</goal>
<goal name="sign_of_j" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
<proof prover="3"><result status="valid" time="4.23"/></proof>
</goal>
<goal name="mantissa_of_j" proved="true">
<proof prover="1"><result status="valid" time="0.16" steps="121"/></proof>
<proof prover="0"><result status="valid" time="0.16" steps="121"/></proof>
<proof prover="3"><result status="valid" time="1.54"/></proof>
<proof prover="5"><result status="valid" time="2.61"/></proof>
<proof prover="5"><result status="valid" time="3.02"/></proof>
<proof prover="9"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="exp_of_j" proved="true">
<proof prover="1"><result status="valid" time="0.17" steps="122"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="105"/></proof>
<proof prover="3"><result status="valid" time="1.53"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.00"/></proof>
<proof prover="9"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="int_of_bv" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="94"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="95"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10"/></proof>
<proof prover="9"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="MainResultBits" proved="true">
<proof prover="1"><result status="valid" time="0.15" steps="130"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="104"/></proof>
<proof prover="3"><result status="valid" time="1.06"/></proof>
</goal>
<goal name="MainResultSign" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Sign_of_xor_j" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="85"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Exp_of_xor_j" proved="true">
<proof prover="1"><result status="valid" time="1.72" steps="492"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="128"/></proof>
<proof prover="3"><result status="valid" time="1.64"/></proof>
<proof prover="5"><result status="valid" time="2.98"/></proof>
<proof prover="9"><result status="valid" time="0.69"/></proof>
......@@ -59,17 +59,17 @@
<proof prover="9"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="MainResultZero" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="104"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="105"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="3.06"/></proof>
<proof prover="9"><result status="valid" time="1.30"/></proof>
<proof prover="9"><result status="valid" time="1.06"/></proof>
</goal>
<goal name="sign_neg" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="144"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult" proved="true">
<proof prover="1"><result status="valid" time="1.90" steps="320"/></proof>
<proof prover="0"><result status="valid" time="1.34" steps="368"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,16 +2,16 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="10" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" proved="true">
<theory name="Bitwalker" proved="true">
<goal name="nth64" proved="true">
<proof prover="10"><result status="valid" time="0.02" steps="91"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="90"/></proof>
</goal>
<goal name="nth8" proved="true">
<proof prover="10"><result status="valid" time="0.06" steps="226"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="208"/></proof>
</goal>
<goal name="VC maxvalue" expl="VC for maxvalue" proved="true">
<transf name="compute_in_goal" proved="true" >
......@@ -236,17 +236,17 @@
<goal name="VC poke_8bit_array.5.0" expl="postcondition" proved="true">
<transf name="case" proved="true" arg1="(div i 8 = o)">
<goal name="VC poke_8bit_array.5.0.0" expl="true case (postcondition)" proved="true">
<proof prover="10"><result status="valid" time="0.15" steps="262"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="258"/></proof>
</goal>
<goal name="VC poke_8bit_array.5.0.1" expl="false case (postcondition)" proved="true">
<proof prover="10"><result status="valid" time="0.12" steps="176"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="176"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC poke_8bit_array.6" expl="postcondition" proved="true">
<proof prover="10"><result status="valid" time="0.10" steps="169"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="169"/></proof>
</goal>
</transf>
</goal>
......@@ -437,7 +437,7 @@
<proof prover="12"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC pokethenpeek.9" expl="postcondition" proved="true">
<proof prover="10"><result status="valid" time="0.09" steps="149"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="149"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment