Commit d8172077 authored by MARCHE Claude's avatar MARCHE Claude

update sessions

parent 673b1c10
......@@ -2,51 +2,50 @@
<!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="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../gcd_bezout.mlw" proved="true">
<theory name="GcdBezout" proved="true">
<goal name="VC gcd" expl="VC for gcd" proved="true">
<transf name="split_goal_right" proved="true" >
<transf name="split_vc" proved="true" >
<goal name="VC gcd.0" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.1" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.3" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.4" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC gcd.6" expl="loop variant decrease" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC gcd.7" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="38"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC gcd.8" expl="loop invariant preservation" proved="true">
<proof prover="0"><undone/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC gcd.9" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.10" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="1.51" steps="64"/></proof>
<proof prover="2"><result status="valid" time="0.21" steps="36"/></proof>
</goal>
<goal name="VC gcd.11" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC gcd.12" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -3,28 +3,28 @@
"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="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../cvc3.why">
<theory name="Test">
<goal name="test1">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="unknown" time="0.36"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="0.01"/></proof>
<proof prover="7"><result status="unknown" time="0.03"/></proof>
</goal>
<goal name="test2">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="0.01"/></proof>
<proof prover="7"><result status="unknown" time="0.19"/></proof>
</goal>
<goal name="test3" proved="true">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -5,8 +5,8 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="12" name="Eprover" version="1.8-001" timelimit="2" steplimit="0" memlimit="1000"/>
......@@ -16,8 +16,8 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -25,8 +25,8 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -34,32 +34,32 @@
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="10"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="smoke1">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="unknown" time="0.02"/></proof>
<proof prover="11"><result status="unknown" time="0.16"/></proof>
</goal>
<goal name="smoke3">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="unknown" time="0.01"/></proof>
<proof prover="11"><result status="unknown" time="0.17"/></proof>
</goal>
<goal name="smoke5">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="unknown" time="0.01"/></proof>
<proof prover="11"><result status="unknown" time="0.15"/></proof>
<proof prover="12"><result status="timeout" time="2.00"/></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