Commit f3af1893 authored by Andrei Paskevich's avatar Andrei Paskevich

examples: remove phony limits from sessions

parent c80f6b7a
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Spass" version="3.7" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Spass" version="3.7" timelimit="6" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="30" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="6" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../algo63.mlw" expanded="true">
<theory name="Algo63" sum="0097fa1af38060be8e585e2cfc854e2a" expanded="true">
<goal name="WP_parameter exchange" expl="VC for exchange">
......
......@@ -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="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="8ab02ef07be464ccc7c31dda9dd33adb" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
......
......@@ -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="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="83b400a3fbe590385036b24b91ab4989" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
......
......@@ -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="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="3b44ec37df3232d188580bcf31db876f" expanded="true">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true">
......
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="1" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="0"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="0d719c3e6262bb28f7a388d2aa2d5410" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
......
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" 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="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<file name="../association_list.mlw">
<theory name="Assoc" sum="12adb5d5e7c156493bafb1bd121c4586">
<goal name="appear_append">
......@@ -163,12 +163,12 @@
<proof prover="4"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_cut.9" expl="9. postcondition">
<proof prover="4" steplimit="0"><result status="valid" time="0.11" steps="312"/></proof>
<proof prover="4"><result status="valid" time="0.11" steps="312"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter model_split" expl="VC for model_split">
<proof prover="4" steplimit="0"><result status="valid" time="0.15" steps="686"/></proof>
<proof prover="4"><result status="valid" time="0.15" steps="686"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,47 +2,47 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="2" steplimit="1" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="2" memlimit="0"/>
<file name="../avl.mlw">
<theory name="SelectionTypes" sum="8ee3f641805a143e052f3881ea88fc8c">
<goal name="rebuild_aternative_def">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.07" steps="88"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.07" steps="88"/></proof>
</goal>
</theory>
<theory name="AVL" sum="14e0e79e1c62330bf7a8042003faef03">
<goal name="M.M.assoc">
<proof prover="1" steplimit="1"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="M.M.neutral">
<proof prover="1" steplimit="1"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter real_height_nonnegative" expl="VC for real_height_nonnegative">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="28"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="rotation_preserve_model">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter height" expl="VC for height">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="22"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter total" expl="VC for total">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="27"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter node" expl="VC for node">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.03" steps="98"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.03" steps="98"/></proof>
</goal>
<goal name="WP_parameter singleton" expl="VC for singleton">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.04" steps="63"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.13" steps="68"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.13" steps="68"/></proof>
</goal>
<goal name="WP_parameter view" expl="VC for view">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.07" steps="257"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.07" steps="257"/></proof>
</goal>
<goal name="WP_parameter balance" expl="VC for balance">
<transf name="split_goal_wp">
......@@ -157,13 +157,13 @@
<proof prover="1"><result status="valid" time="0.37" steps="583"/></proof>
</goal>
<goal name="WP_parameter decompose_front" expl="VC for decompose_front">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.09" steps="242"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.09" steps="242"/></proof>
</goal>
<goal name="WP_parameter decompose_back_node" expl="VC for decompose_back_node">
<proof prover="1"><result status="valid" time="0.48" steps="726"/></proof>
</goal>
<goal name="WP_parameter decompose_back" expl="VC for decompose_back">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.11" steps="302"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.11" steps="302"/></proof>
</goal>
<goal name="WP_parameter front_node" expl="VC for front_node">
<proof prover="1"><result status="valid" time="0.15" steps="309"/></proof>
......@@ -172,10 +172,10 @@
<proof prover="1"><result status="valid" time="0.08" steps="190"/></proof>
</goal>
<goal name="WP_parameter back_node" expl="VC for back_node">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.05" steps="118"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.05" steps="118"/></proof>
</goal>
<goal name="WP_parameter back" expl="VC for back">
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.03" steps="81"/></proof>
<proof prover="1" timelimit="2" memlimit="0"><result status="valid" time="0.03" steps="81"/></proof>
</goal>
<goal name="WP_parameter fuse" expl="VC for fuse">
<proof prover="2"><result status="valid" time="0.24"/></proof>
......@@ -187,13 +187,13 @@
<proof prover="1"><result status="valid" time="0.34" steps="563"/></proof>
</goal>
<goal name="WP_parameter join" expl="VC for join">
<proof prover="2" timelimit="5" steplimit="0" memlimit="1000"><result status="valid" time="0.50"/></proof>
<proof prover="2" timelimit="5" memlimit="1000"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="WP_parameter concat" expl="VC for concat">
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter default_split" expl="VC for default_split">
<proof prover="1" steplimit="1"><result status="valid" time="0.02" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
<goal name="WP_parameter insert" expl="VC for insert">
<transf name="split_goal_wp">
......
......@@ -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="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<file name="../monoid.mlw">
<theory name="Monoid" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......
......@@ -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="Alt-Ergo" version="1.01" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="3" memlimit="1000"/>
<file name="../preorder.mlw">
<theory name="Full" sum="41eddb6a5f9e7172479be99f6dc563ca">
<goal name="Eq.Refl">
......
......@@ -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="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<file name="../priority_queue.mlw">
<theory name="PQueue" sum="a8f2dd09a268c50fc0a71d952b1c9e0e">
<goal name="S.O.Trans">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="M.WP_parameter assoc_m" expl="VC for assoc_m">
<transf name="split_goal_wp">
......@@ -40,28 +40,28 @@
</transf>
</goal>
<goal name="M.WP_parameter neutral_m" expl="VC for neutral_m">
<proof prover="1" steplimit="1"><result status="valid" time="0.05"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="M.assoc">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="M.neutral">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="M.M.assoc">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="M.M.neutral">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="M.WP_parameter zero" expl="VC for zero">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.02" steps="1"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
<goal name="M.WP_parameter op" expl="VC for op">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.18" steps="97"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.18" steps="97"/></proof>
</goal>
<goal name="D.WP_parameter measure" expl="VC for measure">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="3"/></proof>
<proof prover="3" 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">
<transf name="split_goal_wp">
......@@ -279,70 +279,70 @@
</transf>
</goal>
<goal name="Sel.M.assoc">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="Sel.M.neutral">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="Sel.M.sum_def_nil">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="Sel.M.sum_def_cons">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="2"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="Sel.balancing_positive">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="1"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="Sel.selection_empty">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="3"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="3"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL M zero" expl="VC for avl AVL M zero">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="1"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL M op" expl="VC for avl AVL M op">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="1"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL D measure" expl="VC for avl AVL D measure">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.03" steps="1"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part">
<proof prover="3" timelimit="3" steplimit="1"><result status="valid" time="0.04" steps="102"/></proof>
<proof prover="3" 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">
<proof prover="3" steplimit="1"><result status="valid" time="0.03" steps="75"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="WP_parameter as_bag_bounds" expl="VC for as_bag_bounds">
<proof prover="3" steplimit="1"><result status="valid" time="0.08" steps="62"/></proof>
<proof prover="3"><result status="valid" time="0.08" steps="62"/></proof>
</goal>
<goal name="WP_parameter as_bag_membership" expl="VC for as_bag_membership">
<proof prover="3" steplimit="1"><result status="valid" time="0.07" steps="131"/></proof>
<proof prover="3"><result status="valid" time="0.07" steps="131"/></proof>
</goal>
<goal name="WP_parameter m" expl="VC for m">
<proof prover="3" steplimit="1"><result status="valid" time="0.04" steps="2"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="2"/></proof>
</goal>
<goal name="WP_parameter correction" expl="VC for correction">
<proof prover="3"><result status="valid" time="0.16" steps="397"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="3" steplimit="1"><result status="valid" time="0.07" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.07" steps="14"/></proof>
</goal>
<goal name="WP_parameter singleton" expl="VC for singleton">
<proof prover="3" steplimit="1"><result status="valid" time="0.03" steps="90"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="3" steplimit="1"><result status="valid" time="0.03" steps="82"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
<goal name="WP_parameter merge" expl="VC for merge">
<proof prover="3" steplimit="1"><result status="valid" time="0.03" steps="46"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="46"/></proof>
</goal>
<goal name="WP_parameter remove_count" expl="VC for remove_count">
<proof prover="3" steplimit="1"><result status="valid" time="0.25" steps="374"/></proof>
<proof prover="3"><result status="valid" time="0.25" steps="374"/></proof>
</goal>
<goal name="WP_parameter extract_min" expl="VC for extract_min">
<proof prover="3"><result status="valid" time="0.62" steps="994"/></proof>
</goal>
<goal name="WP_parameter min" expl="VC for min">
<proof prover="3" steplimit="1"><result status="valid" time="0.11" steps="89"/></proof>
<proof prover="3"><result status="valid" time="0.11" steps="89"/></proof>
</goal>
<goal name="WP_parameter pop_min" expl="VC for pop_min">
<proof prover="3"><result status="valid" time="1.86" steps="1913"/></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="2" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="c7ad4c6b81728dbd18a1c23ee5747ec2">
<goal name="M.assoc">
......@@ -118,7 +118,7 @@
<proof prover="2"><result status="valid" time="0.13" steps="329"/></proof>
</goal>
<goal name="WP_parameter remove" expl="VC for remove">
<proof prover="2" steplimit="0"><result status="valid" time="0.15" steps="346"/></proof>
<proof prover="2"><result status="valid" time="0.15" steps="346"/></proof>
</goal>
<goal name="WP_parameter cut" expl="VC for cut">
<proof prover="2"><result status="valid" time="0.05" steps="46"/></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="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<file name="../sorted.mlw">
<theory name="Increasing" sum="33bff6ba91e99a4e930bd71eb88f6a0e">
<goal name="smaller_lower_bound">
......
This diff is collapsed.
......@@ -2,10 +2,10 @@
<!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="6" steplimit="1" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="1" memlimit="4000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.4.1" timelimit="60" steplimit="1" memlimit="4000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="4000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="6" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.4.1" timelimit="60" memlimit="4000"/>
<prover id="9" name="Z3" version="4.4.0" timelimit="5" memlimit="4000"/>
<file name="../bag.mlw" expanded="true">
<theory name="Bag" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -61,7 +61,7 @@
<proof prover="1" timelimit="76" memlimit="1000"><result status="valid" time="10.80"/></proof>
</goal>
<goal name="WP_parameter remove.8" expl="8. assertion">
<proof prover="0" timelimit="5" steplimit="-1"><result status="valid" time="0.06" steps="34"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="34"/></proof>
</goal>
<goal name="WP_parameter remove.9" expl="9. type invariant">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02" steps="14"/></proof>
......@@ -70,7 +70,7 @@
<proof prover="0" memlimit="1000"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter remove.11" expl="11. type invariant">
<proof prover="1" timelimit="5" steplimit="-1"><result status="valid" time="2.35"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="2.35"/></proof>
<proof prover="9"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter remove.12" expl="12. postcondition">
......@@ -89,7 +89,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter remove.17" expl="17. assertion">
<proof prover="0" timelimit="5" steplimit="-1"><result status="valid" time="0.03" steps="25"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
<goal name="WP_parameter remove.18" expl="18. type invariant">
<proof prover="0" memlimit="1000"><result status="valid" time="0.01" steps="12"/></proof>
......
......@@ -2,15 +2,15 @@
<!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" steplimit="1" memlimit="4000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="15" steplimit="1" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="15" steplimit="1" memlimit="0"/>
<prover id="7" name="Vampire" version="0.6" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="9" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" memlimit="4000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="15" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="15" memlimit="0"/>
<prover id="7" name="Vampire" version="0.6" timelimit="5" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<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"/>
<file name="../bellman_ford.mlw" expanded="true">
<theory name="Graph" sum="a445091f6d55fb03cbfd6988f8e23631" expanded="true">
<goal name="vertices_cardinal_pos">
......
......@@ -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="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="7c8646b76f7105e1357a0dac5eef6893" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
......
......@@ -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="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../binary_sqrt.mlw" expanded="true">
<theory name="BinarySqrt" sum="6b669d31cbc3c11118695754ff2ebc1b" expanded="true">
<goal name="WP_parameter sqrt" expl="VC for sqrt" expanded="true">
......
......@@ -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="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="6" memlimit="1000"/>
<file name="../binomial_heap.mlw" expanded="true">
<theory name="BinomialHeap" sum="69f761ca58435723990c69900429c264" expanded="true">
<goal name="WP_parameter size_nonnneg" expl="VC for size_nonnneg">
......
......@@ -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="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="30" memlimit="1000"/>
<file name="../bitcount.mlw" expanded="true">
<theory name="BitCount8bit_fact" sum="eb4b1bf6da7b0da8d18857818ce50281" expanded="true">
<goal name="nth_as_bv_is_int">
......@@ -151,7 +151,7 @@
<goal name="WP_parameter proof0.3.1" expl="1. VC for proof0" expanded="true">
<transf name="introduce_premises" expanded="true">
<goal name="WP_parameter proof0.3.1.1" expl="1. VC for proof0" expanded="true">
<proof prover="2" steplimit="-1"><result status="valid" time="0.17"/></proof>
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
......
......@@ -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="Alt-Ergo" version="0.99.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="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="01976ddc6bd80d04acbe32f98fd3ce49">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
......
......@@ -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.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"/>
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" memlimit="4000"/>
<prover id="9" name="Z3" version="3.2" timelimit="3" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvector.why" expanded="true">
<theory name="BitVector" sum="d28eacb18daec312a94869cf046a4a41">
<goal name="Nth_bw_xor_v1true">
......
......@@ -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="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="5" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="30" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......
......@@ -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="Gappa" version="1.2.0" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="60" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="60" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../double_of_int.why" expanded="true">
<theory name="DoubleOfInt" sum="87ee559ceb9ab752593b5ea1c5d09b6e" expanded="true">
<goal name="nth_j1">
......
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4"