Commit 1b5d6ac5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update sessions tests-provers

parent 8eef974b
This diff is collapsed.
......@@ -2,248 +2,226 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.5.0" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ieee_float.mlw" expanded="true">
<theory name="A" sum="48c8d108a86ab8b4c79ec7491cfe6354" expanded="true">
<goal name="ebsb32" expanded="true">
<theory name="A" sum="48c8d108a86ab8b4c79ec7491cfe6354">
<goal name="ebsb32">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ebsb64" expanded="true">
<goal name="ebsb64">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="78"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="a" expanded="true">
<goal name="a">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="82"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="M603_018" sum="44b31db83ce2d23dd4c2cbdb77947371" expanded="true">
<goal name="VC triplet" expl="VC for triplet">
<transf name="split_goal_wp">
<goal name="VC triplet" expl="VC for triplet" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC triplet.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="1.05"/></proof>
<proof prover="4"><result status="valid" time="2.65"/></proof>
<proof prover="4"><result status="valid" time="4.39"/></proof>
</goal>
<goal name="VC triplet.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="4.95" steps="10733"/></proof>
<proof prover="3"><result status="valid" time="1.86"/></proof>
<proof prover="4"><result status="valid" time="0.79"/></proof>
<proof prover="2"><result status="valid" time="5.97" steps="10733"/></proof>
<proof prover="4"><result status="valid" time="1.02"/></proof>
<proof prover="7"><result status="valid" time="0.97"/></proof>
</goal>
<goal name="VC triplet.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.21"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="161"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.22"/></proof>
<proof prover="6"><result status="valid" time="0.82"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC triplet.4" expl="4. assertion">
<proof prover="0"><result status="outofmemory" time="4.61"/></proof>
<goal name="VC triplet.4" expl="4. assertion" expanded="true">
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="outofmemory" time="6.39"/></proof>
<proof prover="7"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC triplet.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.29"/></proof>
<proof prover="2"><result status="valid" time="1.13" steps="2244"/></proof>
<proof prover="3"><result status="valid" time="0.62"/></proof>
<proof prover="5"><result status="valid" time="0.30"/></proof>
<proof prover="5"><result status="valid" time="0.44"/></proof>
<proof prover="6"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="VC triplet.6" expl="6. assertion">
<proof prover="3"><result status="valid" time="2.34"/></proof>
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="8.23" steps="20126"/></proof>
</goal>
<goal name="VC triplet.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="184"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.29"/></proof>
<proof prover="5"><result status="valid" time="0.42"/></proof>
<proof prover="6"><result status="valid" time="0.88"/></proof>
<proof prover="7"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC triplet.8" expl="8. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="7"><result status="valid" time="4.38"/></proof>
</goal>
<goal name="VC triplet.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="94"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.15"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC triplet.10" expl="10. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="7"><result status="valid" time="3.91"/></proof>
</goal>
</transf>
</goal>
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.14"/></proof>
<goal name="G1">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="74"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.14"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="3.34"/></proof>
<goal name="G2">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.24" steps="560"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.08"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="G3">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G4" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="G4">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5" expanded="true">
<proof prover="0"><result status="valid" time="0.14"/></proof>
<goal name="G5">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="74"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.14"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G6" expanded="true">
<proof prover="0"><result status="valid" time="3.31"/></proof>
<goal name="G6">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.12" steps="286"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G7" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="G7">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G8" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="G8">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G9" expanded="true">
<goal name="G9">
<proof prover="2"><result status="valid" time="1.04" steps="2136"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G10" expanded="true">
<goal name="G10">
<proof prover="2"><result status="valid" time="2.36" steps="4829"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="M121_039_nonlinear" sum="c02f213417aeb7b1be2861bd7a5eb39f" expanded="true">
<goal name="VC test" expl="VC for test" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC test.1" expl="1. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<goal name="VC test.1" expl="1. assertion" expanded="true">
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="unknown" time="5.00"/></proof>
<proof prover="6"><result status="timeout" time="5.00"/></proof>
<proof prover="7"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC test.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC test.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC test.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC test.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.15"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="88"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.15"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC test.6" expl="6. assertion" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="valid" time="0.58"/></proof>
<goal name="VC test.6" expl="6. assertion">
<proof prover="7"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="VC test.7" expl="7. assertion" expanded="true">
<proof prover="0"><result status="outofmemory" time="4.57"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="outofmemory" time="4.57"/></proof>
<proof prover="7"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC test.8" expl="8. assertion" expanded="true">
<proof prover="0"><result status="outofmemory" time="4.43"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="outofmemory" time="6.65"/></proof>
<proof prover="7"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC test.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="91"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC test.10" expl="10. assertion">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="valid" time="0.17"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.19"/></proof>
<proof prover="7"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC test.11" expl="11. postcondition">
<proof prover="0"><result status="outofmemory" time="4.39"/></proof>
<proof prover="1"><result status="unknown" time="9.88"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="valid" time="4.32"/></proof>
<proof prover="5"><result status="unknown" time="9.84"/></proof>
<proof prover="7"><result status="valid" time="0.74"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="LB09_025_conversion" sum="e37934a097957d67aab9959d430b17b3" expanded="true">
<theory name="LB09_025_conversion" sum="8212d7d314945879bf55ee660ae056e6" expanded="true">
<goal name="VC fti" expl="VC for fti" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC fti.1" expl="1. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="unknown" time="5.00"/></proof>
<proof prover="6"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC fti.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="unknown" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="5"><result status="unknown" time="5.00"/></proof>
<proof prover="6"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="VC fti.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="73"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......
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