Commit f413eaea authored by MARCHE Claude's avatar MARCHE Claude

update sessions with Coq 8.7.1

parent 68701e11
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<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="2" name="Coq" version="8.6.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -33,34 +33,34 @@
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="progress" expl="">
<proof prover="2" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="2" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="many_steps_seq" expl="">
<proof prover="2" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
<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" expl="">
<proof prover="2" edited="imp_n_Imp_eval_subst_expr_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" edited="imp_n_Imp_eval_subst_expr_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="eval_subst" expl="">
<proof prover="2" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.35"/></proof>
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="skip_rule" expl="">
<proof prover="6"><result status="valid" time="0.04" steps="113"/></proof>
</goal>
<goal name="assign_rule" expl="">
<proof prover="2" edited="imp_n_Imp_assign_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_assign_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="seq_rule" expl="">
<proof prover="2" edited="imp_n_Imp_seq_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_seq_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="2" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="2" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="consequence_rule" expl="">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......
......@@ -2,26 +2,26 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../wp2.mlw" expanded="true">
<theory name="Imp" sum="4d6ec4c3ea3a39365f84600c953b8179">
<goal name="eval_subst_term" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_term_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="eval_term_change_free" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_term_change_free_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_term_change_free_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="eval_subst" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_subst_1.v"><result status="valid" time="0.37"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_subst_1.v"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="eval_swap" expl="">
<proof prover="2" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="eval_change_free" expl="">
<proof prover="1" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="check_skip" expl="">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -29,10 +29,10 @@
<proof prover="7" memlimit="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="1" edited="wp2_Imp_steps_non_neg_1.v"><result status="valid" time="0.36"/></proof>
<proof prover="0" edited="wp2_Imp_steps_non_neg_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="many_steps_seq" expl="">
<proof prover="1" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
<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">
......@@ -49,14 +49,14 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="Test55" expl="">
<proof prover="1" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_Test55_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_Test55_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="Ass42" expl="">
<proof prover="2" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.06" steps="100"/></proof>
</goal>
<goal name="If42" expl="">
<proof prover="1" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.00"/></proof>
<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">
......@@ -64,28 +64,28 @@
<proof prover="2" memlimit="1000"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="skip_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_skip_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="wp2_HoareLogic_skip_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="assign_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="seq_rule" expl="">
<proof prover="5" timelimit="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.48"/></proof>
<proof prover="0" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="assert_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_assert_rule_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="wp2_HoareLogic_assert_rule_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="assert_rule_ext" expl="">
<proof prover="1" edited="wp2_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="wp2_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="1" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="0" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="while_rule_ext" expl="">
<proof prover="1" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
<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">
......@@ -107,7 +107,7 @@
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.06" steps="94"/></proof>
</goal>
<goal name="WP_parameter compute_writes.2" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter compute_writes.3" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="42"/></proof>
......@@ -125,16 +125,16 @@
<proof prover="7"><result status="valid" time="0.04" steps="48"/></proof>
</goal>
<goal name="WP_parameter compute_writes.8" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_3.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_3.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter compute_writes.9" expl="variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter compute_writes.10" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_4.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_4.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="WP_parameter compute_writes.11" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_compute_writes_2.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_compute_writes_2.v"><result status="valid" time="0.34"/></proof>
</goal>
</transf>
</goal>
......@@ -168,7 +168,7 @@
<proof prover="7"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="WP_parameter wp.8" expl="postcondition">
<proof prover="1" edited="wp2_WP_WP_WP_parameter_wp_1.v"><result status="valid" time="0.32"/></proof>
<proof prover="0" edited="wp2_WP_WP_WP_parameter_wp_1.v"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter wp.9" expl="postcondition">
<proof prover="2" timelimit="3"><result status="valid" time="0.04"/></proof>
......@@ -179,7 +179,7 @@
<proof prover="7"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter wp.11" expl="postcondition">
<proof prover="1" timelimit="5" edited="wp2_WP_WP_WP_parameter_wp_2.v"><result status="valid" time="0.87"/></proof>
<proof prover="0" timelimit="5" edited="wp2_WP_WP_WP_parameter_wp_2.v"><result status="valid" time="0.87"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -31,16 +31,16 @@
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="to_nat_of_zero2" expl="">
<proof prover="0" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="to_nat_of_zero" expl="">
<proof prover="0" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
<proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="to_nat_of_one" expl="">
<proof prover="0" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="0.96"/></proof>
<proof prover="1" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="0.96"/></proof>
</goal>
<goal name="to_nat_sub_footprint" expl="">
<proof prover="0" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="1.22"/></proof>
<proof prover="1" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="1.58"/></proof>
</goal>
<goal name="nth_from_int_low_even" expl="">
<proof prover="2"><result status="valid" time="0.02" steps="68"/></proof>
......@@ -72,7 +72,7 @@
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_from_int2c_plus_pow2" expl="">
<proof prover="0" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.68"/></proof>
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
</goal>
</theory>
......@@ -132,10 +132,10 @@
<proof prover="10"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="to_nat_0x00000001" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="86.14"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="67.72"/></proof>
</goal>
<goal name="to_nat_0x00000003" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="65.79"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="58.95"/></proof>
</goal>
<goal name="to_nat_0x00000007" expl="">
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="53.94"/></proof>
......@@ -153,7 +153,7 @@
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="25.82"/></proof>
</goal>
<goal name="to_nat_0x000000FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="26.48"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="19.45"/></proof>
</goal>
<goal name="to_nat_0x000001FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="17.53"/></proof>
......@@ -165,19 +165,19 @@
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="11.02"/></proof>
</goal>
<goal name="to_nat_0x00000FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="10.38"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="7.98"/></proof>
</goal>
<goal name="to_nat_0x00001FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.88"/></proof>
</goal>
<goal name="to_nat_0x00003FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="5.48"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.80"/></proof>
</goal>
<goal name="to_nat_0x00007FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.14"/></proof>
</goal>
<goal name="to_nat_0x0000FFFF" expl="">
<proof prover="6"><result status="valid" time="3.18"/></proof>
<proof prover="6"><result status="valid" time="2.75"/></proof>
</goal>
<goal name="to_nat_0x0001FFFF" expl="">
<proof prover="6"><result status="valid" time="2.32"/></proof>
......@@ -186,7 +186,7 @@
<proof prover="6"><result status="valid" time="1.77"/></proof>
</goal>
<goal name="to_nat_0x0007FFFF" expl="">
<proof prover="6"><result status="valid" time="1.56"/></proof>
<proof prover="6"><result status="valid" time="1.14"/></proof>
</goal>
<goal name="to_nat_0x000FFFFF" expl="">
<proof prover="6"><result status="valid" time="0.89"/></proof>
......
......@@ -4,8 +4,8 @@
<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="Coq" version="8.6.1" timelimit="30" 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" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -28,7 +28,7 @@
</goal>
<goal name="exp_one" expl="" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.23" steps="668"/></proof>
<proof prover="2" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="mantissa_one" expl="">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
......
......@@ -5,8 +5,8 @@
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double_of_int.why" expanded="true">
......@@ -44,7 +44,7 @@
</goal>
<goal name="nth_const3" expl="">
<proof prover="1"><result status="valid" time="0.10" steps="98"/></proof>
<proof prover="4"><result status="valid" time="1.03"/></proof>
<proof prover="4"><result status="valid" time="0.78"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="nth_const4" expl="">
......@@ -54,7 +54,7 @@
</goal>
<goal name="nth_const5" expl="">
<proof prover="1"><result status="valid" time="0.11" steps="99"/></proof>
<proof prover="4"><result status="valid" time="1.07"/></proof>
<proof prover="4"><result status="valid" time="0.83"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="nth_const6" expl="">
......@@ -86,7 +86,7 @@
<proof prover="8"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="exp_const" expl="">
<proof prover="3" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="to_nat_mantissa_1" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
......@@ -133,7 +133,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.28"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.85"/></proof>
<proof prover="8"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="nth_0_30" expl="">
......@@ -162,10 +162,10 @@
<proof prover="8"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_pos" expl="">
<proof prover="3" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="lemma1_pos" expl="">
<proof prover="3" timelimit="6" edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"><result status="valid" time="1.39"/></proof>
<proof prover="5" timelimit="6" edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"><result status="valid" time="1.39"/></proof>
</goal>
<goal name="jpxorx_neg" expl="">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -174,10 +174,10 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_neg" expl="">
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.06"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.06"/></proof>
</goal>
<goal name="lemma1_neg" expl="">
<proof prover="3" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="5" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="lemma1" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="95"/></proof>
......@@ -190,7 +190,7 @@
<proof prover="4" timelimit="10"><result status="valid" time="1.98"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" expl="">
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="2.08"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="2.08"/></proof>
</goal>
<goal name="to_nat_bv32_bv64" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="90"/></proof>
......@@ -213,10 +213,10 @@
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="lemma2" expl="">
<proof prover="3" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="23.13"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="18.90"/></proof>
</goal>
<goal name="nth_var4" expl="">
<proof prover="1"><result status="valid" time="1.44" steps="148"/></proof>
<proof prover="1"><result status="valid" time="1.18" steps="148"/></proof>
<proof prover="4"><result status="valid" time="1.06"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
</goal>
......@@ -243,7 +243,7 @@
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="lemma3" expl="">
<proof prover="4"><result status="valid" time="2.44"/></proof>
<proof prover="4"><result status="valid" time="1.88"/></proof>
</goal>
<goal name="nth_var9" expl="">
<proof prover="1"><result status="valid" time="0.10" steps="95"/></proof>
......@@ -267,7 +267,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="var_value0" expl="">
<proof prover="3" timelimit="30" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.14"/></proof>
<proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.14"/></proof>
</goal>
<goal name="from_int_sum" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
......@@ -298,10 +298,10 @@
<proof prover="2"><result status="valid" time="0.22"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.97"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="MainResult" expl="">
<proof prover="1"><result status="valid" time="1.56" steps="139"/></proof>
<proof prover="1"><result status="valid" time="1.30" steps="139"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.99"/></proof>
......
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" 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="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -18,10 +18,10 @@
<proof prover="10"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="1" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="4" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="pow2pos" expl="">
<proof prover="1" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.49"/></proof>
<proof prover="4" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.49"/></proof>
</goal>
<goal name="pow2_0" expl="">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -345,7 +345,7 @@
</goal>
<goal name="pow2_53" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="2.80"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="2.38"/></proof>
<proof prover="9"><result status="valid" time="1.95"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="56"/></proof>
</goal>
......@@ -357,7 +357,7 @@
</goal>
<goal name="pow2_55" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.45"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.98"/></proof>
<proof prover="9"><result status="valid" time="2.11"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="58"/></proof>
</goal>
......@@ -431,7 +431,7 @@
<proof prover="10"><result status="valid" time="0.24" steps="99"/></proof>
</goal>
<goal name="Mod_pow2_gen" expl="">
<proof prover="1" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
<proof prover="4" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
</goal>
</theory>
<theory name="Pow2real" sum="be9777507e5ec2c24863ac75e4faf243" expanded="true">
......@@ -467,25 +467,25 @@
<proof prover="10"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Power_non_null_aux" expl="">
<proof prover="1" edited="power2_Pow2real_Power_non_null_aux_1.v"><result status="valid" time="0.65"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_non_null_aux_1.v"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="Power_neg_aux" expl="">
<proof prover="1" edited="power2_Pow2real_Power_neg_aux_1.v"><result status="valid" time="0.68"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_neg_aux_1.v"><result status="valid" time="0.68"/></proof>
</goal>
<goal name="Power_non_null" expl="">
<proof prover="1" edited="power2_Pow2real_Power_non_null_1.v"><result status="valid" time="0.64"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_non_null_1.v"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="Power_neg" expl="">
<proof prover="10"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="Power_sum_aux" expl="">
<proof prover="1" edited="power2_Pow2real_Power_sum_aux_1.v"><result status="valid" time="0.62"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_sum_aux_1.v"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="1" edited="power2_Pow2real_Power_sum_1.v"><result status="valid" time="0.62"/></proof>
<proof prover="4" edited="power2_Pow2real_Power_sum_1.v"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="Pow2_int_real" expl="">
<proof prover="1" edited="power2_Pow2real_Pow2_int_real_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="4" edited="power2_Pow2real_Pow2_int_real_1.v"><result status="valid" time="0.71"/></proof>
</goal>
</theory>
</file>
......
......@@ -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="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../bresenham.mlw" expanded="true">
<theory name="M" sum="3da6ad55dc32260aace6cf777010522a" expanded="true">
<goal name="closest" expl="" expanded="true">
<proof prover="2" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="WP_parameter bresenham" expl="VC for bresenham" expanded="true">
<transf name="split_goal_wp" expanded="true">
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="e32351513bba9a37f680056dd466bcee" expanded="true">
<goal name="t" expl="" expanded="true">
<proof prover="1" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../13849.why" expanded="true">
<theory name="T" sum="fe6d0a97ed129807ad9b025e583a359d" expanded="true">
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../13854.why">
<theory name="T" sum="e0ed6fa44df780ea63fc8d3dbdece469" expanded="true">
<goal name="g" expl="" expanded="true">
<proof prover="1" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13854_T_x_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="13854_T_x_1.v"><result status="valid" time="0.30"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
......@@ -135,13 +135,13 @@
<proof prover="14"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Tan_pi_4" expl="" expanded="true">
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="Tan_pi_3" expl="" expanded="true">
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="Atan_1" expl="" expanded="true">
<proof prover="1" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="0" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,8 +3,8 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="5" name="CVC3" version="2.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -13,7 +13,7 @@
<file name="../decrease1.mlw" expanded="true">
<theory name="Decrease1" sum="e498d06be6ac431d95eb341af5140b44" expanded="true">
<goal name="decrease1_induction" expl="" expanded="true">
<proof prover="3" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="0.40"/></proof>
<proof prover="1" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="WP_parameter search" expl="VC for search" expanded="true">
<transf name="split_goal_wp" expanded="true">
......
......@@ -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="Coq" version="8.7.1" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../dfa_example.mlw" expanded="true">
<theory name="DfaExample" sum="609db869d4cfe35076ba1a796f8c66a9" expanded="true">
<goal name="nil_notin_r1" expl="">
<proof prover="2" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.26"/></proof>
<proof prover="0" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="7" memlimit="4000"><result status="valid" time="0.08" steps="140"/></proof>
</goal>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>