Commit 579ea58c authored by MARCHE Claude's avatar MARCHE Claude

fix small bug in why3replay, updated sessions

parent 47852eec
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
......@@ -219,7 +219,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" proved="true" sum="b5bb23cfdbeddba673e2913aa853d26a">
<theory name="BitCounting32" proved="true" sum="d5ad1e97cb81202bd50a599e10f3e7ab">
<goal name="WP_parameter proof0" expl="VC for proof0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter proof0.0" expl="assertion" proved="true">
......@@ -235,12 +235,7 @@
<goal name="WP_parameter proof0.2" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter proof0.2.0" expl="VC for proof0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter proof0.2.0.0" expl="VC for proof0" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
<proof prover="7"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter proof0.2.1" expl="VC for proof0" proved="true">
<proof prover="1"><result status="valid" time="0.41" steps="348"/></proof>
......
......@@ -8,7 +8,7 @@
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../dijkstra.mlw" proved="true">
<theory name="DijkstraShortestPath" proved="true" sum="b4a2739dd87f01c10b91469adbe3aa50">
<theory name="DijkstraShortestPath" proved="true" sum="4d2b897a0ad84be2f910318d0c53a763">
<goal name="WP_parameter relax" expl="VC for relax" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
......@@ -28,16 +28,12 @@
<goal name="Path_shortest_path" proved="true">
<transf name="assert" proved="true" arg1="(forall sn. forall d. 0 &lt;= d &lt; sn -&gt; forall v. path src v d -&gt; exists d&apos;:int. shortest_path src v d&apos; /\ d&apos; &lt;= d)">
<goal name="Path_shortest_path.0" proved="true">
<transf name="intros" proved="true" arg1="sn">
<transf name="induction" proved="true" arg1="sn">
<goal name="Path_shortest_path.0.0" proved="true">
<transf name="induction" proved="true" arg1="sn" arg2="0">
<goal name="Path_shortest_path.0.0.0" proved="true">
<proof prover="1" timelimit="60"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Path_shortest_path.0.0.1" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Path_shortest_path.0.1" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
......@@ -140,48 +136,12 @@
<proof prover="1"><result status="valid" time="0.17" steps="495"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6" expl="VC for shortest_path_code" proved="true">
<transf name="introduce_premises" proved="true" >
<transf name="case" proved="true" arg1="(v = v1)">
<goal name="WP_parameter shortest_path_code.11.0.6.0" expl="VC for shortest_path_code" proved="true">
<transf name="destruct" proved="true" arg1="H22">
<goal name="WP_parameter shortest_path_code.11.0.6.0.0" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="57"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.0.1" expl="VC for shortest_path_code" proved="true">
<transf name="destruct" proved="true" arg1="H">
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.0" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1" expl="VC for shortest_path_code" proved="true">
<transf name="destruct" proved="true" arg1="H">
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.0" expl="VC for shortest_path_code" proved="true">
<transf name="destruct" proved="true" arg1="H23">
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.0.0" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.0.1" expl="VC for shortest_path_code" proved="true">
<transf name="destruct" proved="true" arg1="H12">
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.0.1.0" expl="VC for shortest_path_code" proved="true">
<transf name="case" proved="true" arg1="(v = v1)">
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.0.1.0.0" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="1.03" steps="1296"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.0.1.0.1" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.0.1.1.1" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.85" steps="1248"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
<proof prover="3"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.1" expl="VC for shortest_path_code" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
......@@ -208,71 +168,15 @@
<goal name="WP_parameter shortest_path_code.16.0.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(inv_succ src visited q d)">
<goal name="WP_parameter shortest_path_code.16.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(mem src visited)">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="instantiate" proved="true" arg1="inside_or_exit" arg2="visited">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="instantiate" proved="true" arg1="inside_or_exit" arg2="src">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="instantiate" proved="true" arg1="inside_or_exit" arg2="x">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="instantiate" proved="true" arg1="inside_or_exit" arg2="dx">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(mem x visited \/ (exists y:vertex. exists z: vertex. exists dy:int. mem y visited /\ not mem z visited /\ mem z (g_succ y) /\ path src y dy /\ ((dy + weight y z) &lt;= dx)))">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.1" expl="loop invariant preservation" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.1.0" expl="loop invariant preservation" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.1.0.0" expl="loop invariant preservation" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.1.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(mem z q)">
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.1.0.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.30" steps="405"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.0.1.0.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.20" steps="355"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.0.0.0.0.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="68"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="54"/></proof>
</goal>
</transf>
<proof prover="3"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.09" steps="268"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
......@@ -13,7 +13,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</theory>
<theory name="LinearProbing" proved="true" sum="b2532c89540c0e18d81a28c73edc3fbb">
<theory name="LinearProbing" proved="true" sum="4910a66acb99936519108ba8402e5c87">
<goal name="bucket_bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
......@@ -341,7 +341,7 @@
<goal name="WP_parameter resize.24.0.0" expl="type invariant" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter resize.24.0.0.0" expl="VC for resize" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -361,11 +361,11 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter resize.24.0.0.6" expl="VC for resize" proved="true">
<proof prover="0"><result status="valid" time="0.49" steps="204"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter resize.24.0.0.7" expl="VC for resize" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
<proof prover="0"><result status="valid" time="1.27" steps="296"/></proof>
<proof prover="2"><result status="valid" time="0.54"/></proof>
</goal>
</transf>
</goal>
......@@ -438,7 +438,7 @@
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="WP_parameter add.9.0.7" expl="VC for add" proved="true">
<proof prover="4"><result status="valid" time="0.94"/></proof>
<proof prover="4"><result status="valid" time="0.71"/></proof>
</goal>
</transf>
</goal>
......@@ -818,10 +818,10 @@
<proof prover="0"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="WP_parameter remove.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="22"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter remove.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="22"/></proof>
</goal>
<goal name="WP_parameter remove.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="22"/></proof>
......
This diff is collapsed.
......@@ -7,11 +7,11 @@
<prover id="2" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../triangle_inequality.why" proved="true">
<theory name="CauchySchwarzInequality" proved="true" sum="669d0ea7a951e32b06dc65d8dd012951">
<theory name="CauchySchwarzInequality" proved="true" sum="028eeb3c0da238696d03921fac93ef00">
<goal name="norm2_pos" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
......@@ -34,9 +34,21 @@
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="p_val_part" proved="true">
<transf name="unfold" proved="true" arg1="p" arg2="p_val_part">
<transf name="unfold" proved="true" arg1="p">
<goal name="p_val_part.0" proved="true">
<proof prover="5"><result status="valid" time="0.97" steps="15"/></proof>
<transf name="unfold" proved="true" arg1="norm2">
<goal name="p_val_part.0.0" proved="true">
<transf name="unfold" proved="true" arg1="dot">
<goal name="p_val_part.0.0.0" proved="true">
<transf name="unfold" proved="true" arg1="sqr">
<goal name="p_val_part.0.0.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.10" steps="4"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
......
This diff is collapsed.
This diff is collapsed.
......@@ -8,7 +8,7 @@
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../quicksort.mlw" proved="true">
<theory name="Quicksort" proved="true" sum="f6f86ab72796298cc25f1a200c614063">
<theory name="Quicksort" proved="true" sum="e2ce40232d6da5372b38a6a9ea72d93a">
<goal name="WP_parameter quick_rec" expl="VC for quick_rec" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter quick_rec.0" expl="index in array bounds" proved="true">
......@@ -221,7 +221,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</theory>
<theory name="Quicksort3way" proved="true" sum="90ad8db46f76e9d72e4041ca4ef72510">
<theory name="Quicksort3way" proved="true" sum="2e873de01db508cb089c0ce4ef6e9719">
<goal name="WP_parameter quick_rec" expl="VC for quick_rec" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter quick_rec.0" expl="index in array bounds" proved="true">
......
This diff is collapsed.
This diff is collapsed.
......@@ -9,7 +9,7 @@
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../vstte12_ring_buffer.mlw" proved="true">
<theory name="RingBuffer" proved="true" sum="25d98fd88e17781f4c7a96d403466e0c">
<theory name="RingBuffer" proved="true" sum="586116bfb760bb694b8273e1f1a8b69a">
<goal name="WP_parameter create" expl="VC for create" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
......
......@@ -363,7 +363,7 @@ let () =
exit 1
in
Debug.dprintf debug " done.@.";
if !opt_obsolete_only && not found_detached
if !opt_obsolete_only && not (found_detached || found_obs)
then
begin
eprintf "Session is not obsolete, hence not replayed@.";
......
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