fix sessions broken by change in generalize transformation

examples/multiprecision/div/why3session.xml

@@ -1146,7 +1146,7 @@
    <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.71.8" expl="VC for wmpn_divrem_1" proved="true">
-   <proof prover="0"><result status="valid" time="2.65"/></proof>
+   <proof prover="0"><result status="valid" time="2.19"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.71.9" expl="VC for wmpn_divrem_1" proved="true">
    <proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -1474,7 +1474,7 @@
    <proof prover="2"><result status="valid" time="0.13"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.38" expl="VC for div3by2_inv" proved="true">
-   <proof prover="0"><result status="valid" time="4.07"/></proof>
+   <proof prover="0"><result status="valid" time="3.50"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.39" expl="VC for div3by2_inv" proved="true">
    <proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -2808,12 +2808,10 @@
   <proof prover="5"><result status="valid" time="0.02" steps="78"/></proof>
   </goal>
   <goal name="VC submul_limb.2" expl="loop invariant init" proved="true">
-  <transf name="split_goal_right" proved="true" >
-  </transf>
+  <proof prover="9"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC submul_limb.3" expl="loop invariant init" proved="true">
-  <transf name="split_goal_right" proved="true" >
-  </transf>
+  <proof prover="9"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC submul_limb.4" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.02" steps="29"/></proof>
@@ -4436,7 +4434,7 @@
    <proof prover="2"><result status="valid" time="0.25"/></proof>
    </goal>
    <goal name="VC div_sb_qr.156.7" expl="VC for div_sb_qr" proved="true">
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.64"/></proof>
+   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.46"/></proof>
    </goal>
    <goal name="VC div_sb_qr.156.8" expl="VC for div_sb_qr" proved="true">
    <proof prover="2"><result status="valid" time="0.42"/></proof>
@@ -5301,7 +5299,7 @@
    <proof prover="3"><result status="valid" time="0.07"/></proof>
    </goal>
    <goal name="VC div_sb_qr.170.3" expl="assertion" proved="true">
-   <proof prover="3"><result status="valid" time="0.30"/></proof>
+   <proof prover="3"><result status="valid" time="0.16"/></proof>
    </goal>
    <goal name="VC div_sb_qr.170.4" expl="VC for div_sb_qr" proved="true">
    <proof prover="3"><result status="valid" time="0.08"/></proof>
@@ -5334,7 +5332,7 @@
   <proof prover="2" timelimit="5"><result status="valid" time="0.89"/></proof>
   </goal>
   <goal name="VC div_sb_qr.177" expl="assertion" proved="true">
-  <proof prover="2" timelimit="5"><result status="valid" time="2.12"/></proof>
+  <proof prover="2" timelimit="5"><result status="valid" time="1.78"/></proof>
   </goal>
   <goal name="VC div_sb_qr.178" expl="precondition" proved="true">
   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.52"/></proof>
@@ -5532,7 +5530,7 @@
    </transf>
    </goal>
    <goal name="VC div_sb_qr.196.10" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="6.02"/></proof>
+   <proof prover="0"><result status="valid" time="5.21"/></proof>
    </goal>
    <goal name="VC div_sb_qr.196.11" expl="VC for div_sb_qr" proved="true">
    <proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -5978,7 +5976,7 @@
        <proof prover="2"><result status="valid" time="0.17"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.1" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.35"/></proof>
+       <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.2" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.31"/></proof>
@@ -6002,7 +6000,7 @@
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.9" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.32"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.10" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.31"/></proof>
@@ -6035,7 +6033,7 @@
        <proof prover="2"><result status="valid" time="0.30"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.20" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.32"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.21" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.22"/></proof>
@@ -6074,13 +6072,13 @@
        <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.33" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.32"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.34" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.34"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.35" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.36"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.36" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.26"/></proof>
@@ -6281,7 +6279,7 @@
        <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.102" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.32"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.103" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>

examples/multiprecision/lineardecision/why3session.xml

@@ -3,6 +3,7 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -1137,7 +1138,7 @@
    <proof prover="2"><result status="valid" time="0.13"/></proof>
    </goal>
    <goal name="VC gauss_jordan.37.3" expl="VC for gauss_jordan" proved="true">
-   <proof prover="4"><result status="valid" time="0.26" steps="470"/></proof>
+   <proof prover="4"><result status="valid" time="0.13" steps="470"/></proof>
    </goal>
    <goal name="VC gauss_jordan.37.4" expl="VC for gauss_jordan" proved="true">
    <proof prover="0"><result status="valid" time="0.15"/></proof>
@@ -1169,7 +1170,7 @@
   </goal>
   <goal name="VC gauss_jordan.45" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
-   <goal name="VC gauss_jordan.45.0" expl="VC for gauss_jordan" proved="true">
+   <goal name="VC gauss_jordan.45.0" expl="assertion" proved="true">
    <proof prover="2"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC gauss_jordan.45.1" expl="VC for gauss_jordan" proved="true">
@@ -1186,6 +1187,12 @@
    <goal name="VC gauss_jordan.45.2" expl="VC for gauss_jordan" proved="true">
    <proof prover="2"><result status="valid" time="0.03"/></proof>
    </goal>
+   <goal name="VC gauss_jordan.45.3" expl="VC for gauss_jordan" proved="true">
+   <proof prover="1"><result status="valid" time="0.12"/></proof>
+   </goal>
+   <goal name="VC gauss_jordan.45.4" expl="VC for gauss_jordan" proved="true">
+   <proof prover="1"><result status="valid" time="0.14"/></proof>
+   </goal>
   </transf>
   </goal>
   <goal name="VC gauss_jordan.46" expl="loop invariant preservation" proved="true">

examples/queens/why3session.xml

@@ -3,6 +3,7 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Coq" version="8.7.1" timelimit="0" steplimit="0" memlimit="0"/>
@@ -225,16 +226,16 @@
    <proof prover="10"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC t3.16.2" expl="VC for t3" proved="true">
-   <proof prover="10"><result status="valid" time="0.04"/></proof>
+   <proof prover="1"><result status="valid" time="0.03"/></proof>
    </goal>
    <goal name="VC t3.16.3" expl="VC for t3" proved="true">
-   <proof prover="7"><result status="valid" time="0.02"/></proof>
+   <proof prover="10"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC t3.16.4" expl="VC for t3" proved="true">
-   <proof prover="10"><result status="valid" time="0.04"/></proof>
+   <proof prover="7"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC t3.16.5" expl="VC for t3" proved="true">
-   <proof prover="10"><result status="valid" time="0.03"/></proof>
+   <proof prover="10"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC t3.16.6" expl="VC for t3" proved="true">
    <proof prover="10"><result status="valid" time="0.03"/></proof>
@@ -242,6 +243,9 @@
    <goal name="VC t3.16.7" expl="VC for t3" proved="true">
    <proof prover="10"><result status="valid" time="0.03"/></proof>
    </goal>
+   <goal name="VC t3.16.8" expl="VC for t3" proved="true">
+   <proof prover="10"><result status="valid" time="0.03"/></proof>
+   </goal>
   </transf>
   </goal>
  </transf>

examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml

@@ -5,10 +5,11 @@
 <prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../strassen.mlw" proved="true">
 <theory name="MatrixMultiplication" proved="true">
  <goal name="VC blit" expl="VC for blit" proved="true">
- <proof prover="1"><result status="valid" time="0.24" steps="784"/></proof>
+ <proof prover="1"><result status="valid" time="0.24" steps="787"/></proof>
  </goal>
  <goal name="VC block" expl="VC for block" proved="true">
  <proof prover="1"><result status="valid" time="0.12" steps="225"/></proof>
@@ -40,13 +41,13 @@
   <proof prover="1"><result status="valid" time="0.03" steps="14"/></proof>
   </goal>
   <goal name="VC mult_ijk.3" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="4"/></proof>
+  <proof prover="1"><result status="valid" time="0.03" steps="17"/></proof>
   </goal>
   <goal name="VC mult_ijk.4" expl="loop invariant init" proved="true">
   <proof prover="1"><result status="valid" time="0.03" steps="13"/></proof>
   </goal>
   <goal name="VC mult_ijk.5" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="4"/></proof>
+  <proof prover="1"><result status="valid" time="0.03" steps="22"/></proof>
   </goal>
   <goal name="VC mult_ijk.6" expl="loop invariant init" proved="true">
   <proof prover="1"><result status="valid" time="0.03" steps="40"/></proof>
@@ -116,13 +117,13 @@
   <proof prover="1"><result status="valid" time="0.03" steps="14"/></proof>
   </goal>
   <goal name="VC mult_ikj.3" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="4"/></proof>
+  <proof prover="1"><result status="valid" time="0.03" steps="18"/></proof>
   </goal>
   <goal name="VC mult_ikj.4" expl="loop invariant init" proved="true">
   <proof prover="1"><result status="valid" time="0.04" steps="18"/></proof>
   </goal>
   <goal name="VC mult_ikj.5" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.03" steps="4"/></proof>
+  <proof prover="1"><result status="valid" time="0.03" steps="22"/></proof>
   </goal>
   <goal name="VC mult_ikj.6" expl="loop invariant init" proved="true">
   <proof prover="1"><result status="valid" time="0.03" steps="18"/></proof>
@@ -579,7 +580,7 @@
   <proof prover="1" timelimit="10"><result status="valid" time="2.70" steps="3244"/></proof>
   </goal>
   <goal name="VC strassen.112" expl="assertion" proved="true">
-  <proof prover="1" timelimit="10"><result status="valid" time="3.47" steps="3791"/></proof>
+  <proof prover="1" timelimit="10"><result status="valid" time="3.92" steps="3791"/></proof>
   </goal>
   <goal name="VC strassen.113" expl="precondition" proved="true">
   <transf name="compute_specified" proved="true" >
@@ -1136,19 +1137,19 @@
   <goal name="VC strassen.194" expl="precondition" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC strassen.194.0" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.06" steps="25"/></proof>
-   </goal>
-   <goal name="VC strassen.194.1" expl="precondition" proved="true">
    <transf name="compute_specified" proved="true" >
-    <goal name="VC strassen.194.1.0" expl="precondition" proved="true">
+    <goal name="VC strassen.194.0.0" expl="precondition" proved="true">
     <transf name="introduce_premises" proved="true" >
-     <goal name="VC strassen.194.1.0.0" expl="precondition" proved="true">
-     <proof prover="1" timelimit="5"><result status="valid" time="0.08" steps="29"/></proof>
+     <goal name="VC strassen.194.0.0.0" expl="precondition" proved="true">
+     <proof prover="1" timelimit="5"><result status="valid" time="0.08" steps="28"/></proof>
      </goal>
     </transf>
     </goal>
    </transf>
    </goal>
+   <goal name="VC strassen.194.1" expl="precondition" proved="true">
+   <proof prover="1"><result status="valid" time="0.06" steps="26"/></proof>
+   </goal>
    <goal name="VC strassen.194.2" expl="precondition" proved="true">
    <proof prover="0"><result status="valid" time="0.12"/></proof>
    </goal>
@@ -1160,22 +1161,22 @@
   <goal name="VC strassen.196" expl="precondition" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC strassen.196.0" expl="precondition" proved="true">
-   <proof prover="1" timelimit="5"><result status="valid" time="0.03" steps="25"/></proof>
+   <proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="25"/></proof>
    </goal>
    <goal name="VC strassen.196.1" expl="precondition" proved="true">
-   <proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="26"/></proof>
-   </goal>
-   <goal name="VC strassen.196.2" expl="precondition" proved="true">
    <transf name="compute_specified" proved="true" >
-    <goal name="VC strassen.196.2.0" expl="precondition" proved="true">
+    <goal name="VC strassen.196.1.0" expl="precondition" proved="true">
     <transf name="introduce_premises" proved="true" >
-     <goal name="VC strassen.196.2.0.0" expl="precondition" proved="true">
-     <proof prover="1" timelimit="5"><result status="valid" time="0.98" steps="427"/></proof>
+     <goal name="VC strassen.196.1.0.0" expl="precondition" proved="true">
+     <proof prover="1" timelimit="5"><result status="valid" time="0.07" steps="29"/></proof>
      </goal>
     </transf>
     </goal>
    </transf>
    </goal>
+   <goal name="VC strassen.196.2" expl="precondition" proved="true">
+   <proof prover="1" timelimit="5"><result status="valid" time="3.18" steps="3069"/></proof>
+   </goal>
   </transf>
   </goal>
   <goal name="VC strassen.197" expl="precondition" proved="true">
@@ -1190,22 +1191,22 @@
   <goal name="VC strassen.200" expl="precondition" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC strassen.200.0" expl="precondition" proved="true">
-   <proof prover="1" timelimit="5"><result status="valid" time="0.03" steps="25"/></proof>
-   </goal>
-   <goal name="VC strassen.200.1" expl="precondition" proved="true">
-   <proof prover="1" timelimit="5"><result status="valid" time="0.03" steps="26"/></proof>
-   </goal>
-   <goal name="VC strassen.200.2" expl="precondition" proved="true">
    <transf name="compute_specified" proved="true" >
-    <goal name="VC strassen.200.2.0" expl="precondition" proved="true">
+    <goal name="VC strassen.200.0.0" expl="precondition" proved="true">
     <transf name="introduce_premises" proved="true" >
-     <goal name="VC strassen.200.2.0.0" expl="precondition" proved="true">
-     <proof prover="1" timelimit="5"><result status="valid" time="1.03" steps="447"/></proof>
+     <goal name="VC strassen.200.0.0.0" expl="precondition" proved="true">
+     <proof prover="1" timelimit="5"><result status="valid" time="0.08" steps="28"/></proof>
      </goal>
     </transf>
     </goal>
    </transf>
    </goal>
+   <goal name="VC strassen.200.1" expl="precondition" proved="true">
+   <proof prover="1" timelimit="5"><result status="valid" time="0.03" steps="26"/></proof>
+   </goal>
+   <goal name="VC strassen.200.2" expl="precondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.31"/></proof>
+   </goal>
   </transf>
   </goal>
   <goal name="VC strassen.201" expl="precondition" proved="true">

examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml

@@ -845,10 +845,18 @@
    <proof prover="4"><result status="valid" time="0.02" steps="46"/></proof>
    </goal>
    <goal name="VC main.91.5" expl="assertion" proved="true">
-   <proof prover="4"><result status="valid" time="0.16" steps="305"/></proof>
+   <proof prover="4"><result status="valid" time="0.02" steps="45"/></proof>
    </goal>
    <goal name="VC main.91.6" expl="assertion" proved="true">
-   <proof prover="4"><result status="valid" time="0.72" steps="1120"/></proof>
+   <proof prover="4"><result status="valid" time="0.16" steps="305"/></proof>
+   </goal>
+   <goal name="VC main.91.7" expl="assertion" proved="true">
+   <proof prover="2" timelimit="20"><result status="valid" time="6.58" steps="3764"/></proof>
+   <transf name="split_all_full" proved="true" >
+    <goal name="VC main.91.7.0" expl="assertion" proved="true">
+    <proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="5.30" steps="2977"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>