Skip to content

why3
why3
Commit 627596d6 authored by Johannes Kanig's avatar Johannes Kanig
Browse files
Options

Merge branch 'lri-master' into why3server

parents ec36a6ec cf4020c5
Hide whitespace changes
Inline Side-by-side
Showing with 2289 additions and 1445 deletions
examples/cursor/why3session.xml
View file @ 627596d6
......@@ -7,7 +7,8 @@
<prover id="2" name="CVC4" version="1.3" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="10" steplimit="1" memlimit="1000"/>
<file name="../cursor.mlw">
<prover id="5" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../cursor.mlw" expanded="true">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestCursor" sum="4a864b2c874ceb1b6d23670c5e40f80b">
......@@ -100,9 +101,9 @@
</transf>
</goal>
</theory>
<theory name="IntArrayCursor" sum="b0842edc620996a629ec35b7446b1834">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
<theory name="IntArrayCursor" sum="8090cb9a5eb720659015e09ae27d5ddf" expanded="true">
<goal name="WP_parameter create" expl="VC for create" expanded="true">
<proof prover="5"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
<goal name="WP_parameter has_next" expl="VC for has_next">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......
examples/in_progress/2wp_gen/game/why3session.xml
View file @ 627596d6
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/in_progress/2wp_gen/transfinite/why3session.xml
View file @ 627596d6
......@@ -2,36 +2,36 @@
<!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="1000" memlimit="1"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="1000" memlimit="1"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="1000" memlimit="1"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1000" memlimit="-1"/>
<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="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../transfinite.mlw">
<theory name="IterateCommon" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Iterates" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="IterateProof" sum="f55452db3323b43c0bd8585d92d7a17c">
<theory name="IterateProof" sum="9b37055dcc48fd3f2dc41464fef6519c">
<goal name="tr_reach_compare">
<transf name="induction_pr">
<goal name="tr_reach_compare.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_compare.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_compare.2" expl="2.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_compare.2.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.14"/></proof>
<proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_compare.3" expl="3.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_compare.3.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="52"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
</transf>
</goal>
......@@ -44,7 +44,7 @@
<goal name="separation.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="separation.1.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="44"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="44"/></proof>
</goal>
</transf>
</goal>
......@@ -55,7 +55,7 @@
<goal name="separation.2.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="separation.2.1.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.30"/></proof>
<proof prover="0"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
</goal>
......@@ -68,7 +68,7 @@
<goal name="separation.3.1.1" expl="1.">
<transf name="inline_goal">
<goal name="separation.3.1.1.1" expl="1.">
<proof prover="3" steplimit="1" memlimit="1000"><result status="valid" time="0.72"/></proof>
<proof prover="3"><result status="valid" time="0.72"/></proof>
</goal>
</transf>
</goal>
......@@ -81,25 +81,25 @@
<goal name="all_separation">
<transf name="split_goal_wp">
<goal name="all_separation.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="47"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="all_separation.2" expl="2.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.11" steps="317"/></proof>
<proof prover="4"><result status="valid" time="0.11" steps="317"/></proof>
</goal>
<goal name="all_separation.3" expl="3.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="22"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="all_separation.4" expl="4.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="40"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="40"/></proof>
</goal>
<goal name="all_separation.5" expl="5.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.04" steps="251"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="251"/></proof>
</goal>
<goal name="all_separation.6" expl="6.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.08" steps="625"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="625"/></proof>
</goal>
<goal name="all_separation.7" expl="7.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="108"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="108"/></proof>
</goal>
<goal name="all_separation.8" expl="8.">
<transf name="induction_pr">
......@@ -108,7 +108,7 @@
<goal name="all_separation.8.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="all_separation.8.1.1.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.14"/></proof>
<proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
......@@ -119,7 +119,7 @@
<goal name="all_separation.8.2.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="all_separation.8.2.1.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.29"/></proof>
<proof prover="0"><result status="valid" time="0.29"/></proof>
</goal>
</transf>
</goal>
......@@ -130,7 +130,7 @@
<goal name="all_separation.8.3.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="all_separation.8.3.1.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.14"/></proof>
<proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
......@@ -143,35 +143,35 @@
<goal name="fixpoint_max_proof">
<transf name="split_goal_wp">
<goal name="fixpoint_max_proof.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.08"/></proof>
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="fixpoint_max_proof.2" expl="2.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="283"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="283"/></proof>
</goal>
<goal name="fixpoint_max_proof.3" expl="3.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="fixpoint_max_proof.4" expl="4.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="fixpoint_max_proof.5" expl="5.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="55"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="55"/></proof>
</goal>
<goal name="fixpoint_max_proof.6" expl="6.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="fixpoint_max_proof.7" expl="7.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.32" steps="1089"/></proof>
<proof prover="4"><result status="valid" time="0.32" steps="1089"/></proof>
</goal>
<goal name="fixpoint_max_proof.8" expl="8.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
</transf>
</goal>
<goal name="fixpoint_is_max_proof">
<transf name="split_goal_wp">
<goal name="fixpoint_is_max_proof.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="83"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="83"/></proof>
</goal>
<goal name="fixpoint_is_max_proof.2" expl="2.">
<transf name="induction_pr">
......@@ -180,7 +180,7 @@
<goal name="fixpoint_is_max_proof.2.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="fixpoint_is_max_proof.2.1.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="31"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
</transf>
</goal>
......@@ -191,7 +191,7 @@
<goal name="fixpoint_is_max_proof.2.2.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="fixpoint_is_max_proof.2.2.1.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="1.35"/></proof>
<proof prover="0"><result status="valid" time="1.35"/></proof>
</goal>
</transf>
</goal>
......@@ -202,7 +202,7 @@
<goal name="fixpoint_is_max_proof.2.3.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="fixpoint_is_max_proof.2.3.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="90"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
</transf>
</goal>
......@@ -211,75 +211,75 @@
</transf>
</goal>
<goal name="fixpoint_is_max_proof.3" expl="3.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.05" steps="172"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="172"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_wf">
<transf name="split_goal_wp">
<goal name="tr_reach_wf.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="1.59"/></proof>
<proof prover="0"><result status="valid" time="1.59"/></proof>
</goal>
<goal name="tr_reach_wf.2" expl="2.">
<transf name="compute_specified">
<goal name="tr_reach_wf.2.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.20"/></proof>
<proof prover="0"><result status="valid" time="0.20"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_wf.3" expl="3.">
<transf name="compute_specified">
<goal name="tr_reach_wf.3.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.57"/></proof>
<proof prover="0"><result status="valid" time="0.57"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_wf.4" expl="4.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.06" steps="193"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="193"/></proof>
</goal>
<goal name="tr_reach_wf.5" expl="5.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="9"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="9"/></proof>
</goal>
<goal name="tr_reach_wf.6" expl="6.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="tr_reach_wf.7" expl="7.">
<transf name="compute_specified">
<goal name="tr_reach_wf.7.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.16"/></proof>
<proof prover="0"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_wf.8" expl="8.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="36"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="tr_reach_wf.9" expl="9.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.20" steps="855"/></proof>
<proof prover="4"><result status="valid" time="0.20" steps="855"/></proof>
</goal>
<goal name="tr_reach_wf.10" expl="10.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.08" steps="367"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="367"/></proof>
</goal>
<goal name="tr_reach_wf.11" expl="11.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="56"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
<goal name="tr_reach_wf.12" expl="12.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="42"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="tr_reach_wf.13" expl="13.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.06" steps="233"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="233"/></proof>
</goal>
<goal name="tr_reach_wf.14" expl="14.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="69"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="69"/></proof>
</goal>
<goal name="tr_reach_wf.15" expl="15.">
<transf name="compute_specified">
<goal name="tr_reach_wf.15.1" expl="1.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.55"/></proof>
<proof prover="0"><result status="valid" time="0.55"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_wf.16" expl="16.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.26" steps="790"/></proof>
<proof prover="4"><result status="valid" time="0.26" steps="790"/></proof>
</goal>
<goal name="tr_reach_wf.17" expl="17.">
<transf name="induction_pr">
......@@ -288,7 +288,7 @@
<goal name="tr_reach_wf.17.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_wf.17.1.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.54" steps="1041"/></proof>
<proof prover="4"><result status="valid" time="0.54" steps="1041"/></proof>
</goal>
</transf>
</goal>
......@@ -299,7 +299,7 @@
<goal name="tr_reach_wf.17.2.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_wf.17.2.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="25"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
</transf>
</goal>
......@@ -310,7 +310,7 @@
<goal name="tr_reach_wf.17.3.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_wf.17.3.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.31" steps="538"/></proof>
<proof prover="4"><result status="valid" time="0.31" steps="538"/></proof>
</goal>
</transf>
</goal>
......@@ -319,17 +319,17 @@
</transf>
</goal>
<goal name="tr_reach_wf.18" expl="18.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="2.20" steps="7678"/></proof>
<proof prover="4"><result status="valid" time="2.20" steps="7678"/></proof>
</goal>
<goal name="tr_reach_wf.19" expl="19.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="add_chain">
<transf name="split_goal_wp">
<goal name="add_chain.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.06" steps="367"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="367"/></proof>
</goal>
<goal name="add_chain.2" expl="2.">
<transf name="introduce_premises">
......@@ -338,10 +338,10 @@
<goal name="add_chain.2.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="add_chain.2.1.1.1" expl="1.">
<proof prover="2" steplimit="1" memlimit="1000"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="add_chain.2.1.1.2" expl="2.">
<proof prover="2" steplimit="1" memlimit="1000"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
......@@ -350,24 +350,24 @@
</transf>
</goal>
<goal name="add_chain.3" expl="3.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="123"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="123"/></proof>
</goal>
<goal name="add_chain.4" expl="4.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.07" steps="106"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="106"/></proof>
</goal>
</transf>
</goal>
<goal name="Iterates.tr_reach_separated">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.15"/></proof>
<proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="Iterates.tr_reach_maximum">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="17"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="17"/></proof>
</goal>
<goal name="Iterates.tr_reach_fixpoint">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="Iterates.tr_reach_compare">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="Iterates.tr_reach_transitive">
<transf name="prop_curry">
......@@ -376,21 +376,21 @@
<goal name="tr_reach_transitive.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_transitive.1.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="0"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_transitive.1.2" expl="2.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_transitive.1.2.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="tr_reach_transitive.1.3" expl="3.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="tr_reach_transitive.1.3.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
</transf>
</goal>
......@@ -399,7 +399,7 @@
</transf>
</goal>
<goal name="Iterates.tr_reach_wf">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="34"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
</theory>
<theory name="ChainExtensionCommon" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -408,60 +408,60 @@
</theory>
<theory name="ChainExtensionProof" sum="ced0c5789840022e774b8691ee27b536">
<goal name="extends_preserve_chains">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.03" steps="100"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="100"/></proof>
</goal>
<goal name="extends_preserve_wf_chains">
<transf name="split_goal_wp">
<goal name="extends_preserve_wf_chains.1" expl="1.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="53"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="53"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.2" expl="2.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.3" expl="3.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.4" expl="4.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.27" steps="624"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.27" steps="624"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.5" expl="5.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.26" steps="759"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.26" steps="759"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.6" expl="6.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.04" steps="11"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.04" steps="11"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.7" expl="7.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.8" expl="8.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.9" expl="9.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.10" expl="10.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="9"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="9"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.11" expl="11.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.12" expl="12.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="49"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="49"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.13" expl="13.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="30"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.14" expl="14.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.05" steps="190"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.05" steps="190"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.15" expl="15.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.16" expl="16.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="extends_preserve_wf_chains.17" expl="17.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.04" steps="17"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.04" steps="17"/></proof>
</goal>
</transf>
</goal>
......@@ -474,7 +474,7 @@
<goal name="reach_only_chains.1.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="reach_only_chains.1.1.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.04" steps="4"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="4"/></proof>
</goal>
</transf>
</goal>
......@@ -485,7 +485,7 @@
<goal name="reach_only_chains.1.2.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="reach_only_chains.1.2.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.05" steps="68"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="68"/></proof>
</goal>
</transf>
</goal>
......@@ -496,7 +496,7 @@
<goal name="reach_only_chains.1.3.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="reach_only_chains.1.3.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.07" steps="115"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="115"/></proof>
</goal>
</transf>
</goal>
......@@ -505,7 +505,7 @@
</transf>
</goal>
<goal name="reach_only_chains.2" expl="2.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
</transf>
</goal>
......@@ -518,7 +518,7 @@
<goal name="reach_only_wf_chains.1.1.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="reach_only_wf_chains.1.1.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.04" steps="4"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="4"/></proof>
</goal>
</transf>
</goal>
......@@ -529,7 +529,7 @@
<goal name="reach_only_wf_chains.1.2.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="reach_only_wf_chains.1.2.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.04" steps="34"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="34"/></proof>
</goal>
</transf>
</goal>
......@@ -540,7 +540,7 @@
<goal name="reach_only_wf_chains.1.3.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="reach_only_wf_chains.1.3.1.1" expl="1.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.07" steps="94"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="94"/></proof>
</goal>
</transf>
</goal>
......@@ -549,80 +549,80 @@
</transf>
</goal>
<goal name="reach_only_wf_chains.2" expl="2.">
<proof prover="4" steplimit="1" memlimit="1000"><result status="valid" time="0.04" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="15"/></proof>
</goal>
</transf>
</goal>
<goal name="reach_ch_interval">
<transf name="split_goal_wp">
<goal name="reach_ch_interval.1" expl="1.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.11" steps="437"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.11" steps="437"/></proof>
</goal>
<goal name="reach_ch_interval.2" expl="2.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="3.29" steps="4684"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="3.29" steps="4684"/></proof>
</goal>
<goal name="reach_ch_interval.3" expl="3.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.10" steps="244"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.10" steps="244"/></proof>
</goal>
<goal name="reach_ch_interval.4" expl="4.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.04" steps="18"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.04" steps="18"/></proof>
</goal>
<goal name="reach_ch_interval.5" expl="5.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="reach_ch_interval.6" expl="6.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="42"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="42"/></proof>
</goal>
<goal name="reach_ch_interval.7" expl="7.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="23"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
<goal name="reach_ch_interval.8" expl="8.">
<proof prover="0" steplimit="1" memlimit="1000"><result status="valid" time="0.39"/></proof>
<proof prover="0"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="reach_ch_interval.9" expl="9.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.04" steps="16"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.04" steps="16"/></proof>
</goal>
<goal name="reach_ch_interval.10" expl="10.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.53" steps="1170"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.53" steps="1170"/></proof>
</goal>
<goal name="reach_ch_interval.11" expl="11.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.65" steps="813"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.65" steps="813"/></proof>
</goal>
<goal name="reach_ch_interval.12" expl="12.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.34" steps="876"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.34" steps="876"/></proof>
</goal>
<goal name="reach_ch_interval.13" expl="13.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.31" steps="404"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.31" steps="404"/></proof>
</goal>
<goal name="reach_ch_interval.14" expl="14.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.03" steps="36"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.03" steps="36"/></proof>
</goal>
<goal name="reach_ch_interval.15" expl="15.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.04" steps="29"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="reach_ch_interval.16" expl="16.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="reach_ch_interval.17" expl="17.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="1.04" steps="782"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="1.04" steps="782"/></proof>
</goal>
<goal name="reach_ch_interval.18" expl="18.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.33" steps="683"/></proof>
<proof prover="4" steplimit="-1"><result status="valid" time="0.33" steps="683"/></proof>
</goal>
<goal name="reach_ch_interval.19" expl="19.">
<proof prover="4" steplimit="-1" memlimit="1000"><result status="valid" time="0.04" steps="33"/></proof>