Skip to content
Snippets Groups Projects
Commit adc66fc1 authored by François Bobot's avatar François Bobot
Browse files

[replay] use alt-ergo 1.30 instead of alt-ergo 2.2.0

parent b5b2add1
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
examples/mccarthy/why3session.xml
+ 9
− 9
View file @ adc66fc1
......@@ -38,31 +38,31 @@
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC f91_nonrec.0" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC f91_nonrec.1" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="26"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="26"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="32"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="32"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="200"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="200"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="100"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="100"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="34"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="34"/></proof>
</goal>
<goal name="VC f91_nonrec.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="274"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="274"/></proof>
</goal>
<goal name="VC f91_nonrec.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
</transf>
</goal>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment