diff --git a/examples/binary_sort/why3shapes.gz b/examples/binary_sort/why3shapes.gz
index f794e52fa58e6335b7d6670f58795224a43f19b3..4c2d7dd0892ff6eeb51b2f72b03f6db1d866eae3 100644
Binary files a/examples/binary_sort/why3shapes.gz and b/examples/binary_sort/why3shapes.gz differ
diff --git a/examples/bitvectors/bitvector/why3shapes.gz b/examples/bitvectors/bitvector/why3shapes.gz
index 85c763e7f35015306f261788071d3b9998d6b407..839e4b8799275b1c262ed2ccccce930d1d6dc229 100644
Binary files a/examples/bitvectors/bitvector/why3shapes.gz and b/examples/bitvectors/bitvector/why3shapes.gz differ
diff --git a/examples/euler011/why3session.xml b/examples/euler011/why3session.xml
index f1c50b07570d064e8b3dab860893a191a9676c4b..6d70446c4606cb87c39811392a270c8d9d108385 100644
--- a/examples/euler011/why3session.xml
+++ b/examples/euler011/why3session.xml
@@ -103,10 +103,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="105"/></proof>
</goal>
<goal name="VC find_max.6" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC find_max.7" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="119"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="114"/></proof>
</goal>
<goal name="VC find_max.8" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
@@ -115,22 +115,22 @@
<proof prover="0"><result status="valid" time="0.04" steps="116"/></proof>
</goal>
<goal name="VC find_max.10" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="23"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
<goal name="VC find_max.11" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="127"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="122"/></proof>
</goal>
<goal name="VC find_max.12" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC find_max.13" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="134"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="128"/></proof>
</goal>
<goal name="VC find_max.14" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.15" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="138"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="133"/></proof>
</goal>
<goal name="VC find_max.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
@@ -139,10 +139,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="116"/></proof>
</goal>
<goal name="VC find_max.18" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.19" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="130"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="125"/></proof>
</goal>
<goal name="VC find_max.20" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
@@ -151,58 +151,58 @@
<proof prover="0"><result status="valid" time="0.05" steps="127"/></proof>
</goal>
<goal name="VC find_max.22" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
<goal name="VC find_max.23" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="132"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="127"/></proof>
</goal>
<goal name="VC find_max.24" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC find_max.25" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="134"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="128"/></proof>
</goal>
<goal name="VC find_max.26" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.27" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="139"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="134"/></proof>
</goal>
<goal name="VC find_max.28" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC find_max.29" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="142"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="136"/></proof>
</goal>
<goal name="VC find_max.30" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC find_max.31" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="138"/></proof>
</goal>
<goal name="VC find_max.32" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.33" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="143"/></proof>
</goal>
<goal name="VC find_max.34" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.35" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="139"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="134"/></proof>
</goal>
<goal name="VC find_max.36" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.37" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="141"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="135"/></proof>
</goal>
<goal name="VC find_max.38" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="VC find_max.39" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="146"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="141"/></proof>
</goal>
<goal name="VC find_max.40" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
@@ -211,10 +211,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="120"/></proof>
</goal>
<goal name="VC find_max.42" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.43" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="130"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="125"/></proof>
</goal>
<goal name="VC find_max.44" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
@@ -223,22 +223,22 @@
<proof prover="0"><result status="valid" time="0.05" steps="127"/></proof>
</goal>
<goal name="VC find_max.46" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="21"/></proof>
</goal>
<goal name="VC find_max.47" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="138"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="133"/></proof>
</goal>
<goal name="VC find_max.48" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.49" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="141"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="135"/></proof>
</goal>
<goal name="VC find_max.50" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.51" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="140"/></proof>
</goal>
<goal name="VC find_max.52" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
@@ -247,10 +247,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="127"/></proof>
</goal>
<goal name="VC find_max.54" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.55" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="137"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="132"/></proof>
</goal>
<goal name="VC find_max.56" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
@@ -259,166 +259,166 @@
<proof prover="0"><result status="valid" time="0.04" steps="134"/></proof>
</goal>
<goal name="VC find_max.58" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC find_max.59" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="132"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="127"/></proof>
</goal>
<goal name="VC find_max.60" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC find_max.61" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="134"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="128"/></proof>
</goal>
<goal name="VC find_max.62" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.63" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="139"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="134"/></proof>
</goal>
<goal name="VC find_max.64" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC find_max.65" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="146"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="140"/></proof>
</goal>
<goal name="VC find_max.66" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC find_max.67" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="142"/></proof>
</goal>
<goal name="VC find_max.68" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.69" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="153"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal>
<goal name="VC find_max.70" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.71" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="143"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="138"/></proof>
</goal>
<goal name="VC find_max.72" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="25"/></proof>
</goal>
<goal name="VC find_max.73" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="139"/></proof>
</goal>
<goal name="VC find_max.74" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.75" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="150"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
</goal>
<goal name="VC find_max.76" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC find_max.77" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="141"/></proof>
</goal>
<goal name="VC find_max.78" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC find_max.79" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="142"/></proof>
</goal>
<goal name="VC find_max.80" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.81" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="154"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="148"/></proof>
</goal>
<goal name="VC find_max.82" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC find_max.83" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="157"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="150"/></proof>
</goal>
<goal name="VC find_max.84" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC find_max.85" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="160"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="152"/></proof>
</goal>
<goal name="VC find_max.86" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC find_max.87" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="164"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="157"/></proof>
</goal>
<goal name="VC find_max.88" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.89" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="154"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="148"/></proof>
</goal>
<goal name="VC find_max.90" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC find_max.91" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="156"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
</goal>
<goal name="VC find_max.92" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="30"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="26"/></proof>
</goal>
<goal name="VC find_max.93" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="161"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="155"/></proof>
</goal>
<goal name="VC find_max.94" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.95" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="143"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="138"/></proof>
</goal>
<goal name="VC find_max.96" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.97" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="139"/></proof>
</goal>
<goal name="VC find_max.98" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.99" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="150"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
</goal>
<goal name="VC find_max.100" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.101" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="153"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal>
<goal name="VC find_max.102" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC find_max.103" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="156"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
</goal>
<goal name="VC find_max.104" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC find_max.105" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="160"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="154"/></proof>
</goal>
<goal name="VC find_max.106" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.107" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="150"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
</goal>
<goal name="VC find_max.108" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC find_max.109" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="152"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="146"/></proof>
</goal>
<goal name="VC find_max.110" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC find_max.111" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="157"/></proof>
+ <proof prover="0"><result status="valid" time="0.07" steps="152"/></proof>
</goal>
<goal name="VC find_max.112" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
@@ -427,10 +427,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="120"/></proof>
</goal>
<goal name="VC find_max.114" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.115" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="130"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="125"/></proof>
</goal>
<goal name="VC find_max.116" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
@@ -439,22 +439,22 @@
<proof prover="0"><result status="valid" time="0.04" steps="127"/></proof>
</goal>
<goal name="VC find_max.118" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.119" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="142"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="137"/></proof>
</goal>
<goal name="VC find_max.120" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.121" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="139"/></proof>
</goal>
<goal name="VC find_max.122" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.123" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="144"/></proof>
</goal>
<goal name="VC find_max.124" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
@@ -463,10 +463,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="131"/></proof>
</goal>
<goal name="VC find_max.126" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.127" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="141"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="136"/></proof>
</goal>
<goal name="VC find_max.128" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
@@ -475,58 +475,58 @@
<proof prover="0"><result status="valid" time="0.05" steps="138"/></proof>
</goal>
<goal name="VC find_max.130" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="24"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC find_max.131" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.05" steps="143"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="138"/></proof>
</goal>
<goal name="VC find_max.132" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.133" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="139"/></proof>
</goal>
<goal name="VC find_max.134" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.135" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="150"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
</goal>
<goal name="VC find_max.136" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC find_max.137" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="153"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal>
<goal name="VC find_max.138" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC find_max.139" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="156"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
</goal>
<goal name="VC find_max.140" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC find_max.141" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="160"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="154"/></proof>
</goal>
<goal name="VC find_max.142" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.143" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="150"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="145"/></proof>
</goal>
<goal name="VC find_max.144" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC find_max.145" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="152"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="146"/></proof>
</goal>
<goal name="VC find_max.146" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="26"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC find_max.147" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="157"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="152"/></proof>
</goal>
<goal name="VC find_max.148" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
@@ -535,10 +535,10 @@
<proof prover="0"><result status="valid" time="0.04" steps="131"/></proof>
</goal>
<goal name="VC find_max.150" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find_max.151" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="141"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="136"/></proof>
</goal>
<goal name="VC find_max.152" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
@@ -547,22 +547,22 @@
<proof prover="0"><result status="valid" time="0.05" steps="138"/></proof>
</goal>
<goal name="VC find_max.154" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="VC find_max.155" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="149"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="144"/></proof>
</goal>
<goal name="VC find_max.156" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC find_max.157" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="152"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="146"/></proof>
</goal>
<goal name="VC find_max.158" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="0"><result status="valid" time="0.00" steps="23"/></proof>
</goal>
<goal name="VC find_max.159" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="156"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="151"/></proof>
</goal>
<goal name="VC find_max.160" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
@@ -571,10 +571,10 @@
<proof prover="0"><result status="valid" time="0.05" steps="138"/></proof>
</goal>
<goal name="VC find_max.162" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC find_max.163" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="148"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="143"/></proof>
</goal>
<goal name="VC find_max.164" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="19"/></proof>
diff --git a/examples/euler011/why3shapes.gz b/examples/euler011/why3shapes.gz
index c6db9ef4796cfe8e676b888134f6f0cdaea22ef5..1818c0fa09f8e229c50a3a6bd8939a5c709bdd2e 100644
Binary files a/examples/euler011/why3shapes.gz and b/examples/euler011/why3shapes.gz differ
diff --git a/examples/fenwick/why3session.xml b/examples/fenwick/why3session.xml
index f5467188a42ad8eaedd078a4a60904fc8b20d807..7ffbfd84941dc28a1d1a80d376de552338ce37ed 100644
--- a/examples/fenwick/why3session.xml
+++ b/examples/fenwick/why3session.xml
@@ -15,10 +15,10 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add.1" expl="index in array bounds" proved="true">
- <proof prover="2"><result status="valid" time="0.06"/></proof>
+ <proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC add.2" expl="index in array bounds" proved="true">
- <proof prover="2"><result status="valid" time="0.05"/></proof>
+ <proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC add.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -98,7 +98,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC query.8" expl="index in array bounds" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC query.9" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -107,7 +107,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC query.11" expl="loop variant decrease" proved="true">
- <proof prover="2"><result status="valid" time="0.06"/></proof>
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC query.12" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
@@ -137,7 +137,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC query.21" expl="index in array bounds" proved="true">
- <proof prover="2"><result status="valid" time="0.05"/></proof>
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC query.22" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -146,7 +146,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC query.24" expl="loop variant decrease" proved="true">
- <proof prover="2"><result status="valid" time="0.08"/></proof>
+ <proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC query.25" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
diff --git a/examples/fenwick/why3shapes.gz b/examples/fenwick/why3shapes.gz
index 05421435f1e629d5f732d9d41337de8dc0349912..19d3268b1f343170e503c4848ec99652c4fdfa50 100644
Binary files a/examples/fenwick/why3shapes.gz and b/examples/fenwick/why3shapes.gz differ
diff --git a/examples/hillel_challenge/why3session.xml b/examples/hillel_challenge/why3session.xml
index bae514426cbd0738326cb96a46e4cc052150a548..fb34f06ef94526718f285897ca0c898fb06ef010 100644
--- a/examples/hillel_challenge/why3session.xml
+++ b/examples/hillel_challenge/why3session.xml
@@ -3,8 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../hillel_challenge.mlw" proved="true">
<theory name="Leftpad" proved="true">
<goal name="VC leftpad" expl="VC for leftpad" proved="true">
@@ -48,9 +50,9 @@
<proof prover="3"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="VC unique.11" expl="loop invariant preservation" proved="true">
- <transf name="case" proved="true" arg1="(x=o)">
+ <transf name="case" proved="true" arg1="x=a[i]">
<goal name="VC unique.11.0" expl="true case (loop invariant preservation)" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="88"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="VC unique.11.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(mem x a (i+1) <-> mem x a i)">
@@ -70,12 +72,12 @@
<proof prover="2"><result status="valid" time="0.01" steps="44"/></proof>
</goal>
<goal name="VC unique.12.1" expl="false case (loop invariant preservation)" proved="true">
- <transf name="assert" proved="true" arg1="(not (mem o a i1))">
+ <transf name="assert" proved="true" arg1="(not (mem a[i1] a i1))">
<goal name="VC unique.12.1.0" proved="true">
- <proof prover="0"><result status="valid" time="0.03"/></proof>
+ <proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.12.1.1" expl="false case (loop invariant preservation)" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="92"/></proof>
</goal>
</transf>
</goal>
@@ -88,17 +90,17 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.15" expl="loop invariant preservation" proved="true">
- <transf name="case" proved="true" arg1="(x = o)">
+ <transf name="case" proved="true" arg1="(x=n-1)">
<goal name="VC unique.15.0" expl="true case (loop invariant preservation)" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="54"/></proof>
+ <proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC unique.15.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(mem x a (i+1) <-> mem x a i)">
<goal name="VC unique.15.1.0" proved="true">
- <proof prover="0"><result status="valid" time="0.06"/></proof>
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.15.1.1" expl="false case (loop invariant preservation)" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
+ <proof prover="2"><result status="valid" time="0.00" steps="25"/></proof>
</goal>
</transf>
</goal>
@@ -126,7 +128,7 @@
<goal name="VC fulcrum" expl="VC for fulcrum" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC fulcrum.0" expl="loop invariant init" proved="true">
- <proof prover="0"><result status="valid" time="0.03"/></proof>
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fulcrum.1" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
@@ -135,7 +137,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC fulcrum.3" expl="loop invariant init" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC fulcrum.4" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
@@ -219,7 +221,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_big.3" expl="integer overflow" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_big.4" expl="type invariant" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -253,7 +255,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_big.9" expl="integer overflow" proved="true">
- <proof prover="0"><result status="valid" time="0.03"/></proof>
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_big.10" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -284,7 +286,7 @@
<goal name="VC delta" expl="VC for delta" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC delta.0" expl="integer overflow" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC delta.1" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -302,7 +304,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delta.6" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.06"/></proof>
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC delta.7" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -311,7 +313,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delta.9" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.05"/></proof>
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC delta.10" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -329,7 +331,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delta.15" expl="integer overflow" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC delta.16" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -338,7 +340,7 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC delta.18" expl="integer overflow" proved="true">
- <proof prover="0"><result status="valid" time="0.03"/></proof>
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delta.19" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -441,7 +443,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fulcrum.28" expl="loop invariant preservation" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="38"/></proof>
+ <proof prover="2"><result status="valid" time="0.01" steps="61"/></proof>
</goal>
<goal name="VC fulcrum.29" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -456,10 +458,10 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC fulcrum.33" expl="loop invariant preservation" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="51"/></proof>
</goal>
<goal name="VC fulcrum.34" expl="loop invariant preservation" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="31"/></proof>
+ <proof prover="2"><result status="valid" time="0.01" steps="55"/></proof>
</goal>
<goal name="VC fulcrum.35" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
diff --git a/examples/hillel_challenge/why3shapes.gz b/examples/hillel_challenge/why3shapes.gz
index a1cdaf1012cb3d48aba753b518e2f8bbc9fee542..026340f9b1737b29a949e0ad4c9c72d18cdff942 100644
Binary files a/examples/hillel_challenge/why3shapes.gz and b/examples/hillel_challenge/why3shapes.gz differ
diff --git a/examples/max_matrix/why3shapes.gz b/examples/max_matrix/why3shapes.gz
index 1c13045cec30556c5c21536473b93345a4626200..4a7359b901f9109e16eb36d19fab95a3b6ef0d52 100644
Binary files a/examples/max_matrix/why3shapes.gz and b/examples/max_matrix/why3shapes.gz differ
diff --git a/examples/maximum_subarray/why3shapes.gz b/examples/maximum_subarray/why3shapes.gz
index 7db08d9a52eea78a68bc3ec6d0ada496eb4228ca..53edadada860e4c40d06e0fa6da97b14ad309c32 100644
Binary files a/examples/maximum_subarray/why3shapes.gz and b/examples/maximum_subarray/why3shapes.gz differ
diff --git a/examples/mccarthy/why3session.xml b/examples/mccarthy/why3session.xml
index 469be5b198a48b0709cda1356061f2da63b02d69..fd3752a3b41bb9a3781858037191f0ee575298d1 100644
--- a/examples/mccarthy/why3session.xml
+++ b/examples/mccarthy/why3session.xml
@@ -43,19 +43,19 @@
<proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="loop variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
+ <proof prover="3"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.03" steps="217"/></proof>
+ <proof prover="3"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="loop variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.00" steps="17"/></proof>
+ <proof prover="3"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="3.56" steps="4952"/></proof>
+ <proof prover="3"><result status="valid" time="3.34" steps="4574"/></proof>
</goal>
<goal name="VC f91_nonrec.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="30"/></proof>
diff --git a/examples/mccarthy/why3shapes.gz b/examples/mccarthy/why3shapes.gz
index 690347d0db94ddfde5094c9e59a153eea2a1f9a4..8206e7ee89694d2d90b98a76fd2884532fc9bd2e 100644
Binary files a/examples/mccarthy/why3shapes.gz and b/examples/mccarthy/why3shapes.gz differ
diff --git a/examples/mex/why3shapes.gz b/examples/mex/why3shapes.gz
index 8574b1bcfa1e377ea3e2e21fef5f016dfb2f9941..84ac83f2d854dc8057fc3ff5a00250c68f7dd69f 100644
Binary files a/examples/mex/why3shapes.gz and b/examples/mex/why3shapes.gz differ
diff --git a/examples/pancake_sorting/why3shapes.gz b/examples/pancake_sorting/why3shapes.gz
index ac61513bd14657ad26a07f88aaf537fe67cfd0a3..91bb54badc8d34ae6b5ac2488d14af61fee0135c 100644
Binary files a/examples/pancake_sorting/why3shapes.gz and b/examples/pancake_sorting/why3shapes.gz differ
diff --git a/examples/power/why3shapes.gz b/examples/power/why3shapes.gz
index 24467775f874209c64d8e4065766ccd757700267..fa88b6396b2089e674c2e80dde7e3f476ed8d088 100644
Binary files a/examples/power/why3shapes.gz and b/examples/power/why3shapes.gz differ
diff --git a/examples/power_vc_sp/why3shapes.gz b/examples/power_vc_sp/why3shapes.gz
index 566d8934662434cacf9e21bd2dcd766ebdc5d128..91f508f9bed1aa64306c323c8fd63a2c407e4d71 100644
Binary files a/examples/power_vc_sp/why3shapes.gz and b/examples/power_vc_sp/why3shapes.gz differ
diff --git a/examples/prover/Firstorder_formula_impl/why3session.xml b/examples/prover/Firstorder_formula_impl/why3session.xml
index b752a3ad5b8f874cafd62a6dfa88fc30472d216e..49b1971d0d76b77dfc7b8ecf3c865fcc94ac77d5 100644
--- a/examples/prover/Firstorder_formula_impl/why3session.xml
+++ b/examples/prover/Firstorder_formula_impl/why3session.xml
@@ -1343,7 +1343,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="14"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_fo_formula.20" expl="variant decrease" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.19" steps="93"/></proof>
+ <proof prover="0" timelimit="5"><result status="valid" time="0.07" steps="93"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_fo_formula.21" expl="precondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.13" steps="47"/></proof>
@@ -1716,7 +1716,7 @@
<proof prover="2"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="VC construct_fo_formula.4.2" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.12" steps="244"/></proof>
+ <proof prover="0"><result status="valid" time="0.12" steps="245"/></proof>
</goal>
<goal name="VC construct_fo_formula.4.3" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
@@ -1786,7 +1786,7 @@
<proof prover="0"><result status="valid" time="0.06" steps="77"/></proof>
</goal>
<goal name="VC construct_fo_formula.20.2" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.13" steps="244"/></proof>
+ <proof prover="0"><result status="valid" time="0.13" steps="245"/></proof>
</goal>
<goal name="VC construct_fo_formula.20.3" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
@@ -2348,7 +2348,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.12" steps="25"/></proof>
</goal>
<goal name="VC destruct_fo_formula.26" expl="unreachable point" proved="true">
- <proof prover="0"><result status="valid" time="0.17" steps="25"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="25"/></proof>
</goal>
<goal name="VC destruct_fo_formula.27" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="23"/></proof>
@@ -2616,7 +2616,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="21"/></proof>
</goal>
<goal name="VC destruct_fo_formula.100" expl="unreachable point" proved="true">
- <proof prover="0"><result status="valid" time="0.17" steps="21"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
</goal>
<goal name="VC destruct_fo_formula.101" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="23"/></proof>
@@ -3081,7 +3081,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="67"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_fo_formula.9.3" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.42"/></proof>
+ <proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_fo_formula.9.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.64"/></proof>
diff --git a/examples/prover/Firstorder_formula_impl/why3shapes.gz b/examples/prover/Firstorder_formula_impl/why3shapes.gz
index 8ed1c28691903c3e012be71abea47819a68aa552..938b79ca8af3ef484fa7036d2ed5e2b05fde7516 100644
Binary files a/examples/prover/Firstorder_formula_impl/why3shapes.gz and b/examples/prover/Firstorder_formula_impl/why3shapes.gz differ
diff --git a/examples/prover/Firstorder_formula_spec/why3session.xml b/examples/prover/Firstorder_formula_spec/why3session.xml
index dd0495e29ab27f66972d1a6defcace7aba57b196..816f60220912ca1395db2d1a3414c01810693ba6 100644
--- a/examples/prover/Firstorder_formula_spec/why3session.xml
+++ b/examples/prover/Firstorder_formula_spec/why3session.xml
@@ -48,25 +48,25 @@
<goal name="VC subst_then_rename_composition_lemma_fo_formula" expl="VC for subst_then_rename_composition_lemma_fo_formula" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC subst_then_rename_composition_lemma_fo_formula.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.12"/></proof>
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.2" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
+ <proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.3" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.24"/></proof>
+ <proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.4" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.12"/></proof>
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.5" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.16"/></proof>
+ <proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.6" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.12"/></proof>
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.7" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="t">
@@ -113,25 +113,25 @@
<goal name="VC subst_composition_lemma_fo_formula" expl="VC for subst_composition_lemma_fo_formula" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC subst_composition_lemma_fo_formula.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
+ <proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.12"/></proof>
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.2" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.3" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.4" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.5" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.6" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.7" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="t">
@@ -192,16 +192,16 @@
<proof prover="3"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC subst_identity_lemma_fo_formula.7.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.40"/></proof>
+ <proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC subst_identity_lemma_fo_formula.7.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <proof prover="3"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC subst_identity_lemma_fo_formula.7.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC subst_identity_lemma_fo_formula.7.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.24"/></proof>
+ <proof prover="3"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="VC subst_identity_lemma_fo_formula.7.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.21"/></proof>
@@ -210,7 +210,7 @@
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC subst_identity_lemma_fo_formula.7.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.25"/></proof>
+ <proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
@@ -219,22 +219,22 @@
<goal name="VC renaming_preserve_size_fo_formula" expl="VC for renaming_preserve_size_fo_formula" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC renaming_preserve_size_fo_formula.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.2" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.14"/></proof>
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.3" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.4" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.5" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.6" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.14"/></proof>
diff --git a/examples/prover/Firstorder_formula_spec/why3shapes.gz b/examples/prover/Firstorder_formula_spec/why3shapes.gz
index ea3357240806b57ea6ecb84931e2a259a7cf63d3..5180517701109984ed3715bd52e8c6edb8c4434b 100644
Binary files a/examples/prover/Firstorder_formula_spec/why3shapes.gz and b/examples/prover/Firstorder_formula_spec/why3shapes.gz differ
diff --git a/examples/prover/ISet/why3shapes.gz b/examples/prover/ISet/why3shapes.gz
index d535f854be99e0450390cb6c2ad323c918252eca..bf97aa46920929918a4df2ef06ed967c09385489 100644
Binary files a/examples/prover/ISet/why3shapes.gz and b/examples/prover/ISet/why3shapes.gz differ
diff --git a/examples/prover/Prover/why3session.xml b/examples/prover/Prover/why3session.xml
index fd5d4832ed54b6ae1ef99838af17ffd7390c24c5..26648f3eb97a76b1b7331b5972e7d644672bd74d 100644
--- a/examples/prover/Prover/why3session.xml
+++ b/examples/prover/Prover/why3session.xml
@@ -319,7 +319,7 @@
<goal name="VC branch_conflict_atom.9" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC branch_conflict_atom.9.0" expl="precondition" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.17" steps="273"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.17" steps="218"/></proof>
</goal>
</transf>
</goal>
@@ -425,16 +425,16 @@
<proof prover="7"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="VC branch_conflict_atom.39.0.0.0.2" expl="VC for branch_conflict_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.12" steps="78"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.12" steps="77"/></proof>
</goal>
<goal name="VC branch_conflict_atom.39.0.0.0.3" expl="VC for branch_conflict_atom" proved="true">
<proof prover="7"><result status="valid" time="0.81"/></proof>
</goal>
<goal name="VC branch_conflict_atom.39.0.0.0.4" expl="VC for branch_conflict_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.56"/></proof>
+ <proof prover="7"><result status="valid" time="0.59"/></proof>
</goal>
<goal name="VC branch_conflict_atom.39.0.0.0.5" expl="VC for branch_conflict_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.59"/></proof>
+ <proof prover="7"><result status="valid" time="0.56"/></proof>
</goal>
</transf>
</goal>
@@ -491,7 +491,7 @@
<goal name="VC branch_conflict_neg_atom.11" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC branch_conflict_neg_atom.11.0" expl="precondition" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.15" steps="302"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.15" steps="242"/></proof>
</goal>
</transf>
</goal>
@@ -625,13 +625,13 @@
<proof prover="7"><result status="valid" time="0.86"/></proof>
</goal>
<goal name="VC branch_conflict_neg_atom.42.0.0.0.3" expl="VC for branch_conflict_neg_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.14" steps="78"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.14" steps="77"/></proof>
</goal>
<goal name="VC branch_conflict_neg_atom.42.0.0.0.4" expl="VC for branch_conflict_neg_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.58"/></proof>
+ <proof prover="7"><result status="valid" time="0.55"/></proof>
</goal>
<goal name="VC branch_conflict_neg_atom.42.0.0.0.5" expl="VC for branch_conflict_neg_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.55"/></proof>
+ <proof prover="7"><result status="valid" time="0.58"/></proof>
</goal>
</transf>
</goal>
@@ -846,10 +846,10 @@
<proof prover="7"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="VC clause_conflicts.50.0.0.0.4" expl="VC for clause_conflicts" proved="true">
- <proof prover="7"><result status="valid" time="0.53"/></proof>
+ <proof prover="7"><result status="valid" time="0.55"/></proof>
</goal>
<goal name="VC clause_conflicts.50.0.0.0.5" expl="VC for clause_conflicts" proved="true">
- <proof prover="7"><result status="valid" time="0.55"/></proof>
+ <proof prover="7"><result status="valid" time="0.53"/></proof>
</goal>
</transf>
</goal>
@@ -1249,7 +1249,7 @@
<proof prover="7"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="VC decompose.108.1" expl="assertion" proved="true">
- <proof prover="7"><result status="valid" time="0.45"/></proof>
+ <proof prover="7"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC decompose.108.2" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.76"/></proof>
@@ -1258,7 +1258,7 @@
<proof prover="7"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="VC decompose.108.4" expl="assertion" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.16" steps="117"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.16" steps="116"/></proof>
</goal>
<goal name="VC decompose.108.5" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.50"/></proof>
@@ -1267,7 +1267,7 @@
<proof prover="7"><result status="valid" time="1.43"/></proof>
</goal>
<goal name="VC decompose.108.7" expl="assertion" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.19" steps="262"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.19" steps="261"/></proof>
</goal>
<goal name="VC decompose.108.8" expl="assertion" proved="true">
<transf name="split_all_full" proved="true" >
@@ -1840,19 +1840,19 @@
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC decompose_literal.98.0.0.0.2" expl="VC for decompose_literal" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.23" steps="336"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.23" steps="334"/></proof>
</goal>
<goal name="VC decompose_literal.98.0.0.0.3" expl="VC for decompose_literal" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="337"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="335"/></proof>
</goal>
<goal name="VC decompose_literal.98.0.0.0.4" expl="VC for decompose_literal" proved="true">
<proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC decompose_literal.98.0.0.0.5" expl="VC for decompose_literal" proved="true">
- <proof prover="7"><result status="valid" time="0.54"/></proof>
+ <proof prover="7"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="VC decompose_literal.98.0.0.0.6" expl="VC for decompose_literal" proved="true">
- <proof prover="7"><result status="valid" time="0.51"/></proof>
+ <proof prover="7"><result status="valid" time="0.54"/></proof>
</goal>
</transf>
</goal>
@@ -2728,10 +2728,10 @@
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC contradiction_atom.187.0.0.0.2" expl="VC for contradiction_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.26" steps="311"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.26" steps="309"/></proof>
</goal>
<goal name="VC contradiction_atom.187.0.0.0.3" expl="VC for contradiction_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="312"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="310"/></proof>
</goal>
<goal name="VC contradiction_atom.187.0.0.0.4" expl="VC for contradiction_atom" proved="true">
<proof prover="3"><result status="valid" time="0.13"/></proof>
@@ -2857,13 +2857,13 @@
<proof prover="7"><result status="valid" time="1.05"/></proof>
</goal>
<goal name="VC contradiction_atom.213.0.0.0.3" expl="VC for contradiction_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.16" steps="124"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.16" steps="123"/></proof>
</goal>
<goal name="VC contradiction_atom.213.0.0.0.4" expl="VC for contradiction_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.48"/></proof>
+ <proof prover="7"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="VC contradiction_atom.213.0.0.0.5" expl="VC for contradiction_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.51"/></proof>
+ <proof prover="7"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
</goal>
@@ -3660,16 +3660,16 @@
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.209.0.0.0.2" expl="VC for contradiction_neg_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.15" steps="124"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.15" steps="123"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.209.0.0.0.3" expl="VC for contradiction_neg_atom" proved="true">
<proof prover="7"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.209.0.0.0.4" expl="VC for contradiction_neg_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.60"/></proof>
+ <proof prover="7"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.209.0.0.0.5" expl="VC for contradiction_neg_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.51"/></proof>
+ <proof prover="7"><result status="valid" time="0.60"/></proof>
</goal>
</transf>
</goal>
@@ -3982,19 +3982,19 @@
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC extend_branch.93.0.0.0.2" expl="VC for extend_branch" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="233"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="231"/></proof>
</goal>
<goal name="VC extend_branch.93.0.0.0.3" expl="VC for extend_branch" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.20" steps="234"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.20" steps="232"/></proof>
</goal>
<goal name="VC extend_branch.93.0.0.0.4" expl="VC for extend_branch" proved="true">
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC extend_branch.93.0.0.0.5" expl="VC for extend_branch" proved="true">
- <proof prover="7"><result status="valid" time="0.47"/></proof>
+ <proof prover="7"><result status="valid" time="0.53"/></proof>
</goal>
<goal name="VC extend_branch.93.0.0.0.6" expl="VC for extend_branch" proved="true">
- <proof prover="7"><result status="valid" time="0.53"/></proof>
+ <proof prover="7"><result status="valid" time="0.47"/></proof>
</goal>
</transf>
</goal>
@@ -4432,7 +4432,7 @@
<goal name="VC contradiction_find_atom.108" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC contradiction_find_atom.108.0" expl="precondition" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="577"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="458"/></proof>
</goal>
</transf>
</goal>
@@ -4736,19 +4736,19 @@
<proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC contradiction_find_atom.198.0.0.0.2" expl="VC for contradiction_find_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="297"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="295"/></proof>
</goal>
<goal name="VC contradiction_find_atom.198.0.0.0.3" expl="VC for contradiction_find_atom" proved="true">
- <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="298"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="296"/></proof>
</goal>
<goal name="VC contradiction_find_atom.198.0.0.0.4" expl="VC for contradiction_find_atom" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC contradiction_find_atom.198.0.0.0.5" expl="VC for contradiction_find_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.55"/></proof>
+ <proof prover="7"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="VC contradiction_find_atom.198.0.0.0.6" expl="VC for contradiction_find_atom" proved="true">
- <proof prover="7"><result status="valid" time="0.64"/></proof>
+ <proof prover="7"><result status="valid" time="0.55"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/prover/Prover/why3shapes.gz b/examples/prover/Prover/why3shapes.gz
index a2a17b770ddad602c904ed19b0a82ccc9ae57655..7819a32a627e5e6945dd74ebc1118ebd7475e5fc 100644
Binary files a/examples/prover/Prover/why3shapes.gz and b/examples/prover/Prover/why3shapes.gz differ
diff --git a/examples/prover/Unification/why3session.xml b/examples/prover/Unification/why3session.xml
index fd8a3f36d23536e829b69b501dbdb53768a3b131..74b4f81210ccb78285c3cadd4a0c5ad27718b1ba 100644
--- a/examples/prover/Unification/why3session.xml
+++ b/examples/prover/Unification/why3session.xml
@@ -5,6 +5,7 @@
<prover id="0" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Eprover" version="1.8-001" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -762,11 +763,7 @@
<proof prover="12"><result status="valid" time="0.12" steps="163"/></proof>
</goal>
<goal name="VC unification_term.17" expl="precondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC unification_term.17.0" expl="precondition" proved="true">
- <proof prover="11"><result status="valid" time="0.16"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.07" steps="273"/></proof>
</goal>
<goal name="VC unification_term.18" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.07" steps="27"/></proof>
diff --git a/examples/prover/Unification/why3shapes.gz b/examples/prover/Unification/why3shapes.gz
index 6ce83fb8d1cd963e925f8cc99f158f28ea641caa..21322c85fa8961763eb14f9b47731f3fcc0f7e5a 100644
Binary files a/examples/prover/Unification/why3shapes.gz and b/examples/prover/Unification/why3shapes.gz differ
diff --git a/examples/random_access_list/why3session.xml b/examples/random_access_list/why3session.xml
index 5b5a7733dfb33b8092982caf9b2f108a95526c81..0d7c725def28456d5e6df836adbf23e34ba69b7a 100644
--- a/examples/random_access_list/why3session.xml
+++ b/examples/random_access_list/why3session.xml
@@ -149,33 +149,33 @@
<proof prover="3" timelimit="5"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC lookup.1" expl="variant decrease" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="5"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC lookup.2" expl="precondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="20"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC lookup.3" expl="precondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC lookup.4" expl="variant decrease" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="42"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="VC lookup.5" expl="precondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="38"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="VC lookup.6" expl="precondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="5"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC lookup.7" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC lookup.7.0" expl="postcondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="11"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.06" steps="10"/></proof>
</goal>
<goal name="VC lookup.7.1" expl="postcondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="27"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="66"/></proof>
</goal>
<goal name="VC lookup.7.2" expl="postcondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.06" steps="96"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.01" steps="98"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/random_access_list/why3shapes.gz b/examples/random_access_list/why3shapes.gz
index 2cd3bae6745fb062ef86c0307207d5d621e50ca5..ba811f8fe4d5680d96cfd9ed8f99df995c0c0735 100644
Binary files a/examples/random_access_list/why3shapes.gz and b/examples/random_access_list/why3shapes.gz differ
diff --git a/examples/stdlib/pigeon/why3session.xml b/examples/stdlib/pigeon/why3session.xml
index 9892f306748003ebfc2f1b1a76b379e8277e1037..2003059aac30e953ef5026f924f7500a68496858 100644
--- a/examples/stdlib/pigeon/why3session.xml
+++ b/examples/stdlib/pigeon/why3session.xml
@@ -23,7 +23,6 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC pigeonhole.4" expl="variant decrease" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC pigeonhole.5" expl="precondition" proved="true">
@@ -44,6 +43,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC pigeonhole.10" expl="variant decrease" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC pigeonhole.11" expl="precondition" proved="true">
diff --git a/examples/stdlib/pigeon/why3shapes.gz b/examples/stdlib/pigeon/why3shapes.gz
index 81ad8a4c0d952eae1feb54309c9de7ba85348063..0c09b63f664e7acbd75e228147a42aff0a7fb8c3 100644
Binary files a/examples/stdlib/pigeon/why3shapes.gz and b/examples/stdlib/pigeon/why3shapes.gz differ
diff --git a/examples/stdlib/witness/why3shapes.gz b/examples/stdlib/witness/why3shapes.gz
index 095235365662339d8ef6b8d11fb39b96bcef0c52..f1c9e52b9c2b44d03d9986fb3dc9c652fa7972ac 100644
Binary files a/examples/stdlib/witness/why3shapes.gz and b/examples/stdlib/witness/why3shapes.gz differ
diff --git a/examples/tortoise_and_hare/why3session.xml b/examples/tortoise_and_hare/why3session.xml
index 192be93e92a4a04164d5ec1eb62bd6115287e2fd..a304ca0cb1e35013c4c46779e6f26212d41fb6cd 100644
--- a/examples/tortoise_and_hare/why3session.xml
+++ b/examples/tortoise_and_hare/why3session.xml
@@ -63,16 +63,16 @@
<goal name="VC equality" expl="VC for equality" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC equality.0" expl="variant decrease" proved="true">
- <proof prover="6"><result status="valid" time="0.02"/></proof>
+ <proof prover="6"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC equality.1" expl="precondition" proved="true">
- <proof prover="6"><result status="valid" time="0.03"/></proof>
+ <proof prover="6" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC equality.2" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC equality.3" expl="variant decrease" proved="true">
- <proof prover="6"><result status="valid" time="0.07"/></proof>
+ <proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC equality.4" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
@@ -100,7 +100,7 @@
<proof prover="6" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC equality.10" expl="precondition" proved="true">
- <proof prover="6" timelimit="5"><result status="valid" time="0.03"/></proof>
+ <proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC equality.11" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
@@ -127,7 +127,7 @@
<proof prover="5"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC equality.19" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="73"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
<goal name="VC equality.20" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
diff --git a/examples/tortoise_and_hare/why3shapes.gz b/examples/tortoise_and_hare/why3shapes.gz
index 13a5c69c897dedc87e5bb555e7d197bfc7a28c3e..a8bc84fbd5976b6a90c732bd9fb2d2d4161542fb 100644
Binary files a/examples/tortoise_and_hare/why3shapes.gz and b/examples/tortoise_and_hare/why3shapes.gz differ
diff --git a/examples/tree_of_array/why3shapes.gz b/examples/tree_of_array/why3shapes.gz
index f71bfa416c5a66cc2e8fc7eee64816541aac728e..4627e5615622e2b0683f4a7f5a6fd246729e9950 100644
Binary files a/examples/tree_of_array/why3shapes.gz and b/examples/tree_of_array/why3shapes.gz differ
diff --git a/examples/tree_of_list/why3shapes.gz b/examples/tree_of_list/why3shapes.gz
index fabe3b37d7e01b27d7e4df2f28aef12a61825a6c..b6e9e7dbde1019b8c86aa09d2e9ef3f9aee086b9 100644
Binary files a/examples/tree_of_list/why3shapes.gz and b/examples/tree_of_list/why3shapes.gz differ
diff --git a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
index 7244f3069567693cc2a7304b1f977a2225818c76..e1bb3ba49e6f56db13b0d1fd9321ab74626d793c 100644
--- a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
+++ b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
@@ -218,7 +218,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="4.95"/></proof>
</goal>
<goal name="VC padding.6" expl="assertion" proved="true">
- <proof prover="0" timelimit="20"><result status="valid" time="1.67"/></proof>
+ <proof prover="0" timelimit="20"><result status="valid" time="2.96"/></proof>
</goal>
<goal name="VC padding.7" expl="assertion" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.78" steps="919"/></proof>
@@ -261,10 +261,10 @@
<proof prover="1"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC strassen.6" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
+ <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="VC strassen.7" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="VC strassen.8" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
@@ -1074,7 +1074,7 @@
<proof prover="1"><result status="valid" time="0.10" steps="196"/></proof>
</goal>
<goal name="VC strassen.186" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.14"/></proof>
+ <proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC strassen.187" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.38" steps="1048"/></proof>
diff --git a/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz b/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz
index 1c95b8726d9ab7d2e3b8eb523df45e6d1d88683f..8474142d6ef57eb113e65f496f1a89465fd8a3d8 100644
Binary files a/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz and b/examples/verifythis_2016_matrix_multiplication/strassen/why3shapes.gz differ
diff --git a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
index a0c6e0b623ae2fddd511d85ba9b77319e851e30a..77eeb08390404b63df6567aab056cdbb555bcd41 100644
--- a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
+++ b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
@@ -4,8 +4,10 @@
<why3session shape_version="5">
<prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="5" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2018_array_based_queuing_lock_2.mlw" proved="true">
<theory name="ABQL" proved="true">
<goal name="VC tick" expl="VC for tick" proved="true">
@@ -73,10 +75,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC consecutive_last_push.1" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="75"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="76"/></proof>
</goal>
<goal name="VC consecutive_last_push.2" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.23" steps="163"/></proof>
+ <proof prover="4"><result status="valid" time="0.23" steps="162"/></proof>
</goal>
<goal name="VC consecutive_last_push.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.47"/></proof>
@@ -92,7 +94,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC consecutive_implies_sorted.1" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="75"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="76"/></proof>
</goal>
<goal name="VC consecutive_implies_sorted.2" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="51"/></proof>
@@ -143,7 +145,7 @@
<goal name="VC main" expl="VC for main" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.0" expl="array creation size" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.1" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.18"/></proof>
@@ -152,13 +154,13 @@
<proof prover="3"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC main.3" expl="array creation size" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.4" expl="array creation size" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="13"/></proof>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC main.5" expl="array creation size" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC main.6" expl="safety" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="29"/></proof>
@@ -249,76 +251,76 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.28" expl="safety" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.08" steps="116"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="116"/></proof>
</goal>
<goal name="VC main.29" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="32"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.30" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.32" steps="346"/></proof>
</goal>
<goal name="VC main.31" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="52"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
<goal name="VC main.32" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.29" steps="970"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.33" steps="970"/></proof>
</goal>
<goal name="VC main.33" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="84"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="84"/></proof>
</goal>
<goal name="VC main.34" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.13" steps="57"/></proof>
+ <proof prover="4"><result status="valid" time="0.06" steps="57"/></proof>
</goal>
<goal name="VC main.35" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="78"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.35.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.10" steps="78"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.36" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.23" steps="323"/></proof>
+ <proof prover="4"><result status="valid" time="0.15" steps="323"/></proof>
</goal>
<goal name="VC main.37" expl="loop invariant preservation" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC main.37.0" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="41"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="41"/></proof>
</goal>
<goal name="VC main.37.1" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.27" steps="719"/></proof>
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.33" steps="719"/></proof>
</goal>
<goal name="VC main.37.2" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.12" steps="188"/></proof>
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.07" steps="188"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.38" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
+ <proof prover="5"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC main.39" expl="loop invariant preservation" proved="true">
- <proof prover="1"><result status="valid" time="0.11"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.39.0" expl="VC for main" proved="true">
+ <proof prover="5"><result status="valid" time="0.16"/></proof>
+ </goal>
+ <goal name="VC main.39.1" expl="VC for main" proved="true">
+ <proof prover="5"><result status="valid" time="0.53"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.40" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="VC main.41" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="138"/></proof>
</goal>
<goal name="VC main.42" expl="loop invariant preservation" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC main.42.0" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="45"/></proof>
- </goal>
- <goal name="VC main.42.1" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="45"/></proof>
- </goal>
- </transf>
+ <proof prover="4"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="VC main.43" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.44" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.44.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.03" steps="45"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.45" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -327,7 +329,24 @@
<proof prover="4"><result status="valid" time="0.13" steps="33"/></proof>
</goal>
<goal name="VC main.47" expl="liveness" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <transf name="revert" proved="true" arg1="H41">
+ <goal name="VC main.47.0" expl="liveness" proved="true">
+ <transf name="split_goal_full" proved="true" >
+ <goal name="VC main.47.0.0" expl="liveness" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="48"/></proof>
+ </goal>
+ <goal name="VC main.47.0.1" expl="liveness" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="VC main.47.0.2" expl="liveness" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="144"/></proof>
+ </goal>
+ <goal name="VC main.47.0.3" expl="liveness" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="109"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.48" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
@@ -424,7 +443,7 @@
<proof prover="4"><result status="valid" time="0.03" steps="112"/></proof>
</goal>
<goal name="VC main.56.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.08" steps="109"/></proof>
+ <proof prover="4"><result status="valid" time="0.08" steps="123"/></proof>
</goal>
<goal name="VC main.56.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="47"/></proof>
@@ -436,7 +455,7 @@
<proof prover="4"><result status="valid" time="0.10" steps="195"/></proof>
</goal>
<goal name="VC main.56.5" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.01" steps="203"/></proof>
+ <proof prover="4"><result status="valid" time="0.11" steps="203"/></proof>
</goal>
</transf>
</goal>
@@ -605,39 +624,28 @@
<proof prover="4"><result status="valid" time="0.18" steps="242"/></proof>
</goal>
<goal name="VC main.68" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.68.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.90" steps="361"/></proof>
- </goal>
- </transf>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.87" steps="361"/></proof>
</goal>
<goal name="VC main.69" expl="loop invariant preservation" proved="true">
- <transf name="case" proved="true" arg1="(th=th1)">
- <goal name="VC main.69.0" expl="true case (loop invariant preservation)" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="63"/></proof>
- </goal>
- <goal name="VC main.69.1" expl="false case (loop invariant preservation)" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.55" steps="818"/></proof>
- </goal>
- </transf>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.88" steps="1114"/></proof>
</goal>
<goal name="VC main.70" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.70.0" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.64" steps="292"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="VC main.70.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.73" steps="292"/></proof>
</goal>
- <goal name="VC main.70.1" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="1.06" steps="1287"/></proof>
+ <goal name="VC main.70.1" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="1.41" steps="1467"/></proof>
</goal>
- <goal name="VC main.70.2" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="1.02" steps="1349"/></proof>
+ <goal name="VC main.70.2" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="1.15" steps="1384"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.71" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="th=th1">
<goal name="VC main.71.0" expl="true case (loop invariant preservation)" proved="true">
- <proof prover="4"><result status="valid" time="0.06" steps="143"/></proof>
+ <proof prover="4"><result status="valid" time="0.08" steps="143"/></proof>
</goal>
<goal name="VC main.71.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="replace" proved="true" arg1="memo[th]" arg2="memo1[th]">
@@ -645,23 +653,35 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC main.71.1.1" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="49"/></proof>
+ <proof prover="4"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC main.72" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="1.67"/></proof>
+ <proof prover="0" timelimit="10" memlimit="1000"><result status="valid" time="1.63"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.72.0" expl="VC for main" proved="true">
+ <proof prover="5"><result status="valid" time="0.18"/></proof>
+ </goal>
+ <goal name="VC main.72.1" expl="VC for main" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="VC main.72.1.0" expl="VC for main" proved="true">
+ <proof prover="2" timelimit="30" memlimit="4000"><result status="valid" time="11.81" steps="3770"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.73" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.11" steps="45"/></proof>
</goal>
<goal name="VC main.74" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.06" steps="53"/></proof>
+ <proof prover="4"><result status="valid" time="0.07" steps="53"/></proof>
</goal>
<goal name="VC main.75" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="1.48" steps="567"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="1.45" steps="567"/></proof>
</goal>
<goal name="VC main.76" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="65"/></proof>
@@ -671,58 +691,45 @@
<goal name="VC main.77.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(elts waiting_list <> Nil)">
<goal name="VC main.77.0.0" proved="true">
- <proof prover="4"><result status="valid" time="0.06" steps="70"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="70"/></proof>
</goal>
<goal name="VC main.77.0.1" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="56"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="56"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC main.78" expl="loop invariant preservation" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC main.78.0" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.78.0.0" expl="loop invariant preservation" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.08" steps="49"/></proof>
- </goal>
- </transf>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.78.0" expl="VC for main" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="VC main.78.1" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="VC main.78.1" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.05" steps="296"/></proof>
</goal>
- <goal name="VC main.78.2" expl="loop invariant preservation" proved="true">
+ <goal name="VC main.78.2" expl="VC for main" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="VC main.78.3" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <goal name="VC main.78.3" expl="VC for main" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="VC main.78.4" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.78.4.0" expl="loop invariant preservation" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.04" steps="121"/></proof>
- </goal>
- </transf>
+ <goal name="VC main.78.4" expl="VC for main" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="VC main.78.5" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.78.5.0" expl="loop invariant preservation" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.05" steps="47"/></proof>
- </goal>
- </transf>
+ <goal name="VC main.78.5" expl="VC for main" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="VC main.78.6" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.06" steps="193"/></proof>
+ <goal name="VC main.78.6" expl="VC for main" proved="true">
+ <proof prover="4"><result status="valid" time="0.08" steps="205"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.79" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.23"/></proof>
- <proof prover="4"><result status="valid" time="0.19" steps="217"/></proof>
+ <proof prover="4"><result status="valid" time="0.13" steps="217"/></proof>
</goal>
<goal name="VC main.80" expl="liveness" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="52"/></proof>
</goal>
<goal name="VC main.81" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -764,226 +771,266 @@
<goal name="VC main.89" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.89.0" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.48" steps="1095"/></proof>
+ <proof prover="4"><result status="valid" time="0.48" steps="1058"/></proof>
</goal>
<goal name="VC main.89.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.10" steps="41"/></proof>
+ <proof prover="4"><result status="valid" time="0.10" steps="39"/></proof>
</goal>
<goal name="VC main.89.2" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="1.64" steps="834"/></proof>
+ <proof prover="4"><result status="valid" time="1.63" steps="801"/></proof>
</goal>
<goal name="VC main.89.3" expl="assertion" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.07" steps="163"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.07" steps="152"/></proof>
</goal>
<goal name="VC main.89.4" expl="assertion" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="44"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main.89.5" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="65"/></proof>
+ <proof prover="4"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
<goal name="VC main.89.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC main.89.7" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="112"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="107"/></proof>
</goal>
<goal name="VC main.89.8" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.90" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.90.0" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="44"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC main.90.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="44"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="42"/></proof>
</goal>
<goal name="VC main.90.2" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="50"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="VC main.90.3" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="46"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC main.90.4" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.11" steps="95"/></proof>
+ <proof prover="4"><result status="valid" time="0.11" steps="89"/></proof>
</goal>
<goal name="VC main.90.5" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="125"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="118"/></proof>
</goal>
<goal name="VC main.90.6" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.13" steps="136"/></proof>
+ <proof prover="4"><result status="valid" time="0.13" steps="129"/></proof>
</goal>
<goal name="VC main.90.7" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="54"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="52"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.91" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.91.0" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.39" steps="288"/></proof>
+ <proof prover="4"><result status="valid" time="0.39" steps="278"/></proof>
</goal>
<goal name="VC main.91.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="43"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="41"/></proof>
</goal>
<goal name="VC main.91.2" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="2.55" steps="1555"/></proof>
+ <proof prover="4"><result status="valid" time="2.55" steps="1512"/></proof>
</goal>
<goal name="VC main.91.3" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.60" steps="630"/></proof>
+ <proof prover="4"><result status="valid" time="0.60" steps="632"/></proof>
</goal>
<goal name="VC main.91.4" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="48"/></proof>
+ <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="318"/></proof>
+ <proof prover="4"><result status="valid" time="0.16" steps="305"/></proof>
</goal>
<goal name="VC main.91.6" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.72" steps="1159"/></proof>
+ <proof prover="4"><result status="valid" time="0.72" steps="1120"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.92" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.92.0" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.23" steps="442"/></proof>
+ <proof prover="4"><result status="valid" time="0.23" steps="422"/></proof>
</goal>
<goal name="VC main.92.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.09" steps="239"/></proof>
+ <proof prover="4"><result status="valid" time="0.09" steps="223"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.93" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.93.0" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.16" steps="346"/></proof>
+ <proof prover="4"><result status="valid" time="0.16" steps="338"/></proof>
</goal>
<goal name="VC main.93.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="44"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC main.93.2" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.98" steps="1497"/></proof>
+ <proof prover="4"><result status="valid" time="0.98" steps="1473"/></proof>
</goal>
<goal name="VC main.93.3" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="231"/></proof>
+ <proof prover="4"><result status="valid" time="0.04" steps="219"/></proof>
</goal>
<goal name="VC main.93.4" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.19" steps="206"/></proof>
+ <proof prover="4"><result status="valid" time="0.19" steps="199"/></proof>
</goal>
<goal name="VC main.93.5" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="53"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="51"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.94" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.94.0" expl="assertion" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="3.20" steps="3773"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="3.20" steps="3733"/></proof>
</goal>
<goal name="VC main.94.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="44"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC main.94.2" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="3.34" steps="1129"/></proof>
+ <proof prover="4"><result status="valid" time="2.64" steps="1095"/></proof>
</goal>
<goal name="VC main.94.3" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="53"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="51"/></proof>
</goal>
<goal name="VC main.94.4" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.11" steps="176"/></proof>
+ <proof prover="4"><result status="valid" time="0.11" steps="166"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.95" expl="safety" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.22" steps="293"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.22" steps="284"/></proof>
</goal>
<goal name="VC main.96" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.97" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.63" steps="636"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.63" steps="607"/></proof>
</goal>
<goal name="VC main.98" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.34" steps="569"/></proof>
+ <proof prover="4"><result status="valid" time="0.34" steps="545"/></proof>
</goal>
<goal name="VC main.99" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.09" steps="110"/></proof>
+ <proof prover="4"><result status="valid" time="0.09" steps="102"/></proof>
</goal>
<goal name="VC main.100" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.101" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="56"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="54"/></proof>
</goal>
<goal name="VC main.102" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="113"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.102.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.06" steps="107"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.103" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.56" steps="746"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.39" steps="689"/></proof>
</goal>
<goal name="VC main.104" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.12" steps="242"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.104.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.03" steps="52"/></proof>
+ </goal>
+ <goal name="VC main.104.1" expl="VC for main" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="282"/></proof>
+ </goal>
+ <goal name="VC main.104.2" expl="VC for main" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.09" steps="287"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.105" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="3.74" steps="1713"/></proof>
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
+ <proof prover="3"><result status="valid" time="3.78"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="3.60" steps="1676"/></proof>
</goal>
<goal name="VC main.106" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.41" steps="598"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.36" steps="562"/></proof>
</goal>
<goal name="VC main.107" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.26" steps="341"/></proof>
+ <proof prover="4"><result status="valid" time="0.19" steps="326"/></proof>
</goal>
<goal name="VC main.108" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.58" steps="865"/></proof>
+ <proof prover="4"><result status="valid" time="0.60" steps="898"/></proof>
</goal>
<goal name="VC main.109" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.109.0" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="59"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="57"/></proof>
</goal>
<goal name="VC main.109.1" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.96" steps="557"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.96" steps="542"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.110" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.93" steps="507"/></proof>
+ <proof prover="2"><result status="valid" time="0.71" steps="1165"/></proof>
</goal>
<goal name="VC main.111" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.06"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="VC main.111.0" expl="loop invariant preservation" proved="true">
+ <transf name="assert" proved="true" arg1="(elts waiting_list <> Nil)">
+ <goal name="VC main.111.0.0" proved="true">
+ <proof prover="4"><result status="valid" time="0.06" steps="183"/></proof>
+ </goal>
+ <goal name="VC main.111.0.1" expl="loop invariant preservation" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="1.76" steps="879"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.112" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.112.0" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="47"/></proof>
+ <proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC main.112.1" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="1.74" steps="1031"/></proof>
+ <proof prover="2"><result status="valid" time="0.83" steps="1250"/></proof>
</goal>
<goal name="VC main.112.2" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="3.86" steps="1078"/></proof>
+ <proof prover="2"><result status="valid" time="0.72" steps="1279"/></proof>
</goal>
<goal name="VC main.112.3" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="2.57" steps="1392"/></proof>
+ <proof prover="2"><result status="valid" time="0.73" steps="1231"/></proof>
</goal>
<goal name="VC main.112.4" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="47"/></proof>
+ <proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC main.112.5" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="47"/></proof>
+ <proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC main.112.6" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.07" steps="47"/></proof>
+ <proof prover="5"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.113" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <proof prover="4"><result status="valid" time="0.10" steps="183"/></proof>
</goal>
<goal name="VC main.114" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="48"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.114.0" expl="liveness" proved="true">
+ <proof prover="4"><result status="valid" time="0.05" steps="46"/></proof>
+ </goal>
+ <goal name="VC main.114.1" expl="liveness" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="VC main.114.2" expl="liveness" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="VC main.114.3" expl="liveness" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.115" expl="safety" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="44"/></proof>
@@ -1017,172 +1064,66 @@
<proof prover="4"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
<goal name="VC main.124" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.124.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.03" steps="40"/></proof>
- </goal>
- <goal name="VC main.124.1" expl="VC for main" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="190"/></proof>
- </goal>
- <goal name="VC main.124.2" expl="VC for main" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.09" steps="199"/></proof>
- </goal>
- </transf>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.14" steps="170"/></proof>
</goal>
<goal name="VC main.125" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="0.09"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="123"/></proof>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC main.126" expl="loop invariant preservation" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.16" steps="358"/></proof>
</goal>
<goal name="VC main.127" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="31"/></proof>
+ <proof prover="4"><result status="valid" time="0.10" steps="31"/></proof>
</goal>
<goal name="VC main.128" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.128.0" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="31"/></proof>
- </goal>
- </transf>
+ <proof prover="4"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
<goal name="VC main.129" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="VC main.129.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.03" steps="43"/></proof>
+ </goal>
+ <goal name="VC main.129.1" expl="loop invariant preservation" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="43"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.130" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="43"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="43"/></proof>
</goal>
<goal name="VC main.131" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC main.132" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.132.0" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="33"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="33"/></proof>
</goal>
<goal name="VC main.132.1" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="4"><result status="valid" time="0.04" steps="48"/></proof>
</goal>
<goal name="VC main.132.2" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="44"/></proof>
</goal>
<goal name="VC main.132.3" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="43"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="43"/></proof>
</goal>
<goal name="VC main.132.4" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="67"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="67"/></proof>
</goal>
<goal name="VC main.132.5" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.06" steps="32"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.11" steps="32"/></proof>
</goal>
<goal name="VC main.132.6" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.08" steps="100"/></proof>
+ <proof prover="4"><result status="valid" time="0.10" steps="100"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.133" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.12" steps="31"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main.134" expl="liveness" proved="true">
- <transf name="revert" proved="true" arg1="H41">
- <goal name="VC main.134.0" expl="liveness" proved="true">
- <transf name="split_goal_full" proved="true" >
- <goal name="VC main.134.0.0" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC main.134.0.1" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.01"/></proof>
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC main.134.0.2" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC main.134.0.3" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC main.134.0.4" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC main.134.0.5" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC main.134.0.6" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC main.134.0.7" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC main.134.0.8" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="53"/></proof>
- </goal>
- <goal name="VC main.134.0.9" expl="liveness" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="VC main.134.0.10" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="216"/></proof>
- </goal>
- <goal name="VC main.134.0.11" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="210"/></proof>
- </goal>
- <goal name="VC main.134.0.12" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="VC main.134.0.13" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC main.134.0.14" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.05"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.15" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.06"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.16" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.06"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.17" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.03"/></proof>
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC main.134.0.18" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.19" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.06"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.20" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.21" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC main.134.0.22" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC main.134.0.23" expl="liveness" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main.135" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1206,31 +1147,52 @@
<proof prover="4"><result status="valid" time="0.08" steps="84"/></proof>
</goal>
<goal name="VC main.142" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.06" steps="57"/></proof>
+ <proof prover="4"><result status="valid" time="0.12" steps="57"/></proof>
</goal>
<goal name="VC main.143" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.06" steps="78"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.143.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.04" steps="78"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.144" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.88" steps="2527"/></proof>
+ <transf name="case" proved="true" arg1="(th=th1)">
+ <goal name="VC main.144.0" expl="true case (loop invariant preservation)" proved="true">
+ <proof prover="4"><result status="valid" time="0.04" steps="54"/></proof>
+ </goal>
+ <goal name="VC main.144.1" expl="false case (loop invariant preservation)" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.55" steps="1579"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.145" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.14" steps="299"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.145.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.02" steps="41"/></proof>
+ </goal>
+ <goal name="VC main.145.1" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.80" steps="2178"/></proof>
+ </goal>
+ <goal name="VC main.145.2" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.26" steps="782"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.146" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.38" steps="875"/></proof>
+ <proof prover="5"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC main.147" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="1.79" steps="1953"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="1.88" steps="1953"/></proof>
</goal>
<goal name="VC main.148" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.10" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.11" steps="32"/></proof>
</goal>
<goal name="VC main.149" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.10" steps="138"/></proof>
</goal>
<goal name="VC main.150" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="48"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="VC main.151" expl="loop invariant preservation" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="45"/></proof>
@@ -1264,21 +1226,22 @@
</transf>
</goal>
<goal name="VC main.154" expl="loop invariant preservation" proved="true">
+ <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC main.155" expl="liveness" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC main.155.0" expl="liveness" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="41"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="41"/></proof>
</goal>
<goal name="VC main.155.1" expl="liveness" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.155.2" expl="liveness" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.12" steps="140"/></proof>
</goal>
<goal name="VC main.155.3" expl="liveness" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
</transf>
</goal>
@@ -1304,90 +1267,87 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main.163" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.12" steps="57"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.13" steps="57"/></proof>
</goal>
<goal name="VC main.164" expl="loop invariant preservation" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC main.164.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.10" steps="78"/></proof>
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.165" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.87" steps="2364"/></proof>
+ <proof prover="0"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="VC main.166" expl="loop invariant preservation" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC main.166.0" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="41"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.166.0" expl="VC for main" proved="true">
+ <proof prover="4"><result status="valid" time="0.04" steps="41"/></proof>
</goal>
- <goal name="VC main.166.1" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.57" steps="1701"/></proof>
+ <goal name="VC main.166.1" expl="VC for main" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.57" steps="1348"/></proof>
</goal>
- <goal name="VC main.166.2" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.08" steps="324"/></proof>
+ <goal name="VC main.166.2" expl="VC for main" proved="true">
+ <proof prover="4"><result status="valid" time="0.14" steps="349"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.167" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.26" steps="602"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.21" steps="602"/></proof>
</goal>
<goal name="VC main.168" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="1.35"/></proof>
+ <proof prover="0"><result status="valid" time="1.64"/></proof>
<proof prover="3"><result status="valid" time="0.93"/></proof>
</goal>
<goal name="VC main.169" expl="loop invariant preservation" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="VC main.170" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="138"/></proof>
- </goal>
- <goal name="VC main.171" expl="loop invariant preservation" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC main.171.0" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="45"/></proof>
- </goal>
- <goal name="VC main.171.1" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="45"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.170.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.04" steps="152"/></proof>
</goal>
</transf>
</goal>
+ <goal name="VC main.171" expl="loop invariant preservation" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
<goal name="VC main.172" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="45"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="45"/></proof>
</goal>
<goal name="VC main.173" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.174" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.174.0" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="VC main.174.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="35"/></proof>
</goal>
- <goal name="VC main.174.1" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.05" steps="50"/></proof>
+ <goal name="VC main.174.1" expl="loop invariant preservation" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="VC main.174.2" expl="VC for main" proved="true">
+ <goal name="VC main.174.2" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="VC main.174.3" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="VC main.174.3" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.04" steps="45"/></proof>
</goal>
- <goal name="VC main.174.4" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <goal name="VC main.174.4" expl="loop invariant preservation" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="67"/></proof>
</goal>
- <goal name="VC main.174.5" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="VC main.174.5" expl="loop invariant preservation" proved="true">
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.06" steps="34"/></proof>
</goal>
- <goal name="VC main.174.6" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.08" steps="112"/></proof>
+ <goal name="VC main.174.6" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.08" steps="98"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.175" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.10" steps="33"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="33"/></proof>
</goal>
<goal name="VC main.176" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.14" steps="175"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.177" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -1409,103 +1369,112 @@
</transf>
</goal>
<goal name="VC main.180" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.181" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.182" expl="safety" proved="true">
- <proof prover="4"><result status="valid" time="0.18" steps="408"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.20" steps="408"/></proof>
</goal>
<goal name="VC main.183" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="VC main.184" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.69" steps="887"/></proof>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC main.185" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="173"/></proof>
+ <proof prover="4"><result status="valid" time="0.04" steps="173"/></proof>
</goal>
<goal name="VC main.186" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="1.87" steps="2224"/></proof>
+ <proof prover="4"><result status="valid" time="2.12" steps="2224"/></proof>
</goal>
<goal name="VC main.187" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.28" steps="929"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.29" steps="929"/></proof>
</goal>
<goal name="VC main.188" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.11" steps="63"/></proof>
</goal>
<goal name="VC main.189" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.189.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.04" steps="104"/></proof>
- </goal>
- </transf>
+ <proof prover="4"><result status="valid" time="0.06" steps="94"/></proof>
</goal>
<goal name="VC main.190" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="1.21" steps="3515"/></proof>
+ <proof prover="4"><result status="valid" time="1.36" steps="3515"/></proof>
</goal>
<goal name="VC main.191" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.191.0" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="47"/></proof>
- </goal>
- <goal name="VC main.191.1" expl="VC for main" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.76" steps="2007"/></proof>
- </goal>
- <goal name="VC main.191.2" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.46" steps="1504"/></proof>
- </goal>
- </transf>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.28" steps="676"/></proof>
</goal>
<goal name="VC main.192" expl="loop invariant preservation" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.19" steps="339"/></proof>
</goal>
<goal name="VC main.193" expl="loop invariant preservation" proved="true">
- <proof prover="1"><result status="valid" time="0.14"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC main.194" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="VC main.195" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.07" steps="172"/></proof>
+ <proof prover="4"><result status="valid" time="0.15" steps="172"/></proof>
</goal>
<goal name="VC main.196" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="54"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.196.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.03" steps="51"/></proof>
+ </goal>
+ <goal name="VC main.196.1" expl="VC for main" proved="true">
+ <proof prover="4"><result status="valid" time="0.02" steps="51"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.197" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.198" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.198.0" expl="VC for main" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.03" steps="51"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="VC main.199" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.199.0" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="VC main.199.0" expl="loop invariant preservation" proved="true">
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.199.0.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.08" steps="39"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="VC main.199.1" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="VC main.199.1" expl="loop invariant preservation" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="VC main.199.2" expl="VC for main" proved="true">
+ <goal name="VC main.199.2" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="VC main.199.3" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="VC main.199.3" expl="loop invariant preservation" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="VC main.199.4" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="VC main.199.4" expl="loop invariant preservation" proved="true">
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.199.4.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.04" steps="91"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="VC main.199.5" expl="VC for main" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="VC main.199.5" expl="loop invariant preservation" proved="true">
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC main.199.5.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.05" steps="38"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="VC main.199.6" expl="VC for main" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="122"/></proof>
+ <goal name="VC main.199.6" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.06" steps="122"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.200" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.12" steps="37"/></proof>
</goal>
<goal name="VC main.201" expl="liveness" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1542,7 +1511,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main.210" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.211" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -1661,25 +1630,21 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.14" steps="48"/></proof>
</goal>
<goal name="VC main.221" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.221.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.24" steps="321"/></proof>
- </goal>
- </transf>
+ <proof prover="4"><result status="valid" time="2.61" steps="691"/></proof>
</goal>
<goal name="VC main.222" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="1.50"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="2.66" steps="1419"/></proof>
</goal>
<goal name="VC main.223" expl="loop invariant preservation" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC main.223.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="1.66" steps="700"/></proof>
+ <proof prover="4"><result status="valid" time="1.81" steps="700"/></proof>
</goal>
<goal name="VC main.223.1" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="1.13" steps="1125"/></proof>
+ <proof prover="4"><result status="valid" time="1.10" steps="1125"/></proof>
</goal>
<goal name="VC main.223.2" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="6.47" steps="1077"/></proof>
+ <proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="2.14" steps="1073"/></proof>
</goal>
</transf>
</goal>
@@ -1691,73 +1656,62 @@
<goal name="VC main.224.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="replace" proved="true" arg1="memo[th]" arg2="memo1[th]">
<goal name="VC main.224.1.0" expl="false case (loop invariant preservation)" proved="true">
- <proof prover="3"><result status="valid" time="0.07"/></proof>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC main.224.1.1" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="52"/></proof>
+ <proof prover="4"><result status="valid" time="0.04" steps="52"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC main.225" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.16" steps="283"/></proof>
+ <proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC main.226" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.11" steps="48"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="VC main.227" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.15" steps="231"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="231"/></proof>
</goal>
<goal name="VC main.228" expl="loop invariant preservation" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.228.0" expl="VC for main" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="0.03" steps="63"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="VC main.228.0" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
- <goal name="VC main.228.1" expl="VC for main" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="63"/></proof>
+ <goal name="VC main.228.1" expl="loop invariant preservation" proved="true">
+ <proof prover="4"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.229" expl="loop invariant preservation" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="63"/></proof>
</goal>
<goal name="VC main.230" expl="loop invariant preservation" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC main.230.0" expl="loop invariant preservation" proved="true">
- <transf name="assert" proved="true" arg1="(elts waiting_list <> Nil)">
- <goal name="VC main.230.0.0" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.27" steps="452"/></proof>
- </goal>
- <goal name="VC main.230.0.1" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.04" steps="64"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.231" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.231.0" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="49"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="VC main.231.1" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.04" steps="83"/></proof>
+ <proof prover="4"><result status="valid" time="0.05" steps="83"/></proof>
</goal>
<goal name="VC main.231.2" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="83"/></proof>
+ <proof prover="4"><result status="valid" time="0.06" steps="83"/></proof>
</goal>
<goal name="VC main.231.3" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.05" steps="83"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.05" steps="83"/></proof>
</goal>
<goal name="VC main.231.4" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.10" steps="67"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="67"/></proof>
</goal>
<goal name="VC main.231.5" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.11" steps="50"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="VC main.231.6" expl="loop invariant preservation" proved="true">
- <proof prover="4"><result status="valid" time="0.10" steps="68"/></proof>
+ <proof prover="4"><result status="valid" time="0.07" steps="68"/></proof>
</goal>
</transf>
</goal>
@@ -1765,20 +1719,7 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.13" steps="49"/></proof>
</goal>
<goal name="VC main.233" expl="liveness" proved="true">
- <transf name="split_all_full" proved="true" >
- <goal name="VC main.233.0" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.24" steps="182"/></proof>
- </goal>
- <goal name="VC main.233.1" expl="liveness" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC main.233.2" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.12" steps="51"/></proof>
- </goal>
- <goal name="VC main.233.3" expl="liveness" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.02" steps="52"/></proof>
- </goal>
- </transf>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.66" steps="465"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz
index 9c6f7208a1a07e2dde5ddfbe0faf7401b1e1af09..861bc0598e44090f263d43696873559568880137 100644
Binary files a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz and b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz differ
diff --git a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml
index 8dc2758de1f2a43896ab4f813f8cc974832968d1..210b805d1c4c8d57a4143c09aa4b206a4ab8c341 100644
--- a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml
+++ b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml
@@ -4,6 +4,7 @@
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2018_le_rouge_et_le_noir_1.mlw" proved="true">
<theory name="ColoredTiles" proved="true">
@@ -305,169 +306,45 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC addleft_result" expl="VC for addleft_result" proved="true">
- <transf name="split_vc" proved="true" >
+ <transf name="split_goal_right" proved="true" >
<goal name="VC addleft_result.0" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="2"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="VC addleft_result.1" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC addleft_result.2" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC addleft_result.3" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC addleft_result.4" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC addleft_result.5" expl="assertion" proved="true">
- <transf name="subst" proved="true" arg1="o">
- <goal name="VC addleft_result.5.0" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="H">
- <goal name="VC addleft_result.5.0.0" expl="assertion" proved="true">
- <transf name="subst" proved="true" arg1="o1">
- <goal name="VC addleft_result.5.0.0.0" expl="assertion" proved="true">
- <transf name="subst" proved="true" arg1="o">
- <goal name="VC addleft_result.5.0.0.0.0" expl="assertion" proved="true">
- <transf name="unfold" proved="true" arg1="cnrm">
- <goal name="VC addleft_result.5.0.0.0.0.0" expl="assertion" proved="true">
- <transf name="apply" proved="true" arg1="app_eq">
- <goal name="VC addleft_result.5.0.0.0.0.0.0" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="VC addleft_result.5.0.0.0.0.0.1" proved="true">
- <transf name="apply" proved="true" arg1="ext">
- <goal name="VC addleft_result.5.0.0.0.0.0.1.0" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC addleft_result.6" expl="assertion" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC addleft_result.6.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.40" steps="301"/></proof>
+ <transf name="split_all_full" proved="true" >
+ <goal name="VC addleft_result.6.0" expl="VC for addleft_result" proved="true">
+ <proof prover="2"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC addleft_result.6.1" expl="VC for addleft_result" proved="true">
- <transf name="apply" proved="true" arg1="ext">
- <goal name="VC addleft_result.6.1.0" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
- </goal>
- </transf>
+ <proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
<goal name="VC addleft_result.7" expl="assertion" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="VC addleft_result.7.0" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC addleft_result.7.1" expl="assertion" proved="true">
- <transf name="subst" proved="true" arg1="o">
- <goal name="VC addleft_result.7.1.0" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="<-" arg2="H1">
- <goal name="VC addleft_result.7.1.0.0" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="VC addleft_result.7.2" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="cons_def">
- <goal name="VC addleft_result.7.2.0" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="cons_def">
- <goal name="VC addleft_result.7.2.0.0" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="cons_def">
- <goal name="VC addleft_result.7.2.0.0.0" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="associative">
- <goal name="VC addleft_result.7.2.0.0.0.0" expl="assertion" proved="true">
- <transf name="apply" proved="true" arg1="app_eq">
- <goal name="VC addleft_result.7.2.0.0.0.0.0" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC addleft_result.7.2.0.0.0.0.1" proved="true">
- <transf name="apply" proved="true" arg1="app_eq">
- <goal name="VC addleft_result.7.2.0.0.0.0.1.0" proved="true">
- <transf name="apply" proved="true" arg1="ext">
- <goal name="VC addleft_result.7.2.0.0.0.0.1.0.0" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="VC addleft_result.7.2.0.0.0.0.1.1" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="VC addleft_result.7.3" expl="assertion" proved="true">
- <transf name="subst" proved="true" arg1="o">
- <goal name="VC addleft_result.7.3.0" expl="assertion" proved="true">
- <transf name="rewrite" proved="true" arg1="H">
- <goal name="VC addleft_result.7.3.0.0" expl="assertion" proved="true">
- <transf name="apply" proved="true" arg1="app_eq">
- <goal name="VC addleft_result.7.3.0.0.0" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="VC addleft_result.7.3.0.0.1" proved="true">
- <transf name="apply" proved="true" arg1="ext">
- <goal name="VC addleft_result.7.3.0.0.1.0" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="VC addleft_result.7.4" expl="VC for addleft_result" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
+ <proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC addleft_result.8" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC addleft_result.8.0" expl="postcondition" proved="true">
- <transf name="case" proved="true" arg1="(nr = 0)">
- <goal name="VC addleft_result.8.0.0" expl="true case (postcondition)" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="VC addleft_result.8.0.1" expl="false case (postcondition)" proved="true">
- <transf name="eliminate_let" proved="true" >
- <goal name="VC addleft_result.8.0.1.0" expl="false case (postcondition)" proved="true">
- <transf name="apply" proved="true" arg1="H">
- <goal name="VC addleft_result.8.0.1.0.0" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="VC addleft_result.8.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
@@ -750,7 +627,7 @@
<proof prover="0"><result status="valid" time="0.16" steps="657"/></proof>
</goal>
<goal name="VC enum.10.1.2" expl="VC for enum" proved="true">
- <proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="4.60" steps="5902"/></proof>
+ <proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="5.51" steps="5902"/></proof>
</goal>
</transf>
</goal>
@@ -770,11 +647,7 @@
<goal name="VC enum.13.1" expl="assertion" proved="true">
<transf name="subst" proved="true" arg1="sets">
<goal name="VC enum.13.1.0" expl="assertion" proved="true">
- <transf name="subst" proved="true" arg1="o">
- <goal name="VC enum.13.1.0.0" expl="assertion" proved="true">
- <transf name="apply" proved="true" arg1="h">
- </transf>
- </goal>
+ <transf name="apply" proved="true" arg1="h">
</transf>
</goal>
</transf>
@@ -907,13 +780,13 @@
</transf>
</goal>
<goal name="VC enum.19" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.20" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.21" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.22" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -922,16 +795,16 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.24" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.25" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.26" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="45"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="45"/></proof>
</goal>
<goal name="VC enum.27" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.11" steps="45"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="45"/></proof>
</goal>
<goal name="VC enum.28" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
@@ -998,7 +871,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="140"/></proof>
</goal>
<goal name="VC enum.34" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC enum.35" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1007,7 +880,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.37" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.38" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.13"/></proof>
@@ -1019,7 +892,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.41" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.42" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -1028,13 +901,13 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC enum.44" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.45" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC enum.46" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC enum.47" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
@@ -1098,10 +971,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.52" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="59"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="VC enum.53" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="59"/></proof>
+ <proof prover="0"><result status="valid" time="0.11" steps="59"/></proof>
</goal>
<goal name="VC enum.54" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="170"/></proof>
@@ -1142,33 +1015,33 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.60" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.11" steps="49"/></proof>
+ <proof prover="0"><result status="valid" time="0.11" steps="50"/></proof>
</goal>
<goal name="VC enum.61" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.11" steps="295"/></proof>
+ <proof prover="0"><result status="valid" time="0.11" steps="296"/></proof>
</goal>
<goal name="VC enum.62" expl="assertion" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC enum.62.0" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC enum.62.0.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.52" steps="2233"/></proof>
+ <proof prover="0"><result status="valid" time="0.52" steps="2234"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC enum.63" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC enum.64" expl="index in array bounds" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.65" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC enum.66" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.32"/></proof>
+ <proof prover="3"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="VC enum.67" expl="index in array bounds" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -1176,13 +1049,13 @@
<goal name="VC enum.68" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC enum.68.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.16" steps="369"/></proof>
+ <proof prover="0"><result status="valid" time="0.16" steps="370"/></proof>
</goal>
<goal name="VC enum.68.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.06" steps="192"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="193"/></proof>
</goal>
<goal name="VC enum.68.2" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="1.15"/></proof>
+ <proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
</transf>
</goal>
@@ -1192,37 +1065,37 @@
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC enum.69.1" expl="VC for enum" proved="true">
- <proof prover="1"><result status="valid" time="0.51"/></proof>
+ <proof prover="1"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="VC enum.69.2" expl="VC for enum" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC enum.69.3" expl="VC for enum" proved="true">
- <proof prover="0"><result status="valid" time="0.09" steps="220"/></proof>
+ <proof prover="0"><result status="valid" time="0.22" steps="455"/></proof>
</goal>
</transf>
</goal>
<goal name="VC enum.70" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="59"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="60"/></proof>
</goal>
<goal name="VC enum.71" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="59"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="60"/></proof>
</goal>
<goal name="VC enum.72" expl="loop invariant preservation" proved="true">
- <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.33" steps="798"/></proof>
+ <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.33" steps="799"/></proof>
</goal>
<goal name="VC enum.73" expl="loop invariant preservation" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC enum.73.0" expl="VC for enum" proved="true">
- <proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="0.62" steps="1167"/></proof>
+ <proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="0.62" steps="1168"/></proof>
</goal>
<goal name="VC enum.73.1" expl="VC for enum" proved="true">
- <proof prover="0" timelimit="10"><result status="valid" time="0.34" steps="628"/></proof>
+ <proof prover="0" timelimit="10"><result status="valid" time="0.34" steps="629"/></proof>
</goal>
</transf>
</goal>
<goal name="VC enum.74" expl="loop invariant preservation" proved="true">
- <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.38" steps="861"/></proof>
+ <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.38" steps="862"/></proof>
</goal>
<goal name="VC enum.75" expl="out of loop bounds" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
diff --git a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz
index c526a2bbb077b4b73436564485df578264ebc7b4..162636d5ceb80489f3574aa0a59a130d5c71329c 100644
Binary files a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz and b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz differ
diff --git a/examples/verifythis_2018_mind_the_gap_2/why3session.xml b/examples/verifythis_2018_mind_the_gap_2/why3session.xml
index ce23f8e099aeebbc8de4e5fe3bfe7a544d028720..a0ffd482dd9c21fbe86c88278ef0fe1e389a6131 100644
--- a/examples/verifythis_2018_mind_the_gap_2/why3session.xml
+++ b/examples/verifythis_2018_mind_the_gap_2/why3session.xml
@@ -24,13 +24,13 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC left.4" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="56"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="61"/></proof>
</goal>
<goal name="VC left.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC left.6" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
</transf>
</goal>
@@ -49,13 +49,13 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC right.4" expl="postcondition" proved="true">
- <proof prover="0" memlimit="2000"><result status="valid" time="0.02" steps="52"/></proof>
+ <proof prover="0" memlimit="2000"><result status="valid" time="0.02" steps="61"/></proof>
</goal>
<goal name="VC right.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC right.6" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
</transf>
</goal>
@@ -99,10 +99,10 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC insert.2" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC insert.3" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="173"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="188"/></proof>
</goal>
<goal name="VC insert.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -111,10 +111,10 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC insert.6" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC insert.7" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="94"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="115"/></proof>
</goal>
</transf>
</goal>
@@ -124,7 +124,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delete.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC delete.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
diff --git a/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz b/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz
index a2c928e1e5b8a80a9f4f258855c69298e72f34d6..a785d104cd3d3a08e33b37faa2867d146a055ca9 100644
Binary files a/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz and b/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz differ
diff --git a/examples/vstte12_combinators/why3session.xml b/examples/vstte12_combinators/why3session.xml
index bebd30f30f5ce3a047ef5fb4c56c5366ddb1332c..cc0947f83485dc3e54a52d2fdd49ecf8685c9cec 100644
--- a/examples/vstte12_combinators/why3session.xml
+++ b/examples/vstte12_combinators/why3session.xml
@@ -5,6 +5,7 @@
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../vstte12_combinators.mlw" proved="true">
<theory name="Combinators" proved="true">
<goal name="VC eq" expl="VC for eq" proved="true">
@@ -87,70 +88,60 @@
<goal name="VC value_in_context" expl="VC for value_in_context" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC value_in_context.0" expl="variant decrease" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.1" expl="precondition" proved="true">
- <transf name="destruct_alg_subst" proved="true" arg1="(subst c t)">
+ <transf name="destruct_alg_subst" proved="true" arg1="(subst x1 t)">
<goal name="VC value_in_context.1.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.1.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.1.2" expl="precondition" proved="true">
- <transf name="destruct_alg_subst" proved="true" arg1="x3">
+ <transf name="destruct_alg_subst" proved="true" arg1="x2">
<goal name="VC value_in_context.1.2.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_in_context.1.2.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_in_context.1.2.2" expl="precondition" proved="true">
- <transf name="destruct_alg_subst" proved="true" arg1="x4">
- <goal name="VC value_in_context.1.2.2.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="VC value_in_context.1.2.2.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="VC value_in_context.1.2.2.2" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC value_in_context.2" expl="variant decrease" proved="true">
- <proof prover="2"><result status="valid" time="0.03"/></proof>
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.3" expl="precondition" proved="true">
- <transf name="destruct_alg_subst" proved="true" arg1="(subst c t)">
+ <transf name="destruct_alg_subst" proved="true" arg1="(subst x t)">
<goal name="VC value_in_context.3.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.2" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="x3">
<goal name="VC value_in_context.3.2.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.2.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_in_context.3.2.2" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="x4">
<goal name="VC value_in_context.3.2.2.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.2.2.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_in_context.3.2.2.2" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/vstte12_combinators/why3shapes.gz b/examples/vstte12_combinators/why3shapes.gz
index c9b8d23adb15e9b5270070d185d17e687c593835..0469fa3c568c71ea7f35bf772065cacf063202fa 100644
Binary files a/examples/vstte12_combinators/why3shapes.gz and b/examples/vstte12_combinators/why3shapes.gz differ
diff --git a/src/transform/introduction.ml b/src/transform/introduction.ml
index e26026ead36ed47110a63f91834574e87749b643..f90d2d3c702c476853906c94d2528185513ca10e 100644
--- a/src/transform/introduction.ml
+++ b/src/transform/introduction.ml
@@ -278,11 +278,6 @@ let () = Trans.register_transform
(Trans.decl eliminate_exists None)
~desc:"Replace axioms of the form 'exists x. P' by 'constant x axiom P'."
-let simplify_intros =
- Trans.compose Simplify_formula.simplify_trivial_wp_quantification
- introduce_premises
-
-(*
let subst_filter ls =
Sattr.mem intro_attr ls.ls_name.id_attrs &&
not (Ident.has_a_model_attr ls.ls_name)
@@ -290,7 +285,6 @@ let subst_filter ls =
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered subst_filter)
-*)
let split_vc =
Trans.compose_l
@@ -301,5 +295,4 @@ let () = Trans.register_transform_l
"split_vc" split_vc
~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ \
on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ \
- by@ simplify_trivial_quantifications@ followed@ by@ \
- introduce_premises)."
+ by@ introduce_premises@ followed@ by@ subst_all)."