Commit 4e33158c authored by MARCHE Claude's avatar MARCHE Claude

fix sessions

parent 758071c8
......@@ -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="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="3" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../edit_distance.mlw" proved="true">
......@@ -64,10 +64,10 @@
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="min_dist_equal.0.1.1" proved="true">
<proof prover="0"><result status="valid" time="1.63"/></proof>
<proof prover="3"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="min_dist_equal.0.1.2" proved="true">
<proof prover="0"><result status="valid" time="1.61"/></proof>
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="min_dist_equal.0.1.3" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="131"/></proof>
......@@ -79,7 +79,7 @@
</transf>
</goal>
<goal name="min_dist_diff" proved="true">
<proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="min_dist_eps" proved="true">
<transf name="inline_goal" proved="true" >
......@@ -125,7 +125,7 @@
</theory>
<theory name="EditDistance" proved="true">
<goal name="suffix_length" proved="true">
<proof prover="2" timelimit="5" memlimit="1000" edited="edit_distance_WP_EditDistance_suffix_length_1.v"><result status="valid" time="0.26"/></proof>
<proof prover="2" timelimit="5" memlimit="1000" edited="edit_distance_WP_EditDistance_suffix_length_1.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="VC distance" expl="VC for distance" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -145,10 +145,10 @@
<proof prover="10"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC distance.5" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC distance.6" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC distance.7" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......
......@@ -6,6 +6,7 @@
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="4000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.6.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../linked_list_rev.mlw" proved="true">
<theory name="InPlaceRev" proved="true">
......@@ -383,7 +384,8 @@
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC list_seg_no_repet.9" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="1.64"/></proof>
<proof prover="2" timelimit="10"><result status="valid" time="1.73"/></proof>
<proof prover="4"><result status="valid" time="7.98"/></proof>
</goal>
<goal name="VC list_seg_no_repet.10" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
......
......@@ -14,10 +14,8 @@
<prover id="9" name="Z3" version="3.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="10" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="13" name="CVC4" version="1.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="14" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="15" name="Alt-Ergo" version="1.00.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="16" name="veriT" version="201410" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="17" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="18" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -31,18 +29,16 @@
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="0.17"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.88"/></proof>
<proof prover="4"><result status="valid" time="1.16"/></proof>
<proof prover="5"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="timeout" time="2.00"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.48"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="valid" time="12.98" steps="969"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="valid" time="15.12" steps="969"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.50"/></proof>
<proof prover="15"><result status="timeout" time="1.00"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="1.17" steps="983"/></proof>
<proof prover="18"><result status="valid" time="1.41" steps="989"/></proof>
......@@ -59,19 +55,17 @@
<proof prover="5"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="timeout" time="2.00"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="timeout" time="2.00"/></proof>
<proof prover="15"><result status="unknown" time="1.33"/></proof>
<proof prover="14"><result status="timeout" time="1.00"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="unknown" time="0.57"/></proof>
<proof prover="18"><result status="unknown" time="0.66"/></proof>
<proof prover="19"><result status="timeout" time="2.00"/></proof>
<proof prover="20"><result status="timeout" time="2.00"/></proof>
<proof prover="19"><result status="timeout" time="1.00"/></proof>
<proof prover="20"><result status="timeout" time="1.00"/></proof>
<proof prover="21"><result status="unknown" time="0.07"/></proof>
</goal>
<goal name="G2" proved="true">
......@@ -83,16 +77,14 @@
<proof prover="5"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="timeout" time="2.00"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.62"/></proof>
<proof prover="10"><result status="valid" time="0.79"/></proof>
<proof prover="11"><result status="valid" time="7.72" steps="1007"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="valid" time="9.13" steps="1007"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.27"/></proof>
<proof prover="15"><result status="valid" time="1.82" steps="523"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="0.78" steps="1152"/></proof>
<proof prover="17"><result status="valid" time="0.96" steps="1152"/></proof>
<proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof>
<proof prover="19"><result status="valid" time="0.20"/></proof>
<proof prover="20"><result status="valid" time="0.18"/></proof>
......
......@@ -76,7 +76,6 @@
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC triplet.7" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="5.10"/></proof>
<proof prover="6"><result status="valid" time="4.82"/></proof>
<proof prover="7"><result status="timeout" time="5.00"/></proof>
<proof prover="8"><result status="timeout" time="5.00"/></proof>
......
......@@ -4,6 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.6.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -146,7 +147,7 @@
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC harness2" expl="VC for harness2" proved="true">
<proof prover="6"><result status="valid" time="1.43"/></proof>
<proof prover="2"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="VC test" expl="VC for test" proved="true">
<proof prover="6"><result status="valid" time="0.23"/></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