Commit 47e6a710 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 8e560e42
......@@ -8,10 +8,10 @@
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../priority_queue.mlw" proved="true">
<theory name="PQueue" proved="true">
<goal name="Trans" proved="true">
<goal name="S.O.Trans" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter assoc_m" expl="VC for assoc_m" proved="true">
<goal name="M.WP_parameter assoc_m" expl="VC for assoc_m" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter assoc_m.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -39,28 +39,28 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter neutral_m" expl="VC for neutral_m" proved="true">
<goal name="M.WP_parameter neutral_m" expl="VC for neutral_m" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="assoc" proved="true">
<goal name="M.assoc" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="neutral" proved="true">
<goal name="M.neutral" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="assoc" proved="true">
<goal name="M.M.assoc" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="neutral" proved="true">
<goal name="M.M.neutral" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter zero" expl="VC for zero" proved="true">
<goal name="M.WP_parameter zero" expl="VC for zero" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
<goal name="WP_parameter op" expl="VC for op" proved="true">
<goal name="M.WP_parameter op" expl="VC for op" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.18" steps="97"/></proof>
</goal>
<goal name="WP_parameter measure" expl="VC for measure" proved="true">
<goal name="D.WP_parameter measure" expl="VC for measure" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="3"/></proof>
</goal>
<goal name="WP_parameter monoid_sum_is_min" expl="VC for monoid_sum_is_min" proved="true">
......@@ -278,34 +278,34 @@
</goal>
</transf>
</goal>
<goal name="assoc" proved="true">
<goal name="Sel.M.assoc" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="neutral" proved="true">
<goal name="Sel.M.neutral" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="sum_def_nil" proved="true">
<goal name="Sel.M.sum_def_nil" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="sum_def_cons" proved="true">
<goal name="Sel.M.sum_def_cons" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="balancing_positive" proved="true">
<goal name="Sel.balancing_positive" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="selection_empty" proved="true">
<goal name="Sel.selection_empty" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="3"/></proof>
</goal>
<goal name="WP_parameter avl AVL M zero" expl="VC for avl AVL M zero" proved="true">
<goal name="Sel.WP_parameter avl AVL M zero" expl="VC for avl AVL M zero" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="WP_parameter avl AVL M op" expl="VC for avl AVL M op" proved="true">
<goal name="Sel.WP_parameter avl AVL M op" expl="VC for avl AVL M op" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="WP_parameter avl AVL D measure" expl="VC for avl AVL D measure" proved="true">
<goal name="Sel.WP_parameter avl AVL D measure" expl="VC for avl AVL D measure" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part" proved="true">
<goal name="Sel.WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part" proved="true">
<proof prover="1" timelimit="3"><result status="valid" time="0.04" steps="102"/></proof>
</goal>
<goal name="WP_parameter as_bag_append" expl="VC for as_bag_append" proved="true">
......
This diff is collapsed.
......@@ -29,7 +29,7 @@
<goal name="mod_div_unique.0.1.1.0" expl="false case (true case)" proved="true">
<transf name="assert" proved="true" arg1="(y * (q - div x y) &lt;= - y)">
<goal name="mod_div_unique.0.1.1.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.68"/></proof>
<proof prover="2"><result status="valid" time="0.45"/></proof>
</goal>
<goal name="mod_div_unique.0.1.1.0.1" expl="false case (true case)" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
......@@ -183,7 +183,7 @@
<proof prover="0" timelimit="10"><result status="valid" time="2.36"/></proof>
</goal>
<goal name="Closed_formula_n_5" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.48"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="Closed_formula_n_15" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.30"/></proof>
......
......@@ -525,7 +525,7 @@
<goal name="WP_parameter find_max.90" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter find_max.90.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="185"/></proof>
<proof prover="0"><result status="valid" time="0.29" steps="185"/></proof>
</goal>
</transf>
</goal>
......@@ -533,7 +533,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="WP_parameter find_max.92" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="181"/></proof>
<proof prover="0"><result status="valid" time="0.29" steps="181"/></proof>
</goal>
<goal name="WP_parameter find_max.93" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
......@@ -547,7 +547,7 @@
<goal name="WP_parameter find_max.96" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter find_max.96.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.49" steps="181"/></proof>
<proof prover="0"><result status="valid" time="0.29" steps="181"/></proof>
</goal>
</transf>
</goal>
......@@ -619,7 +619,7 @@
<goal name="WP_parameter find_max.108" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter find_max.108.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.49" steps="181"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="181"/></proof>
</goal>
</transf>
</goal>
......@@ -639,7 +639,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter find_max.114" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="177"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="177"/></proof>
</goal>
<goal name="WP_parameter find_max.115" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
......@@ -647,7 +647,7 @@
<goal name="WP_parameter find_max.116" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter find_max.116.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.49" steps="173"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="173"/></proof>
</goal>
</transf>
</goal>
......@@ -787,7 +787,7 @@
<goal name="WP_parameter find_max.144" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter find_max.144.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.51" steps="181"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="181"/></proof>
</goal>
</transf>
</goal>
......@@ -795,7 +795,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
<goal name="WP_parameter find_max.146" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.48" steps="177"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="177"/></proof>
</goal>
<goal name="WP_parameter find_max.147" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
......@@ -807,13 +807,13 @@
<proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
<goal name="WP_parameter find_max.150" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="177"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="177"/></proof>
</goal>
<goal name="WP_parameter find_max.151" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="WP_parameter find_max.152" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.49" steps="173"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="173"/></proof>
</goal>
<goal name="WP_parameter find_max.153" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
......@@ -847,13 +847,13 @@
<proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
<goal name="WP_parameter find_max.162" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.47" steps="177"/></proof>
<proof prover="0"><result status="valid" time="0.29" steps="177"/></proof>
</goal>
<goal name="WP_parameter find_max.163" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="WP_parameter find_max.164" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.46" steps="173"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="173"/></proof>
</goal>
<goal name="WP_parameter find_max.165" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
......@@ -1139,7 +1139,7 @@
<goal name="WP_parameter find_max.220" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="WP_parameter find_max.220.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.33" steps="167"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="167"/></proof>
</goal>
</transf>
</goal>
......@@ -1815,7 +1815,7 @@
<goal name="WP_parameter find_max.340.0.0" expl="loop invariant preservation" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="WP_parameter find_max.340.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.64" steps="339"/></proof>
<proof prover="0"><result status="valid" time="0.48" steps="339"/></proof>
</goal>
</transf>
</goal>
......@@ -1851,7 +1851,7 @@
<goal name="WP_parameter find_max.344.0.0" expl="loop invariant preservation" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="WP_parameter find_max.344.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="333"/></proof>
<proof prover="0"><result status="valid" time="0.52" steps="348"/></proof>
</goal>
</transf>
</goal>
......
......@@ -83,7 +83,7 @@
</goal>
<goal name="WP_parameter inverse_in_place.13" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="3.34"/></proof>
<proof prover="4"><result status="valid" time="2.80"/></proof>
</goal>
<goal name="WP_parameter inverse_in_place.14" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.46"/></proof>
......
......@@ -796,7 +796,7 @@
<proof prover="2" timelimit="16"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter enum.48.0.0.1" expl="VC for enum" proved="true">
<proof prover="2" timelimit="16"><result status="valid" time="4.92"/></proof>
<proof prover="2" timelimit="16"><result status="valid" time="4.32"/></proof>
</goal>
<goal name="WP_parameter enum.48.0.0.2" expl="VC for enum" proved="true">
<proof prover="2" timelimit="16"><result status="valid" time="0.20"/></proof>
......
......@@ -417,7 +417,7 @@
</transf>
</goal>
<goal name="WP_parameter app.15" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="5.34"/></proof>
<proof prover="0"><result status="valid" time="4.66"/></proof>
</goal>
<goal name="WP_parameter app.16" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="131"/></proof>
......
......@@ -7,10 +7,6 @@
<prover id="5" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../BacktrackArray.mlw" proved="true">
<theory name="Types" proved="true">
</theory>
<theory name="Logic" proved="true">
</theory>
<theory name="Impl" proved="true">
<goal name="WP_parameter create" expl="VC for create" proved="true">
<proof prover="4"><result status="valid" time="0.11" steps="82"/></proof>
......@@ -166,7 +162,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="WP_parameter resize_for.37" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.85" steps="94"/></proof>
<proof prover="4"><result status="valid" time="0.66" steps="94"/></proof>
</goal>
<goal name="WP_parameter resize_for.38" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.23" steps="106"/></proof>
......@@ -237,7 +233,7 @@
<proof prover="1"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="WP_parameter iadd.9.0.3" expl="VC for iadd" proved="true">
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="1"><result status="valid" time="0.54"/></proof>
</goal>
</transf>
</goal>
......
......@@ -437,7 +437,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter compile.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="3.46"/></proof>
<proof prover="1"><result status="valid" time="3.00"/></proof>
</goal>
<goal name="WP_parameter compile.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></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="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../residual.mlw" proved="true">
<theory name="Residuals" proved="true">
......
......@@ -14,8 +14,6 @@
<proof prover="4"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
</theory>
<theory name="Sig" proved="true">
</theory>
<theory name="Rope" proved="true">
<goal name="rope_length_is_string_length" proved="true">
<transf name="induction_ty_lex" proved="true" >
......
......@@ -103,7 +103,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter lm_merge_ok.14" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="2.57"/></proof>
<proof prover="0"><result status="valid" time="2.09"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,8 +6,6 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2016_tree_traversal.mlw" proved="true">
<theory name="Memory" proved="true">
</theory>
<theory name="TreeShape" proved="true">
<goal name="WP_parameter ext_set" expl="VC for ext_set" proved="true">
<proof prover="1"><result status="valid" time="0.12" steps="511"/></proof>
......
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