Skip to content

GitLab

why3
why3
Commit 4383d9c8 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Revert "sessions replayed on moloch" 

This reverts commit 838ed39a.
parent 838ed39a
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 573 additions and 574 deletions
examples/bellman_ford/why3session.xml
View file @ 4383d9c8
This diff is collapsed.
examples/bitvectors/bitvector/why3session.xml
View file @ 4383d9c8
......@@ -2,7 +2,7 @@
<!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.5" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="4000"/>
......@@ -31,16 +31,16 @@
<proof prover="6" memlimit="1000"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="to_nat_of_zero2">
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="1.33"/></proof>
<proof prover="0" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.92"/></proof>
</goal>
<goal name="to_nat_of_zero">
<proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="2.23"/></proof>
<proof prover="0" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="2.78"/></proof>
</goal>
<goal name="to_nat_of_one">
<proof prover="1" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="2.12"/></proof>
<proof prover="0" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="1.79"/></proof>
</goal>
<goal name="to_nat_sub_footprint">
<proof prover="1" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="3.73"/></proof>
<proof prover="0" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="3.73"/></proof>
</goal>
<goal name="nth_from_int_low_even">
<proof prover="2"><result status="valid" time="0.02" steps="68"/></proof>
......@@ -72,7 +72,7 @@
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_from_int2c_plus_pow2">
<proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.86"/></proof>
<proof prover="0" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="1.27"/></proof>
<proof prover="2"><result status="valid" time="0.12" steps="85"/></proof>
</goal>
</theory>
......@@ -108,21 +108,21 @@
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="9"><result status="valid" time="2.59"/></proof>
<proof prover="10"><result status="valid" time="0.78"/></proof>
<proof prover="10"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="Test5">
<proof prover="2"><result status="valid" time="0.05" steps="71"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="0.04"/></proof>
<proof prover="9"><result status="valid" time="2.62"/></proof>
<proof prover="10"><result status="valid" time="0.69"/></proof>
<proof prover="10"><result status="valid" time="0.53"/></proof>
</goal>
<goal name="Test6">
<proof prover="2"><result status="valid" time="0.05" steps="71"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="9" timelimit="9"><result status="valid" time="3.09"/></proof>
<proof prover="10"><result status="valid" time="0.73"/></proof>
<proof prover="9" timelimit="9"><result status="valid" time="2.52"/></proof>
<proof prover="10"><result status="valid" time="0.53"/></proof>
</goal>
<goal name="to_nat_0x00000000">
<proof prover="2"><result status="valid" time="0.04" steps="78"/></proof>
......@@ -132,64 +132,64 @@
<proof prover="10"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="to_nat_0x00000001">
<proof prover="6" timelimit="120" memlimit="1000"><result status="valid" time="96.32"/></proof>
<proof prover="6" timelimit="120" memlimit="1000"><result status="valid" time="72.98"/></proof>
</goal>
<goal name="to_nat_0x00000003">
<proof prover="6" timelimit="120" memlimit="1000"><result status="valid" time="77.48"/></proof>
<proof prover="6" timelimit="120" memlimit="1000"><result status="valid" time="63.35"/></proof>
</goal>
<goal name="to_nat_0x00000007">
<proof prover="6" timelimit="60"><result status="valid" time="67.57"/></proof>
<proof prover="6" timelimit="60"><result status="valid" time="54.99"/></proof>
</goal>
<goal name="to_nat_0x0000000F">
<proof prover="6" timelimit="120" memlimit="1000"><result status="valid" time="61.40"/></proof>
<proof prover="6" timelimit="120" memlimit="1000"><result status="valid" time="46.07"/></proof>
</goal>
<goal name="to_nat_0x0000001F">
<proof prover="6" timelimit="30"><result status="valid" time="50.20"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="38.43"/></proof>
</goal>
<goal name="to_nat_0x0000003F">
<proof prover="6" timelimit="30"><result status="valid" time="39.43"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="31.83"/></proof>
</goal>
<goal name="to_nat_0x0000007F">
<proof prover="6" timelimit="30"><result status="valid" time="32.81"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="26.44"/></proof>
</goal>
<goal name="to_nat_0x000000FF">
<proof prover="6" timelimit="30"><result status="valid" time="29.88"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="21.42"/></proof>
</goal>
<goal name="to_nat_0x000001FF">
<proof prover="6" timelimit="30"><result status="valid" time="21.72"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="17.53"/></proof>
</goal>
<goal name="to_nat_0x000003FF">
<proof prover="6" timelimit="30"><result status="valid" time="20.40"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="14.09"/></proof>
</goal>
<goal name="to_nat_0x000007FF">
<proof prover="6" timelimit="30"><result status="valid" time="16.31"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="11.02"/></proof>
</goal>
<goal name="to_nat_0x00000FFF">
<proof prover="6" timelimit="30"><result status="valid" time="9.99"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="8.79"/></proof>
</goal>
<goal name="to_nat_0x00001FFF">
<proof prover="6" timelimit="30"><result status="valid" time="7.97"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="6.88"/></proof>
</goal>
<goal name="to_nat_0x00003FFF">
<proof prover="6" timelimit="30"><result status="valid" time="7.47"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="5.48"/></proof>
</goal>
<goal name="to_nat_0x00007FFF">
<proof prover="6" timelimit="30"><result status="valid" time="6.23"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="4.14"/></proof>
</goal>
<goal name="to_nat_0x0000FFFF">
<proof prover="6" memlimit="1000"><result status="valid" time="4.35"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="3.18"/></proof>
</goal>
<goal name="to_nat_0x0001FFFF">
<proof prover="6" memlimit="1000"><result status="valid" time="3.35"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="2.32"/></proof>
</goal>
<goal name="to_nat_0x0003FFFF">
<proof prover="6" memlimit="1000"><result status="valid" time="2.33"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="1.77"/></proof>
</goal>
<goal name="to_nat_0x0007FFFF">
<proof prover="6" memlimit="1000"><result status="valid" time="2.22"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="1.56"/></proof>
</goal>
<goal name="to_nat_0x000FFFFF">
<proof prover="6" memlimit="1000"><result status="valid" time="1.09"/></proof>
<proof prover="6" memlimit="1000"><result status="valid" time="0.89"/></proof>
</goal>
<goal name="to_nat_0x00FFFFFF">
<proof prover="6" memlimit="1000"><result status="valid" time="0.28"/></proof>
......
examples/bitvectors/double/why3session.xml
View file @ 4383d9c8
......@@ -4,8 +4,8 @@
<why3session shape_version="4">
<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="Coq" version="8.4pl6" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Coq" version="8.5" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -28,12 +28,12 @@
</goal>
<goal name="exp_one" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.32" steps="805"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.93"/></proof>
<proof prover="2" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.93"/></proof>
</goal>
<goal name="mantissa_one">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.75"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.38"/></proof>
<proof prover="3"><result status="valid" time="0.48"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.78"/></proof>
</goal>
<goal name="double_value_of_1">
<proof prover="0"><result status="valid" time="0.04" steps="94"/></proof>
......
examples/bitvectors/power2/why3session.xml
View file @ 4383d9c8
This diff is collapsed.
examples/bts/12934/why3session.xml
View file @ 4383d9c8
......@@ -2,11 +2,11 @@
<!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.5" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" steplimit="1" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="e32351513bba9a37f680056dd466bcee" expanded="true">
<goal name="t" expanded="true">
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.50"/></proof>
<proof prover="1" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.75"/></proof>
</goal>
</theory>
</file>
......
examples/bts/13849/why3session.xml
View file @ 4383d9c8
......@@ -2,11 +2,11 @@
<!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.5" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" steplimit="1" memlimit="0"/>
<file name="../13849.why" expanded="true">
<theory name="T" sum="fe6d0a97ed129807ad9b025e583a359d" expanded="true">
<goal name="x" expanded="true">
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.50"/></proof>
<proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="0.75"/></proof>
</goal>
</theory>
</file>
......
examples/bts/13854/why3session.xml
View file @ 4383d9c8
......@@ -2,14 +2,14 @@
<!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.5" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="0"/>
<file name="../13854.why">
<theory name="T" sum="e0ed6fa44df780ea63fc8d3dbdece469" expanded="true">
<goal name="g" expanded="true">
<proof prover="0" edited="13854_T_g_1.v"><result status="valid" time="0.74"/></proof>
<proof prover="1" edited="13854_T_g_1.v"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="x" expanded="true">
<proof prover="0" edited="13854_T_x_1.v"><result status="valid" time="0.73"/></proof>
<proof prover="1" edited="13854_T_x_1.v"><result status="valid" time="0.73"/></proof>
</goal>
</theory>
</file>
......
examples/dfa_example/why3session.xml
View file @ 4383d9c8
......@@ -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.5" timelimit="8" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="8" steplimit="1" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="8" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
<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.79"/></proof>
<proof prover="2" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.79"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="7"><result status="valid" time="0.08" steps="140"/></proof>
</goal>
......@@ -36,7 +36,7 @@
<goal name="WP_parameter one_w_in_r1" expl="VC for one_w_in_r1">
<transf name="split_goal_wp">
<goal name="WP_parameter one_w_in_r1.1" expl="1. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.47" steps="377"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.28" steps="377"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.2" expl="2. assertion">
<proof prover="7" memlimit="1000"><result status="valid" time="0.24" steps="386"/></proof>
......
examples/dijkstra/why3session.xml
View file @ 4383d9c8
......@@ -2,7 +2,7 @@
<!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.5" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="0" name="Coq" version="8.4pl6" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
......@@ -40,7 +40,7 @@
<proof prover="8"><result status="valid" time="0.02" steps="9"/></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.01"/></proof>
<proof prover="0" timelimit="5" edited="dijkstra_DijkstraShortestPath_Path_shortest_path_1.v"><result status="valid" time="1.32"/></proof>
</goal>
<goal name="Main_lemma">
<proof prover="3" timelimit="5"><result status="valid" time="0.08"/></proof>
......@@ -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="1.44"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="0.96"/></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="3.55"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="2.50"/></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="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="9.16"/></proof>
<proof prover="0" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_2.v"><result status="valid" time="3.30"/></proof>
</goal>
</transf>
</goal>
......@@ -163,10 +163,10 @@
<transf name="split_goal_wp">
<goal name="WP_parameter shortest_path_code.13.1.1.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="3.20"/></proof>
<proof prover="5"><result status="valid" time="2.18"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.13.1.1.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.27"/></proof>
<proof prover="2"><result status="valid" time="0.78"/></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="1" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="5.85"/></proof>
<proof prover="0" edited="dijkstra_DijkstraShortestPath_WP_parameter_shortest_path_code_3.v"><result status="valid" time="5.85"/></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>
......
examples/double_wp/compiler/why3session.xml
View file @ 4383d9c8
......@@ -6,9 +6,9 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../compiler.mlw" expanded="true">
<theory name="Compile_aexpr" sum="f149c7930975bd42aaeb1fca31573102" expanded="true">
<goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr">
......@@ -459,10 +459,10 @@
<proof prover="2"><result status="valid" time="0.12" steps="37"/></proof>
</goal>
<goal name="WP_parameter compile_bexpr.34.1.1.5" expl="5. VC for compile_bexpr">
<proof prover="2"><result status="valid" time="0.53" steps="202"/></proof>
<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.58" steps="172"/></proof>
<proof prover="2"><result status="valid" time="0.32" steps="172"/></proof>
</goal>
</transf>
</goal>
......@@ -564,7 +564,7 @@
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter compile_bexpr.52.1.1.5" expl="5. VC for compile_bexpr">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
......@@ -1929,7 +1929,7 @@
<proof prover="2"><result status="valid" time="0.25" steps="47"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.2" expl="2. VC for compile_com">
<proof prover="2"><result status="valid" time="0.43" steps="58"/></proof>
<proof prover="2"><result status="valid" time="0.20" steps="58"/></proof>
</goal>
<goal name="WP_parameter compile_com.34.1.1.3" expl="3. VC for compile_com">
<proof prover="2"><result status="valid" time="0.28" steps="57"/></proof>
......@@ -1938,43 +1938,43 @@
<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.38" steps="57"/></proof>
<proof prover="2"><result status="valid" time="0.19" 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.76" steps="394"/></proof>
<proof prover="2"><result status="valid" time="0.95" 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.34" steps="63"/></proof>
<proof prover="2"><result status="valid" time="0.18" 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.41" 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.46" 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.37" steps="56"/></proof>
<proof prover="2"><result status="valid" time="0.19" 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.60" steps="365"/></proof>
<proof prover="2"><result status="valid" time="0.98" 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.62" steps="94"/></proof>
<proof prover="2"><result status="valid" time="0.43" 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.45" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.28" 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.58" 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.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.34" 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.18" expl="18. VC for compile_com">
<proof prover="2"><result status="valid" time="0.28" steps="73"/></proof>
......@@ -2031,7 +2031,7 @@
<proof prover="2"><result status="valid" time="0.15" steps="39"/></proof>
</goal>
<goal name="WP_parameter compile_com.45.1.1.2" expl="2. VC for compile_com">
<proof prover="6" timelimit="60" memlimit="2000"><result status="valid" time="0.30"/></proof>
<proof prover="6" timelimit="60" memlimit="2000"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="WP_parameter compile_com.45.1.1.3" expl="3. VC for compile_com">
<proof prover="2"><result status="valid" time="0.20" steps="48"/></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.16"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="1.48"/></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="0.93"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="1.35"/></proof>
<proof prover="6" timelimit="20"><result status="valid" time="0.83"/></proof>
<proof prover="0"><result status="valid" time="0.53"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="1.07"/></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="4" edited="compiler_Compile_com_WP_parameter_compile_com_1.v"><result status="valid" time="2.75"/></proof>
<proof prover="7" edited="compiler_Compile_com_WP_parameter_compile_com_1.v"><result status="valid" time="2.75"/></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,16 +3139,16 @@
<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.40" steps="58"/></proof>
<proof prover="2"><result status="valid" time="0.24" 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.59" 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.42" 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>
......
examples/fibonacci/why3session.xml
View file @ 4383d9c8
......@@ -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.5" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="7" name="Vampire" version="0.6" timelimit="3" steplimit="1" memlimit="0"/>
......@@ -447,12 +447,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="0" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="0.92"/></proof>
<proof prover="1" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="0.92"/></proof>
</goal>
</transf>
</goal>
<goal name="fib_m">
<proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="0.82"/></proof>
<proof prover="1" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="WP_parameter fibo" expl="VC for fibo">
<proof prover="2" memlimit="0"><result status="valid" time="0.00"/></proof>
......
examples/find/why3session.xml
View file @ 4383d9c8
......@@ -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.5" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="10" steplimit="1" memlimit="0"/>
<file name="../find.mlw" 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="0" edited="find_WP_FIND_WP_parameter_find_4.v"><result status="valid" time="3.17"/></proof>
<proof prover="2" edited="find_WP_FIND_WP_parameter_find_4.v"><result status="valid" time="8.99"/></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>
......
examples/foveoos11-cm/tree_max/why3session.xml
View file @ 4383d9c8
......@@ -2,12 +2,12 @@
<!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.5" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="0"/>
<file name="../tree_max.mlw" expanded="true">
<theory name="BinTree" sum="1f182bb1a6b4dfd59a83a5161c6e4344" expanded="true">
<goal name="ge_trans" expanded="true">
<proof prover="0" edited="tree_max_BinTree_ge_trans_1.v"><result status="valid" time="0.50"/></proof>
<proof prover="1" edited="tree_max_BinTree_ge_trans_1.v"><result status="valid" time="0.77"/></proof>
</goal>
</theory>
<theory name="TreeMax" sum="4a8e21471d157deb418f79d060f4a727" expanded="true">
......
examples/foveoos11_challenge2/why3session.xml
View file @ 4383d9c8
......@@ -2,12 +2,12 @@
<!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.5" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="0"/>
<file name="../foveoos11_challenge2.mlw" expanded="true">
<theory name="MaximumTree" sum="a00e1f9c636259085c5337c363a52ea1" expanded="true">
<goal name="size_nonneg" expanded="true">
<proof prover="0" edited="foveoos11_challenge2_WP_MaximumTree_size_nonneg_1.v"><result status="valid" time="0.50"/></proof>
<proof prover="1" edited="foveoos11_challenge2_WP_MaximumTree_size_nonneg_1.v"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="WP_parameter maximum" expl="VC for maximum" expanded="true">
<proof prover="2"><result status="valid" time="0.56" steps="812"/></proof>
......
examples/foveoos11_challenge3/why3session.xml
View file @ 4383d9c8
......@@ -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.5" timelimit="15" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="15" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../foveoos11_challenge3.mlw" expanded="true">
<theory name="TwoEqualElements" sum="3d208f83289660e2a89799af50e126d8" expanded="true">
......@@ -49,7 +49,7 @@
<proof prover="4"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter two_equal_elements.14" expl="14. loop invariant preservation">
<proof prover="0" edited="foveoos11_challenge3_WP_TwoEqualElements_WP_parameter_two_equal_elements_1.v"><result status="valid" time="10.63"/></proof>
<proof prover="2" edited="foveoos11_challenge3_WP_TwoEqualElements_WP_parameter_two_equal_elements_1.v"><result status="valid" time="12.18"/></proof>
</goal>
<goal name="WP_parameter two_equal_elements.15" expl="15. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.03" steps="21"/></proof>
......@@ -85,7 +85,7 @@
<proof prover="4"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter two_equal_elements.26" expl="26. loop invariant preservation">
<proof prover="0" edited="foveoos11_challenge3_WP_TwoEqualElements_WP_parameter_two_equal_elements_2.v"><result status="valid" time="3.34"/></proof>
<proof prover="2" edited="foveoos11_challenge3_WP_TwoEqualElements_WP_parameter_two_equal_elements_2.v"><result status="valid" time="3.34"/></proof>
</goal>
<goal name="WP_parameter two_equal_elements.27" expl="27. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.04" steps="21"/></proof>
......@@ -118,13 +118,13 @@
<proof prover="4"><result status="valid" time="0.08" steps="70"/></proof>
</goal>
<goal name="WP_parameter two_equal_elements.37" expl="37. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.28" steps="120"/></proof>
<proof prover="4"><result status="valid" time="0.14" steps="120"/></proof>
</goal>
<goal name="WP_parameter two_equal_elements.38" expl="38. loop invariant preservation">