Skip to content

GitLab

why3
why3
Commit 1540521f authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

Fix a session

parent b874d942
Hide whitespace changes
Inline Side-by-side
Showing with 14 additions and 14 deletions
examples/multiprecision/sqrtrem/why3session.xml
View file @ 1540521f
......@@ -441,10 +441,10 @@
<goal name="VC wmpn_sqrtrem2.54.1" expl="VC for wmpn_sqrtrem2" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_strict_lr">
<goal name="VC wmpn_sqrtrem2.54.1.0" expl="apply premises" proved="true">
<proof prover="5"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem2.54.1.1" expl="apply premises" proved="true">
<proof prover="5"><result status="valid" time="0.13"/></proof>
<proof prover="5"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
......@@ -2172,10 +2172,10 @@
<goal name="VC wmpn_dc_sqrtrem.200.3" expl="VC for wmpn_dc_sqrtrem" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_lr">
<goal name="VC wmpn_dc_sqrtrem.200.3.0" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.61"/></proof>
<proof prover="6"><result status="valid" time="0.57"/></proof>
</goal>
<goal name="VC wmpn_dc_sqrtrem.200.3.1" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.57"/></proof>
<proof prover="6"><result status="valid" time="0.61"/></proof>
</goal>
</transf>
</goal>
......@@ -2536,10 +2536,10 @@
<goal name="VC wmpn_dc_sqrtrem.247.2" expl="VC for wmpn_dc_sqrtrem" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_lr">
<goal name="VC wmpn_dc_sqrtrem.247.2.0" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.28"/></proof>
<proof prover="6"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC wmpn_dc_sqrtrem.247.2.1" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.27"/></proof>
<proof prover="6"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
......@@ -2840,10 +2840,10 @@
<goal name="VC wmpn_dc_sqrtrem.286.2" expl="VC for wmpn_dc_sqrtrem" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_lr">
<goal name="VC wmpn_dc_sqrtrem.286.2.0" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.27"/></proof>
<proof prover="6"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC wmpn_dc_sqrtrem.286.2.1" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.30"/></proof>
<proof prover="6"><result status="valid" time="0.27"/></proof>
</goal>
</transf>
</goal>
......@@ -2975,10 +2975,10 @@
<goal name="VC sqrt_norm.1.3" expl="VC for sqrt_norm" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_lr">
<goal name="VC sqrt_norm.1.3.0" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="50"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="VC sqrt_norm.1.3.1" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="50"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
</transf>
</goal>
......@@ -3024,10 +3024,10 @@
<goal name="VC sqrt_norm.1.17" expl="VC for sqrt_norm" proved="true">
<transf name="apply" proved="true" arg1="prod_compat_lr">
<goal name="VC sqrt_norm.1.17.0" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.14"/></proof>
<proof prover="6"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC sqrt_norm.1.17.1" expl="apply premises" proved="true">
<proof prover="6"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
......@@ -3765,10 +3765,10 @@
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.156" expl="precondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="3.92"/></proof>
<proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.157" expl="precondition" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.30"/></proof>
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_sqrtrem.158" expl="division by zero" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.69"/></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