Commit 7e515963 authored by MARCHE Claude's avatar MARCHE Claude

queens: fix session

parent df519f9c
......@@ -3,9 +3,9 @@
"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="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -89,7 +89,7 @@
<proof prover="6"><result status="valid" time="0.16" steps="504"/></proof>
</goal>
<goal name="VC t3.4.10" expl="VC for t3" proved="true">
<proof prover="6"><result status="valid" time="0.30" steps="352"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="352"/></proof>
</goal>
<goal name="VC t3.4.11" expl="VC for t3" proved="true">
<transf name="inline_goal" proved="true" >
......@@ -136,21 +136,24 @@
<goal name="VC t3.6.4" expl="VC for t3" proved="true">
<proof prover="10"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC t3.6.5" expl="VC for t3">
<proof prover="1" obsolete="true" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="unknown" time="0.00" steps="0"/></proof>
<goal name="VC t3.6.5" expl="VC for t3" proved="true">
<proof prover="4" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="1.37"/></proof>
</goal>
<goal name="VC t3.6.6" expl="VC for t3" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="VC t3.6.6.0" expl="VC for t3" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="VC t3.6.7" expl="VC for t3" proved="true">
<proof prover="0"><result status="valid" time="0.86"/></proof>
<goal name="VC t3.6.7" expl="VC for t3">
</goal>
<goal name="VC t3.6.8" expl="VC for t3" proved="true">
<proof prover="10"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC t3.6.9" expl="VC for t3" proved="true">
<proof prover="0"><result status="valid" time="3.20"/></proof>
<proof prover="0"><result status="valid" time="2.56"/></proof>
</goal>
<goal name="VC t3.6.10" expl="VC for t3" proved="true">
<proof prover="10"><result status="valid" time="0.87"/></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