ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

fix sessions

Browse Source
This commit is contained in:
Claude Marche
2021-06-25 10:26:57 +02:00
parent 00730321d1
commit 62d925e898
573 changed files with 7586 additions and 7547 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
examples/decrease1/why3session.xml
View File

@@ -22,31 +22,31 @@
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="search&#39;vc.3" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="search&#39;vc.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="search&#39;vc.5" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="search&#39;vc.6" expl="loop variant decrease" proved="true">
<goal name="search&#39;vc.5" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="search&#39;vc.6" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="search&#39;vc.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="search&#39;vc.8" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="11716"/></proof>
</goal>
<goal name="search&#39;vc.9" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="search&#39;vc.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="search&#39;vc.11" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="search&#39;vc.12" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
@@ -59,22 +59,22 @@
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="search_rec&#39;vc.1" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="search_rec&#39;vc.2" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="search_rec&#39;vc.3" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="search_rec&#39;vc.4" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="search_rec&#39;vc.5" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="search_rec&#39;vc.6" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="search_rec&#39;vc.7" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="22635"/></proof>

BIN
examples/decrease1/why3shapes.gz
View File

Binary file not shown.