updated obsolete sessions

examples/add_list/why3session.xml

@@ -71,7 +71,7 @@
     locfile="../add_list.mlw"
     loclnum="44" loccnumb="4" loccnume="8"
     expl="VC for main"
-    sum="127fcdeab244cfbe4aec7fce6fdb7015"
+    sum="1e59a24fb282a191a17e4debdff0ca6e"
     proved="true"
     expanded="true"
     shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
@@ -106,7 +106,7 @@
     locfile="../add_list.mlw"
     loclnum="63" loccnumb="4" loccnume="7"
     expl="VC for sum"
-    sum="1c4542683e081bd2f3c3310ee00d1644"
+    sum="113394ababdb929cb6daae79f2cf228e"
     proved="true"
     expanded="true"
     shape="itCV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FfIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
@@ -134,7 +134,7 @@
     locfile="../add_list.mlw"
     loclnum="86" loccnumb="4" loccnume="8"
     expl="VC for main"
-    sum="80a39093aaa0fa258939e15895a7ebf1"
+    sum="9a71ed6f77f4b28ff9d67782ed191026"
     proved="true"
     expanded="true"
     shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">

examples/algo64/why3session.xml

@@ -43,7 +43,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="1. precondition"
-      sum="14d442b4820bcd8a9b4451df6a4b26b0"
+      sum="153b0a4ec87c1b7e4f4d4bc2ccec7568"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -63,7 +63,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="2. variant decrease"
-      sum="baaff721097293a6b7300bf2ebadade8"
+      sum="d52fa8437c333e33dfcab95b688273a1"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -83,7 +83,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="3. precondition"
-      sum="d75ab7d682afc5e6ce4fcecba4b6b9bf"
+      sum="d824dc170165d3d1bd7f3e8aa5e84688"
       proved="true"
       expanded="true"
       shape="ainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -103,7 +103,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="4. assertion"
-      sum="a5d2ec75c570aab7ea1d4214627ec136"
+      sum="a2985e78ef08b400f95948a9160374ea"
       proved="true"
       expanded="true"
       shape="apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -123,7 +123,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="5. variant decrease"
-      sum="c3367cf5d49eba7c5470313bd16c122a"
+      sum="f1c89158dd889a67f6ec2b53de972207"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -143,7 +143,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="6. precondition"
-      sum="c28c61c377b86f8f567e7faa06beb325"
+      sum="74c8e5dfdcaff3e9e3b7cf11e06af710"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -163,7 +163,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="7. assertion"
-      sum="3a8a5f4370467868497a7044ff8b4b14"
+      sum="ffc073f16103d696d99568ec5ba9f74a"
       proved="true"
       expanded="true"
       shape="apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -183,7 +183,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="8. postcondition"
-      sum="993ac877509f5322a1f21b7ea6ee0b88"
+      sum="08fdd2672d24fafbe0f05ee5f635f6e9"
       proved="true"
       expanded="true"
       shape="apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -203,7 +203,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="9. postcondition"
-      sum="de7baf4df5c0adb5ede8feab3eec1f5d"
+      sum="35ebeae2f5fbe5224561cff570ab23b9"
       proved="true"
       expanded="true"
       shape="asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -231,7 +231,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="10. postcondition"
-      sum="ed3209cafe36a6b310b180fc021fac82"
+      sum="e6bf165a8862cc0215e1fe933570e6fe"
       proved="true"
       expanded="true"
       shape="apermut_subV3V3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -251,7 +251,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="11. postcondition"
-      sum="8239ff0463764f17dfdff17f3552b48c"
+      sum="07f6b005264964017be91678f79e1b36"
       proved="true"
       expanded="true"
       shape="asorted_subV3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">

examples/arm/why3session.xml

@@ -50,7 +50,7 @@
     locfile="../arm.mlw"
     loclnum="120" loccnumb="6" loccnume="18"
     expl="VC for path_init_l2"
-    sum="be65e531a5cbe80f994990f8c4c9def6"
+    sum="19ae2913cea5458fb6929fc9f238efaf"
     proved="true"
     expanded="true"
     shape="ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F">
@@ -78,7 +78,7 @@
     locfile="../arm.mlw"
     loclnum="127" loccnumb="6" loccnume="18"
     expl="VC for path_l2_exit"
-    sum="bf489e6e0f7c734a74e018900e78e6a4"
+    sum="bca45c9a7ef7fbe8792f11db8c6319ef"
     proved="true"
     expanded="true"
     shape="ainfix =V0c9Iainfix =V4aFalseIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F">

examples/assigning_meanings_to_programs/why3session.xml

@@ -51,7 +51,7 @@
     locfile="../assigning_meanings_to_programs.mlw"
     loclnum="38" loccnumb="6" loccnume="14"
     expl="VC for division"
-    sum="352ca50c3d4c76f18b7506ce94f9c734"
+    sum="4177aab49b97cc922d533db26f687096"
     proved="true"
     expanded="true"
     shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F">

examples/binary_search/why3session.xml

@@ -36,7 +36,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.17"/>
     </proof>
     <proof
      prover="1"
@@ -59,7 +59,7 @@
     locfile="../binary_search.mlw"
     loclnum="60" loccnumb="6" loccnume="19"
     expl="VC for binary_search"
-    sum="2ded482b93801cf9ecea5676d0a962b6"
+    sum="5954021440d95809176c18fd90076bd1"
     proved="true"
     expanded="true"
     shape="iainfix &lt;=V4V3iainfix &lt;agetV2V5V1ainfix &lt;ainfix -V3V6ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V7V3Aainfix &lt;=V6V7Iainfix =agetV2V7V1Iainfix &lt;V7V0Aainfix &lt;=c0V7FAainfix &lt;V3V0Aainfix &lt;=c0V6Iainfix =V6ainfix +V5c1Fiainfix &gt;agetV2V5V1ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix &lt;=V5V3Aainfix &lt;=V4V5FAainfix &lt;=V4V3ainfix =agetV2V10V1NIainfix &lt;V10V0Aainfix &lt;=c0V10FIainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
@@ -86,7 +86,7 @@
     locfile="../binary_search.mlw"
     loclnum="100" loccnumb="6" loccnume="19"
     expl="VC for binary_search"
-    sum="b37d691aded290cf8f122f4c3f686b9b"
+    sum="5b4387f4a334e94903ccf100c1be36b8"
     proved="true"
     expanded="true"
     shape="iainfix &lt;=V4V3iainfix &lt;agetV2V6V1ainfix &lt;ainfix -V3V7ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V3Aainfix &lt;=V7V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V3V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V6c1FAainfix &lt;=ainfix +V6c1amax_intAainfix &lt;=amin_intainfix +V6c1iainfix &gt;agetV2V6V1ainfix &lt;ainfix -V9V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V9Aainfix &lt;=V4V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V9V0Aainfix &lt;=c0V4Iainfix =V9ainfix -V6c1FAainfix &lt;=ainfix -V6c1amax_intAainfix &lt;=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=V6V3Aainfix &lt;=V4V6Lainfix +V4adivV5c2Aainfix &lt;=ainfix +V4adivV5c2amax_intAainfix &lt;=amin_intainfix +V4adivV5c2Lainfix -V3V4Aainfix &lt;=ainfix -V3V4amax_intAainfix &lt;=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix &lt;V11V0Aainfix &lt;=c0V11FIainfix &lt;=V12V3Aainfix &lt;=V4V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V13ainfix -V0c1Aainfix &lt;=c0V13Iainfix =agetV2V13V1Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Aainfix &lt;=ainfix -V0c1amax_intAainfix &lt;=amin_intainfix -V0c1Iainfix &lt;=agetV2V14agetV2V15Iainfix &lt;V15V0Aainfix &lt;=V14V15Aainfix &lt;=c0V14FAainfix &lt;=V0amax_intAainfix &lt;=c0V0FF">
@@ -98,7 +98,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.16"/>
+     <result status="valid" time="0.80"/>
     </proof>
    </goal>
   </theory>

examples/binary_sqrt/why3session.xml

@@ -39,7 +39,7 @@
       locfile="../binary_sqrt.mlw"
       loclnum="11" loccnumb="10" loccnume="14"
       expl="1. postcondition"
-      sum="251e9c36cabe9e7b9541d0f06a00b8da"
+      sum="79254120c3e4af8106f3cdeac0a909e2"
       proved="true"
       expanded="true"
       shape="ainfix <V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix <=ainfix *c0.c0.V0Iainfix <c1.V1Aainfix <V0V1Iainfix <c0.V1Aainfix <=c0.V0F">
@@ -59,7 +59,7 @@
       locfile="../binary_sqrt.mlw"
       loclnum="11" loccnumb="10" loccnume="14"
       expl="2. precondition"
-      sum="63b9ff6626db8664fff81a5f7ae74ffb"
+      sum="4ba0f0d5cc8e31fd68cbb64d33e924b0"
       proved="true"
       expanded="true"
       shape="ainfix <c0.ainfix *c2.V1Aainfix <=c0.V0Iainfix <c1.V1Aainfix <V0V1NIainfix <c0.V1Aainfix <=c0.V0F">
@@ -79,7 +79,7 @@
       locfile="../binary_sqrt.mlw"
       loclnum="11" loccnumb="10" loccnume="14"
       expl="3. postcondition"
-      sum="82efdbe2db3161daca3a638eb5423416"
+      sum="f85232ad6aec8823270dceb2eb6f02b1"
       proved="true"
       expanded="true"
       shape="ainfix <V0ainfix *ainfix +iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V1ainfix +iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V1Aainfix <=ainfix *iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2iainfix <=ainfix *ainfix +V2V1ainfix +V2V1V0ainfix +V2V1V2V0Iainfix <V0ainfix *ainfix +V2ainfix *c2.V1ainfix +V2ainfix *c2.V1Aainfix <=ainfix *V2V2V0FIainfix <c0.ainfix *c2.V1Aainfix <=c0.V0Iainfix <c1.V1Aainfix <V0V1NIainfix <c0.V1Aainfix <=c0.V0F">

examples/bitvectors/double/why3session.xml

@@ -63,7 +63,7 @@
     name="nth_one2"
     locfile="../double.why"
     loclnum="74" loccnumb="8" loccnume="16"
-    sum="5477c865128db4a06170fe56521033ea"
+    sum="6c5ab56d5ca58c8563265ef1e76caaff"
     proved="true"
     expanded="true"
     shape="ainfix =anthaoneV0aTrueIainfix <=V0c61Aainfix <=c52V0F">
@@ -80,7 +80,7 @@
     name="nth_one3"
     locfile="../double.why"
     loclnum="75" loccnumb="8" loccnume="16"
-    sum="4e7b6a6c83accd8455de3bcec4837f83"
+    sum="9b7649e3d4b50c0652cca89ce17ffb16"
     proved="true"
     expanded="false"
     shape="ainfix =anthaoneV0aFalseIainfix <=V0c63Aainfix <=c62V0F">
@@ -90,14 +90,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.62"/>
+     <result status="valid" time="0.31"/>
     </proof>
    </goal>
    <goal
     name="sign_one"
     locfile="../double.why"
     loclnum="77" loccnumb="8" loccnume="16"
-    sum="83d7589239f4c6d2e0b47583806bbcb0"
+    sum="4d768e8050c8a290ad59f6fb9c3648f3"
     proved="true"
     expanded="false"
     shape="ainfix =asignaoneaFalse">
@@ -146,7 +146,7 @@
     name="exp_one"
     locfile="../double.why"
     loclnum="78" loccnumb="8" loccnume="15"
-    sum="13ba2625ca3b65718fabd943e1118361"
+    sum="5cc0aeaf0df1030578dc94096e87e552"
     proved="true"
     expanded="false"
     shape="ainfix =aexpaonec1023">
@@ -156,7 +156,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.77"/>
+     <result status="valid" time="1.63"/>
     </proof>
     <proof
      prover="3"
@@ -172,7 +172,7 @@
     name="mantissa_one"
     locfile="../double.why"
     loclnum="79" loccnumb="8" loccnume="20"
-    sum="d68b4d3fc28fe2b05825830ca598d542"
+    sum="911f111a48f29e043cd6271df6d92b7b"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaaonec0">
@@ -205,7 +205,7 @@
     name="double_value_of_1"
     locfile="../double.why"
     loclnum="81" loccnumb="8" loccnume="25"
-    sum="ea478edc5021232fd4ec18211014adc7"
+    sum="3c554760bb4cb8554fc679a00a8da995"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64aonec1.0">

examples/bitvectors/neg_as_xor/why3session.xml

@@ -56,7 +56,7 @@
     name="sign_of_j"
     locfile="../neg_as_xor.why"
     loclnum="15" loccnumb="8" loccnume="17"
-    sum="7b992f0a4a99d2dd8aae9c7d40278786"
+    sum="497dc675e45b2db4dad3ac9ac57894ba"
     proved="true"
     expanded="true"
     shape="ainfix =asignajaTrue">
@@ -73,7 +73,7 @@
     name="mantissa_of_j"
     locfile="../neg_as_xor.why"
     loclnum="16" loccnumb="8" loccnume="21"
-    sum="8e1c2eee6de312bd6c82d7cbd1732b05"
+    sum="ba45c67869c2b86e0a2ce419b0bcfa19"
     proved="true"
     expanded="true"
     shape="ainfix =amantissaajc0">
@@ -122,7 +122,7 @@
     name="exp_of_j"
     locfile="../neg_as_xor.why"
     loclnum="17" loccnumb="8" loccnume="16"
-    sum="372763ac7057bf0479a0525ae7232e67"
+    sum="ca84bfe984f0638331493bb8e52727da"
     proved="true"
     expanded="true"
     shape="ainfix =aexpajc0">
@@ -171,7 +171,7 @@
     name="int_of_bv"
     locfile="../neg_as_xor.why"
     loclnum="18" loccnumb="8" loccnume="17"
-    sum="4763b9cc56af1466f0d3108247919fd7"
+    sum="3e0d947e2994b4f99cd11906a7700aba"
     proved="true"
     expanded="true"
     shape="ainfix =adouble_of_bv64ajc0.0">
@@ -220,7 +220,7 @@
     name="MainResultBits"
     locfile="../neg_as_xor.why"
     loclnum="20" loccnumb="8" loccnume="22"
-    sum="f9c9fe0f29f9376ea99027e00a082411"
+    sum="1a697819ec0cbae299653ca632f5f1f4"
     proved="true"
     expanded="true"
     shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix <V1c63Aainfix <=c0V1FF">
@@ -245,7 +245,7 @@
     name="MainResultSign"
     locfile="../neg_as_xor.why"
     loclnum="23" loccnumb="8" loccnume="22"
-    sum="6ac0e368139525cdc5eedf4b769ab059"
+    sum="18ddc34735ee8af58fd72b703041d953"
     proved="true"
     expanded="true"
     shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
@@ -270,7 +270,7 @@
     name="Sign_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="25" loccnumb="8" loccnume="21"
-    sum="602f83b9ace3a2e59586724412ca3130"
+    sum="67da7e6f5b583e2adde22650d74059ef"
     proved="true"
     expanded="true"
     shape="ainfix =asignabw_xorV0ajanotbasignV0F">
@@ -319,7 +319,7 @@
     name="Exp_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="27" loccnumb="8" loccnume="20"
-    sum="5f45026471fde20dda83ced0e62d734a"
+    sum="2b0fb2b39ee0b71651449f67ff8412b8"
     proved="true"
     expanded="true"
     shape="ainfix =aexpabw_xorV0ajaexpV0F">
@@ -360,7 +360,7 @@
     name="Mantissa_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="29" loccnumb="8" loccnume="25"
-    sum="9b73a75fc27480d6d0839e2be297e2f9"
+    sum="e4819744b3225fae14c6be40ea5ddabd"
     proved="true"
     expanded="true"
     shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
@@ -401,7 +401,7 @@
     name="MainResultZero"
     locfile="../neg_as_xor.why"
     loclnum="31" loccnumb="8" loccnume="22"
-    sum="994df33f05bbfbc0789f5fa722860871"
+    sum="350d1e94fdacee12e4a02f4851da9e75"
     proved="true"
     expanded="true"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
@@ -450,7 +450,7 @@
     name="sign_neg"
     locfile="../neg_as_xor.why"
     loclnum="34" loccnumb="8" loccnume="16"
-    sum="ca5190c335e6b10c88de7d9ae77b3a6d"
+    sum="d86dc14cd3ca2f95f975108838091849"
     proved="true"
     expanded="true"
     shape="ainfix =asign_valueanotbasignV0aprefix -.asign_valueasignV0F">
@@ -475,7 +475,7 @@
     name="MainResult"
     locfile="../neg_as_xor.why"
     loclnum="36" loccnumb="8" loccnume="18"
-    sum="0527e74303854de8721478d3f66f58e0"
+    sum="25abfbe70a15d3f664614891fe738283"
     proved="true"
     expanded="true"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix <aexpV0c2047Aainfix <c0aexpV0F">

examples/bresenham/why3session.xml

@@ -50,7 +50,7 @@
     locfile="../bresenham.mlw"
     loclnum="37" loccnumb="6" loccnume="15"
     expl="VC for bresenham"
-    sum="fe09ae734dc2879db30932410f48877f"
+    sum="736302fef90c12f3a196a9e494b6371c"
     proved="true"
     expanded="true"
     shape="iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
@@ -65,7 +65,7 @@
       locfile="../bresenham.mlw"
       loclnum="37" loccnumb="6" loccnume="15"
       expl="1. loop invariant init"
-      sum="bd81b4fdc325ed4c1817f2fe8ba0534c"
+      sum="e4caaafdcfd3fbf6a6f8e26a5a2f738c"
       proved="true"
       expanded="true"
       shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
@@ -101,7 +101,7 @@
       locfile="../bresenham.mlw"
       loclnum="37" loccnumb="6" loccnume="15"
       expl="2. assertion"
-      sum="d25ea2d770fc42bc51c4f38f2f096402"
+      sum="2d47ce5f0b792d072f91e114587cab0c"
       proved="true"
       expanded="true"
       shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2F">
@@ -113,7 +113,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.12"/>
+       <result status="valid" time="0.33"/>
       </proof>
       <proof
        prover="1"
@@ -129,7 +129,7 @@
       locfile="../bresenham.mlw"
       loclnum="37" loccnumb="6" loccnume="15"
       expl="3. loop invariant preservation"
-      sum="59e10792d717223c19c8e4837192ca5e"
+      sum="168f0b247960a9dfb57a7096bd2efd23"
       proved="true"
       expanded="true"
       shape="ainvariant_V4V1V3Aainfix &lt;=V4ainfix +ax2c1Aainfix &lt;=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix &lt;V0c0IabestV2V1Iainfix &lt;=V2ax2Iainvariant_V2V1V0Aainfix &lt;=V2ainfix +ax2c1Aainfix &lt;=c0V2F">
@@ -157,7 +157,7 @@
       locfile="../bresenham.mlw"
       loclnum="37" loccnumb="6" loccnume="15"
       expl="4. loop variant decrease"
-      sum="ee4f95539c19c762bcba88e2ce78969d"
+      sum="a83d16777345a751f88200e197c81fcb"
       proved="true"
       expanded="true"
       shape="ainfix &lt;ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix &lt;=c0ainfix -ainfix +ax2c1V2Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix &lt;V0c0IabestV2V1Iainfix &lt;=V2ax2Iainvariant_V2V1V0Aainfix &lt;=V2ainfix +ax2c1Aainfix &lt;=c0V2F">
@@ -193,7 +193,7 @@
       locfile="../bresenham.mlw"
       loclnum="37" loccnumb="6" loccnume="15"
       expl="5. loop invariant preservation"
-      sum="40b416abffcc09273f6398805f4443d9"
+      sum="cedcc39ff09d00d69cff5e7168358c03"
       proved="true"
       expanded="true"
       shape="ainvariant_V5V3V4Aainfix &lt;=V5ainfix +ax2c1Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix &lt;V0c0NIabestV2V1Iainfix &lt;=V2ax2Iainvariant_V2V1V0Aainfix &lt;=V2ainfix +ax2c1Aainfix &lt;=c0V2F">
@@ -221,7 +221,7 @@
       locfile="../bresenham.mlw"
       loclnum="37" loccnumb="6" loccnume="15"
       expl="6. loop variant decrease"
-      sum="faab75dd68890e792537dd45a28fc2d9"
+      sum="1ca0b146fd9f3bd8b0837a3d6037871e"
       proved="true"
       expanded="true"
       shape="ainfix &lt;ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix &lt;=c0ainfix -ainfix +ax2c1V2Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix &lt;V0c0NIabestV2V1Iainfix &lt;=V2ax2Iainvariant_V2V1V0Aainfix &lt;=V2ainfix +ax2c1Aainfix &lt;=c0V2F">

examples/bts/13853/why3session.xml

@@ -38,9 +38,9 @@
    <goal
     name="WP_parameter g"
     locfile="../13853.mlw"
-    loclnum="18" loccnumb="8" loccnume="9"
+    loclnum="17" loccnumb="8" loccnume="9"
     expl="VC for g"
-    sum="d1ffc8c2c26ed4983c02dfc6585d5cfc"
+    sum="671340a818a92578552fd5fec6035817"
     proved="true"
     expanded="false"
     shape="t">

examples/bts/13854/why3session.xml

@@ -37,7 +37,7 @@
     name="x"
     locfile="../13854.why"
     loclnum="8" loccnumb="7" loccnume="8"
-    sum="ba32ebfe4b80558ad1d3f7feea2edd39"
+    sum="435ec01d268249598a20febc4e71aa3b"
     proved="true"
     expanded="true"
     shape="ainfix =aAaTuple0aBN">

examples/bts/fsetint/why3session.xml

@@ -103,7 +103,7 @@
     name="mem_integer"
     locfile="../fsetint.why"
     loclnum="13" loccnumb="8" loccnume="19"
-    sum="7d2a234b1f346b41796c44ccad2aab56"
+    sum="9ffa692caa04cddd289b902664e6d758"
     proved="false"
     expanded="true"
     shape="amemV0aintegerF">
@@ -160,7 +160,7 @@
     name="foo"
     locfile="../fsetint.why"
     loclnum="15" loccnumb="7" loccnume="10"
-    sum="ebe87aa3b38585553fcbdcdb64f97aa6"
+    sum="98f6e78fbd3f6e82548f42970ed744cc"
     proved="false"
     expanded="true"
     shape="f">
@@ -224,7 +224,7 @@
     name="foo"
     locfile="../fsetint.why"
     loclnum="30" loccnumb="7" loccnume="10"
-    sum="1c7eb0d2bb90b9326b27e12a6ecb3571"
+    sum="b82f29b3068c71a75e3b2ba964080211"
     proved="false"
     expanded="true"
     shape="f">

examples/check-builtin/ac/why3session.xml

@@ -72,7 +72,7 @@
     name="G2"
     locfile="../ac.why"
     loclnum="6" loccnumb="12" loccnume="14"
-    sum="e06054735062c16b430a6567a13b93c5"
+    sum="103962acd732d3cb59ce50596f0b8f05"
     proved="true"
     expanded="true"
     shape="ainfix =afafV0V1V2afV0afV1V2F">

examples/check-builtin/array/why3session.xml

@@ -96,7 +96,7 @@
     name="G2"
     locfile="../array.why"
     loclnum="6" loccnumb="7" loccnume="9"
-    sum="967864cdce2b291ed2fb7e58f3da73b7"
+    sum="38bd50e1a687c7a7c325602b465c4535"
     proved="true"
     expanded="true"
     shape="ainfix =agetasetV4V0V3V2V1Iainfix =agetV4V2V1Iainfix =V2V0NFF">
@@ -153,7 +153,7 @@
     name="G3"
     locfile="../array.why"
     loclnum="10" loccnumb="7" loccnume="9"
-    sum="22d64a682cbaa87a659cbad9ef966a6c"
+    sum="4daa75e79ebd968dc3edcc45287c92ee"
     proved="true"
     expanded="true"
     shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
@@ -210,7 +210,7 @@
     name="G4"
     locfile="../array.why"
     loclnum="13" loccnumb="7" loccnume="9"
-    sum="ed7aa4648b1ebe314c2ffb999e036fb0"
+    sum="d10b305a403914fcf89d2be61c20641c"
     proved="true"
     expanded="true"
     shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">

examples/check-builtin/bool/why3session.xml

@@ -72,7 +72,7 @@
     name="G2"
     locfile="../bool.why"
     loclnum="5" loccnumb="11" loccnume="13"
-    sum="efd2761635736fe9f7e1c96978337792"
+    sum="bc31588c69598f7eb53de8570583977e"
     proved="true"
     expanded="true"
     shape="ainfix =V0aFalseOainfix =V0aTrueF">
@@ -113,7 +113,7 @@
     name="G3"
     locfile="../bool.why"
     loclnum="6" loccnumb="11" loccnume="13"
-    sum="89e5bebeb38bdbb1abf2b1818c837e25"
+    sum="748209c7ed2ad6f059044132d8222014"
     proved="true"
     expanded="true"
     shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">

examples/check-builtin/euclideandivision/why3session.xml

@@ -84,7 +84,7 @@
     name="G2"
     locfile="../euclideandivision.why"
     loclnum="4" loccnumb="12" loccnume="14"
-    sum="4cabfbebf4f8e8b354b818911c84a23b"
+    sum="745918b963a9d41966c5586359bca763"
     proved="true"
     expanded="true"
     shape="ainfix =adivc10c3c3">

examples/check-builtin/floats/why3session.xml

@@ -48,7 +48,7 @@
     name="Round_double_01"
     locfile="../floats.why"
     loclnum="14" loccnumb="7" loccnume="22"
-    sum="524b958620ee72b56a88d39ddf10c66b"
+    sum="ae7284b960a7438f854da5237df9ca40"
     proved="true"
     expanded="true"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
@@ -65,7 +65,7 @@
     name="Test00"
     locfile="../floats.why"
     loclnum="17" loccnumb="8" loccnume="14"
-    sum="2406a4444efbdf06656af7797c88b2ec"
+    sum="c9368b1862f1132ca9bd5e0b90ea8ff7"
     proved="true"
     expanded="true"
     shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
@@ -106,7 +106,7 @@
     name="Test01"
     locfile="../floats.why"
     loclnum="19" loccnumb="8" loccnume="14"
-    sum="0a734b398a8f3398c372be9d801b0f1f"
+    sum="91b6a4c39189389865537962fa8ecd63"
     proved="true"
     expanded="true"
     shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
@@ -123,7 +123,7 @@
     name="Test02"
     locfile="../floats.why"
     loclnum="25" loccnumb="8" loccnume="14"
-    sum="619f18054ab61d7e55d5e0d69c2261d0"