Update obsolete proofs

creusot-rs · Oct 23, 2023 · 45fced7 · 45fced7
1 parent 43baa33
commit 45fced7
Show file tree

Hide file tree

Showing 11 changed files with 177 additions and 175 deletions.
diff --git a/creusot/tests/should_succeed/bdd/why3session.xml b/creusot/tests/should_succeed/bdd/why3session.xml
diff --git a/creusot/tests/should_succeed/bdd/why3shapes.gz b/creusot/tests/should_succeed/bdd/why3shapes.gz
diff --git a/creusot/tests/should_succeed/constrained_types/why3shapes.gz b/creusot/tests/should_succeed/constrained_types/why3shapes.gz
diff --git a/creusot/tests/should_succeed/knapsack_full/why3session.xml b/creusot/tests/should_succeed/knapsack_full/why3session.xml
diff --git a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz
diff --git a/creusot/tests/should_succeed/slices/02_std/why3session.xml b/creusot/tests/should_succeed/slices/02_std/why3session.xml
@@ -9,29 +9,29 @@
  <goal name="binary_search&#39;vc" expl="VC for binary_search" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="binary_search&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.010000" steps="82"/></proof>
+  <proof prover="0"><result status="valid" time="0.010000" steps="79"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.017370" steps="20"/></proof>
+  <proof prover="0"><result status="valid" time="0.017370" steps="19"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.013155" steps="21"/></proof>
+  <proof prover="0"><result status="valid" time="0.013155" steps="20"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.3" expl="precondition" proved="true">
   <transf name="destruct_term" proved="true" arg1="_5">
    <goal name="binary_search&#39;vc.3.0" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.126562" steps="985"/></proof>
+   <proof prover="0"><result status="valid" time="0.126562" steps="982"/></proof>
    </goal>
    <goal name="binary_search&#39;vc.3.1" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.020800" steps="45"/></proof>
+   <proof prover="0"><result status="valid" time="0.020800" steps="44"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="binary_search&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.022953" steps="26"/></proof>
+  <proof prover="0"><result status="valid" time="0.022953" steps="25"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.010000" steps="27"/></proof>
+  <proof prover="0"><result status="valid" time="0.010000" steps="26"/></proof>
   </goal>
  </transf>
  </goal>

diff --git a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz
diff --git a/creusot/tests/should_succeed/sum/why3session.xml b/creusot/tests/should_succeed/sum/why3session.xml
@@ -4,14 +4,14 @@
 <why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="3" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
 <path name=".."/><path name="sum.mlcfg"/>
 <theory name="Sum_SumFirstN" proved="true">
  <goal name="sum_first_n&#39;vc" expl="VC for sum_first_n" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="sum_first_n&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.013914" steps="41513"/></proof>
+  <proof prover="2"><result status="valid" time="0.013914" steps="46455"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.1" expl="precondition" proved="true">
   <proof prover="0"><result status="valid" time="0.106520" steps="19"/></proof>
@@ -23,7 +23,7 @@
   <proof prover="0"><result status="valid" time="0.008401" steps="16"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.4" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.008354" steps="3858"/></proof>
+  <proof prover="2"><result status="valid" time="0.008354" steps="3858"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.5" expl="loop invariant init" proved="true">
   <proof prover="0"><result status="valid" time="0.008896" steps="37"/></proof>
@@ -32,10 +32,10 @@
   <proof prover="0"><result status="valid" time="0.014020" steps="215"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.7" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.007377" steps="102"/></proof>
+  <proof prover="0"><result status="valid" time="0.007377" steps="101"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.8" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="1.297002" steps="14357"/></proof>
+  <proof prover="0"><result status="valid" time="0.405841" steps="14361"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.9" expl="integer overflow" proved="true">
   <transf name="split_vc" proved="true" >
@@ -49,7 +49,7 @@
      <goal name="sum_first_n&#39;vc.9.0.0.1" expl="VC for sum_first_n" proved="true">
      <transf name="inline_goal" proved="true" >
       <goal name="sum_first_n&#39;vc.9.0.0.1.0" expl="VC for sum_first_n" proved="true">
-      <proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="2.985778" steps="2745056"/></proof>
+      <proof prover="2" timelimit="30" memlimit="4000"><result status="valid" time="0.251319" steps="1076869"/></proof>
       </goal>
      </transf>
      </goal>
@@ -63,15 +63,15 @@
   <proof prover="1"><result status="valid" time="0.108026" steps="11558"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.11" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.526379" steps="4693"/></proof>
+  <proof prover="0"><result status="valid" time="0.173264" steps="4705"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.12" expl="loop invariant preservation" proved="true">
   <transf name="assert" proved="true" arg1="(to_int i = length (inner produced))">
    <goal name="sum_first_n&#39;vc.12.0" expl="asserted formula" proved="true">
-   <proof prover="0"><result status="valid" time="0.100016" steps="1242"/></proof>
+   <proof prover="0"><result status="valid" time="0.100016" steps="1240"/></proof>
    </goal>
    <goal name="sum_first_n&#39;vc.12.1" expl="loop invariant preservation" proved="true">
-   <proof prover="0"><result status="valid" time="0.581701" steps="3556"/></proof>
+   <proof prover="0"><result status="valid" time="0.235500" steps="3565"/></proof>
    </goal>
   </transf>
   </goal>

diff --git a/creusot/tests/should_succeed/sum/why3shapes.gz b/creusot/tests/should_succeed/sum/why3shapes.gz
diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="1" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
@@ -14,31 +14,31 @@
   <proof prover="3"><result status="valid" time="0.155020" steps="11262"/></proof>
   </goal>
   <goal name="search&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.028733" steps="78009"/></proof>
+  <proof prover="0"><result status="valid" time="0.028733" steps="84507"/></proof>
   </goal>
   <goal name="search&#39;vc.2" expl="integer overflow" proved="true">
-  <proof prover="2"><result status="valid" time="0.009606" steps="24"/></proof>
+  <proof prover="2"><result status="valid" time="0.009606" steps="23"/></proof>
   </goal>
   <goal name="search&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.016841" steps="30"/></proof>
+  <proof prover="2"><result status="valid" time="0.016841" steps="29"/></proof>
   </goal>
   <goal name="search&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.019284" steps="78646"/></proof>
+  <proof prover="0"><result status="valid" time="0.019284" steps="85188"/></proof>
   </goal>
   <goal name="search&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.008654" steps="19"/></proof>
+  <proof prover="2"><result status="valid" time="0.008654" steps="18"/></proof>
   </goal>
   <goal name="search&#39;vc.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.035544" steps="6802"/></proof>
+  <proof prover="0"><result status="valid" time="0.035544" steps="6802"/></proof>
   </goal>
   <goal name="search&#39;vc.7" expl="loop invariant init" proved="true">
   <proof prover="2"><result status="valid" time="0.010443" steps="25"/></proof>
   </goal>
   <goal name="search&#39;vc.8" expl="loop invariant init" proved="true">
-  <proof prover="2"><result status="valid" time="0.010430" steps="48"/></proof>
+  <proof prover="2"><result status="valid" time="0.010430" steps="47"/></proof>
   </goal>
   <goal name="search&#39;vc.9" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.023052" steps="111688"/></proof>
+  <proof prover="0"><result status="valid" time="0.023052" steps="124542"/></proof>
   </goal>
   <goal name="search&#39;vc.10" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.030444" steps="52"/></proof>
@@ -47,13 +47,13 @@
   <proof prover="2"><result status="valid" time="0.008926" steps="56"/></proof>
   </goal>
   <goal name="search&#39;vc.12" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.019476" steps="117187"/></proof>
+  <proof prover="0"><result status="valid" time="0.019476" steps="130704"/></proof>
   </goal>
   <goal name="search&#39;vc.13" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.009955" steps="9225"/></proof>
+  <proof prover="0"><result status="valid" time="0.009955" steps="9225"/></proof>
   </goal>
   <goal name="search&#39;vc.14" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.086810" steps="81"/></proof>
+  <proof prover="2"><result status="valid" time="0.086810" steps="79"/></proof>
   </goal>
   <goal name="search&#39;vc.15" expl="loop invariant init" proved="true">
   <proof prover="2"><result status="valid" time="0.008849" steps="65"/></proof>
@@ -62,25 +62,25 @@
   <proof prover="2"><result status="valid" time="0.013109" steps="94"/></proof>
   </goal>
   <goal name="search&#39;vc.17" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.354446" steps="559499"/></proof>
+  <proof prover="0"><result status="valid" time="0.075230" steps="412578"/></proof>
   </goal>
   <goal name="search&#39;vc.18" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.024488" steps="120265"/></proof>
+  <proof prover="0"><result status="valid" time="0.024488" steps="134017"/></proof>
   </goal>
   <goal name="search&#39;vc.19" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.209528" steps="963"/></proof>
+  <proof prover="2"><result status="valid" time="0.055409" steps="967"/></proof>
   </goal>
   <goal name="search&#39;vc.20" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.020785" steps="131"/></proof>
   </goal>
   <goal name="search&#39;vc.21" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.018639" steps="133"/></proof>
+  <proof prover="2"><result status="valid" time="0.018639" steps="131"/></proof>
   </goal>
   <goal name="search&#39;vc.22" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.027655" steps="158666"/></proof>
+  <proof prover="0"><result status="valid" time="0.027655" steps="152896"/></proof>
   </goal>
   <goal name="search&#39;vc.23" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="1.075828" steps="1174393"/></proof>
+  <proof prover="0"><result status="valid" time="0.114528" steps="620054"/></proof>
   </goal>
   <goal name="search&#39;vc.24" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.009833" steps="142"/></proof>
@@ -92,28 +92,28 @@
   <proof prover="3"><result status="valid" time="0.191848" steps="18051"/></proof>
   </goal>
   <goal name="search&#39;vc.27" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="1.096586" steps="1383344"/></proof>
+  <proof prover="0"><result status="valid" time="0.119033" steps="624778"/></proof>
   </goal>
   <goal name="search&#39;vc.28" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.652882" steps="50295"/></proof>
+  <proof prover="3"><result status="valid" time="0.326537" steps="50293"/></proof>
   </goal>
   <goal name="search&#39;vc.29" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.029358" steps="131941"/></proof>
+  <proof prover="0"><result status="valid" time="0.029358" steps="146430"/></proof>
   </goal>
   <goal name="search&#39;vc.30" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.704137" steps="2678"/></proof>
+  <proof prover="2"><result status="valid" time="0.151645" steps="2638"/></proof>
   </goal>
   <goal name="search&#39;vc.31" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="1.259282" steps="7835"/></proof>
+  <proof prover="2"><result status="valid" time="0.329596" steps="7202"/></proof>
   </goal>
   <goal name="search&#39;vc.32" expl="postcondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.296736" steps="22306"/></proof>
+  <proof prover="3"><result status="valid" time="0.139861" steps="22306"/></proof>
   </goal>
   <goal name="search&#39;vc.33" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.524357" steps="621383"/></proof>
+  <proof prover="0"><result status="valid" time="0.083467" steps="447276"/></proof>
   </goal>
   <goal name="search&#39;vc.34" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.182961" steps="274286"/></proof>
+  <proof prover="0"><result status="valid" time="0.046369" steps="285721"/></proof>
   </goal>
  </transf>
  </goal>

diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz