Commit 8a9be73d authored by Martin Clochard's avatar Martin Clochard Committed by Martin Clochard

update obsolete sessions

parent 8645fe60
......@@ -26,10 +26,10 @@
<proof prover="2"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter model_congruence.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.48" steps="705"/></proof>
<proof prover="2"><result status="valid" time="0.48" steps="538"/></proof>
</goal>
<goal name="WP_parameter model_congruence.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="22"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
</transf>
</goal>
......@@ -37,15 +37,15 @@
<proof prover="2"><result status="valid" time="0.03" steps="106"/></proof>
</goal>
<goal name="WP_parameter model_singleton" expl="VC for model_singleton">
<proof prover="2"><result status="valid" time="0.02" steps="57"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="66"/></proof>
</goal>
<goal name="WP_parameter model_concat" expl="VC for model_concat">
<transf name="split_goal_wp">
<goal name="WP_parameter model_concat.1" expl="1. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="78"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="108"/></proof>
</goal>
<goal name="WP_parameter model_concat.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="66"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="92"/></proof>
</goal>
<goal name="WP_parameter model_concat.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="38"/></proof>
......@@ -66,7 +66,7 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter model_concat.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.09" steps="214"/></proof>
<proof prover="2"><result status="valid" time="0.09" steps="239"/></proof>
</goal>
<goal name="WP_parameter model_concat.10" expl="10. postcondition">
<proof prover="3"><result status="valid" time="0.05"/></proof>
......@@ -74,7 +74,7 @@
</transf>
</goal>
</theory>
<theory name="AssocSorted" sum="2e0f9c7892a452f3254c3fe19efc136a" expanded="true">
<theory name="AssocSorted" sum="c234d7458c225ff847c0ef368a2e5830" expanded="true">
<goal name="Eq.Refl" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -88,54 +88,54 @@
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter increasing_unique" expl="VC for increasing_unique">
<proof prover="2"><result status="valid" time="0.07" steps="101"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="99"/></proof>
</goal>
<goal name="WP_parameter model_cut" expl="VC for model_cut">
<transf name="split_goal_wp">
<goal name="WP_parameter model_cut.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.04" steps="63"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="59"/></proof>
</goal>
<goal name="WP_parameter model_cut.2" expl="2. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter model_cut.2.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="0.08" steps="186"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.08" steps="224"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="221"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.5" expl="5. assertion">
<proof prover="2"><result status="valid" time="0.03" steps="41"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="36"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.6" expl="6. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="0"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter model_cut.3" expl="3. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter model_cut.3.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="0.08" steps="199"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="201"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.08" steps="195"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="187"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.5" expl="5. assertion">
<proof prover="2"><result status="valid" time="0.03" steps="41"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="36"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.6" expl="6. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="0"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="17b24b654430c0ca1c74a07fad6b17d2" expanded="true">
<theory name="BraunHeaps" sum="7060adca73c80720f325a69f935be0c1" expanded="true">
<goal name="WP_parameter root_is_min" expl="VC for root_is_min">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
......
......@@ -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.4pl4" timelimit="8" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="8" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" memlimit="4000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
......@@ -11,7 +11,7 @@
<file name="../dfa_example.mlw" expanded="true">
<theory name="DfaExample" sum="660b70fa1d4035d9e6c3f57fd8521252" expanded="true">
<goal name="nil_notin_r1">
<proof prover="0" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.86"/></proof>
<proof prover="2" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.86"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.08" steps="336"/></proof>
</goal>
......@@ -47,10 +47,10 @@
</goal>
<goal name="WP_parameter one_w_in_r1.4" expl="4. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter one_w_in_r1.4.1" expl="1. postcondition">
<goal name="WP_parameter one_w_in_r1.4.1" expl="1. VC for one_w_in_r1">
<proof prover="7"><result status="valid" time="0.25" steps="337"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.4.2" expl="2. postcondition">
<goal name="WP_parameter one_w_in_r1.4.2" expl="2. VC for one_w_in_r1">
<proof prover="7"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</transf>
......@@ -73,13 +73,13 @@
</goal>
<goal name="WP_parameter astate1.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter astate1.3.1" expl="1. postcondition">
<goal name="WP_parameter astate1.3.1" expl="1. VC for astate1">
<proof prover="7"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter astate1.3.2" expl="2. postcondition">
<goal name="WP_parameter astate1.3.2" expl="2. VC for astate1">
<proof prover="7"><result status="valid" time="0.06" steps="48"/></proof>
</goal>
<goal name="WP_parameter astate1.3.3" expl="3. postcondition">
<goal name="WP_parameter astate1.3.3" expl="3. VC for astate1">
<proof prover="7"><result status="valid" time="0.05" steps="37"/></proof>
</goal>
</transf>
......
......@@ -13,7 +13,7 @@
<prover id="9" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="10" name="Coq" version="8.4pl6" timelimit="30" memlimit="1000"/>
<file name="../dijkstra.mlw" expanded="true">
<theory name="DijkstraShortestPath" sum="5f5ed2756f88b78330f194b16c40702d" expanded="true">
<theory name="DijkstraShortestPath" sum="bb0b932410c359a55c38f0af7239d5dd" 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">
......@@ -41,14 +41,14 @@
</transf>
</goal>
<goal name="Path_inversion">
<proof prover="8"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="Path_shortest_path">
<proof prover="10" timelimit="5" edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="Main_lemma">
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="9"><result status="valid" time="1.44" steps="3054"/></proof>
<proof prover="9"><result status="valid" time="0.39" steps="937"/></proof>
</goal>
<goal name="Completeness_lemma">
<transf name="induction_pr">
......@@ -139,7 +139,7 @@
<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="1.06"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.72"/></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>
......@@ -148,7 +148,7 @@
<proof prover="2" timelimit="10"><result status="valid" time="2.78"/></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="335"/></proof>
<proof prover="8"><result status="valid" time="0.16" steps="337"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.12.1.6" expl="6. VC for shortest_path_code">
<proof prover="8"><result status="valid" time="0.12" steps="156"/></proof>
......@@ -189,7 +189,7 @@
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="17. loop invariant preservation">
<proof prover="10" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="10.74"/></proof>
<proof prover="10" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="5.96"/></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>
......
......@@ -10,7 +10,7 @@
<prover id="6" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<file name="../compiler.mlw" expanded="true">
<theory name="Compile_aexpr" sum="6061032436274b8da23671f90b4a9c1f">
<theory name="Compile_aexpr" sum="f149c7930975bd42aaeb1fca31573102">
<goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr">
<transf name="split_goal_wp">
<goal name="WP_parameter compile_aexpr.1" expl="1. precondition">
......@@ -248,7 +248,7 @@
</transf>
</goal>
</theory>
<theory name="Compile_bexpr" sum="e08e81e0609cedfb34c0e36bb92ecb4a">
<theory name="Compile_bexpr" sum="384513fa31fd946a4ad2aea39767d030">
<goal name="WP_parameter compile_bexpr" expl="VC for compile_bexpr">
<transf name="split_goal_wp">
<goal name="WP_parameter compile_bexpr.1" expl="1. precondition">
......@@ -462,7 +462,7 @@
<proof prover="2"><result status="valid" time="0.38" steps="202"/></proof>
</goal>
<goal name="WP_parameter compile_bexpr.34.1.1.6" expl="6. VC for compile_bexpr">
<proof prover="2"><result status="valid" time="0.50" steps="172"/></proof>
<proof prover="2"><result status="valid" time="0.30" steps="172"/></proof>
</goal>
</transf>
</goal>
......@@ -1742,7 +1742,7 @@
</transf>
</goal>
</theory>
<theory name="Compile_com" sum="fe7ce14af0d07ab93374da923427bdf0">
<theory name="Compile_com" sum="85bdd7a6f37746b44787b4d7142cdecf">
<goal name="WP_parameter compile_com" expl="VC for compile_com">
<transf name="split_goal_wp">
<goal name="WP_parameter compile_com.1" expl="1. precondition">
......@@ -1938,40 +1938,40 @@
<proof prover="2"><result status="valid" time="0.22" steps="59"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.5" expl="5. VC for compile_com">
<proof prover="2"><result status="valid" time="0.42" steps="57"/></proof>
<proof prover="2"><result status="valid" time="0.20" steps="57"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.6" expl="6. VC for compile_com">
<proof prover="2"><result status="valid" time="1.78" steps="394"/></proof>
<proof prover="2"><result status="valid" time="0.97" steps="394"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.7" expl="7. VC for compile_com">
<proof prover="2"><result status="valid" time="0.44" steps="63"/></proof>
<proof prover="2"><result status="valid" time="0.19" steps="63"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.8" expl="8. VC for compile_com">
<proof prover="2"><result status="valid" time="0.47" steps="65"/></proof>
<proof prover="2"><result status="valid" time="0.21" steps="65"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.9" expl="9. VC for compile_com">
<proof prover="2"><result status="valid" time="0.48" steps="67"/></proof>
<proof prover="2"><result status="valid" time="0.22" steps="67"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.10" expl="10. VC for compile_com">
<proof prover="2"><result status="valid" time="0.43" steps="56"/></proof>
<proof prover="2"><result status="valid" time="0.18" steps="56"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.11" expl="11. VC for compile_com">
<proof prover="2"><result status="valid" time="1.47" steps="365"/></proof>
<proof prover="2"><result status="valid" time="0.95" steps="365"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.12" expl="12. VC for compile_com">
<proof prover="6"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.13" expl="13. VC for compile_com">
<proof prover="2"><result status="valid" time="0.48" steps="94"/></proof>
<proof prover="2"><result status="valid" time="0.29" steps="94"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.14" expl="14. VC for compile_com">
<proof prover="2"><result status="valid" time="0.57" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.29" steps="93"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.15" expl="15. VC for compile_com">
<proof prover="2"><result status="valid" time="0.63" steps="94"/></proof>
<proof prover="2"><result status="valid" time="0.32" steps="94"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.16" expl="16. VC for compile_com">
<proof prover="2"><result status="valid" time="0.44" steps="67"/></proof>
<proof prover="2"><result status="valid" time="0.21" steps="67"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.17" expl="17. VC for compile_com">
<proof prover="2"><result status="valid" time="0.21" steps="65"/></proof>
......@@ -3086,12 +3086,12 @@
<goal name="WP_parameter compile_com.45.1.1.6" expl="6. VC for compile_com">
<transf name="eliminate_builtin">
<goal name="WP_parameter compile_com.45.1.1.6.1" expl="1. VC for compile_com">
<proof prover="1" timelimit="20"><result status="valid" time="2.06"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="1.39"/></proof>
<transf name="inline_goal">
<goal name="WP_parameter compile_com.45.1.1.6.1.1" expl="1. VC for compile_com">
<proof prover="0"><result status="valid" time="1.03"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="1.60"/></proof>
<proof prover="6" timelimit="20"><result status="valid" time="0.97"/></proof>
<proof prover="0"><result status="valid" time="0.53"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="1.06"/></proof>
<proof prover="6" timelimit="20"><result status="valid" time="0.56"/></proof>
</goal>
</transf>
</goal>
......@@ -3109,7 +3109,7 @@
<proof prover="2"><result status="valid" time="0.12" steps="40"/></proof>
</goal>
<goal name="WP_parameter compile_com.47" expl="47. precondition">
<proof prover="7" edited="compiler_Compile_com_WP_parameter_compile_com_1.v"><result status="valid" time="4.09"/></proof>
<proof prover="7" edited="compiler_Compile_com_WP_parameter_compile_com_1.v"><result status="valid" time="3.15"/></proof>
</goal>
<goal name="WP_parameter compile_com.48" expl="48. precondition">
<proof prover="2"><result status="valid" time="0.14" steps="40"/></proof>
......@@ -3139,22 +3139,22 @@
<proof prover="2"><result status="valid" time="0.29" steps="54"/></proof>
</goal>
<goal name="WP_parameter compile_com.54.1.1.2" expl="2. VC for compile_com">
<proof prover="2"><result status="valid" time="0.44" steps="58"/></proof>
<proof prover="2"><result status="valid" time="0.23" steps="58"/></proof>
</goal>
<goal name="WP_parameter compile_com.54.1.1.3" expl="3. VC for compile_com">
<proof prover="2"><result status="valid" time="0.36" steps="58"/></proof>
</goal>
<goal name="WP_parameter compile_com.54.1.1.4" expl="4. VC for compile_com">
<proof prover="2"><result status="valid" time="0.57" steps="80"/></proof>
<proof prover="2"><result status="valid" time="0.30" steps="80"/></proof>
</goal>
<goal name="WP_parameter compile_com.54.1.1.5" expl="5. VC for compile_com">
<proof prover="2"><result status="valid" time="0.45" steps="69"/></proof>
<proof prover="2"><result status="valid" time="0.26" steps="69"/></proof>
</goal>
<goal name="WP_parameter compile_com.54.1.1.6" expl="6. VC for compile_com">
<proof prover="2"><result status="valid" time="0.33" steps="69"/></proof>
</goal>
<goal name="WP_parameter compile_com.54.1.1.7" expl="7. VC for compile_com">
<proof prover="2"><result status="valid" time="0.43" steps="69"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="69"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -10,7 +10,7 @@
<prover id="5" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="6" name="Vampire" version="0.6" timelimit="5" memlimit="4000"/>
<file name="../largest_prime_factor.mlw" expanded="true">
<theory name="PrimeFactor" sum="ce0f187a1b211897e791aa5943ef1a84" expanded="true">
<theory name="PrimeFactor" sum="12b4a559359f4d61b31d560dd2587a37" expanded="true">
<goal name="WP_parameter smallest_divisor" expl="VC for smallest_divisor">
<transf name="split_goal_wp">
<goal name="WP_parameter smallest_divisor.1" expl="1. assertion">
......@@ -34,7 +34,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter smallest_divisor.1.7" expl="7. assertion">
<proof prover="4"><result status="valid" time="0.03" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter smallest_divisor.1.8" expl="8. assertion">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -43,7 +43,7 @@
<proof prover="4"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="WP_parameter smallest_divisor.1.10" expl="10. assertion">
<proof prover="4"><result status="valid" time="0.14" steps="34"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="34"/></proof>
</goal>
</transf>
</goal>
......
......@@ -7,4 +7,3 @@ Require BuiltIn.
Theorem G2 : False.
Qed.
......@@ -5,7 +5,7 @@
<prover id="1" name="Coq" version="8.4pl6" timelimit="4" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="0"/>
<file name="../hello_proof.why" expanded="true">
<theory name="HelloProof" sum="e175689ddad45c34275767ac95f484d5" expanded="true">
<theory name="HelloProof" sum="950ac4a3a878a2cf96b1798f390c3a39" expanded="true">
<goal name="G1" expanded="true">
<proof prover="2" memlimit="1000"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
......@@ -13,7 +13,7 @@
<proof prover="2" timelimit="4"><result status="unknown" time="0.00"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="G2.1" expl="1." expanded="true">
<proof prover="1" edited="hello_proof_HelloProof_G2_1.v"><result status="unknown" time="0.78"/></proof>
<proof prover="1" edited="hello_proof_HelloProof_G2_1.v"><result status="unknown" time="0.76"/></proof>
<proof prover="2" memlimit="1000"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="G2.2" expl="2." expanded="true">
......
......@@ -8,7 +8,7 @@
<prover id="6" name="CVC4" version="1.3" timelimit="1" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.95.2" timelimit="15" memlimit="1000"/>
<file name="../random_access_list.mlw" expanded="true">
<theory name="RandomAccessList" sum="4f5e850e802b209157f63926846d59e0">
<theory name="RandomAccessList" sum="17a4d9a5822d0b71b874a00afa504ddb">
<goal name="WP_parameter length_flatten" expl="VC for length_flatten">
<transf name="split_goal_wp">
<goal name="WP_parameter length_flatten.1" expl="1. variant decrease">
......
......@@ -8,7 +8,7 @@
<prover id="4" name="Z3" version="4.3.2" timelimit="6" memlimit="1000"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<file name="../sieve.mlw" expanded="true">
<theory name="Sieve" sum="a4ff6967cc063435496d968c626846f0" expanded="true">
<theory name="Sieve" sum="a3fc383ce2ea2023cf0da48f1f4c958a" expanded="true">
<goal name="WP_parameter incr" expl="VC for incr">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
......@@ -75,10 +75,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
<goal name="WP_parameter sieve.15.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.86" steps="83"/></proof>
<proof prover="0"><result status="valid" time="0.84" steps="83"/></proof>
</goal>
<goal name="WP_parameter sieve.15.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="30"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="WP_parameter sieve.15.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.05" steps="65"/></proof>
......@@ -110,13 +110,13 @@
<proof prover="0"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="WP_parameter sieve.19.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.06" steps="39"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="WP_parameter sieve.19.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.14" steps="74"/></proof>
</goal>
<goal name="WP_parameter sieve.19.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="26"/></proof>
</goal>
<goal name="WP_parameter sieve.19.6" expl="6. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="35"/></proof>
......
......@@ -19,7 +19,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
</theory>
<theory name="Iteration" sum="2c31a081b486a7999a2cf635e7cb3b2c" expanded="true">
<theory name="Iteration" sum="31fb4ef8d79c1ff62c5bb0f69982f06c" expanded="true">
<goal name="sizek_nonneg">
<transf name="induction_ty_lex">
<goal name="sizek_nonneg.1" expl="1.">
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment