Commit 28ff8fdc authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent 394dc418
......@@ -8,7 +8,7 @@
<file name="../formula.why">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="PropositionalCalculus" sum="7ca365b7b7386e0bf1ce16a164074533" expanded="true">
<theory name="PropositionalCalculus" sum="8e90228c74fc9a58ce016c323f7a8bff" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
......
......@@ -8,7 +8,7 @@
<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"/>
<file name="../imp_n.why" expanded="true">
<theory name="Imp" sum="49dea7a154c8410b9f73a20cca68e63a" expanded="true">
<theory name="Imp" sum="c5b2f605219b1db882298415fdd56cc4" expanded="true">
<goal name="ident_eq_dec">
<proof prover="6"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
......
......@@ -35,7 +35,7 @@
<proof prover="1" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.99"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="43e242b3d12bc39d4b29f9b888732dc9">
<theory name="TestSemantics" sum="c3f64f8e046da17539cc77734ed8e87c">
<goal name="Test13">
<proof prover="2" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="2"/></proof>
......@@ -56,7 +56,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.06" steps="100"/></proof>
</goal>
<goal name="If42">
<proof prover="1" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.43"/></proof>
<proof prover="1" timelimit="5" memlimit="1000" edited="wp2_TestSemantics_If42_1.v"><result status="valid" time="1.99"/></proof>
</goal>
</theory>
<theory name="HoareLogic" sum="82e50c9c6ac0f07e1bde1792daeea9d0">
......@@ -67,7 +67,7 @@
<proof prover="1" edited="wp2_HoareLogic_skip_rule_1.v"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="assign_rule">
<proof prover="1" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="0.89"/></proof>
<proof prover="1" edited="wp2_HoareLogic_assign_rule_1.v"><result status="valid" time="1.12"/></proof>
</goal>
<goal name="seq_rule">
<proof prover="5" timelimit="3"><result status="valid" time="0.07"/></proof>
......@@ -82,13 +82,13 @@
<proof prover="1" edited="wp2_HoareLogic_assert_rule_ext_1.v"><result status="valid" time="1.17"/></proof>
</goal>
<goal name="while_rule">
<proof prover="1" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.99"/></proof>
<proof prover="1" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="1.19"/></proof>
</goal>
<goal name="while_rule_ext">
<proof prover="1" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="1.12"/></proof>
</goal>
</theory>
<theory name="WP" sum="fecbd41e24059a14cd35723bb1094997">
<theory name="WP" sum="60d483dfb3680562a74d6cbbecffcb0d">
<goal name="assigns_refl">
<proof prover="7" timelimit="3" memlimit="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../priority_queue.mlw">
<theory name="PQueue" sum="a8f2dd09a268c50fc0a71d952b1c9e0e">
<theory name="PQueue" sum="1b05d147800303d87e8b645d07f6e2fe">
<goal name="S.O.Trans">
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
......@@ -74,7 +74,7 @@
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter monoid_sum_is_min.2.2" expl="2. VC for monoid_sum_is_min">
<proof prover="1"><result status="valid" time="1.06"/></proof>
<proof prover="1"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="WP_parameter monoid_sum_is_min.2.3" expl="3. VC for monoid_sum_is_min">
<proof prover="6"><result status="valid" time="0.20"/></proof>
......@@ -126,12 +126,12 @@
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.3" expl="3. VC for selected_part">
<proof prover="3"><result status="valid" time="1.95" steps="4193"/></proof>
<proof prover="3"><result status="valid" time="2.35" steps="4193"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="1.92" steps="1561"/></proof>
<proof prover="3"><result status="valid" time="2.24" steps="1561"/></proof>
</goal>
<goal name="WP_parameter selected_part.4" expl="4. postcondition">
<transf name="split_goal_wp">
......@@ -179,7 +179,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter selected_part.5.2.1.1.2" expl="2. VC for selected_part">
<proof prover="1"><result status="valid" time="0.80"/></proof>
<proof prover="1"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="WP_parameter selected_part.5.2.1.1.3" expl="3. VC for selected_part">
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
......@@ -256,7 +256,7 @@
<goal name="WP_parameter first_minimum_caracterisation.12" expl="12. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter first_minimum_caracterisation.12.1" expl="1. VC for first_minimum_caracterisation">
<proof prover="1"><result status="valid" time="1.18"/></proof>
<proof prover="1"><result status="valid" time="1.44"/></proof>
</goal>
<goal name="WP_parameter first_minimum_caracterisation.12.2" expl="2. VC for first_minimum_caracterisation">
<proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
......
......@@ -14,7 +14,7 @@
</theory>
<theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="BagImpl" sum="8044c27621c87bd642caf406894f291b">
<theory name="BagImpl" sum="be3c60cc8e8e109af24c48babccc2623">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
......@@ -25,7 +25,7 @@
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="3"><result status="valid" time="0.38"/></proof>
<proof prover="5"><result status="valid" time="11.31"/></proof>
<proof prover="5"><result status="valid" time="13.15"/></proof>
</goal>
<goal name="WP_parameter get" expl="VC for get">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
......@@ -55,10 +55,10 @@
</goal>
<goal name="WP_parameter remove.6" expl="6. assertion">
<proof prover="1"><result status="valid" time="1.75"/></proof>
<proof prover="5"><result status="valid" time="1.13"/></proof>
<proof prover="5"><result status="valid" time="1.35"/></proof>
</goal>
<goal name="WP_parameter remove.7" expl="7. assertion">
<proof prover="1" timelimit="76"><result status="valid" time="8.17"/></proof>
<proof prover="1" timelimit="76"><result status="valid" time="10.36"/></proof>
</goal>
<goal name="WP_parameter remove.8" expl="8. assertion">
<proof prover="0" timelimit="5" memlimit="4000"><result status="valid" time="0.06" steps="34"/></proof>
......@@ -70,7 +70,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter remove.11" expl="11. type invariant">
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="1.73"/></proof>
<proof prover="1" timelimit="5" memlimit="4000"><result status="valid" time="2.10"/></proof>
<proof prover="9"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter remove.12" expl="12. postcondition">
......@@ -110,7 +110,7 @@
</transf>
</goal>
</theory>
<theory name="Harness" sum="5ec8c49a5e09c3af067f6882a666a776">
<theory name="Harness" sum="901ee9672cc52ecfd65dc95727d9f5fb">
<goal name="WP_parameter test1" expl="VC for test1">
<transf name="split_goal_wp">
<goal name="WP_parameter test1.1" expl="1. assertion">
......
This diff is collapsed.
......@@ -8,7 +8,7 @@
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<file name="../fsetint.why" expanded="true">
<theory name="Th1" sum="ef22ff2d63b0de72f33a0af8c29d811b" expanded="true">
<theory name="Th1" sum="178010da29c32755768dd2cabaa41efd" expanded="true">
<goal name="l_false" expanded="true">
<proof prover="0"><result status="timeout" time="3.01"/></proof>
<proof prover="4"><result status="timeout" time="3.01"/></proof>
......@@ -17,7 +17,7 @@
<proof prover="7"><result status="timeout" time="3.01"/></proof>
</goal>
</theory>
<theory name="Th2" sum="53142f5d6cc187e6f3955620e5ff5704" expanded="true">
<theory name="Th2" sum="76c066c8522aa7f70876d2be74b3ce00" expanded="true">
<goal name="mem_integer" expanded="true">
<proof prover="0"><result status="timeout" time="3.11"/></proof>
<proof prover="4"><result status="timeout" time="3.02"/></proof>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count.mlw" expanded="true">
<theory name="CoincidenceCount" sum="a8232d091a24913e7b296b0a1514ac32" expanded="true">
<theory name="CoincidenceCount" sum="17b09e5c8a51c7635f8c46ed79d78cff" expanded="true">
<goal name="drop_left">
<proof prover="2"><result status="valid" time="0.15" steps="486"/></proof>
</goal>
......@@ -64,7 +64,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="1.86"/></proof>
<proof prover="0"><result status="valid" time="2.19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.17" expl="17. assertion">
<transf name="inline_goal">
......
......@@ -6,7 +6,7 @@
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count_list.mlw" expanded="true">
<theory name="CoincidenceCount" sum="e1c38f7c433de1db1bf331338e6cd93a">
<theory name="CoincidenceCount" sum="9a0ad21c9ece5af6e3bf77ad2c0d1d81">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
......@@ -34,7 +34,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="1.01" steps="3244"/></proof>
<proof prover="0"><result status="valid" time="1.24" steps="3244"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
......@@ -58,7 +58,7 @@
</transf>
</goal>
</theory>
<theory name="CoincidenceCountAnyType" sum="78e504df0782d826d8b4c2b2ed1accd6">
<theory name="CoincidenceCountAnyType" sum="2effd4ea5f064da956ab4d367f092582">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
......
......@@ -11,7 +11,7 @@
<file name="../cursor.mlw" expanded="true">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestCursor" sum="4a864b2c874ceb1b6d23670c5e40f80b">
<theory name="TestCursor" sum="f91a40a09c844cedc29add1f7e489e9f">
<goal name="WP_parameter sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="WP_parameter sum.1" expl="1. loop invariant init">
......
......@@ -9,7 +9,7 @@
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../dijkstra.mlw" expanded="true">
<theory name="DijkstraShortestPath" sum="bb0b932410c359a55c38f0af7239d5dd" expanded="true">
<theory name="DijkstraShortestPath" sum="927fe939ad868be15f33edef384e9149" expanded="true">
<goal name="WP_parameter relax" expl="VC for relax">
<transf name="split_goal_wp">
<goal name="WP_parameter relax.1" expl="1. postcondition">
......@@ -134,13 +134,13 @@
<proof prover="8"><result status="valid" time="0.04" steps="86"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.2" expl="2. VC for shortest_path_code">
<proof prover="2" timelimit="10"><result status="valid" time="0.72"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="1.24"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.3" expl="3. VC for shortest_path_code">
<proof prover="8"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.4" expl="4. VC for shortest_path_code">
<proof prover="2" timelimit="10"><result status="valid" time="2.50"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="2.90"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.5" expl="5. VC for shortest_path_code">
<proof prover="8"><result status="valid" time="0.16" steps="337"/></proof>
......@@ -149,7 +149,7 @@
<proof prover="8"><result status="valid" time="0.12" steps="156"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.7" expl="7. VC for shortest_path_code">
<proof prover="0" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="2.35"/></proof>
<proof prover="0" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="3.53"/></proof>
</goal>
</transf>
</goal>
......@@ -184,7 +184,7 @@
<proof prover="5"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="17. loop invariant preservation">
<proof prover="0" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="1.62"/></proof>
<proof prover="0" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="6.18"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.18" expl="18. loop variant decrease">
<proof prover="8"><result status="valid" time="0.07" steps="73"/></proof>
......
This diff is collapsed.
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="4000" memlimit="4000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="4000" memlimit="4000"/>
<file name="../esterel.mlw" expanded="true">
<theory name="Esterel" sum="a43de3ed68b03982f261f5072b3943c0" expanded="true">
<theory name="Esterel" sum="5ed3b4e094b8d2ed11fbc86ef3db67b1" expanded="true">
<goal name="WP_parameter union" expl="VC for union" expanded="true">
<proof prover="1"><result status="valid" time="0.20" steps="219"/></proof>
</goal>
......
......@@ -6,12 +6,12 @@
<file name="../finite_tarski.mlw" expanded="true">
<theory name="Tarski" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Tarski_rec" sum="1e15043844e2905232cb4e614e5f8246" expanded="true">
<theory name="Tarski_rec" sum="ce480e189cfd29d29e9e2e61ceebe833" expanded="true">
<goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
</theory>
<theory name="Tarski_while" sum="dc3a928b725935c70c892f235fee1d02" expanded="true">
<theory name="Tarski_while" sum="dfcdd727fd1b802f81fc5c84ff819eda" expanded="true">
<goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="0"><result status="valid" time="0.19"/></proof>
</goal>
......
......@@ -25,7 +25,7 @@
</transf>
</goal>
</theory>
<theory name="Lemmas" sum="e854d03b7c4acc5d88dd8c36e7048e5c">
<theory name="Lemmas" sum="69586628d3c613c629b078044197f281">
<goal name="mem_app">
<transf name="induction_ty_lex">
<goal name="mem_app.1" expl="1.">
......@@ -141,7 +141,7 @@
<goal name="inverse_white">
<transf name="compute_in_goal">
<goal name="inverse_white.1" expl="1.">
<proof prover="1"><result status="valid" time="0.21" steps="268"/></proof>
<proof prover="1"><result status="valid" time="0.34" steps="268"/></proof>
</goal>
</transf>
</goal>
......@@ -156,7 +156,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="final_unique.1.2" expl="2.">
<proof prover="1"><result status="valid" time="0.41" steps="736"/></proof>
<proof prover="1"><result status="valid" time="0.58" steps="736"/></proof>
</goal>
</transf>
</goal>
......@@ -439,7 +439,7 @@
<goal name="sub_valid_coloring.3.1.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="sub_valid_coloring.3.1.1.1.1" expl="1.">
<proof prover="9" edited="koda_ruskey_KodaRuskey_Spec_sub_valid_coloring_1.v"><result status="valid" time="4.89"/></proof>
<proof prover="9" edited="koda_ruskey_KodaRuskey_Spec_sub_valid_coloring_1.v"><result status="valid" time="6.55"/></proof>
</goal>
<goal name="sub_valid_coloring.3.1.1.1.2" expl="2.">
<proof prover="0" timelimit="6"><result status="valid" time="0.04"/></proof>
......@@ -504,7 +504,7 @@
<proof prover="1" timelimit="11"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter sub_valid_coloring_white.10" expl="10. postcondition">
<proof prover="9" edited="koda_ruskey_KodaRuskey_Spec_WP_parameter_sub_valid_coloring_white_1.v"><result status="valid" time="3.81"/></proof>
<proof prover="9" edited="koda_ruskey_KodaRuskey_Spec_WP_parameter_sub_valid_coloring_white_1.v"><result status="valid" time="4.84"/></proof>
</goal>
</transf>
</goal>
......@@ -578,7 +578,7 @@
</transf>
</goal>
</theory>
<theory name="KodaRuskey" sum="0609bde6b8371dc2a23b9313ecdb9946">
<theory name="KodaRuskey" sum="36a4845e80d79eb1bc0cec1b749891e7">
<goal name="WP_parameter enum" expl="VC for enum">
<transf name="split_goal_wp">
<goal name="WP_parameter enum.1" expl="1. unreachable point">
......@@ -929,7 +929,7 @@
<proof prover="0" timelimit="6" steplimit="-1"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter enum.81" expl="81. postcondition">
<proof prover="0" timelimit="6"><result status="valid" time="5.32"/></proof>
<proof prover="0" timelimit="6"><result status="valid" time="6.21"/></proof>
</goal>
<goal name="WP_parameter enum.82" expl="82. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
......
......@@ -132,7 +132,7 @@
</transf>
</goal>
</theory>
<theory name="InPlaceRevSeq" sum="98a75103e20b687045d666de85976237" expanded="true">
<theory name="InPlaceRevSeq" sum="678d4dadc1ebc5c4177a189d61c186e3" expanded="true">
<goal name="non_empty_seq">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
......@@ -429,7 +429,7 @@
<proof prover="0"><result status="valid" time="2.23"/></proof>
</goal>
<goal name="WP_parameter app.22" expl="22. postcondition">
<proof prover="2"><result status="valid" time="4.66"/></proof>
<proof prover="2"><result status="valid" time="5.69"/></proof>
</goal>
</transf>
</goal>
......
......@@ -73,7 +73,7 @@
<proof prover="8"><result status="valid" time="0.03"/></proof>
<proof prover="9"><result status="valid" time="0.07"/></proof>
<proof prover="11"><result status="valid" time="0.17"/></proof>
<proof prover="12"><result status="valid" time="1.27"/></proof>
<proof prover="12"><result status="valid" time="1.57"/></proof>
</goal>
<goal name="G4">
<proof prover="2"><result status="valid" time="0.53"/></proof>
......@@ -82,13 +82,13 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.07"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="1.30"/></proof>
<proof prover="12"><result status="valid" time="1.56"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="LambdaCalc2" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Example2" sum="c8e9d589927db3f00259a435c5be136b" expanded="true">
<theory name="Example2" sum="15e91ffa458219a3505c872fc2e5e8d1" expanded="true">
<goal name="G1">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
......
......@@ -11,7 +11,7 @@
<file name="../queens.mlw" expanded="true">
<theory name="S" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="NQueensSetsTermination" sum="b44f56b69863b041a34e03255cab618a" expanded="true">
<theory name="NQueensSetsTermination" sum="a8c1538297aff624b6696504fd055dc6" expanded="true">
<goal name="WP_parameter t" expl="VC for t">
<transf name="split_goal_wp">
<goal name="WP_parameter t.1" expl="1. loop invariant init">
......@@ -45,7 +45,7 @@
<proof prover="2" timelimit="25" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="NQueensSets" sum="8441d968bed235b87289f0fdcd9a077e" expanded="true">
<theory name="NQueensSets" sum="84359e2bc8fb69649020ceea88e72918" expanded="true">
<goal name="WP_parameter t3" expl="VC for t3">
<transf name="split_goal_wp">
<goal name="WP_parameter t3.1" expl="1. loop invariant init">
......@@ -155,13 +155,13 @@
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter t3.4.6" expl="6. VC for t3">
<proof prover="1" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="2.44"/></proof>
<proof prover="1" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="3.13"/></proof>
</goal>
<goal name="WP_parameter t3.4.7" expl="7. VC for t3">
<proof prover="1" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_6.v"><result status="valid" time="1.60"/></proof>
</goal>
<goal name="WP_parameter t3.4.8" expl="8. VC for t3">
<proof prover="2" timelimit="55"><result status="valid" time="18.66"/></proof>
<proof prover="2" timelimit="55"><result status="valid" time="21.13"/></proof>
</goal>
<goal name="WP_parameter t3.4.9" expl="9. VC for t3">
<proof prover="0"><result status="valid" time="0.08"/></proof>
......
This diff is collapsed.
......@@ -164,7 +164,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
</theory>
<theory name="RandomAccessListWithSeq" sum="701496b887c032d33ad42fbd0e63f7fa" expanded="true">
<theory name="RandomAccessListWithSeq" sum="c27fac8421ae533080ca82841e5a3275" expanded="true">
<goal name="WP_parameter size" expl="VC for size">
<transf name="split_goal_wp">
<goal name="WP_parameter size.1" expl="1. postcondition">
......
......@@ -5,8 +5,8 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../residual.mlw" expanded="true">
......@@ -47,7 +47,7 @@
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.10.2" expl="2. VC for accepts_epsilon">
<proof prover="0" timelimit="60" memlimit="4000"><result status="valid" time="7.82" steps="10703"/></proof>
<proof prover="0" timelimit="60" memlimit="4000"><result status="valid" time="6.18" steps="10703"/></proof>
</goal>
</transf>
</goal>
......@@ -60,7 +60,7 @@
</transf>
</goal>
<goal name="inversion_mem_star_gen">
<proof prover="5" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.70"/></proof>
<proof prover="3" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.90"/></proof>
<transf name="induction_pr">
<goal name="inversion_mem_star_gen.1" expl="1.">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -131,7 +131,7 @@
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter residual.9" expl="9. postcondition">
<proof prover="5" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="0.63"/></proof>
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="1.02"/></proof>
</goal>
<goal name="WP_parameter residual.10" expl="10. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
......@@ -140,16 +140,16 @@
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.11" expl="11. postcondition" expanded="true">
<proof prover="5" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.71"/></proof>
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="WP_parameter residual.12" expl="12. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="52"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="1.62"/></proof>
<proof prover="2"><result status="valid" time="0.98"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.13" expl="13. postcondition" expanded="true">
<proof prover="5" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.50"/></proof>
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.86"/></proof>
</goal>
</transf>
</goal>
......
......@@ -8,7 +8,7 @@
</theory>
<theory name="GraphShape" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SchorrWaite" sum="5cdd637225548b2bcec592ea4db1065e" expanded="true">
<theory name="SchorrWaite" sum="fff0d08f435a9cc7f0ce6b34b7547c29" expanded="true">
<goal name="WP_parameter black" expl="VC for black">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
......@@ -411,13 +411,13 @@
<proof prover="0"><result status="valid" time="0.79" steps="503"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.133" expl="133. postcondition">
<proof prover="0"><result status="valid" time="0.77" steps="416"/></proof>
<proof prover="0"><result status="valid" time="0.57" steps="416"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.134" expl="134. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="60"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.135" expl="135. postcondition">
<proof prover="0"><result status="valid" time="0.49" steps="383"/></proof>
<proof prover="0"><result status="valid" time="0.32" steps="383"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.136" expl="136. VC for schorr_waite">
<proof prover="0"><result status="valid" time="0.02" steps="24"/></proof>
......@@ -480,7 +480,7 @@
<proof prover="0"><result status="valid" time="0.12" steps="121"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.156" expl="156. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.13" steps="571"/></proof>
<proof prover="0"><result status="valid" time="0.78" steps="571"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.157" expl="157. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.24" steps="192"/></proof>
......@@ -489,10 +489,10 @@
<proof prover="0"><result status="valid" time="0.42" steps="357"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.159" expl="159. loop invariant preservation">
<proof prover="0"><result status="valid" time="3.92" steps="1262"/></proof>
<proof prover="0"><result status="valid" time="2.93" steps="1262"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.160" expl="160. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.30" steps="704"/></proof>
<proof prover="0"><result status="valid" time="1.05" steps="704"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.161" expl="161. VC for schorr_waite">
<proof prover="0"><result status="valid" time="0.03" steps="25"/></proof>
......
......@@ -32,10 +32,10 @@
</theory>
<theory name="ArrayPermut" sum="c35e6a30805f654f329783c9ec01270c">
<goal name="exchange_permut_sub">
<proof prover="2" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="3.65"/></proof>
<proof prover="2" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="4.53"/></proof>
</goal>
<goal name="permut_sub_weakening">
<proof prover="2" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="1.21"/></proof>
<proof prover="2" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="1.46"/></proof>
</goal>
<goal name="exchange_permut_all">
<proof prover="4"><result status="valid" time="0.06"/></proof>
......@@ -55,7 +55,7 @@
</theory>
<theory name="ToList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ToSeq" sum="4d13eb3ec2ac0cea8847c8b058ea3d8b">
<theory name="ToSeq" sum="972d3973679c1b19bf79339fb847c382">
<goal name="WP_parameter to_seq_length" expl="VC for to_seq_length">
<transf name="split_goal_wp">
<goal name="WP_parameter to_seq_length.1" expl="1. variant decrease">
......
......@@ -34,7 +34,7 @@
</theory>
<theory name="Mem" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Elements" sum="26b8d407081a0df014fdec443dd1bbf1">
<theory name="Elements" sum="8bdd844429293cfd31fd0f17ecbc15a7">
<goal name="elements_mem">
<transf name="induction_ty_lex">
<goal name="elements_mem.1" expl="1.">
......@@ -261,13 +261,13 @@
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="sorted_append.1.6" expl="6.">
<proof prover="2"><result status="valid" time="1.62"/></proof>
<proof prover="2"><result status="valid" time="2.32"/></proof>
</goal>
<goal name="sorted_append.1.7" expl="7.">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
<goal name="sorted_append.1.8" expl="8.">
<proof prover="1"><result status="valid" time="1.63"/></proof>
<proof prover="1"><result status="valid" time="2.38"/></proof>
</goal>
</transf>
</goal>
......@@ -312,7 +312,7 @@
<proof prover="4"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="rev_append_sorted_incr.1.8" expl="8.">
<proof prover="4"><result status="valid" time="1.13"/></proof>
<proof prover="4"><result status="valid" time="1.49"/></proof>
</goal>
</transf>
</goal>
......@@ -431,7 +431,7 @@