Commit 2c0ebae6 authored by Andrei Paskevich's avatar Andrei Paskevich

update obsolete sessions

parent 4f8752a6
......@@ -3,103 +3,105 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" proved="true">
<theory name="BinarySort" proved="true">
<goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
<proof prover="0"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC binary_sort" expl="VC for binary_sort" proved="true">
<transf name="split_goal_right" proved="true" >
<transf name="split_vc" proved="true" >
<goal name="VC binary_sort.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC binary_sort.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_sort.2" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC binary_sort.3" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC binary_sort.4" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_sort.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_sort.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_sort.7" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC binary_sort.8" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="VC binary_sort.9" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="40"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC binary_sort.10" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC binary_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="22"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC binary_sort.12" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC binary_sort.13" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC binary_sort.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="22"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="25"/></proof>
</goal>
<goal name="VC binary_sort.15" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="21"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC binary_sort.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_sort.17" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC binary_sort.18" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC binary_sort.19" expl="assertion" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.50" steps="419"/></proof>
</goal>
<goal name="VC binary_sort.20" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC binary_sort.21" expl="loop invariant preservation" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC binary_sort.21.0" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(j=k)">
<goal name="VC binary_sort.21.0.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.50" steps="1019"/></proof>
<transf name="inline_goal" proved="true" >
<goal name="VC binary_sort.19.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC binary_sort.19.0.0" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="VC binary_sort.19.0.1" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="2.31" steps="1188"/></proof>
</goal>
<goal name="VC binary_sort.21.0.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.80" steps="689"/></proof>
<goal name="VC binary_sort.19.0.2" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC binary_sort.20" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
<goal name="VC binary_sort.21" expl="loop invariant preservation" proved="true">
<proof prover="8"><result status="valid" time="1.81" steps="1154"/></proof>
</goal>
<goal name="VC binary_sort.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="8"><result status="valid" time="0.03" steps="114"/></proof>
</goal>
<goal name="VC binary_sort.23" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC binary_sort.24" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="8"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC binary_sort.25" expl="out of loop bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="8"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
This diff is collapsed.
......@@ -3,8 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compare.mlw" proved="true">
<theory name="Compare" proved="true">
......@@ -14,7 +13,7 @@
<proof prover="5"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="VC wmpn_cmp.1" expl="loop invariant init" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="VC wmpn_cmp.2" expl="integer overflow" proved="true">
......@@ -27,7 +26,7 @@
<proof prover="5"><result status="valid" time="0.04" steps="46"/></proof>
</goal>
<goal name="VC wmpn_cmp.5" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="VC wmpn_cmp.6" expl="integer overflow" proved="true">
......@@ -40,11 +39,11 @@
<proof prover="5"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC wmpn_cmp.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="28"/></proof>
</goal>
<goal name="VC wmpn_cmp.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="VC wmpn_cmp.11" expl="precondition" proved="true">
......@@ -54,20 +53,20 @@
<proof prover="5"><result status="valid" time="0.04" steps="51"/></proof>
</goal>
<goal name="VC wmpn_cmp.13" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="23"/></proof>
</goal>
<goal name="VC wmpn_cmp.14" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="24"/></proof>
</goal>
<goal name="VC wmpn_cmp.15" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_cmp.16" expl="assertion" proved="true">
<transf name="inline_all" proved="true" >
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.16.0" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="19"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
</goal>
</transf>
</goal>
......@@ -82,22 +81,22 @@
</transf>
</goal>
<goal name="VC wmpn_cmp.18" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_cmp.19" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_cmp.20" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="26"/></proof>
</goal>
<goal name="VC wmpn_cmp.21" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_cmp.22" expl="assertion" proved="true">
<transf name="inline_all" proved="true" >
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.22.0" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.05" steps="20"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="37"/></proof>
</goal>
</transf>
</goal>
......@@ -112,17 +111,17 @@
</transf>
</goal>
<goal name="VC wmpn_cmp.24" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.23" steps="43"/></proof>
</goal>
<goal name="VC wmpn_cmp.25" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_cmp.26" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_cmp.27" expl="loop variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC wmpn_cmp.28" expl="loop invariant preservation" proved="true">
......@@ -135,7 +134,7 @@
<proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="VC wmpn_cmp.31" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_cmp.32" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.10" steps="37"/></proof>
......
This diff is collapsed.
......@@ -4,9 +4,8 @@
<why3session shape_version="4">
<prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../lemmas.mlw" proved="true">
<theory name="Lemmas" proved="true">
......@@ -98,7 +97,6 @@
<goal name="VC value_sub_frame_shift.4.0.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -185,7 +183,7 @@
<proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
</goal>
<goal name="VC value_zero.2" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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