Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 378b4f7d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update sessions with Coq 8.7.1

parent ec2714e9
......@@ -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="3" name="CVC3" version="2.4.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -35,7 +35,7 @@
<proof prover="12"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="0" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="1" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.31"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="86970d496f2db125feae52276a283ee6">
......@@ -57,7 +57,7 @@
<proof prover="9"><result status="valid" time="0.05" steps="107"/></proof>
</goal>
<goal name="If42" expl="">
<proof prover="0" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="0.81"/></proof>
<proof prover="1" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="0.81"/></proof>
</goal>
</theory>
<theory name="Typing" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -90,14 +90,14 @@
<proof prover="9"><result status="valid" time="0.08" steps="143"/></proof>
</goal>
<goal name="eval_type_term.1.4" expl="">
<proof prover="0" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="1.50"/></proof>
<proof prover="1" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="1.50"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="type_preservation" expl="">
<proof prover="0" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="1.52"/></proof>
<proof prover="1" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="1.52"/></proof>
</goal>
</theory>
<theory name="FreshVariables" sum="e8d942e6e9d0add73d0d37a3267da968">
......@@ -171,7 +171,7 @@
<proof prover="9"><result status="valid" time="0.30" steps="655"/></proof>
</goal>
<goal name="eval_msubst.1.11" expl="">
<proof prover="0" edited="blocking_semantics5_FreshVariables_eval_msubst_2.v"><result status="valid" time="0.80"/></proof>
<proof prover="1" edited="blocking_semantics5_FreshVariables_eval_msubst_2.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="eval_msubst.1.12" expl="">
<proof prover="9"><result status="valid" time="0.30" steps="561"/></proof>
......@@ -189,7 +189,7 @@
<proof prover="9"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="eval_swap_term.1.2" expl="">
<proof prover="0" edited="blocking_semantics5_FreshVariables_eval_swap_term_1.v"><result status="valid" time="0.93"/></proof>
<proof prover="1" edited="blocking_semantics5_FreshVariables_eval_swap_term_1.v"><result status="valid" time="0.93"/></proof>
</goal>
<goal name="eval_swap_term.1.3" expl="">
<proof prover="3"><result status="valid" time="0.05"/></proof>
......@@ -256,7 +256,7 @@
</transf>
</goal>
<goal name="eval_swap" expl="">
<proof prover="0" memlimit="4000" edited="blocking_semantics5_FreshVariables_eval_swap_3.v"><result status="valid" time="0.33"/></proof>
<proof prover="1" memlimit="4000" edited="blocking_semantics5_FreshVariables_eval_swap_3.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="eval_term_change_free" expl="">
<transf name="induction_ty_lex">
......@@ -327,7 +327,7 @@
<proof prover="9"><result status="valid" time="0.07" steps="89"/></proof>
</goal>
<goal name="eval_change_free.1.11" expl="">
<proof prover="0" edited="blocking_semantics5_FreshVariables_eval_change_free_4.v"><result status="valid" time="1.30"/></proof>
<proof prover="1" edited="blocking_semantics5_FreshVariables_eval_change_free_4.v"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="eval_change_free.1.12" expl="">
<proof prover="9"><result status="valid" time="0.18" steps="280"/></proof>
......@@ -339,32 +339,32 @@
</theory>
<theory name="HoareLogic" sum="23cedd132ddce3b408fd64127096ec7a">
<goal name="many_steps_seq" expl="">
<proof prover="0" edited="blocking_semantics5_HoareLogic_many_steps_seq_1.v"><result status="valid" time="0.92"/></proof>
<proof prover="1" edited="blocking_semantics5_HoareLogic_many_steps_seq_1.v"><result status="valid" time="0.92"/></proof>
</goal>
<goal name="consequence_rule" expl="">
<proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="skip_rule" expl="">
<proof prover="0" edited="blocking_semantics5_HoareLogic_skip_rule_1.v"><result status="valid" time="0.43"/></proof>
<proof prover="1" edited="blocking_semantics5_HoareLogic_skip_rule_1.v"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="assign_rule" expl="">
<proof prover="0" timelimit="12" edited="blocking_semantics5_HoareLogic_assign_rule_1.v"><result status="valid" time="1.12"/></proof>
<proof prover="1" timelimit="12" edited="blocking_semantics5_HoareLogic_assign_rule_1.v"><result status="valid" time="1.12"/></proof>
</goal>
<goal name="seq_rule" expl="">
<proof prover="7"><result status="valid" time="0.09"/></proof>
<proof prover="12"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="0" edited="blocking_semantics5_HoareLogic_if_rule_1.v"><result status="valid" time="0.94"/></proof>
<proof prover="1" edited="blocking_semantics5_HoareLogic_if_rule_1.v"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="assert_rule" expl="">
<proof prover="0" edited="blocking_semantics5_HoareLogic_assert_rule_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="1" edited="blocking_semantics5_HoareLogic_assert_rule_1.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="assert_rule_ext" expl="">
<proof prover="0" edited="blocking_semantics5_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="1" edited="blocking_semantics5_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="0" edited="blocking_semantics5_HoareLogic_while_rule_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="1" edited="blocking_semantics5_HoareLogic_while_rule_1.v"><result status="valid" time="0.46"/></proof>
</goal>
</theory>
<theory name="WP" sum="5cc3a5597ba7d5d9898b25547d8addba">
......@@ -379,7 +379,7 @@
<proof prover="12"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="monotonicity.1.2" expl="">
<proof prover="0" timelimit="30" edited="blocking_semantics5_WP_monotonicity_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="1" timelimit="30" edited="blocking_semantics5_WP_monotonicity_1.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="monotonicity.1.3" expl="">
<proof prover="3" timelimit="5"><result status="valid" time="0.14"/></proof>
......@@ -392,7 +392,7 @@
<proof prover="3" timelimit="5"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="monotonicity.1.6" expl="">
<proof prover="0" edited="blocking_semantics5_WP_monotonicity_3.v"><result status="valid" time="0.40"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_monotonicity_3.v"><result status="valid" time="0.40"/></proof>
</goal>
</transf>
</goal>
......@@ -410,7 +410,7 @@
<proof prover="9"><result status="valid" time="0.55" steps="1402"/></proof>
</goal>
<goal name="distrib_conj.1.3" expl="">
<proof prover="0" edited="blocking_semantics5_WP_distrib_conj_2.v"><result status="valid" time="0.95"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_distrib_conj_2.v"><result status="valid" time="0.95"/></proof>
</goal>
<goal name="distrib_conj.1.4" expl="">
<proof prover="9"><result status="valid" time="0.34" steps="959"/></proof>
......@@ -421,14 +421,14 @@
<proof prover="9"><result status="valid" time="0.14" steps="333"/></proof>
</goal>
<goal name="distrib_conj.1.6" expl="">
<proof prover="0" edited="blocking_semantics5_WP_distrib_conj_3.v"><result status="valid" time="0.63"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_distrib_conj_3.v"><result status="valid" time="0.63"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="wp_preserved_by_reduction" expl="">
<proof prover="0" memlimit="4000" edited="blocking_semantics5_WP_wp_preserved_by_reduction_4.v"><result status="valid" time="1.76"/></proof>
<proof prover="1" memlimit="4000" edited="blocking_semantics5_WP_wp_preserved_by_reduction_4.v"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="progress" expl="">
<transf name="induction_ty_lex">
......@@ -441,27 +441,27 @@
<proof prover="12"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="progress.1.2" expl="">
<proof prover="0" edited="blocking_semantics5_WP_progress_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_progress_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="progress.1.3" expl="">
<proof prover="0" edited="blocking_semantics5_WP_progress_2.v"><result status="valid" time="0.83"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_progress_2.v"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="progress.1.4" expl="">
<proof prover="0" edited="blocking_semantics5_WP_progress_3.v"><result status="valid" time="0.35"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_progress_3.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="progress.1.5" expl="">
<proof prover="3" timelimit="5"><result status="valid" time="0.45"/></proof>
<proof prover="11"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="progress.1.6" expl="">
<proof prover="0" edited="blocking_semantics5_WP_progress_5.v"><result status="valid" time="0.39"/></proof>
<proof prover="1" edited="blocking_semantics5_WP_progress_5.v"><result status="valid" time="0.39"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="wp_soundness" expl="">
<proof prover="0" timelimit="30" edited="blocking_semantics5_WP_wp_soundness_1.v"><result status="valid" time="0.44"/></proof>
<proof prover="1" timelimit="30" edited="blocking_semantics5_WP_wp_soundness_1.v"><result status="valid" time="0.44"/></proof>
</goal>
</theory>
</file>
......
......@@ -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.46"/></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.48"/></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.75"/></proof>
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
</goal>
</theory>
......
......@@ -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">
......@@ -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>
......@@ -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="1.74"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.74"/></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="1.74"/></proof>
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="1.74"/></proof>
</goal>
<goal name="to_nat_bv32_bv64" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="90"/></proof>
......@@ -213,7 +213,7 @@
<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.61"/></proof>
</goal>
<goal name="nth_var4" expl="">
<proof prover="1"><result status="valid" time="1.14" steps="148"/></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>
......
......@@ -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.61"/></proof>
<proof prover="4" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.61"/></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.74"/></proof>
</goal>
<goal name="pow2_0" expl="">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -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="129a1971aba7e377549f155f30711f18" 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>