mjrty.mlw: added an Alt-Ergo proof

parent f9932cac
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
<why3session
name="programs/mjrty/why3session.xml">
name="examples/programs/mjrty/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -13,16 +13,16 @@
<file
name="../mjrty.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="WP Mjrty"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="23" loccnumb="7" loccnume="12"
verified="true"
expanded="true">
<goal
name="WP_parameter mjrty"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="parameter mjrty"
sum="fc07dad1d800281bea37ac841b0af063"
......@@ -37,12 +37,12 @@
expanded="true">
<goal
name="WP_parameter mjrty.1"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="precondition"
sum="72eeaf0a52b00587bb44186cf7684c34"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -57,12 +57,12 @@
</goal>
<goal
name="WP_parameter mjrty.2"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="8c80860154d704d8feccbf25d6ed8201"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V2c0V0V0FIainfix =c0c0Iainfix &gt;c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -77,12 +77,12 @@
</goal>
<goal
name="WP_parameter mjrty.3"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="17a6b30882551a3e38238bc1f914b344"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;ainfix *c2anum_ofaTuple2V1agetV1c0c0V0V0Iainfix &gt;ainfix *c2c0V0Iainfix =c0c0NIainfix &gt;c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -97,12 +97,12 @@
</goal>
<goal
name="WP_parameter mjrty.4"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="f50957fa579c515f37062b6fd7a1c0da"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V3c0V0V0FIainfix &gt;c0ainfix -V0c1Iainfix =V2c0FIainfix &gt;ainfix *c2c0V0NIainfix =c0c0NIainfix &gt;c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -117,12 +117,12 @@
</goal>
<goal
name="WP_parameter mjrty.5"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop initialization"
sum="b6cb140b96afe8ef7d7a5217f8351ad9"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2V2V0Aainfix =V2anum_ofaTuple2V1agetV1c0c0c0Iainfix &lt;=c0ainfix -V0c1Iainfix =V2c0FIainfix &gt;ainfix *c2c0V0NIainfix =c0c0NIainfix &gt;c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -137,12 +137,12 @@
</goal>
<goal
name="WP_parameter mjrty.6"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="abc62c9d552926387dceed07066c9874"
proved="true"
expanded="false"
expanded="true"
shape="iainfix =agetV1V4agetV1c0iainfix &gt;ainfix *c2V5V0ainfix &gt;ainfix *c2anum_ofaTuple2V1agetV1c0c0V0V0ainfix &lt;=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1agetV1c0c0ainfix +V4c1Aainfix =V5anum_ofaTuple2V1agetV1c0c0ainfix +V4c1Iainfix =V5ainfix +V3c1Fainfix &lt;=ainfix *c2V3V0Aainfix =V3anum_ofaTuple2V1agetV1c0c0ainfix +V4c1Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;=ainfix *c2V3V0Aainfix =V3anum_ofaTuple2V1agetV1c0c0V4Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFIainfix &lt;=c0ainfix -V0c1Iainfix =V2c0FIainfix &gt;ainfix *c2c0V0NIainfix =c0c0NIainfix &gt;c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -157,12 +157,12 @@
</goal>
<goal
name="WP_parameter mjrty.7"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="1f54e3602eec3b1b3c091f358710a41b"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V4c0V0V0FIainfix &lt;=ainfix *c2V3V0Aainfix =V3anum_ofaTuple2V1agetV1c0c0ainfix +ainfix -V0c1c1FIainfix &lt;=c0ainfix -V0c1Iainfix =V2c0FIainfix &gt;ainfix *c2c0V0NIainfix =c0c0NIainfix &gt;c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -177,12 +177,12 @@
</goal>
<goal
name="WP_parameter mjrty.8"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop initialization"
sum="d5bc8a2e764b6b76b3840971b2685abc"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V2c0c0ainfix -c0c0Iainfix =V2agetV1c0NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1agetV1c0c0c0c0ainfix -c0c0Aainfix &gt;=anum_ofaTuple2V1agetV1c0c0c0c0Aainfix &lt;=c0c0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -197,12 +197,12 @@
</goal>
<goal
name="WP_parameter mjrty.9"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="36b007adbdb89de59cb69962619b1580"
proved="true"
expanded="false"
expanded="true"
shape="iainfix =V2c0ainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0ainfix +V4c1ainfix -ainfix +V4c1V6Iainfix =V7V5NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V5c0ainfix +V4c1V6ainfix -ainfix +V4c1V6Aainfix &gt;=anum_ofaTuple2V1V5c0ainfix +V4c1V6Aainfix &lt;=V6ainfix +V4c1Aainfix &lt;=c0V6Iainfix =V6c1FIainfix =V5agetV1V4FAainfix &lt;V4V0Aainfix &lt;=c0V4iainfix =V3agetV1V4ainfix &lt;=ainfix *c2anum_ofaTuple2V1V9c0ainfix +V4c1ainfix -ainfix +V4c1V8Iainfix =V9V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V8ainfix -ainfix +V4c1V8Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +V4c1V8Aainfix &lt;=V8ainfix +V4c1Aainfix &lt;=c0V8Iainfix =V8ainfix +V2c1Fainfix &lt;=ainfix *c2anum_ofaTuple2V1V11c0ainfix +V4c1ainfix -ainfix +V4c1V10Iainfix =V11V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V10ainfix -ainfix +V4c1V10Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +V4c1V10Aainfix &lt;=V10ainfix +V4c1Aainfix &lt;=c0V10Iainfix =V10ainfix -V2c1FAainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V12c0V4ainfix -V4V2Iainfix =V12V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -212,12 +212,12 @@
expanded="true">
<goal
name="WP_parameter mjrty.9.1"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="ef671dc1cbd85f14d605cf5fe6289788"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V5c0V4ainfix -V4V2Iainfix =V5V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -232,12 +232,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.2"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="491957b4f10a589522afc356557a6a81"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=c0V6Iainfix =V6c1FIainfix =V5agetV1V4FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -252,12 +252,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.3"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="d71352978ebb1c695941d6c38206fddf"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=V6ainfix +V4c1Iainfix =V6c1FIainfix =V5agetV1V4FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -272,12 +272,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.4"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="b03849daab50bf8bc79dcafd13c65228"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anum_ofaTuple2V1V5c0ainfix +V4c1V6Iainfix =V6c1FIainfix =V5agetV1V4FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -292,12 +292,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.5"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="1f2604bc1d8a9511b4202d252a3f74c6"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V5c0ainfix +V4c1V6ainfix -ainfix +V4c1V6Iainfix =V6c1FIainfix =V5agetV1V4FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -312,15 +312,23 @@
</goal>
<goal
name="WP_parameter mjrty.9.6"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="0c77e013c6e8c3f8203706e3f652102a"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0ainfix +V4c1ainfix -ainfix +V4c1V6Iainfix =V7V5NFIainfix =V6c1FIainfix =V5agetV1V4FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V8c0V4ainfix -V4V2Iainfix =V8V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
<proof
prover="0"
timelimit="10"
memlimit="800"
obsolete="false"
archived="false">
<result status="valid" time="3.74"/>
</proof>
<proof
prover="1"
timelimit="10"
......@@ -332,12 +340,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.7"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="a2ddeec6e45416ed38bb9b1a9ab745dc"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V5c0V4ainfix -V4V2Iainfix =V5V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -352,12 +360,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.8"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="6eed3cedf1e031652a323570b08bdee6"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=c0V5Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -372,12 +380,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.9"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="a06fa0d63e33592dd8ccc177008337a7"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=V5ainfix +V4c1Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -392,12 +400,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.10"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="2cbdbc310b13b0c48ad62169e113373c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anum_ofaTuple2V1V3c0ainfix +V4c1V5Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -412,12 +420,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.11"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="99ba45fb45a9e12f97a8f39569f82671"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V5ainfix -ainfix +V4c1V5Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -432,12 +440,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.12"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="7f8a9586a6d91f71ef95fc9bd273ba38"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0ainfix +V4c1ainfix -ainfix +V4c1V5Iainfix =V6V3NFIainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -452,12 +460,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.13"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="b33bbdd15f8ff527046b81ad3109dbf7"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=c0V5Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -472,12 +480,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.14"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="9b4fa8da561c9a7c4a52bde72fa58647"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=V5ainfix +V4c1Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -492,12 +500,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.15"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="05f62a0dcff079ecc838ed1f8f02a5c3"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anum_ofaTuple2V1V3c0ainfix +V4c1V5Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -512,12 +520,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.16"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="d8ce8bc02073ec66a684a5e1be84cc0f"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V5ainfix -ainfix +V4c1V5Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -532,12 +540,12 @@
</goal>
<goal
name="WP_parameter mjrty.9.17"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="10d9f9f5f1b998fad179ff340542c8c0"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0ainfix +V4c1ainfix -ainfix +V4c1V5Iainfix =V6V3NFIainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix &gt;=anum_ofaTuple2V1V3c0V4V2Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &lt;=V4ainfix -V0c1Aainfix &lt;=c0V4FFFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -554,12 +562,12 @@
</goal>
<goal
name="WP_parameter mjrty.10"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="64008301ef496d82543c243b16b7b06c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V4c0V0V0FIainfix =V2c0Iainfix &lt;=ainfix *c2anum_ofaTuple2V1V5c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V5V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -574,12 +582,12 @@
</goal>
<goal
name="WP_parameter mjrty.11"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="a6cb7408237241994e49db39717f6016"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;ainfix *c2anum_ofaTuple2V1V3c0V0V0Iainfix &gt;ainfix *c2V2V0Iainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V4c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V4V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -594,12 +602,12 @@
</goal>
<goal
name="WP_parameter mjrty.12"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="daff8976e879995c244d7a2ab25704df"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2anum_ofaTuple2V1V5c0V0V0FIainfix &gt;c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V6c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V6V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -614,12 +622,12 @@
</goal>
<goal
name="WP_parameter mjrty.13"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop initialization"
sum="f0dad71bbe306ea5d7ed02fcad6b51a7"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=ainfix *c2V4V0Aainfix =V4anum_ofaTuple2V1V3c0c0Iainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V5c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V5V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -634,7 +642,7 @@
</goal>
<goal
name="WP_parameter mjrty.14"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="2091ed98e676cc195e517fa0f6e3c3b8"
......@@ -649,12 +657,12 @@
expanded="true">
<goal
name="WP_parameter mjrty.14.1"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="bf67bbe59a4272c06d84342676e1dcb0"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix &lt;=V6ainfix -V0c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -669,12 +677,12 @@
</goal>
<goal
name="WP_parameter mjrty.14.2"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="9bde60875486aeb18fdbd76b38f353d0"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V7anum_ofaTuple2V1V3c0ainfix +V6c1Iainfix =V7ainfix +V5c1FIainfix =agetV1V6V3Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix &lt;=V6ainfix -V0c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V8c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V8V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -689,12 +697,12 @@
</goal>
<goal
name="WP_parameter mjrty.14.3"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="0b62c264acfc34fbd532dcbb0304e39b"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;ainfix *c2anum_ofaTuple2V1V3c0V0V0Iainfix &gt;ainfix *c2V7V0Iainfix =V7anum_ofaTuple2V1V3c0ainfix +V6c1Iainfix =V7ainfix +V5c1FIainfix =agetV1V6V3Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix &lt;=V6ainfix -V0c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V8c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V8V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -709,12 +717,12 @@
</goal>
<goal
name="WP_parameter mjrty.14.4"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="8fbd42c08477bfcc63dcc7c9b0cc48fc"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V7anum_ofaTuple2V1V3c0ainfix +V6c1Iainfix &gt;ainfix *c2V7V0NIainfix =V7anum_ofaTuple2V1V3c0ainfix +V6c1Iainfix =V7ainfix +V5c1FIainfix =agetV1V6V3Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix &lt;=V6ainfix -V0c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V8c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V8V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -729,7 +737,7 @@
</goal>
<goal
name="WP_parameter mjrty.14.5"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="c81d76200324e40f25a34ef9a6ae8255"
......@@ -749,12 +757,12 @@
</goal>
<goal
name="WP_parameter mjrty.14.6"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="1ad282c4fd71ed3a5b3e78cc1a1d32f9"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V5anum_ofaTuple2V1V3c0ainfix +V6c1Iainfix =agetV1V6V3NIainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix &lt;=V6ainfix -V0c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V0c1Iainfix =V4c0FIainfix &gt;ainfix *c2V2V0NIainfix =V2c0NIainfix &lt;=ainfix *c2anum_ofaTuple2V1V7c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V7V3NFAainfix &lt;=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix &gt;=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix &lt;=V2ainfix +ainfix -V0c1c1Aainfix &lt;=c0V2FFIainfix &lt;=c0ainfix -V0c1Iainfix &lt;c0V0Aainfix &lt;=c0c0Iainfix &lt;=c1V0FF">
<label
name="expl:parameter mjrty"/>
......@@ -769,7 +777,7 @@
</goal>
<goal
name="WP_parameter mjrty.14.7"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="5ac9cf76697c0ede2306c67ab0be8d73"
......@@ -791,7 +799,7 @@
</goal>
<goal
name="WP_parameter mjrty.15"
locfile="programs/mjrty/../mjrty.mlw"
locfile="examples/programs/mjrty/../mjrty.mlw"
loclnum="42" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="1adc447738e8a93fc6df600d0d34d8fe"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment