Commit 9b5dfd04 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update sessions, part 4

parent 17fdb23c
......@@ -32,8 +32,8 @@
version="2.19"/>
<file
name="../fibonacci.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="Fibonacci"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
......@@ -173,7 +173,7 @@
name="FibonacciLogarithmic"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="68" loccnumb="7" loccnume="27"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter logfib"
......@@ -181,14 +181,14 @@
loclnum="82" loccnumb="10" loccnume="16"
expl="parameter logfib"
sum="3966dacbc1855018004e996b874f27fa"
proved="false"
expanded="false"
proved="true"
expanded="true"
shape="iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter logfib.1"
......@@ -197,7 +197,7 @@
expl="normal postcondition"
sum="adf3fda094b1f16d576b23cf13147c8d"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
......@@ -240,11 +240,19 @@
loclnum="82" loccnumb="10" loccnume="16"
expl="variant decreases"
sum="4464035e38e634573f8cf479606f0013"
proved="false"
expanded="false"
proved="true"
expanded="true"
shape="ainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter logfib.3"
......@@ -253,7 +261,7 @@
expl="precondition"
sum="914eb29f581e4f81f1dc88e3cd6a2125"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=adivV0c2c0Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
......
......@@ -12,21 +12,25 @@
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Coq"
version="8.3pl4"/>
<prover
id="3"
id="4"
name="Z3"
version="2.19"/>
<file
name="../gcd.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="EuclideanAlgorithm"
locfile="examples/programs/gcd/../gcd.mlw"
loclnum="4" loccnumb="7" loccnume="25"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter gcd"
......@@ -34,14 +38,14 @@
loclnum="10" loccnumb="10" loccnume="13"
expl="parameter gcd"
sum="e7fb9f71ca8d13171325c792ae210df1"
proved="false"
proved="true"
expanded="true"
shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix &gt;=amodV0V1c0Aainfix &gt;=V1c0Aainfix &lt;amodV0V1V1Aainfix &lt;=c0V1Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:parameter gcd"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter gcd.1"
......@@ -55,7 +59,7 @@
<label
name="expl:parameter gcd"/>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -85,11 +89,27 @@
loclnum="10" loccnumb="10" loccnume="13"
expl="variant decreases"
sum="bc3a27e8c6c197ade6b87e38ae3d4e11"
proved="false"
expanded="false"
proved="true"
expanded="true"
shape="ainfix &lt;amodV0V1V1Aainfix &lt;=c0V1Iainfix =V1c0NIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:parameter gcd"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.19"/>
</proof>
<proof
prover="2"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter gcd.3"
......@@ -103,7 +123,7 @@
<label
name="expl:parameter gcd"/>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -139,7 +159,7 @@
<label
name="expl:parameter gcd"/>
<proof
prover="2"
prover="3"
timelimit="10"
memlimit="0"
edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"
......
......@@ -20,13 +20,13 @@
version="2.19"/>
<file
name="../generate_all_trees.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="GenerateAllTrees"
locfile="examples/programs/generate_all_trees/../generate_all_trees.mlw"
loclnum="11" loccnumb="7" loccnume="23"
verified="false"
verified="true"
expanded="true">
<goal
name="size_nonneg"
......@@ -104,14 +104,14 @@
loclnum="46" loccnumb="6" loccnume="13"
expl="parameter combine"
sum="78cdc48f8299be6bad6f1184f9a0e5f2"
proved="false"
proved="true"
expanded="true"
shape="ainfix =asizeV7V2Aainfix =asizeV6V0Aainfix =V5aNodeV6V7EqamemV5V4FAadistinctV4IamemV10V3AamemV9V1Aainfix =V8aNodeV9V10EqamemV8V4FAadistinctV4FAadistinctV1ACV11aNilamemV14V3AamemV13V11Aainfix =V12aNodeV13V14EqamemV12aNilFAadistinctaNilaConsVVamemV21V3AamemV20V11Aainfix =V19aNodeV20V21EqamemV19ainfix ++V18V17FAadistinctainfix ++V18V17IamemV23V3Aainfix =V22aNodeV15V23EqamemV22V18FAadistinctV18FAadistinctV3IamemV26V3AamemV25V16Aainfix =V24aNodeV25V26EqamemV24V17FAadistinctV17FAadistinctV16Aainfix &lt;alengthV16alengthV11Aainfix &lt;=c0alengthV11ACV27aNilamemV29V27Aainfix =V28aNodeV15V29EqamemV28aNilFAadistinctaNilaConsVVamemV34V27Aainfix =V33aNodeV15V34EqamemV33aConsaNodeV15V30V32FAadistinctaConsaNodeV15V30V32IamemV36V31Aainfix =V35aNodeV15V36EqamemV35V32FAadistinctV32FAadistinctV31Aainfix &lt;alengthV31alengthV27Aainfix &lt;=c0alengthV27IadistinctV27FIadistinctV11FIaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter combine.1"
......@@ -140,7 +140,7 @@
expl="parameter combine"
sum="9f34b3f0c0ed469a7c1f0f792c1d9f73"
proved="true"
expanded="false"
expanded="true"
shape="CV4aNiltaConsVVCV7aNilamemV9V7Aainfix =V8aNodeV5V9EqamemV8aNilFAadistinctaNilaConsVVtIadistinctV7FIadistinctV4FIaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
......@@ -159,11 +159,19 @@
loclnum="46" loccnumb="6" loccnume="13"
expl="parameter combine"
sum="29d81edec274fe49d08199931a6a1144"
proved="false"
expanded="false"
proved="true"
expanded="true"
shape="CV4aNiltaConsVVCV7aNiltaConsVVainfix &lt;alengthV9alengthV7Aainfix &lt;=c0alengthV7IadistinctV7FIadistinctV4FIaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter combine.4"
......@@ -172,7 +180,7 @@
expl="parameter combine"
sum="71797cfd966a4e42da29ec6399fbf061"
proved="true"
expanded="false"
expanded="true"
shape="CV4aNiltaConsVVCV7aNiltaConsVVadistinctV9IadistinctV7FIadistinctV4FIaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
......@@ -269,11 +277,19 @@
loclnum="46" loccnumb="6" loccnume="13"
expl="parameter combine"
sum="a4a69b3990bceb8b76c66c0536b26f00"
proved="false"
proved="true"
expanded="false"
shape="CV4aNiltaConsVVainfix &lt;alengthV6alengthV4Aainfix &lt;=c0alengthV4IadistinctV4FIaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter combine.7"
......@@ -322,7 +338,7 @@
expl="parameter combine"
sum="89cc567a58039d2c950a49eab8f574a9"
proved="true"
expanded="false"
expanded="true"
shape="CV4aNiltaConsVVamemV11V3AamemV10V4Aainfix =V9aNodeV10V11EqamemV9ainfix ++V8V7FAadistinctainfix ++V8V7IamemV13V3Aainfix =V12aNodeV5V13EqamemV12V8FAadistinctV8FIadistinctV3IamemV16V3AamemV15V6Aainfix =V14aNodeV15V16EqamemV14V7FAadistinctV7FIadistinctV6Aainfix &lt;alengthV6alengthV4Aainfix &lt;=c0alengthV4IadistinctV4FIaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
......@@ -419,7 +435,7 @@
expl="normal postcondition"
sum="11e0d49295a3c4dc0088accb09487672"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =asizeV7V2Aainfix =asizeV6V0Aainfix =V5aNodeV6V7EqamemV5V4FAadistinctV4IamemV10V3AamemV9V1Aainfix =V8aNodeV9V10EqamemV8V4FAadistinctV4FIadistinctV1Iaall_treesV2V3Aainfix &lt;=c0V2Aaall_treesV0V1Aainfix &lt;=c0V0F">
<label
name="expl:parameter combine"/>
......@@ -498,7 +514,7 @@
expl="parameter all_trees"
sum="59bba6a055b744b57c32e32bbe73f227"
proved="true"
expanded="false"
expanded="true"
shape="aall_treesV3agetV2V3Iainfix &lt;=V3V0Aainfix &lt;=c0V3FIaall_treesV4agetV2V4Iainfix &lt;V4ainfix +V0c1Aainfix &lt;=c0V4FAaall_treesV8agetV7V8Iainfix &lt;V8ainfix +V5c1Aainfix &lt;=c0V8FIainfix &lt;asizeV10ainfix +ainfix -V5c1c1Aainfix =asizeV9V5Aainfix =V9aNodeV10V11EqamemV9agetV7V5FAadistinctagetV7V5Aaall_treesV12agetV7V12Iainfix &lt;V12V5Aainfix &lt;=c0V12FAainfix &lt;asizeV17ainfix +V13c1Aainfix =asizeV16V5Aainfix =V16aNodeV17V18EqamemV16agetV15V5FAadistinctagetV15V5Aaall_treesV19agetV15V19Iainfix &lt;V19V5Aainfix &lt;=c0V19FIainfix =V15asetV7V5ainfix ++V14agetV7V5FAainfix &lt;V5ainfix +V0c1Aainfix &lt;=c0V5Iainfix =asizeV22ainfix -ainfix -V5c1V13Aainfix =asizeV21V13Aainfix =V20aNodeV21V22EqamemV20V14FAadistinctV14FAaall_treesainfix -ainfix -V5c1V13agetV7ainfix -ainfix -V5c1V13Aainfix &lt;=c0ainfix -ainfix -V5c1V13Aaall_treesV13agetV7V13Aainfix &lt;=c0V13Aainfix &lt;V13ainfix +V0c1Aainfix &lt;=c0V13Aainfix &lt;ainfix -ainfix -V5c1V13ainfix +V0c1Aainfix &lt;=c0ainfix -ainfix -V5c1V13Aainfix &lt;V5ainfix +V0c1Aainfix &lt;=c0V5Iainfix &lt;asizeV24V13Aainfix =asizeV23V5Aainfix =V23aNodeV24V25EqamemV23agetV7V5FAadistinctagetV7V5Aaall_treesV26agetV7V26Iainfix &lt;V26V5Aainfix &lt;=c0V26FIainfix &lt;=V13ainfix -V5c1Aainfix &lt;=c0V13FFAainfix &lt;asizeV28c0Aainfix =asizeV27V5Aainfix =V27aNodeV28V29EqamemV27agetV6V5FAadistinctagetV6V5Aaall_treesV30agetV6V30Iainfix &lt;V30V5Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V5c1Aaall_treesV31agetV6V31Iainfix &lt;V31ainfix +V5c1Aainfix &lt;=c0V31FIainfix &gt;c0ainfix -V5c1Iainfix =V6asetV2V5aNilFAainfix &lt;V5ainfix +V0c1Aainfix &lt;=c0V5Iaall_treesV32agetV2V32Iainfix &lt;V32V5Aainfix &lt;=c0V32FIainfix &lt;=V5V0Aainfix &lt;=c1V5FFAaall_treesV33agetV1V33Iainfix &lt;V33c1Aainfix &lt;=c0V33FIainfix &lt;=c1V0Aaall_treesV34agetV1V34Iainfix &lt;=V34V0Aainfix &lt;=c0V34FIainfix &gt;c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFAainfix &lt;c0ainfix +V0c1Aainfix &lt;=c0c0Aainfix &gt;=ainfix +V0c1c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter all_trees"/>
......@@ -573,7 +589,7 @@
expl="for loop initialization"
sum="f820302a240feff47638086dce068a7f"
proved="true"
expanded="false"
expanded="true"
shape="aall_treesV2agetV1V2Iainfix &lt;V2c1Aainfix &lt;=c0V2FIainfix &lt;=c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFIainfix &lt;c0ainfix +V0c1Aainfix &lt;=c0c0Iainfix &gt;=ainfix +V0c1c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter all_trees"/>
......@@ -610,7 +626,7 @@
expl="for loop preservation"
sum="d239acbc7d02721cf60699825967be2e"
proved="true"
expanded="false"
expanded="true"
shape="aall_treesV6agetV5V6Iainfix &lt;V6ainfix +V3c1Aainfix &lt;=c0V6FIainfix &lt;asizeV8ainfix +ainfix -V3c1c1Aainfix =asizeV7V3Aainfix =V7aNodeV8V9EqamemV7agetV5V3FAadistinctagetV5V3Aaall_treesV10agetV5V10Iainfix &lt;V10V3Aainfix &lt;=c0V10FAainfix &lt;asizeV15ainfix +V11c1Aainfix =asizeV14V3Aainfix =V14aNodeV15V16EqamemV14agetV13V3FAadistinctagetV13V3Aaall_treesV17agetV13V17Iainfix &lt;V17V3Aainfix &lt;=c0V17FIainfix =V13asetV5V3ainfix ++V12agetV5V3FAainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iainfix =asizeV20ainfix -ainfix -V3c1V11Aainfix =asizeV19V11Aainfix =V18aNodeV19V20EqamemV18V12FAadistinctV12FAaall_treesainfix -ainfix -V3c1V11agetV5ainfix -ainfix -V3c1V11Aainfix &lt;=c0ainfix -ainfix -V3c1V11Aaall_treesV11agetV5V11Aainfix &lt;=c0V11Aainfix &lt;V11ainfix +V0c1Aainfix &lt;=c0V11Aainfix &lt;ainfix -ainfix -V3c1V11ainfix +V0c1Aainfix &lt;=c0ainfix -ainfix -V3c1V11Aainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iainfix &lt;asizeV22V11Aainfix =asizeV21V3Aainfix =V21aNodeV22V23EqamemV21agetV5V3FAadistinctagetV5V3Aaall_treesV24agetV5V24Iainfix &lt;V24V3Aainfix &lt;=c0V24FIainfix &lt;=V11ainfix -V3c1Aainfix &lt;=c0V11FFAainfix &lt;asizeV26c0Aainfix =asizeV25V3Aainfix =V25aNodeV26V27EqamemV25agetV4V3FAadistinctagetV4V3Aaall_treesV28agetV4V28Iainfix &lt;V28V3Aainfix &lt;=c0V28FIainfix &lt;=c0ainfix -V3c1Aaall_treesV29agetV4V29Iainfix &lt;V29ainfix +V3c1Aainfix &lt;=c0V29FIainfix &gt;c0ainfix -V3c1Iainfix =V4asetV2V3aNilFAainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iaall_treesV30agetV2V30Iainfix &lt;V30V3Aainfix &lt;=c0V30FIainfix &lt;=V3V0Aainfix &lt;=c1V3FFIainfix &lt;=c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFIainfix &lt;c0ainfix +V0c1Aainfix &lt;=c0c0Iainfix &gt;=ainfix +V0c1c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter all_trees"/>
......@@ -685,7 +701,7 @@
expl="for loop preservation"
sum="ff0568dc018f1b672a89f2c142d9fd10"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;asizeV10ainfix +V6c1Aainfix =asizeV9V3Aainfix =V9aNodeV10V11EqamemV9agetV8V3FAadistinctagetV8V3Aaall_treesV12agetV8V12Iainfix &lt;V12V3Aainfix &lt;=c0V12FIainfix =V8asetV5V3ainfix ++V7agetV5V3FAainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iainfix =asizeV15ainfix -ainfix -V3c1V6Aainfix =asizeV14V6Aainfix =V13aNodeV14V15EqamemV13V7FAadistinctV7FAaall_treesainfix -ainfix -V3c1V6agetV5ainfix -ainfix -V3c1V6Aainfix &lt;=c0ainfix -ainfix -V3c1V6Aaall_treesV6agetV5V6Aainfix &lt;=c0V6Aainfix &lt;V6ainfix +V0c1Aainfix &lt;=c0V6Aainfix &lt;ainfix -ainfix -V3c1V6ainfix +V0c1Aainfix &lt;=c0ainfix -ainfix -V3c1V6Aainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iainfix &lt;asizeV17V6Aainfix =asizeV16V3Aainfix =V16aNodeV17V18EqamemV16agetV5V3FAadistinctagetV5V3Aaall_treesV19agetV5V19Iainfix &lt;V19V3Aainfix &lt;=c0V19FIainfix &lt;=V6ainfix -V3c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V3c1Iainfix =V4asetV2V3aNilFIainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iaall_treesV20agetV2V20Iainfix &lt;V20V3Aainfix &lt;=c0V20FIainfix &lt;=V3V0Aainfix &lt;=c1V3FFIainfix &lt;=c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFIainfix &lt;c0ainfix +V0c1Aainfix &lt;=c0c0Iainfix &gt;=ainfix +V0c1c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter all_trees"/>
......@@ -890,7 +906,7 @@
expl="for loop preservation"
sum="a36a4c71c36851b48d4786aecc3e9e45"
proved="true"
expanded="false"
expanded="true"
shape="aall_treesV6agetV5V6Iainfix &lt;V6ainfix +V3c1Aainfix &lt;=c0V6FIainfix &lt;asizeV8ainfix +ainfix -V3c1c1Aainfix =asizeV7V3Aainfix =V7aNodeV8V9EqamemV7agetV5V3FAadistinctagetV5V3Aaall_treesV10agetV5V10Iainfix &lt;V10V3Aainfix &lt;=c0V10FFIainfix &lt;=c0ainfix -V3c1Iainfix =V4asetV2V3aNilFIainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iaall_treesV11agetV2V11Iainfix &lt;V11V3Aainfix &lt;=c0V11FIainfix &lt;=V3V0Aainfix &lt;=c1V3FFIainfix &lt;=c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFIainfix &lt;c0ainfix +V0c1Aainfix &lt;=c0c0Iainfix &gt;=ainfix +V0c1c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter all_trees"/>
......@@ -905,7 +921,7 @@
expl="for loop preservation"
sum="e9f2fefd0517146e26d49dd7a9f7d775"
proved="true"
expanded="false"
expanded="true"
shape="amemV7agetV5V6qainfix =asizeV7V6FAadistinctagetV5V6Iainfix &lt;V6ainfix +V3c1Aainfix =c0V6Oainfix &lt;c0V6FIainfix &lt;asizeV9ainfix +ainfix -V3c1c1Aainfix =asizeV8V3Aainfix =V8aNodeV9V10EqamemV8agetV5V3FAadistinctagetV5V3AamemV12agetV5V11qainfix =asizeV12V11FAadistinctagetV5V11Iainfix &lt;V11V3Aainfix =c0V11Oainfix &lt;c0V11FFIainfix =c0ainfix -V3c1Oainfix &lt;c0ainfix -V3c1Iainfix =V4asetV2V3aNilFIainfix &lt;V3ainfix +V0c1Aainfix =c0V3Oainfix &lt;c0V3IamemV14agetV2V13qainfix =asizeV14V13FAadistinctagetV2V13Iainfix &lt;V13V3Aainfix =c0V13Oainfix &lt;c0V13FIainfix =V3V0Oainfix &lt;V3V0Aainfix =c1V3Oainfix &lt;c1V3FFIainfix =c1V0Oainfix &lt;c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFIainfix &lt;c0ainfix +V0c1Aainfix =c0c0Oainfix &lt;c0c0Iainfix &lt;=c0ainfix +V0c1Iainfix &lt;=c0V0F">
<label
name="expl:parameter all_trees"/>
......
......@@ -10,15 +10,19 @@
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<file
name="../insertion_sort_list.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="M"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="4" loccnumb="7" loccnume="8"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter insert"
......@@ -26,14 +30,14 @@
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="d02d16309dfde41102e8d45efca5d33a"
proved="false"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix &lt;=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix &lt;alengthV3alengthV1Aainfix &lt;=c0alengthV1IasortedV1F">
<label
name="expl:parameter insert"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter insert.1"
......@@ -81,11 +85,27 @@
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="15c6091d425cf0844b57e066a6569536"
proved="false"
expanded="false"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVainfix &lt;alengthV3alengthV1Aainfix &lt;=c0alengthV1Iainfix &lt;=V0V2NIasortedV1F">
<label
name="expl:parameter insert"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insert.4"
......
......@@ -20,13 +20,13 @@
version="2.19"/>
<file
name="../quicksort.mlw"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="Quicksort"
locfile="examples/programs/quicksort/../quicksort.mlw"
loclnum="8" loccnumb="7" loccnume="16"
verified="false"
verified="true"
expanded="true">
<goal
name="WP_parameter swap"
......@@ -54,14 +54,14 @@
loclnum="24" loccnumb="10" loccnume="19"
expl="parameter quick_rec"
sum="249a70494608c0f3c50b5a73ee683f29"
proved="false"
proved="true"
expanded="true"
shape="iainfix &lt;V1V2apermut_subV3V9V1ainfix +V2c1Aasorted_subV9V1ainfix +V2c1Iapermut_subV8V9ainfix +V5c1ainfix +V2c1Aasorted_subV9ainfix +V5c1ainfix +V2c1FAainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Aainfix &lt;ainfix -ainfix +c1V2ainfix +V5c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1FAainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5FAainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10ainfix +V2c1Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FAiainfix &lt;agetV6V12V4ainfix &lt;V13ainfix +V12c1Aainfix &lt;=V1V13Aainfix =agetV14V1V4Aapermut_subV3V14V1ainfix +V2c1Aainfix &gt;=agetV14V15V4Iainfix &lt;V15ainfix +V12c1Aainfix &lt;V13V15FAainfix &lt;agetV14V16V4Iainfix &lt;=V16V13Aainfix &lt;V1V16FIaexchangeV6V14V12V13FAainfix &lt;V13V0Aainfix &lt;=c0V13Aainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix =V13ainfix +V5c1Fainfix &lt;V5ainfix +V12c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V17V4Iainfix &lt;V17ainfix +V12c1Aainfix &lt;V5V17FAainfix &lt;agetV6V18V4Iainfix &lt;=V18V5Aainfix &lt;V1V18FAainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix &lt;V5V12Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V19V4Iainfix &lt;V19V12Aainfix &lt;V5V19FAainfix &lt;agetV6V20V4Iainfix &lt;=V20V5Aainfix &lt;V1V20FIainfix &lt;=V12V2Aainfix &lt;=ainfix +V1c1V12FFAainfix &lt;V1ainfix +V1c1Aainfix &lt;=V1V1Aainfix =agetV3V1V4Aapermut_subV3V3V1ainfix +V2c1Aainfix &gt;=agetV3V21V4Iainfix &lt;V21ainfix +V1c1Aainfix &lt;V1V21FAainfix &lt;agetV3V22V4Iainfix &lt;=V22V1Aainfix &lt;V1V22FIainfix &lt;=ainfix +V1c1V2Aapermut_subV3V25V1ainfix +V2c1Aasorted_subV25V1ainfix +V2c1Iapermut_subV24V25ainfix +V1c1ainfix +V2c1Aasorted_subV25ainfix +V1c1ainfix +V2c1FAainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Aainfix &lt;ainfix -ainfix +c1V2ainfix +V1c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV23V24V1ainfix +ainfix -V1c1c1Aasorted_subV24V1ainfix +ainfix -V1c1c1FAainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V23V1V1FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Aainfix &lt;V1V0Aainfix &lt;=c0V1apermut_subV3V3V1ainfix +V2c1Aasorted_subV3V1ainfix +V2c1Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
<transf
name="split_goal"
proved="false"
proved="true"
expanded="true">
<goal
name="WP_parameter quick_rec.1"
......@@ -90,7 +90,7 @@
expl="precondition"
sum="f0264c9d84f13ef1f3c52a07f6315e31"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
......@@ -109,11 +109,19 @@
loclnum="24" loccnumb="10" loccnume="19"
expl="variant decreases"
sum="15925c29f20c2eb01559842d47903abc"
proved="false"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V5V1V1FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter quick_rec.4"
......@@ -122,7 +130,7 @@
expl="precondition"
sum="463b5aa83a2eeb8f9f46ee9de31ec66f"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
......@@ -141,11 +149,19 @@
loclnum="24" loccnumb="10" loccnume="19"
expl="variant decreases"
sum="b3b26832da85724cf67f7fcba275e395"
proved="false"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1V2ainfix +V1c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V5V1V1FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter quick_rec.6"
......@@ -154,7 +170,7 @@
expl="precondition"
sum="794e9cd11b6b075b915358f10b59f4fa"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V5V1V1FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
......@@ -512,7 +528,7 @@
expl="precondition"
sum="059a74dee4e615505d141e9316d6bf29"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
......@@ -608,11 +624,19 @@
loclnum="24" loccnumb="10" loccnume="19"
expl="variant decreases"
sum="be9f2c84276087caca25ca4f60f358cf"
proved="false"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V2c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter quick_rec.12"
......@@ -640,11 +664,19 @@
loclnum="24" loccnumb="10" loccnume="19"
expl="variant decreases"
sum="0d87c4c290ea56ee746c56c1cf18d511"
proved="false"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -ainfix +c1V2ainfix +V5c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9ainfix +V2c1Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
<proof
prover="0"
timelimit="300"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter quick_rec.14"
......@@ -694,7 +726,7 @@
expl="normal postcondition"
sum="6a139601a5e33cd2f884233e599e44e7"
proved="true"
expanded="false"
expanded="true"
shape="apermut_subV3V3V1ainfix +V2c1Aasorted_subV3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1FF">
<label
name="expl:parameter quick_rec"/>
......@@ -753,7 +785,7 @@
expl="parameter quicksort"
sum="16f7ff8159777a6412f12facdb163853"
proved="true"
expanded="false"
expanded="true"
shape="apermutamk arrayV0V1amk arrayV0V2Aasorted_subV2c0V0Iapermut_subV1V2c0ainfix +ainfix -V0c1c1Aasorted_subV2c0ainfix +ainfix -V0c1c1FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0FF">
<label
name="expl:parameter quicksort"/>
......
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