ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity

Change the definition of Invariant on Multisets

Browse Source 
To workaround an imprecision in the detection of proof cycles.
This commit is contained in:
Claire Dross
2024-10-08 12:12:29 +02:00
parent 106bdfeecd
commit ec7a9e2ca2
64 changed files with 5065 additions and 4751 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
src/spark-containers-functional-multisets.adb
View File

@@ -521,7 +521,8 @@ is
---------------
function Invariant (Container : Map; Card : Big_Natural) return Boolean is
(Card = Cardinality_Rec (Container));
(if Length (Container) = 0 then Card = 0
else Card = Cardinality_Rec (Container));
--------------
-- Is_Empty --

14
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset/why3session.xml
View File

@@ -20,10 +20,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="26"/></proof>
<proof prover="1"><result status="valid" steps="1911"/></proof>
<proof prover="2"><result status="valid" steps="17399"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="782"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -38,10 +38,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2029"/></proof>
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="1011"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="108"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

926
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__Oeq/why3session.xml
View File

File diff suppressed because it is too large Load Diff

320
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__Ole/why3session.xml
View File

File diff suppressed because it is too large Load Diff

86
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__add/why3session.xml
View File

@@ -14,17 +14,17 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="4"/></proof>
<proof prover="1"><result status="valid" steps="1329"/></proof>
<proof prover="2"><result status="valid" steps="901"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1345"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1399"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1415"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -32,16 +32,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="2724"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2740"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2154"/></proof>
<proof prover="2"><result status="valid" steps="1743"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2170"/></proof>
<proof prover="2"><result status="valid" steps="1759"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -50,8 +50,8 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2571"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2587"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -62,10 +62,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2490"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid"/></proof>
<proof prover="2"><result status="valid" steps="1908"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -77,10 +77,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="2750"/></proof>
<proof prover="2"><result status="valid" steps="2253"/></proof>
<proof prover="4"><result status="valid" steps="649"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2766"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -89,10 +89,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="0"><result status="valid" steps="22"/></proof>
<proof prover="1"><result status="valid" steps="2661"/></proof>
<proof prover="2"><result status="valid" steps="2325"/></proof>
<proof prover="4"><result status="valid" steps="715"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2677"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.19" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -101,14 +101,14 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="0"><result status="valid" steps="25"/></proof>
<proof prover="1"><result status="valid" steps="3111"/></proof>
<proof prover="2"><result status="valid" steps="2625"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3127"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.22" proved="true">
<proof prover="0"><result status="valid" steps="25"/></proof>
<proof prover="1"><result status="valid" steps="2998"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3014"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -119,26 +119,26 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2745"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2761"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.26" proved="true">
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="3551"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3567"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3561"/></proof>
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="3577"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2714"/></proof>
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="2730"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>

138
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__add__2/why3session.xml
View File

@@ -29,17 +29,17 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="18"/></proof>
<proof prover="1"><result status="valid" steps="2191"/></proof>
<proof prover="2"><result status="valid" steps="2124"/></proof>
<proof prover="4"><result status="valid" steps="122"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2207"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2593"/></proof>
<proof prover="1"><result status="valid" steps="2609"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -47,53 +47,53 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="18"/></proof>
<proof prover="1"><result status="valid" steps="2260"/></proof>
<proof prover="2"><result status="valid" steps="2209"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2276"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="valid" steps="18"/></proof>
<proof prover="1"><result status="valid" steps="2726"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2742"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="valid" steps="144"/></proof>
<proof prover="1"><result status="valid" steps="5345"/></proof>
<proof prover="2"><result status="valid" steps="21070"/></proof>
<proof prover="4"><result status="unknown" steps="405"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5371"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="valid" steps="622"/></proof>
<proof prover="1"><result status="valid" steps="41487"/></proof>
<proof prover="2"><result status="valid" steps="29319"/></proof>
<proof prover="4"><result status="unknown" steps="478"/></proof>
<proof prover="0"><result status="valid" steps="627"/></proof>
<proof prover="1"><result status="valid" steps="43602"/></proof>
<proof prover="2"><result status="valid" steps="32159"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="valid" steps="22"/></proof>
<proof prover="1"><result status="valid" steps="3058"/></proof>
<proof prover="2"><result status="valid" steps="2797"/></proof>
<proof prover="1"><result status="valid" steps="3074"/></proof>
<proof prover="2"><result status="valid" steps="2821"/></proof>
<proof prover="4"><result status="valid" steps="305"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="valid" steps="18"/></proof>
<proof prover="1"><result status="valid" steps="2195"/></proof>
<proof prover="2"><result status="valid" steps="2134"/></proof>
<proof prover="4"><result status="valid" steps="122"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2211"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2273"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2289"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="21101"/></proof>
<proof prover="0"><result status="valid" steps="325"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -107,31 +107,31 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="0"><result status="valid" steps="51"/></proof>
<proof prover="1"><result status="valid" steps="3491"/></proof>
<proof prover="2"><result status="valid" steps="30245"/></proof>
<proof prover="4"><result status="valid" steps="1432"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3507"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.22" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.23" proved="true">
<proof prover="0"><result status="valid" steps="780"/></proof>
<proof prover="1"><result status="valid" steps="5662"/></proof>
<proof prover="2"><result status="valid" steps="33899"/></proof>
<proof prover="4"><result status="unknown" steps="1985"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5711"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.24" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="6268"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="8356"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2262"/></proof>
<proof prover="2"><result status="valid" steps="3510"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2278"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.26" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -140,10 +140,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="3482"/></proof>
<proof prover="2"><result status="valid" steps="3568"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3498"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.29" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -153,9 +153,9 @@
</goal>
<goal name="def&#39;vc.31" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="3474"/></proof>
<proof prover="2"><result status="valid" steps="3661"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="3677"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.32" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -167,8 +167,8 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.35" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3746"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3762"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -180,9 +180,9 @@
</goal>
<goal name="def&#39;vc.38" proved="true">
<proof prover="0"><result status="valid" steps="40"/></proof>
<proof prover="1"><result status="valid" steps="3645"/></proof>
<proof prover="2"><result status="valid" steps="4110"/></proof>
<proof prover="4"><result status="valid" steps="2284"/></proof>
<proof prover="1"><result status="valid" steps="3661"/></proof>
<proof prover="2"><result status="valid" steps="4126"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.39" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -191,14 +191,14 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.41" proved="true">
<proof prover="0"><result status="valid" steps="56"/></proof>
<proof prover="1"><result status="valid" steps="4107"/></proof>
<proof prover="2"><result status="valid" steps="4424"/></proof>
<proof prover="4"><result status="valid" steps="4492"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="4123"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.42" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3994"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4010"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -209,28 +209,28 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.45" proved="true">
<proof prover="0"><result status="valid" steps="1650"/></proof>
<proof prover="1"><result status="valid" steps="8032"/></proof>
<proof prover="0"><result status="valid" steps="1638"/></proof>
<proof prover="1"><result status="valid" steps="8273"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.46" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="6246"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="6487"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.47" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="8788"/></proof>
<proof prover="1"><result status="valid" steps="9007"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.48" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="76853"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="31256"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
</transf>
</goal>

76
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__aggr_include/why3session.xml
View File

@@ -17,8 +17,8 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1291"/></proof>
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1307"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -38,17 +38,17 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2064"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2080"/></proof>
<proof prover="2"><result status="valid" steps="3365"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1812"/></proof>
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="1828"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -57,18 +57,18 @@
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="valid" steps="15"/></proof>
<proof prover="1"><result status="valid" steps="3204"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3220"/></proof>
<proof prover="2"><result status="valid" steps="20808"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2154"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2170"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="2"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -77,18 +77,18 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2646"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2662"/></proof>
<proof prover="2"><result status="valid" steps="2115"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2874"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2890"/></proof>
<proof prover="2"><result status="valid" steps="2228"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.19" proved="true">
@@ -98,8 +98,8 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2892"/></proof>
<proof prover="0"><result status="valid" steps="30"/></proof>
<proof prover="1"><result status="valid" steps="2908"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -113,8 +113,8 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2946"/></proof>
<proof prover="0"><result status="valid" steps="26"/></proof>
<proof prover="1"><result status="valid" steps="2962"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -122,9 +122,9 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2929"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2945"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
@@ -134,10 +134,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.30" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3019"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="35"/></proof>
<proof prover="1"><result status="valid" steps="3035"/></proof>
<proof prover="2"><result status="valid" steps="2656"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.31" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -153,14 +153,14 @@
</goal>
<goal name="def&#39;vc.35" proved="true">
<proof prover="0"><result status="valid" steps="18"/></proof>
<proof prover="1"><result status="valid" steps="5375"/></proof>
<proof prover="2"><result status="valid" steps="28709"/></proof>
<proof prover="1"><result status="valid" steps="5391"/></proof>
<proof prover="2"><result status="valid" steps="28932"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.36" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="7634"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7808"/></proof>
<proof prover="2"><result status="valid" steps="29621"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.37" proved="true">
@@ -168,8 +168,8 @@
</goal>
<goal name="def&#39;vc.38" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7491"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7703"/></proof>
<proof prover="2"><result status="valid" steps="28921"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.39" proved="true">

14
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__cardinality/why3session.xml
View File

@@ -15,8 +15,8 @@
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="1"><result status="valid" steps="1431"/></proof>
<proof prover="2"><result status="valid" steps="911"/></proof>
<proof prover="1"><result status="valid" steps="1447"/></proof>
<proof prover="2"><result status="valid" steps="927"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
@@ -24,8 +24,8 @@
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="8"/></proof>
<proof prover="1"><result status="valid" steps="1754"/></proof>
<proof prover="2"><result status="valid" steps="1189"/></proof>
<proof prover="1"><result status="valid" steps="1770"/></proof>
<proof prover="2"><result status="valid" steps="1205"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
@@ -41,9 +41,9 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="47"/></proof>
<proof prover="1"><result status="valid" steps="3103"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3240"/></proof>
<proof prover="2"><result status="unknown" steps="16000"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>

44
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__cardinality_rec/why3session.xml
View File

@@ -17,10 +17,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="98"/></proof>
<proof prover="2"><result status="valid" steps="73"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="15"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -32,31 +32,31 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="2"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="98"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="100"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="574"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="2962"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="523"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="7"/></proof>
<proof prover="1"><result status="valid" steps="1386"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="2690"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -65,25 +65,25 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1693"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1394"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="900"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1727"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -92,7 +92,7 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="69"/></proof>
<proof prover="1"><result status="valid" steps="1370"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
@@ -109,8 +109,8 @@
<goal name="def&#39;vc.22" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4552"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

20
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__choose/why3session.xml
View File

@@ -15,8 +15,8 @@
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1291"/></proof>
<proof prover="2"><result status="valid" steps="906"/></proof>
<proof prover="1"><result status="valid"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
@@ -26,15 +26,15 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="valid" steps="35"/></proof>
<proof prover="1"><result status="valid" steps="4964"/></proof>
<proof prover="2"><result status="valid" steps="13136"/></proof>
<proof prover="0"><result status="valid" steps="22"/></proof>
<proof prover="1"><result status="valid" steps="4021"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="1"><result status="valid" steps="2174"/></proof>
<proof prover="2"><result status="valid" steps="1426"/></proof>
<proof prover="1"><result status="valid" steps="2190"/></proof>
<proof prover="2"><result status="valid" steps="1442"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
@@ -44,9 +44,9 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="92"/></proof>
<proof prover="1"><result status="valid" steps="5340"/></proof>
<proof prover="2"><result status="valid" steps="14392"/></proof>
<proof prover="0"><result status="valid" steps="103"/></proof>
<proof prover="1"><result status="valid" steps="5434"/></proof>
<proof prover="2"><result status="valid" steps="14599"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>

30
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__contains/why3session.xml
View File

@@ -21,9 +21,9 @@
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="4"/></proof>
<proof prover="1"><result status="valid" steps="1437"/></proof>
<proof prover="2"><result status="valid" steps="917"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1453"/></proof>
<proof prover="2"><result status="valid" steps="933"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -35,22 +35,22 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="valid" steps="59"/></proof>
<proof prover="1"><result status="valid" steps="3061"/></proof>
<proof prover="2"><result status="valid" steps="11765"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3125"/></proof>
<proof prover="2"><result status="valid" steps="11972"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1872"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="53"/></proof>
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="1888"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="1872"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1888"/></proof>
<proof prover="2"><result status="valid" steps="1593"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
</transf>
</goal>

4
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__default_count/why3session.xml
View File

@@ -14,9 +14,9 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="10"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="10"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">

512
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__difference/why3session.xml
View File

File diff suppressed because it is too large Load Diff

22
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__element/why3session.xml
View File

@@ -14,8 +14,8 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="8"/></proof>
<proof prover="1"><result status="valid" steps="1453"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1469"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -26,27 +26,27 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2174"/></proof>
<proof prover="0"><result status="valid" steps="10"/></proof>
<proof prover="1"><result status="valid" steps="2190"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2182"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2198"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="93"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2404"/></proof>
<proof prover="1"><result status="valid" steps="2420"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="valid" steps="10"/></proof>
<proof prover="1"><result status="valid" steps="2418"/></proof>
<proof prover="2"><result status="valid" steps="1687"/></proof>
<proof prover="1"><result status="valid" steps="2434"/></proof>
<proof prover="2"><result status="valid" steps="1703"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
@@ -54,7 +54,7 @@
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2262"/></proof>
<proof prover="1"><result status="valid" steps="2278"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>

28
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__empty_multiset/why3session.xml
View File

@@ -16,23 +16,23 @@
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="10"/></proof>
<proof prover="2"><result status="valid" steps="10"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="1"><result status="valid" steps="1771"/></proof>
<proof prover="2"><result status="valid" steps="11437"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="15"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1291"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="0"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1307"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -41,10 +41,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="valid" steps="27"/></proof>
<proof prover="1"><result status="valid" steps="3794"/></proof>
<proof prover="2"><result status="valid" steps="14034"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3820"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
</transf>
</goal>

6
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__eq_elements_checks__eq_reflexive/why3session.xml
View File

@@ -23,10 +23,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="327"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="10"/></proof>
</goal>
</transf>
</goal>

6
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__eq_elements_checks__eq_symmetric/why3session.xml
View File

@@ -29,10 +29,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="4"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="473"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="20"/></proof>
</goal>
</transf>
</goal>

4
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__eq_elements_checks__eq_transitive/why3session.xml
View File

@@ -32,9 +32,9 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="valid" steps="7"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="593"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="1997"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
</transf>

196
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__equal_except/why3session.xml
View File

@@ -20,8 +20,8 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2047"/></proof>
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="2063"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -30,9 +30,9 @@
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2589"/></proof>
<proof prover="2"><result status="valid" steps="1725"/></proof>
<proof prover="4"><result status="valid" steps="465"/></proof>
<proof prover="1"><result status="valid" steps="2605"/></proof>
<proof prover="2"><result status="valid" steps="1741"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -41,10 +41,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2441"/></proof>
<proof prover="2"><result status="valid" steps="1787"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2457"/></proof>
<proof prover="2"><result status="valid" steps="1803"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -56,112 +56,121 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="valid" steps="22"/></proof>
<proof prover="1"><result status="valid" steps="2373"/></proof>
<proof prover="2"><result status="valid" steps="1796"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="45"/></proof>
<proof prover="1"><result status="valid" steps="3327"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2623"/></proof>
<proof prover="0"><result status="valid" steps="57"/></proof>
<proof prover="1"><result status="valid" steps="3298"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="valid" steps="30"/></proof>
<proof prover="1"><result status="valid" steps="4433"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="45"/></proof>
<proof prover="1"><result status="valid" steps="3327"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3298"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="2641"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4481"/></proof>
<proof prover="2"><result status="valid" steps="20763"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2486"/></proof>
<proof prover="2"><result status="valid" steps="1938"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="2657"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.19" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2502"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="523"/></proof>
</goal>
<goal name="def&#39;vc.20" proved="true">
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2576"/></proof>
<proof prover="2"><result status="valid" steps="1998"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.22" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2592"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.23" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.24" proved="true">
<proof prover="0"><result status="valid" steps="24"/></proof>
<proof prover="1"><result status="valid" steps="2512"/></proof>
<proof prover="2"><result status="valid" steps="2013"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2512"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.26" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="4711"/></proof>
<proof prover="0"><result status="valid" steps="53"/></proof>
<proof prover="1"><result status="valid" steps="3616"/></proof>
<proof prover="2"><result status="valid" steps="21723"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="0"><result status="valid" steps="69"/></proof>
<proof prover="1"><result status="valid" steps="3571"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2559"/></proof>
<proof prover="2"><result status="valid" steps="2064"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="53"/></proof>
<proof prover="1"><result status="valid" steps="3616"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.29" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3571"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.30" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2729"/></proof>
<proof prover="2"><result status="valid" steps="2167"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4759"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.31" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.32" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2575"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.33" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2780"/></proof>
<proof prover="2"><result status="valid" steps="2227"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.34" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2745"/></proof>
<proof prover="2"><result status="valid" steps="2183"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.35" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -170,34 +179,34 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.37" proved="true">
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2676"/></proof>
<proof prover="2"><result status="valid" steps="2271"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2796"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.38" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.39" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2781"/></proof>
<proof prover="2"><result status="valid" steps="2372"/></proof>
<proof prover="4"><result status="valid" steps="601"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.40" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.41" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2692"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.42" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2871"/></proof>
<proof prover="2"><result status="valid" steps="2432"/></proof>
<proof prover="4"><result status="valid" steps="672"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.43" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2797"/></proof>
<proof prover="2"><result status="valid" steps="2388"/></proof>
<proof prover="4"><result status="valid" steps="601"/></proof>
</goal>
<goal name="def&#39;vc.44" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -206,32 +215,47 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.46" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="1"><result status="valid" steps="2887"/></proof>
<proof prover="2"><result status="valid" steps="2448"/></proof>
<proof prover="4"><result status="valid" steps="672"/></proof>
</goal>
<goal name="def&#39;vc.47" proved="true">
<proof prover="0"><result status="valid" steps="89"/></proof>
<proof prover="1"><result status="valid" steps="4896"/></proof>
<proof prover="2"><result status="valid" steps="22743"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.48" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.49" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4881"/></proof>
<proof prover="2"><result status="valid" steps="22743"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.50" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.51" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="3537"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4944"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.52" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.53" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4929"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.54" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.55" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3553"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="608"/></proof>
</goal>
</transf>
</goal>
</theory>

40
tests/V818-010__functional_multiset_proof/proof/sessions/my_multiset__first/why3session.xml
View File

@@ -17,14 +17,14 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1725"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1741"/></proof>
<proof prover="2"><result status="valid" steps="4684"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="4"/></proof>
<proof prover="1"><result status="valid" steps="1645"/></proof>
<proof prover="1"><result status="valid" steps="1661"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -32,14 +32,14 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1715"/></proof>
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="1"><result status="valid" steps="1731"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="1"><result status="valid" steps="1719"/></proof>
<proof prover="1"><result status="valid" steps="1735"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
@@ -47,16 +47,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1761"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="10"/></proof>
<proof prover="1"><result status="valid" steps="1777"/></proof>
<proof prover="2"><result status="valid" steps="1400"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1765"/></proof>
<proof prover="2"><result status="valid" steps="1411"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="10"/></proof>
<proof prover="1"><result status="valid" steps="1781"/></proof>
<proof prover="2"><result status="valid" steps="1427"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -66,14 +66,14 @@
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2151"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2167"/></proof>
<proof prover="2"><result status="valid" steps="12554"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="5816"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5832"/></proof>
<proof prover="2"><result status="valid" steps="19305"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
</transf>

Some files were not shown because too many files have changed in this diff Show More