Commit 078a7e64 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

replay obsolete sessions

parent 7caecf0f
......@@ -7,7 +7,7 @@
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binomial_heap.mlw" expanded="true">
<theory name="BinomialHeap" sum="a4b20c3f0b661937cb05ebc19298c2ba" expanded="true">
<theory name="BinomialHeap" sum="29e615152758f1877eb6b8f1337e9f22" expanded="true">
<goal name="VC size_nonnneg" expl="VC for size_nonnneg">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="3d8c813c16bfe39e1ebc7795ba216b68">
<theory name="Test_proofinuse" sum="56dbf919cc4930dbaacdba6442726774">
<goal name="VC shift_is_div" expl="VC for shift_is_div">
<proof prover="1" timelimit="1"><result status="valid" time="0.11" steps="111"/></proof>
</goal>
......
......@@ -2,9 +2,10 @@
<!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="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="320a27ff6d5b9e231da1e9f9dee7818c" expanded="true">
<theory name="BraunHeaps" sum="d55c672dc562dbea343cabfcc2fc8ad9" expanded="true">
<goal name="VC le_root" expl="VC for le_root">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
......@@ -23,8 +24,8 @@
<goal name="VC extract" expl="VC for extract">
<proof prover="1"><result status="valid" time="0.97" steps="2514"/></proof>
</goal>
<goal name="VC replace_min" expl="VC for replace_min" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC replace_min" expl="VC for replace_min">
<transf name="split_goal_wp">
<goal name="VC replace_min.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="127"/></proof>
</goal>
......@@ -75,8 +76,8 @@
</goal>
</transf>
</goal>
<goal name="VC merge" expl="VC for merge" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC merge" expl="VC for merge">
<transf name="split_goal_wp">
<goal name="VC merge.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="53"/></proof>
</goal>
......@@ -134,27 +135,27 @@
<proof prover="1"><result status="valid" time="0.02" steps="144"/></proof>
</goal>
<goal name="VC size_height" expl="VC for size_height">
<proof prover="1"><result status="valid" time="0.12" steps="613"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.12" steps="613"/></proof>
</goal>
<goal name="VC inv_height" expl="VC for inv_height" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC inv_height" expl="VC for inv_height">
<transf name="split_goal_wp">
<goal name="VC inv_height.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.07" steps="260"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.07" steps="260"/></proof>
</goal>
<goal name="VC inv_height.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC inv_height.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC inv_height.4" expl="4. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="VC inv_height.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC inv_height.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="4.97" steps="860"/></proof>
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
......
......@@ -106,7 +106,7 @@
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerIntTest" sum="1abff7712bc37edc4cc97fd8c0c09795" expanded="true">
<theory name="PowerIntTest" sum="ea585215cae636c207832fffd3f1d4a7" expanded="true">
<goal name="Pow_2_2" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
......
......@@ -2,17 +2,19 @@
<!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="0" memlimit="1000"/>
<prover id="0" name="CVC3" version="2.4.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="5" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="2000"/>
<file name="../dyck.mlw" expanded="true">
<theory name="Dyck" sum="9d87ac2884462a57dcbb693d75da2f21">
<goal name="dyck_word_first">
<proof prover="3"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
</theory>
<theory name="Check" sum="8c6bb5950e463bd1819f22238b2cecc2" expanded="true">
<theory name="Check" sum="98025cff3e4290dc9214eee12a5f7650" expanded="true">
<goal name="VC same_prefix" expl="VC for same_prefix">
<proof prover="3"><result status="valid" time="0.02" steps="67"/></proof>
</goal>
......@@ -48,11 +50,12 @@
</transf>
</goal>
<goal name="VC is_dyck_rec.5" expl="5. exceptional postcondition" expanded="true">
<transf name="inline_all" expanded="true">
<goal name="VC is_dyck_rec.5.1" expl="1. exceptional postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
<proof prover="0"><result status="timeout" time="30.00"/></proof>
<proof prover="1" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="2" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="3" memlimit="2000"><result status="timeout" time="4.99"/></proof>
<proof prover="4"><result status="timeout" time="5.02"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC is_dyck_rec.6" expl="6. exceptional postcondition">
<transf name="inline_all">
......@@ -75,12 +78,9 @@
<goal name="VC is_dyck" expl="VC for is_dyck">
<transf name="split_goal_wp">
<goal name="VC is_dyck.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC is_dyck.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.72"/></proof>
</goal>
<goal name="VC is_dyck.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......
......@@ -394,7 +394,7 @@
<proof prover="1" timelimit="6"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="Solve" sum="8581e5f8c38bcb0738c0d9f28cafbb39" expanded="true">
<theory name="Solve" sum="7d630f88a5541a4c56d5f07af13ed4e3" expanded="true">
<goal name="VC f" expl="VC for f" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC f.1" expl="1. loop invariant init">
......@@ -444,7 +444,7 @@
<proof prover="4" timelimit="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC f.16" expl="16. loop invariant preservation" expanded="true">
<proof prover="2" timelimit="60"><result status="valid" time="14.54"/></proof>
<proof prover="2" timelimit="60"><result status="valid" time="10.04"/></proof>
<metas
expanded="true">
<ts_pos name="real" arity="0" id="real" ip_theory="BuiltIn">
......
......@@ -164,7 +164,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="FibonacciLogarithmic" sum="6997a4bbb411ae9d62554c252c4c4b21">
<theory name="FibonacciLogarithmic" sum="82f92a9ae937c6e26e61244170604014">
<goal name="VC m1110" expl="VC for m1110">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
......@@ -192,7 +192,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC logfib.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.29" steps="90"/></proof>
<proof prover="1"><result status="valid" time="0.29" steps="81"/></proof>
</goal>
</transf>
</goal>
......
......@@ -2,38 +2,47 @@
<!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" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw" expanded="true">
<theory name="McCarthy91" sum="d0ab9c573ee2fb06c1965f930c12cf9f" expanded="true">
<theory name="McCarthy91" sum="81c9febcdaa020d9d8678a39cb979ac8" expanded="true">
<goal name="VC f91" expl="VC for f91" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC f91.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="VC f91.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC f91.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC f91_nonrec.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="2. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.01" steps="255"/></proof>
<goal name="VC f91_nonrec.2" expl="2. loop variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
<goal name="VC f91_nonrec.3" expl="3. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="31"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<goal name="VC f91_nonrec.4" expl="4. loop variant decrease">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="5. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.14" steps="294"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="49"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -2,9 +2,10 @@
<!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="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../power.mlw" expanded="true">
<theory name="FastExponentiation" sum="839b2e44daa108b9b86aa21ef5a0e5a6" expanded="true">
<theory name="FastExponentiation" sum="a939f6c06f282e02fa2899bb24b48a88" expanded="true">
<goal name="VC fast_exp" expl="VC for fast_exp" expanded="true">
<proof prover="2"><result status="valid" time="0.18" steps="54"/></proof>
</goal>
......@@ -20,7 +21,7 @@
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC fast_exp_imperative.4" expl="4. assertion">
<proof prover="2"><result status="valid" time="0.04" steps="12"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fast_exp_imperative.5" expl="5. loop variant decrease">
<proof prover="2"><result status="valid" time="0.49" steps="11"/></proof>
......@@ -32,7 +33,7 @@
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC fast_exp_imperative.8" expl="8. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fast_exp_imperative.9" expl="9. loop variant decrease">
<proof prover="2"><result status="valid" time="0.26" steps="22"/></proof>
......
......@@ -8,7 +8,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../sum_of_digits.mlw" expanded="true">
<theory name="Euler290" sum="d988319e386fa68be71dd86a48252769" expanded="true">
<theory name="Euler290" sum="fea5102aaf2c7bdd7ee94a69b0aadcb3" expanded="true">
<goal name="Base">
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.01" steps="5"/></proof>
......@@ -32,7 +32,7 @@
</goal>
<goal name="VC f.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="2.70"/></proof>
<proof prover="2"><result status="valid" time="2.17" steps="310"/></proof>
<proof prover="2"><result status="valid" time="2.17" steps="304"/></proof>
</goal>
<goal name="VC f.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.02"/></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