Commit 856a2088 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent 13d953d2
......@@ -3,15 +3,17 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="15" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC3" version="2.2" timelimit="15" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<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="64b694a314ef1dbe118406287800fba2" expanded="true">
<theory name="DijkstraShortestPath" sum="5f5ed2756f88b78330f194b16c40702d" 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">
......@@ -39,13 +41,14 @@
</transf>
</goal>
<goal name="Path_inversion">
<proof prover="8"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="Path_shortest_path">
<proof prover="1" timelimit="5" edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"><result status="valid" time="1.26"/></proof>
<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="8"><result status="valid" time="1.72" steps="1291"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="9"><result status="valid" time="1.44" steps="3054"/></proof>
</goal>
<goal name="Completeness_lemma">
<transf name="induction_pr">
......@@ -78,7 +81,6 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="15"><result status="valid" time="15.85"/></proof>
<proof prover="8" timelimit="15"><result status="valid" time="0.05" steps="67"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.6" expl="6. loop invariant init">
......@@ -152,7 +154,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="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="3.90"/></proof>
<proof prover="10" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="3.90"/></proof>
</goal>
</transf>
</goal>
......@@ -187,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="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="5.60"/></proof>
<proof prover="10" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="10.74"/></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>
......
......@@ -138,7 +138,6 @@
<transf name="compute_specified">
<goal name="WP_parameter inil.1.2.1.1" expl="1. VC for inil">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="unknown" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
......@@ -7,16 +7,16 @@
<prover id="4" name="Gappa" version="1.1.1" timelimit="2" memlimit="0"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="3" memlimit="0"/>
<file name="../my_cosine.why" expanded="true">
<theory name="CosineSingle" sum="755ee8878730ca0c5dd106b03f1b8590" expanded="true">
<theory name="CosineSingle" sum="019a78f095283927a6b919da92d1c881" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="3.06"/></proof>
<proof prover="0" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="4.63"/></proof>
<proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="TotalErrorFullyExpanded" expanded="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="TotalErrorExpanded" expanded="true">
<proof prover="5"><result status="valid" time="0.34" steps="26"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="26"/></proof>
</goal>
<goal name="TotalError" expanded="true">
<proof prover="5" timelimit="10"><result status="valid" time="0.08" steps="28"/></proof>
......
......@@ -6,9 +6,9 @@
<prover id="1" name="MetiTarski" version="2.2" timelimit="5" memlimit="4000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<file name="../real.why" expanded="true">
<theory name="CosineSingle" sum="46cd6f72186946bb0faaa2aacb6342be" expanded="true">
<theory name="CosineSingle" sum="07d8b5837de2d4c94b4fcaab63e15669" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="3.42"/></proof>
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="4.15"/></proof>
<proof prover="1"><result status="valid" time="0.15"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
......
......@@ -5,6 +5,9 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="30" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../vacid_0_build_maze.mlw" expanded="true">
<theory name="UnionFind_pure" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
......@@ -14,11 +17,11 @@
</theory>
<theory name="Graph_sig" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="BuildMaze" sum="b6fc415df228095034c4fcd7f50ab6f1" expanded="true">
<theory name="BuildMaze" sum="6bb2c1fde6b6517a4e09739fe5a829d8" expanded="true">
<goal name="Ineq1">
<transf name="split_goal_wp">
<goal name="Ineq1.1" expl="1.">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Ineq1.2" expl="2.">
<proof prover="0"><result status="valid" time="0.21"/></proof>
......@@ -28,62 +31,65 @@
<goal name="WP_parameter add_edge_and_union" expl="VC for add_edge_and_union">
<transf name="split_goal_wp">
<goal name="WP_parameter add_edge_and_union.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter add_edge_and_union.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="WP_parameter add_edge_and_union.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="2.73"/></proof>
<proof prover="2"><result status="valid" time="16.72" steps="7390"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter build_maze" expl="VC for build_maze" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter build_maze.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter build_maze.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter build_maze.3" expl="3. loop invariant init">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter build_maze.4" expl="4. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter build_maze.5" expl="5. precondition">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter build_maze.6" expl="6. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter build_maze.7" expl="7. assertion">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter build_maze.8" expl="8. assertion">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter build_maze.9" expl="9. precondition">
<proof prover="2"><result status="valid" time="0.30"/></proof>
<proof prover="2"><result status="valid" time="0.30" steps="48"/></proof>
</goal>
<goal name="WP_parameter build_maze.10" expl="10. precondition">
<proof prover="2"><result status="valid" time="0.29"/></proof>
<proof prover="2"><result status="valid" time="0.29" steps="78"/></proof>
</goal>
<goal name="WP_parameter build_maze.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="3.05"/></proof>
<proof prover="4"><result status="valid" time="2.14" steps="811"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter build_maze.12" expl="12. loop invariant preservation">
<proof prover="2"><result status="valid" time="18.44"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter build_maze.13" expl="13. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.79"/></proof>
<proof prover="3"><result status="valid" time="2.53"/></proof>
<proof prover="4"><result status="valid" time="1.08" steps="519"/></proof>
</goal>
<goal name="WP_parameter build_maze.14" expl="14. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
<goal name="WP_parameter build_maze.15" expl="15. postcondition">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="59"/></proof>
</goal>
</transf>
</goal>
......
......@@ -10,7 +10,7 @@
<prover id="5" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../verifythis_PrefixSumRec.mlw" expanded="true">
<theory name="PrefixSumRec" sum="6d81c9f0aa6d78cffe93173557ccd286" expanded="true">
<theory name="PrefixSumRec" sum="ee494c5f3d4aa78c6f6a6f28a36bfbe6" expanded="true">
<goal name="Div_mod_2">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -32,11 +32,11 @@
</goal>
<goal name="WP_parameter phase1_frame.2" expl="2. precondition">
<proof prover="2" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="28"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter phase1_frame.3" expl="3. precondition">
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="4"><result status="valid" time="0.17" steps="38"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter phase1_frame.4" expl="4. variant decrease">
......@@ -50,11 +50,10 @@
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter phase1_frame.6" expl="6. precondition">
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="4"><result status="valid" time="0.19" steps="47"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter phase1_frame.7" expl="7. postcondition">
<proof prover="4"><result status="valid" time="0.41" steps="84"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter phase1_frame.8" expl="8. postcondition">
......@@ -71,11 +70,11 @@
</goal>
<goal name="WP_parameter phase1_frame2.2" expl="2. precondition">
<proof prover="2" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="28"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter phase1_frame2.3" expl="3. precondition">
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="45"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter phase1_frame2.4" expl="4. variant decrease">
......@@ -89,13 +88,12 @@
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter phase1_frame2.6" expl="6. precondition">
<proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="4"><result status="valid" time="0.33" steps="45"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter phase1_frame2.7" expl="7. postcondition">
<proof prover="0" timelimit="30"><result status="valid" time="0.57"/></proof>
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="4" timelimit="30" memlimit="1000"><result status="valid" time="5.23" steps="175"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="WP_parameter phase1_frame2.8" expl="8. postcondition">
......@@ -123,7 +121,6 @@
</goal>
<goal name="WP_parameter upsweep.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="5.32"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -152,13 +149,11 @@
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter upsweep.9" expl="9. assertion">
<proof prover="0" timelimit="15"><result status="valid" time="8.88"/></proof>
<proof prover="4"><result status="valid" time="0.90" steps="154"/></proof>
<proof prover="4"><result status="valid" time="1.54" steps="224"/></proof>
<proof prover="5" timelimit="15"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="WP_parameter upsweep.10" expl="10. assertion">
<proof prover="0"><result status="valid" time="3.19"/></proof>
<proof prover="4"><result status="valid" time="0.98" steps="156"/></proof>
<proof prover="4"><result status="valid" time="1.84" steps="260"/></proof>
<proof prover="5"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter upsweep.11" expl="11. assertion">
......@@ -191,7 +186,7 @@
</goal>
<goal name="WP_parameter upsweep.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="1.72"/></proof>
<proof prover="4"><result status="valid" time="0.24" steps="88"/></proof>
<proof prover="4"><result status="valid" time="0.24" steps="86"/></proof>
<proof prover="5"><result status="valid" time="2.50"/></proof>
</goal>
<goal name="WP_parameter upsweep.17" expl="17. assertion">
......@@ -305,23 +300,23 @@
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter downsweep.8" expl="8. assertion">
<proof prover="3"><result status="valid" time="3.91"/></proof>
<proof prover="3"><result status="valid" time="5.68"/></proof>
<proof prover="4"><result status="valid" time="0.48" steps="32"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter downsweep.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="4"><result status="valid" time="0.38" steps="48"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter downsweep.10" expl="10. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="4"><result status="valid" time="0.42" steps="50"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter downsweep.11" expl="11. assertion">
<proof prover="1" timelimit="5"><result status="valid" time="0.55"/></proof>
<proof prover="6"><result status="valid" time="0.12" steps="58"/></proof>
<proof prover="6"><result status="valid" time="0.12" steps="57"/></proof>
</goal>
<goal name="WP_parameter downsweep.12" expl="12. variant decrease">
<proof prover="4"><result status="valid" time="0.02" steps="22"/></proof>
......@@ -346,7 +341,7 @@
</goal>
<goal name="WP_parameter downsweep.16" expl="16. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="7.13"/></proof>
<proof prover="3"><result status="valid" time="8.60"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="29"/></proof>
<proof prover="5"><result status="valid" time="0.16"/></proof>
</goal>
......@@ -415,7 +410,7 @@
<goal name="WP_parameter downsweep.28" expl="28. postcondition">
<proof prover="0"><result status="valid" time="5.49"/></proof>
<proof prover="4"><result status="valid" time="0.17" steps="81"/></proof>
<proof prover="5" timelimit="15"><result status="valid" time="2.43"/></proof>
<proof prover="5" timelimit="15"><result status="valid" time="5.32"/></proof>
</goal>
<goal name="WP_parameter downsweep.29" expl="29. postcondition">
<proof prover="0"><result status="valid" time="7.08"/></proof>
......@@ -467,7 +462,7 @@
</goal>
<goal name="WP_parameter compute_sums.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.28"/></proof>
<proof prover="4"><result status="valid" time="0.80" steps="131"/></proof>
<proof prover="4"><result status="valid" time="0.80" steps="175"/></proof>
<proof prover="5"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter compute_sums.5" expl="5. index in array bounds">
......@@ -619,7 +614,7 @@
<goal name="WP_parameter test_harness.14" expl="14. assertion">
<proof prover="0" timelimit="30"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="0.84"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="1.04"/></proof>
<proof prover="3" timelimit="30"><result status="valid" time="0.66"/></proof>
<proof prover="4" timelimit="30" memlimit="1000"><result status="valid" time="0.02" steps="40"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="0.04"/></proof>
......
......@@ -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.4pl4" timelimit="10" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" memlimit="0"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="4" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="5" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
......@@ -45,7 +45,7 @@
</transf>
</goal>
</theory>
<theory name="BFS" sum="5846be4f5e134b08034954a2eaf8f555" expanded="true">
<theory name="BFS" sum="1c4e9affeb06eecd52118ffdf9845b83" expanded="true">
<goal name="WP_parameter fill_next" expl="VC for fill_next">
<transf name="split_goal_wp">
<goal name="WP_parameter fill_next.1" expl="1. loop invariant init">
......@@ -63,7 +63,7 @@
<proof prover="9" memlimit="0"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter fill_next.3.3" expl="3. VC for fill_next">
<proof prover="9" memlimit="0"><result status="valid" time="0.04" steps="148"/></proof>
<proof prover="9" memlimit="0"><result status="valid" time="0.04" steps="149"/></proof>
</goal>
<goal name="WP_parameter fill_next.3.4" expl="4. VC for fill_next">
<proof prover="6"><result status="valid" time="0.01"/></proof>
......@@ -88,7 +88,7 @@
<goal name="WP_parameter fill_next.5.4" expl="4. VC for fill_next">
<transf name="inline_goal">
<goal name="WP_parameter fill_next.5.4.1" expl="1. VC for fill_next">
<proof prover="9" memlimit="0"><result status="valid" time="0.06" steps="111"/></proof>
<proof prover="9" memlimit="0"><result status="valid" time="0.06" steps="112"/></proof>
</goal>
</transf>
</goal>
......@@ -103,10 +103,10 @@
<proof prover="9" memlimit="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter fill_next.7.2" expl="2. VC for fill_next">
<proof prover="9" memlimit="0"><result status="valid" time="0.07" steps="257"/></proof>
<proof prover="9" memlimit="0"><result status="valid" time="0.07" steps="261"/></proof>
</goal>
<goal name="WP_parameter fill_next.7.3" expl="3. VC for fill_next">
<proof prover="9" memlimit="0"><result status="valid" time="0.06" steps="82"/></proof>
<proof prover="9" memlimit="0"><result status="valid" time="0.06" steps="85"/></proof>
</goal>
</transf>
</goal>
......@@ -196,7 +196,6 @@
</goal>
<goal name="WP_parameter bfs.5.3" expl="3. VC for bfs">
<proof prover="5"><result status="valid" time="2.77"/></proof>
<proof prover="7"><result status="timeout" time="4.97"/></proof>
</goal>
<goal name="WP_parameter bfs.5.4" expl="4. VC for bfs">
<proof prover="9" memlimit="0"><result status="valid" time="0.01" steps="17"/></proof>
......@@ -224,7 +223,7 @@
<proof prover="9" timelimit="5"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter bfs.8" expl="8. postcondition">
<proof prover="0" edited="vstte12_bfs_WP_BFS_WP_parameter_bfs_1.v"><result status="valid" time="1.24"/></proof>
<proof prover="1" edited="vstte12_bfs_WP_BFS_WP_parameter_bfs_1.v"><result status="valid" time="0.95"/></proof>
</goal>
</transf>
</goal>
......
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