Commit 39507b0d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update more sessions

parent 74208e03
......@@ -2,6 +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="5" memlimit="4000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="15" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
......@@ -12,37 +13,36 @@
<prover id="9" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="12" name="Coq" version="8.4pl6" timelimit="5" memlimit="4000"/>
<file name="../bellman_ford.mlw" expanded="true">
<theory name="Graph" sum="a445091f6d55fb03cbfd6988f8e23631">
<goal name="vertices_cardinal_pos">
<proof prover="6" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="path_in_vertices">
<proof prover="12" timelimit="10" memlimit="0" edited="bf_Graph_path_in_vertices_2.v"><result status="valid" time="1.70"/></proof>
<proof prover="0" timelimit="10" memlimit="0" edited="bf_Graph_path_in_vertices_2.v"><result status="valid" time="0.89"/></proof>
</goal>
<goal name="long_path_decomposition_pigeon1">
<proof prover="12" timelimit="8" memlimit="1000" edited="bellman_ford_Graph_long_path_decomposition_pigeon1_1.v"><result status="valid" time="2.47"/></proof>
<proof prover="0" timelimit="8" memlimit="1000" edited="bellman_ford_Graph_long_path_decomposition_pigeon1_1.v"><result status="valid" time="1.55"/></proof>
</goal>
<goal name="long_path_decomposition_pigeon2">
<proof prover="6"><result status="valid" time="0.06" steps="46"/></proof>
</goal>
<goal name="long_path_decomposition_pigeon3">
<proof prover="12" timelimit="7" memlimit="1000" edited="bellman_ford_Graph_long_path_decomposition_pigeon3_1.v"><result status="valid" time="3.45"/></proof>
<proof prover="0" timelimit="7" memlimit="1000" edited="bellman_ford_Graph_long_path_decomposition_pigeon3_1.v"><result status="valid" time="1.97"/></proof>
</goal>
<goal name="long_path_decomposition">
<proof prover="12" memlimit="1000" edited="bellman_ford_Graph_long_path_decomposition_1.v"><result status="valid" time="2.94"/></proof>
<proof prover="0" memlimit="1000" edited="bellman_ford_Graph_long_path_decomposition_1.v"><result status="valid" time="1.68"/></proof>
</goal>
<goal name="simple_path">
<proof prover="12" timelimit="10" memlimit="0" edited="bf_Graph_simple_path_1.v"><result status="valid" time="3.78"/></proof>
<proof prover="0" timelimit="10" memlimit="0" edited="bf_Graph_simple_path_1.v"><result status="valid" time="2.31"/></proof>
</goal>
<goal name="key_lemma_1">
<proof prover="12" timelimit="10" memlimit="0" edited="bf_Graph_key_lemma_1_1.v"><result status="valid" time="5.38"/></proof>
<proof prover="0" timelimit="10" memlimit="0" edited="bf_Graph_key_lemma_1_1.v"><result status="valid" time="3.37"/></proof>
</goal>
</theory>
<theory name="BellmanFord" sum="00f154fefe471aee2a2d873c070061de" expanded="true">
<goal name="key_lemma_2">
<proof prover="12" edited="bf_WP_BellmanFord_key_lemma_2_1.v"><result status="valid" time="30.19"/></proof>
<proof prover="0" edited="bf_WP_BellmanFord_key_lemma_2_1.v"><result status="valid" time="7.80"/></proof>
</goal>
<goal name="WP_parameter relax" expl="VC for relax">
<transf name="split_goal_wp">
......@@ -51,20 +51,20 @@
<goal name="WP_parameter relax.1.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter relax.1.1.1" expl="1. postcondition">
<proof prover="12" timelimit="10" memlimit="0" edited="bf_WP_BellmanFord_WP_parameter_relax_7.v"><result status="valid" time="2.88"/></proof>
<proof prover="0" timelimit="10" memlimit="0" edited="bf_WP_BellmanFord_WP_parameter_relax_7.v"><result status="valid" time="1.87"/></proof>
</goal>
<goal name="WP_parameter relax.1.1.2" expl="2. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter relax.1.1.3" expl="3. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.68"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter relax.1.1.4" expl="4. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.54"/></proof>
<proof prover="6" timelimit="18" memlimit="0"><result status="valid" time="1.72" steps="880"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.23"/></proof>
<proof prover="6" timelimit="18" memlimit="0"><result status="valid" time="0.75" steps="880"/></proof>
</goal>
<goal name="WP_parameter relax.1.1.5" expl="5. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="1.18"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.44"/></proof>
</goal>
</transf>
</goal>
......@@ -79,11 +79,11 @@
<proof prover="6" timelimit="15" memlimit="0"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="WP_parameter relax.2.1.2" expl="2. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.49"/></proof>
<proof prover="6" timelimit="15" memlimit="0"><result status="valid" time="0.61" steps="408"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.18"/></proof>
<proof prover="6" timelimit="15" memlimit="0"><result status="valid" time="0.26" steps="408"/></proof>
</goal>
<goal name="WP_parameter relax.2.1.3" expl="3. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.74"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="WP_parameter relax.2.1.4" expl="4. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.08"/></proof>
......@@ -105,7 +105,7 @@
<goal name="WP_parameter bellman_ford.1.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter bellman_ford.1.1.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="5.25"/></proof>
<proof prover="4"><result status="valid" time="2.63"/></proof>
<proof prover="7"><result status="valid" time="0.16"/></proof>
<proof prover="11"><result status="valid" time="0.11"/></proof>
</goal>
......@@ -132,10 +132,10 @@
<proof prover="6" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.4" expl="4. exceptional postcondition">
<proof prover="12" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_20.v"><result status="valid" time="3.68"/></proof>
<proof prover="0" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_20.v"><result status="valid" time="2.10"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.5" expl="5. loop invariant preservation">
<proof prover="8"><result status="valid" time="2.18" steps="633"/></proof>
<proof prover="8"><result status="valid" time="0.91" steps="638"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.6" expl="6. loop variant decrease">
<proof prover="6" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="18"/></proof>
......@@ -146,7 +146,7 @@
<goal name="WP_parameter bellman_ford.8" expl="8. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter bellman_ford.8.1" expl="1. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.23"/></proof>
<proof prover="2" memlimit="0"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="103"/></proof>
</goal>
......@@ -216,11 +216,11 @@
<proof prover="6" timelimit="10"><result status="valid" time="0.05" steps="94"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.2" expl="2. VC for bellman_ford">
<proof prover="2" timelimit="5"><result status="valid" time="0.93"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.38" steps="544"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.59"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="1.35" steps="544"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.3" expl="3. VC for bellman_ford">
<proof prover="2"><result status="valid" time="21.90"/></proof>
<proof prover="2"><result status="valid" time="15.66"/></proof>
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
......@@ -1196,9 +1196,9 @@
<goal name="WP_parameter bellman_ford.14.2.1.3" expl="3. VC for bellman_ford">
<transf name="eliminate_builtin">
<goal name="WP_parameter bellman_ford.14.2.1.3.1" expl="1. VC for bellman_ford">
<proof prover="2"><result status="valid" time="0.87"/></proof>
<proof prover="8"><result status="valid" time="2.35" steps="1580"/></proof>
<proof prover="9"><result status="valid" time="0.49"/></proof>
<proof prover="2"><result status="valid" time="0.50"/></proof>
<proof prover="8"><result status="valid" time="1.52" steps="1775"/></proof>
<proof prover="9"><result status="valid" time="0.32"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......@@ -1210,7 +1210,7 @@
<proof prover="6" timelimit="10"><result status="valid" time="0.10" steps="155"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.14.2.1.5" expl="5. VC for bellman_ford">
<proof prover="2"><result status="valid" time="18.03"/></proof>
<proof prover="2"><result status="valid" time="10.57"/></proof>
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
......@@ -2188,7 +2188,7 @@
<goal name="WP_parameter bellman_ford.14.2.1.5.1" expl="1. VC for bellman_ford">
<proof prover="2"><result status="valid" time="0.45"/></proof>
<proof prover="8"><result status="valid" time="0.38" steps="547"/></proof>
<proof prover="9"><result status="valid" time="0.69"/></proof>
<proof prover="9"><result status="valid" time="0.32"/></proof>
<proof prover="10"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -2207,7 +2207,7 @@
<goal name="WP_parameter bellman_ford.16" expl="16. assertion">
<transf name="inline_goal">
<goal name="WP_parameter bellman_ford.16.1" expl="1. assertion">
<proof prover="6" timelimit="54"><result status="valid" time="7.78" steps="752"/></proof>
<proof prover="6" timelimit="54"><result status="valid" time="4.07" steps="752"/></proof>
</goal>
</transf>
</goal>
......@@ -2219,7 +2219,7 @@
<proof prover="6"><result status="valid" time="0.04" steps="62"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.17.1.2" expl="2. loop invariant preservation">
<proof prover="12" timelimit="30" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_17.v"><result status="valid" time="2.00"/></proof>
<proof prover="0" timelimit="30" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_17.v"><result status="valid" time="2.00"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.17.1.3" expl="3. loop invariant preservation">
<proof prover="2" timelimit="5"><result status="valid" time="0.04"/></proof>
......@@ -2227,7 +2227,7 @@
<proof prover="6"><result status="valid" time="0.07" steps="31"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.17.1.4" expl="4. loop invariant preservation">
<proof prover="12" timelimit="30" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_18.v"><result status="valid" time="2.22"/></proof>
<proof prover="0" timelimit="30" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_18.v"><result status="valid" time="2.22"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.17.1.5" expl="5. loop invariant preservation">
<proof prover="6" timelimit="15"><result status="valid" time="0.04" steps="31"/></proof>
......@@ -2246,7 +2246,7 @@
<proof prover="6"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.21" expl="21. exceptional postcondition">
<proof prover="12" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_15.v"><result status="valid" time="3.04"/></proof>
<proof prover="0" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_15.v"><result status="valid" time="2.54"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.22" expl="22. loop invariant preservation">
<transf name="split_goal_wp">
......@@ -2272,7 +2272,7 @@
<proof prover="6" timelimit="15" memlimit="0"><result status="valid" time="0.11" steps="100"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.25.2" expl="2. postcondition">
<proof prover="12" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_19.v"><result status="valid" time="1.68"/></proof>
<proof prover="0" memlimit="1000" edited="bf_WP_BellmanFord_WP_parameter_bellman_ford_19.v"><result status="valid" time="1.68"/></proof>
</goal>
<goal name="WP_parameter bellman_ford.25.3" expl="3. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.14"/></proof>
......
......@@ -2,13 +2,13 @@
<!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="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="10" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="8" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="4b3f5b71a28db1ecea74d9fd0780e47d" expanded="true">
......@@ -18,7 +18,7 @@
</goal>
<goal name="sign_of_j">
<proof prover="1"><result status="valid" time="0.15" steps="108"/></proof>
<proof prover="3"><result status="valid" time="0.95"/></proof>
<proof prover="3"><result status="valid" time="0.65"/></proof>
<proof prover="6"><result status="valid" time="0.09" steps="100"/></proof>
</goal>
<goal name="mantissa_of_j">
......@@ -32,12 +32,12 @@
</goal>
<goal name="exp_of_j">
<proof prover="1"><result status="valid" time="0.17" steps="124"/></proof>
<proof prover="3"><result status="valid" time="0.75"/></proof>
<proof prover="4"><result status="valid" time="0.99"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.13"/></proof>
<proof prover="3"><result status="valid" time="0.46"/></proof>
<proof prover="4"><result status="valid" time="0.70"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.71"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="107"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
<proof prover="9"><result status="valid" time="1.08"/></proof>
<proof prover="9"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="int_of_bv">
<proof prover="1"><result status="valid" time="0.06" steps="94"/></proof>
......@@ -79,17 +79,17 @@
</goal>
<goal name="Mantissa_of_xor_j">
<proof prover="3"><result status="valid" time="0.66"/></proof>
<proof prover="4"><result status="valid" time="1.52"/></proof>
<proof prover="5"><result status="valid" time="3.44"/></proof>
<proof prover="4"><result status="valid" time="0.71"/></proof>
<proof prover="5"><result status="valid" time="2.67"/></proof>
<proof prover="7"><result status="valid" time="0.08"/></proof>
<proof prover="9"><result status="valid" time="1.56"/></proof>
<proof prover="9"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="MainResultZero">
<proof prover="1"><result status="valid" time="0.07" steps="104"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.94"/></proof>
<proof prover="5"><result status="valid" time="5.27"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.88" steps="142"/></proof>
<proof prover="5"><result status="valid" time="3.14"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.15" steps="142"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
<proof prover="9"><result status="valid" time="1.36"/></proof>
</goal>
......@@ -100,8 +100,8 @@
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult">
<proof prover="1"><result status="valid" time="2.85" steps="339"/></proof>
<proof prover="8" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="2.50"/></proof>
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="1.78"/></proof>
<proof prover="1"><result status="valid" time="1.86" steps="326"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<prover id="7" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<file name="../bresenham.mlw" expanded="true">
<theory name="M" sum="5088e1f34697cf917d7cdf19ff3d873f" expanded="true">
<goal name="closest" expanded="true">
<proof prover="7" edited="bresenham_M_closest_1.v"><result status="valid" time="1.96"/></proof>
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="1.19"/></proof>
</goal>
<goal name="WP_parameter bresenham" expl="VC for bresenham" expanded="true">
<transf name="split_goal_wp" expanded="true">
......@@ -23,8 +23,8 @@
<proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter bresenham.3" expl="3. assertion" expanded="true">
<proof prover="4"><result status="valid" time="3.76" steps="132"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="2.75" steps="129"/></proof>
<proof prover="4"><result status="valid" time="1.67" steps="132"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="1.18" steps="129"/></proof>
</goal>
<goal name="WP_parameter bresenham.4" expl="4. loop invariant preservation" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" memlimit="0"/>
<prover id="0" name="Coq" version="8.4pl4" timelimit="10" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="e32351513bba9a37f680056dd466bcee" expanded="true">
<goal name="t" expanded="true">
<proof prover="1" edited="12934_BTS12934_t_1.v"><result status="valid" time="1.01"/></proof>
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.78"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" memlimit="0"/>
<prover id="0" name="Coq" version="8.4pl4" timelimit="10" memlimit="0"/>
<file name="../13849.why">
<theory name="T" sum="fe6d0a97ed129807ad9b025e583a359d" expanded="true">
<goal name="x" expanded="true">
<proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="1.52"/></proof>
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.78"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" memlimit="0"/>
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="0"/>
<file name="../13854.why">
<theory name="T" sum="e0ed6fa44df780ea63fc8d3dbdece469" expanded="true">
<goal name="g" expanded="true">
<proof prover="1" edited="13854_T_g_1.v"><result status="valid" time="1.36"/></proof>
<proof prover="0" edited="13854_T_g_1.v"><result status="valid" time="0.77"/></proof>
</goal>
<goal name="x" expanded="true">
<proof prover="1" edited="13854_T_x_1.v"><result status="valid" time="1.33"/></proof>
<proof prover="0" edited="13854_T_x_1.v"><result status="valid" time="0.77"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,27 +2,27 @@
<!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="2" name="CVC3" version="2.4.1" timelimit="8" memlimit="4000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="4000"/>
<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="6" name="CVC4" version="1.3" timelimit="5" memlimit="4000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="8" memlimit="1000"/>
<prover id="8" name="Coq" version="8.4pl6" timelimit="8" memlimit="1000"/>
<file name="../dfa_example.mlw" expanded="true">
<theory name="DfaExample" sum="232fc35be86c76110da1b6569b43a992" expanded="true">
<goal name="nil_notin_r1">
<proof prover="4"><result status="valid" time="0.25"/></proof>
<proof prover="0" 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>
<proof prover="8" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="WP_parameter all_in_r0" expl="VC for all_in_r0">
<proof prover="5"><result status="valid" time="0.74" steps="1040"/></proof>
<proof prover="5"><result status="valid" time="0.40" steps="1040"/></proof>
</goal>
<goal name="ends_with_one">
<transf name="split_goal_wp">
<goal name="ends_with_one.1" expl="1.">
<proof prover="2" timelimit="5"><result status="valid" time="1.69"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.76"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -38,15 +38,15 @@
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="one_w_in_r1">
<proof prover="4"><result status="valid" time="0.45"/></proof>
<proof prover="4"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="zero_w_in_r2">
<proof prover="4"><result status="valid" time="1.11"/></proof>
<proof prover="5"><result status="valid" time="0.57" steps="993"/></proof>
<proof prover="4"><result status="valid" time="0.50"/></proof>
<proof prover="5"><result status="valid" time="0.27" steps="993"/></proof>
</goal>
<goal name="one_w_in_r2">
<proof prover="4"><result status="valid" time="1.21"/></proof>
<proof prover="5"><result status="valid" time="0.49" steps="577"/></proof>
<proof prover="4"><result status="valid" time="0.47"/></proof>
<proof prover="5"><result status="valid" time="0.21" steps="577"/></proof>
</goal>
<goal name="WP_parameter astate1" expl="VC for astate1">
<transf name="split_goal_wp">
......
......@@ -2,28 +2,28 @@
<!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="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="30" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
<prover id="4" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<file name="../euler001.mlw" expanded="true">
<theory name="DivModHints" sum="f7fdece9a19249c4382a43566f166530">
<goal name="mod_div_unique">
<proof prover="4" memlimit="0" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="1.47"/></proof>
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="0.87"/></proof>
</goal>
<goal name="mod_succ_1">
<proof prover="4" memlimit="0" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="1.55"/></proof>
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="mod_succ_2">
<proof prover="4" memlimit="0" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="1.54"/></proof>
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.98"/></proof>
</goal>
<goal name="div_succ_1">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="div_succ_2">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="1.23"/></proof>
<proof prover="3" timelimit="30" memlimit="1000"><result status="valid" time="3.22" steps="76"/></proof>
<proof prover="2"><result status="valid" time="0.76"/></proof>
<proof prover="3" timelimit="30" memlimit="1000"><result status="valid" time="1.96" steps="76"/></proof>
</goal>
<goal name="mod2_mul2">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
......@@ -61,7 +61,7 @@
</theory>
<theory name="TriangularNumbers" sum="91847fa59365859f1ae00cac3b34c298">
<goal name="tr_mod_2">
<proof prover="4" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="1.16"/></proof>
<proof prover="0" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.86"/></proof>
</goal>
<goal name="tr_repr">
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
......@@ -76,7 +76,7 @@
<theory name="SumMultiple" sum="90bf0acc57cc35c41e0a28734c52e85d">
<goal name="mod_15">
<proof prover="1"><result status="valid" time="0.13"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="1.20" steps="86"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.71" steps="86"/></proof>
</goal>
<goal name="Closed_formula_0">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -84,14 +84,14 @@
<proof prover="3" memlimit="1000"><result status="valid" time="0.31" steps="62"/></proof>
</goal>
<goal name="Closed_formula_n">
<proof prover="1" timelimit="10"><result status="valid" time="2.02"/></proof>
<proof prover="3" timelimit="10" memlimit="1000"><result status="valid" time="5.45" steps="44"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="1.43"/></proof>
<proof prover="3" timelimit="10" memlimit="1000"><result status="valid" time="4.53" steps="44"/></proof>
</goal>
<goal name="Closed_formula_n_3">
<proof prover="1" timelimit="10"><result status="valid" time="3.20"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="2.40"/></proof>
</goal>
<goal name="Closed_formula_n_5">
<proof prover="1" timelimit="5"><result status="valid" time="0.52"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="Closed_formula_n_15">
<proof prover="1" timelimit="5"><result status="valid" time="0.30"/></proof>
......@@ -115,7 +115,7 @@
<proof prover="3" memlimit="1000"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="Closed_Formula">
<proof prover="4" timelimit="30" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="1.00"/></proof>
<proof prover="0" timelimit="30" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="1.00"/></proof>
</goal>
</theory>
<theory name="Euler001" sum="270c2a79b43cdbc70abf108abe165df9">
......
......@@ -2,6 +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="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="4000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="6" memlimit="4000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" memlimit="0"/>
......@@ -11,7 +12,6 @@
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<prover id="9" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="10" name="Eprover" version="1.8-001" timelimit="5" memlimit="0"/>
<prover id="11" name="Coq" version="8.4pl6" timelimit="10" memlimit="0"/>
<file name="../fibonacci.mlw" expanded="true">
<theory name="FibonacciTest" sum="039ab6528f220dfe0fc1771500be60d0">
<goal name="isfib_2_1">
......@@ -303,7 +303,7 @@
<proof prover="8"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter zeckendorf_fast.20" expl="20. loop invariant preservation">
<proof prover="3" memlimit="1000"><result status="valid" time="0.12"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter zeckendorf_fast.21" expl="21. loop variant decrease">
<proof prover="8"><result status="valid" time="0.02" steps="32"/></proof>
......@@ -449,12 +449,12 @@
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter logfib.4" expl="4. postcondition">
<proof prover="11" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="1.19"/></proof>
<proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="1.19"/></proof>
</goal>
</transf>
</goal>
<goal name="fib_m">
<proof prover="11" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="1.05"/></proof>
<proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="1.05"/></proof>
</goal>
<goal name="WP_parameter fibo" expl="VC for fibo">
<proof prover="2" memlimit="0"><result status="valid" time="0.00"/></proof>
......
......@@ -2,9 +2,9 @@
<!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="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="1000"/>
<prover id="5" name="Coq" version="8.4pl6" timelimit="10" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" memlimit="0"/>
<file name="../find.mlw" expanded="true">
<theory name="FIND" sum="5e3d7cfba4383daa9a34fcbe127a106b" expanded="true">
......@@ -111,7 +111,7 @@
<proof prover="4" memlimit="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="WP_parameter find.22" expl="22. loop invariant preservation" expanded="true">
<proof prover="5" edited="find_WP_FIND_WP_parameter_find_4.v"><result status="valid" time="9.16"/></proof>
<proof prover="0" edited="find_WP_FIND_WP_parameter_find_4.v"><result status="valid" time="9.16"/></proof>
</goal>
<goal name="WP_parameter find.23" expl="23. loop variant decrease">
<proof prover="4" memlimit="0"><result status="valid" time="0.03" steps="45"/></proof>
......
......@@ -2,17 +2,17 @@
<!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="5" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="0"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="5" memlimit="0"/>
<file name="../tree_max.mlw" expanded="true">