Skip to content

GitLab

why3
why3
Commit 83265f53 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

Fix sessions

parent 22ab5177
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1583 additions and 1246 deletions
examples/multiprecision/add/why3session.xml
View file @ 83265f53
This diff is collapsed.
examples/multiprecision/div/why3session.xml
View file @ 83265f53
This diff is collapsed.
examples/multiprecision/sub/why3session.xml
View file @ 83265f53
This diff is collapsed.
examples/multiprecision/valuation/why3session.xml
View file @ 83265f53
......@@ -4,7 +4,7 @@
<why3session shape_version="5">
<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="2000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" 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="../valuation.mlw" proved="true">
......@@ -43,7 +43,7 @@
<goal name="VC valuation.6" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC valuation.6.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="1.78"/></proof>
<proof prover="0"><result status="valid" time="1.22"/></proof>
</goal>
<goal name="VC valuation.6.1" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -67,7 +67,7 @@
</transf>
</goal>
<goal name="power_ge_1" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.05"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="power_ge_1.0" proved="true">
<transf name="induction" proved="true" arg1="e">
......@@ -141,43 +141,43 @@
</transf>
</goal>
<goal name="VC valuation_monotonous" expl="VC for valuation_monotonous" proved="true">
<transf name="split_vc" proved="true" >
<transf name="split_goal_right" proved="true" >
<goal name="VC valuation_monotonous.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC valuation_monotonous.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC valuation_monotonous.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC valuation_monotonous.3" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC valuation_monotonous.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_monotonous.5" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC valuation_monotonous.6" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC valuation_monotonous.6.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="11"/></proof>
<transf name="split_goal_right" proved="true" >
<goal name="VC valuation_monotonous.6.0" expl="VC for valuation_monotonous" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC valuation_monotonous.6.1" expl="VC for valuation_monotonous" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC valuation_monotonous.6.2" expl="VC for valuation_monotonous" proved="true">
<proof prover="5"><result status="valid" time="0.12" steps="111"/></proof>
<proof prover="5" timelimit="1"><result status="valid" time="0.10" steps="111"/></proof>
</goal>
<goal name="VC valuation_monotonous.6.3" expl="VC for valuation_monotonous" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC valuation_monotonous.7" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="5" timelimit="1"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
</transf>
</goal>
......@@ -190,10 +190,10 @@
<goal name="VC valuation_times_nondiv" expl="VC for valuation_times_nondiv" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC valuation_times_nondiv.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.2" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></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