Commit 9e416f60 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated proof session

parent 8abbc30e
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
<why3session
name="examples/programs/vacid_0_sparse_array_2/why3session.xml" shape_version="2">
name="vacid_0_sparse_array_2/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -24,19 +24,19 @@
expanded="true">
<theory
name="SparseArray"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="1" loccnumb="7" loccnume="18"
verified="true"
expanded="true">
<goal
name="WP_parameter create"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="56" loccnumb="6" loccnume="12"
expl="normal postcondition"
sum="dfc36251fe88ae04ca726a5b14233732"
sum="8dd16abbaeea439a210ea2dc4fa74db9"
proved="true"
expanded="true"
shape="ainfix =agetV4agetV2V6V6Aainfix &lt;agetV2V6V5Aainfix &lt;=c0agetV2V6Iainfix &lt;V6c0Aainfix &lt;=c0V6FAainfix =V3V1Aainfix =V5V3Aainfix &lt;=V5amaxlenAainfix &lt;=c0V5Aainfix &lt;=c0c0Aainfix =V5V0Iainfix =V5V0FIainfix =V3V0FIainfix =V1V0FIainfix &lt;=V0amaxlenAainfix &lt;=c0V0F">
expanded="false"
shape="ainfix =agetV5agetV3V7V7Aainfix &lt;agetV3V7V6Aainfix &lt;=c0agetV3V7Iainfix &lt;V7c0Aainfix &lt;=c0V7FAainfix =V4V2Aainfix =V6V4Aainfix &lt;=V6amaxlenAainfix &lt;=c0V6Aainfix &lt;=c0c0Aainfix =V6V0Aainfix =V1V1Aainfix =c0c0Iainfix =V6V0FIainfix =V4V0FIainfix =V2V0FIainfix &lt;=V0amaxlenAainfix &lt;=c0V0F">
<label
name="expl:parameter create"/>
<proof
......@@ -45,18 +45,18 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="67" loccnumb="6" loccnume="10"
expl="parameter test"
sum="d08b0f733c75e367feb0bee9abd6906f"
sum="1b28fcae061e64c39839a7045dc9b006"
proved="true"
expanded="true"
shape="iainfix &lt;=c0agetV8V5iainfix &lt;agetV8V5V6ais_eltV9V5qainfix =agetV7V10V5Aainfix &lt;V10V3Aainfix &lt;=c0V10LagetV8V5Aainfix &lt;V5V2Aainfix &lt;=c0V5ais_eltV9V5NAainfix &lt;V5V2Aainfix &lt;=c0V5ais_eltV9V5NAainfix &lt;V5V2Aainfix &lt;=c0V5Iainfix =agetV8agetV7V11V11Aainfix &lt;agetV7V11V0Aainfix &lt;=c0agetV7V11Iainfix &lt;V11V6Aainfix &lt;=c0V11FAainfix =V2V3Aainfix =V0V2Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V5V0Aainfix &lt;=c0V5Lamk sparse_arrayamk arrayV0V1amk arrayV2V8amk arrayV3V7V6V4FF">
expanded="false"
shape="iainfix &lt;=c0agetV7V4iainfix &lt;agetV7V4V5ais_eltV9V4qainfix =agetV6V10V4Aainfix &lt;V10V2Aainfix &lt;=c0V10LagetV7V4Aainfix &lt;V4V1Aainfix &lt;=c0V4ais_eltV9V4NAainfix &lt;V4V1Aainfix &lt;=c0V4ais_eltV9V4NAainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix =agetV7agetV6V11V11Aainfix &lt;agetV6V11V0Aainfix &lt;=c0agetV6V11Iainfix &lt;V11V5Aainfix &lt;=c0V11FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V5V0Aainfix &lt;=c0V5Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V8amk arrayV1V7amk arrayV2V6V5V3FF">
<label
name="expl:parameter test"/>
<proof
......@@ -70,12 +70,12 @@
</goal>
<goal
name="WP_parameter get"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="72" loccnumb="6" loccnume="9"
expl="parameter get"
sum="242d5a1f982bdd8940dc7d15ae87d928"
proved="true"
expanded="true"
expanded="false"
shape="iainfix =V10aTrueainfix =agetV8V4avalueV9V4Aainfix &lt;V4V0Aainfix &lt;=c0V4ainfix =V3avalueV9V4Iais_eltV9V4qainfix =V10aTrueFAainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV7agetV6V11V11Aainfix &lt;agetV6V11V0Aainfix &lt;=c0agetV6V11Iainfix &lt;V11V5Aainfix &lt;=c0V11FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V5V0Aainfix &lt;=c0V5Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V8amk arrayV1V7amk arrayV2V6V5V3FF">
<label
name="expl:parameter get"/>
......@@ -90,11 +90,11 @@
</goal>
<goal
name="permutation"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="84" loccnumb="8" loccnume="19"
sum="1d6e877bdbe7427e5d1d1bab50dd875d"
proved="true"
expanded="true"
expanded="false"
shape="ais_eltV0V1Iainfix &lt;V1alengthV0Aainfix &lt;=c0V1FIainfix =acardV0alengthV0Iainfix =amixfix []aindexV0amixfix []abackV0V2V2Aainfix &lt;amixfix []abackV0V2alengthavaluesV0Aainfix &lt;=c0amixfix []abackV0V2Iainfix &lt;V2acardV0Aainfix &lt;=c0V2FAainfix =alengthaindexV0alengthabackV0Aainfix =alengthavaluesV0alengthaindexV0Aainfix &lt;=alengthavaluesV0amaxlenAainfix &lt;=acardV0alengthavaluesV0Aainfix &lt;=c0acardV0F">
<proof
prover="2"
......@@ -103,12 +103,12 @@
edited="vacid_0_sparse_array_2_SparseArray_permutation_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.62"/>
<result status="valid" time="0.69"/>
</proof>
</goal>
<goal
name="WP_parameter set"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="parameter set"
sum="26e8d824331c080cbac06323274e9eb5"
......@@ -123,12 +123,12 @@
expanded="true">
<goal
name="WP_parameter set.1"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="precondition"
sum="7d6d2c71d1920223f418cf25106d7edb"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V11V11Aainfix &lt;agetV7V11V0Aainfix &lt;=c0agetV7V11Iainfix &lt;V11V6Aainfix &lt;=c0V11FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -143,12 +143,12 @@
</goal>
<goal
name="WP_parameter set.2"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="precondition"
sum="ce635a0afa5532bc5da90d151731d68d"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =agetV8agetV7V13V13Aainfix &lt;agetV7V13V0Aainfix &lt;=c0agetV7V13Iainfix &lt;V13V6Aainfix &lt;=c0V13FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V14V14Aainfix &lt;agetV7V14V0Aainfix &lt;=c0agetV7V14Iainfix &lt;V14V6Aainfix &lt;=c0V14FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -158,17 +158,17 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter set.3"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="assertion"
sum="1c4150a82edc3ad355d361c2e1030b08"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V6V0Iainfix =V13aTrueNIais_eltV12V4qainfix =V13aTrueFIainfix =agetV8agetV7V14V14Aainfix &lt;agetV7V14V0Aainfix &lt;=c0agetV7V14Iainfix &lt;V14V6Aainfix &lt;=c0V14FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V15V15Aainfix &lt;agetV7V15V0Aainfix &lt;=c0agetV7V15Iainfix &lt;V15V6Aainfix &lt;=c0V15FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -186,7 +186,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="3"
......@@ -194,17 +194,17 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.17"/>
<result status="valid" time="0.18"/>
</proof>
</goal>
<goal
name="WP_parameter set.4"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="precondition"
sum="4bf7c4cfd4cfe88985fc77ad899480a9"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix &lt;V6V0Iainfix =V13aTrueNIais_eltV12V4qainfix =V13aTrueFIainfix =agetV8agetV7V14V14Aainfix &lt;agetV7V14V0Aainfix &lt;=c0agetV7V14Iainfix &lt;V14V6Aainfix &lt;=c0V14FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V15V15Aainfix &lt;agetV7V15V0Aainfix &lt;=c0agetV7V15Iainfix &lt;V15V6Aainfix &lt;=c0V15FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -214,17 +214,17 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter set.5"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="precondition"
sum="5bbea5f5ceee016d53aaee2d392c0580"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V6V2Aainfix &lt;=c0V6Iainfix =V14asetV8V4V6FIainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix &lt;V6V0Iainfix =V13aTrueNIais_eltV12V4qainfix =V13aTrueFIainfix =agetV8agetV7V15V15Aainfix &lt;agetV7V15V0Aainfix &lt;=c0agetV7V15Iainfix &lt;V15V6Aainfix &lt;=c0V15FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V16V16Aainfix &lt;agetV7V16V0Aainfix &lt;=c0agetV7V16Iainfix &lt;V16V6Aainfix &lt;=c0V16FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -239,7 +239,7 @@
</goal>
<goal
name="WP_parameter set.6"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="normal postcondition"
sum="538cea778d1639a177ca57234d25006a"
......@@ -254,7 +254,7 @@
expanded="true">
<goal
name="WP_parameter set.6.1"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="parameter set"
sum="1dbd5af4186c4bdfc237589647971dbd"
......@@ -269,15 +269,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="3"
......@@ -285,17 +277,17 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter set.6.2"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="parameter set"
sum="3cc2259ed3dc8e61e876a79071bc4c2e"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =avalueV17V18avalueV10V18Iainfix =V18V4NFIainfix =V16ainfix +V6c1Lamk sparse_arrayamk arrayV0V11amk arrayV1V14amk arrayV2V15V16V3FIainfix =V15asetV7V6V4FIainfix &lt;V6V2Aainfix &lt;=c0V6Iainfix =V14asetV8V4V6FIainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix &lt;V6V0Iainfix =V13aTrueNIais_eltV12V4qainfix =V13aTrueFIainfix =agetV8agetV7V19V19Aainfix &lt;agetV7V19V0Aainfix &lt;=c0agetV7V19Iainfix &lt;V19V6Aainfix &lt;=c0V19FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V20V20Aainfix &lt;agetV7V20V0Aainfix &lt;=c0agetV7V20Iainfix &lt;V20V6Aainfix &lt;=c0V20FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -305,7 +297,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.30"/>
<result status="unknown" time="0.31"/>
</proof>
<proof
prover="1"
......@@ -313,7 +305,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.48"/>
</proof>
<proof
prover="3"
......@@ -321,17 +313,17 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.26"/>
<result status="valid" time="1.23"/>
</proof>
</goal>
<goal
name="WP_parameter set.6.3"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="type invariant"
sum="d525a1867e134f6bd34c7a8166acb5c6"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =agetV14agetV15V18V18Aainfix &lt;agetV15V18V0Aainfix &lt;=c0agetV15V18Iainfix &lt;V18V16Aainfix &lt;=c0V18FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V16V0Aainfix &lt;=c0V16Iainfix =avalueV17V19avalueV10V19Iainfix =V19V4NFAainfix =avalueV17V4V5Iainfix =V16ainfix +V6c1Lamk sparse_arrayamk arrayV0V11amk arrayV1V14amk arrayV2V15V16V3FIainfix =V15asetV7V6V4FIainfix &lt;V6V2Aainfix &lt;=c0V6Iainfix =V14asetV8V4V6FIainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix &lt;V6V0Iainfix =V13aTrueNIais_eltV12V4qainfix =V13aTrueFIainfix =agetV8agetV7V20V20Aainfix &lt;agetV7V20V0Aainfix &lt;=c0agetV7V20Iainfix &lt;V20V6Aainfix &lt;=c0V20FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V21V21Aainfix &lt;agetV7V21V0Aainfix &lt;=c0agetV7V21Iainfix &lt;V21V6Aainfix &lt;=c0V21FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -341,7 +333,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.00"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
......@@ -349,7 +341,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
......@@ -357,19 +349,19 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.85"/>
<result status="valid" time="0.84"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter set.7"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="96" loccnumb="6" loccnume="9"
expl="normal postcondition"
sum="b028721243de9f745dac7e213a072b82"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =avalueV12V14avalueV10V14Iainfix =V14V4NFAainfix =avalueV12V4V5Iainfix =V13aTrueNNIais_eltV12V4qainfix =V13aTrueFIainfix =agetV8agetV7V15V15Aainfix &lt;agetV7V15V0Aainfix &lt;=c0agetV7V15Iainfix &lt;V15V6Aainfix &lt;=c0V15FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =V11asetV9V4V5Lamk sparse_arrayamk arrayV0V11amk arrayV1V8amk arrayV2V7V6V3FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV8agetV7V16V16Aainfix &lt;agetV7V16V0Aainfix &lt;=c0agetV7V16Iainfix &lt;V16V6Aainfix &lt;=c0V16FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix &lt;V4V0Aainfix &lt;=c0V4Lamk sparse_arrayamk arrayV0V9amk arrayV1V8amk arrayV2V7V6V3FF">
<label
name="expl:parameter set"/>
......@@ -387,18 +379,18 @@
</theory>
<theory
name="Harness"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="110" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter harness"
locfile="examples/programs/vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
locfile="vacid_0_sparse_array_2/../vacid_0_sparse_array_2.mlw"
loclnum="120" loccnumb="6" loccnume="13"
expl="parameter harness"
sum="1dfed8a873a33bddf0ddfee647bf1d9f"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =avalueV27c0adefaultAainfix &lt;c0V9Aainfix &lt;=c0c0Aainfix =avalueV22c0adefaultAainfix &lt;c0V0Aainfix &lt;=c0c0Aainfix =avalueV27c5adefaultAainfix &lt;c5V9Aainfix &lt;=c0c5Aainfix =avalueV22c7adefaultAainfix &lt;c7V0Aainfix &lt;=c0c7Aainfix =avalueV27c7ac2Aainfix &lt;c7V9Aainfix &lt;=c0c7Aainfix =avalueV22c5ac1Aainfix &lt;c5V0Aainfix &lt;=c0c5Iainfix =agetV25agetV24V28V28Aainfix &lt;agetV24V28V9Aainfix &lt;=c0agetV24V28Iainfix &lt;V28V23Aainfix &lt;=c0V28FAainfix =V11V13Aainfix =V9V11Aainfix &lt;=V9amaxlenAainfix &lt;=V23V9Aainfix &lt;=c0V23Aainfix =avalueV27V29avalueV17V29Iainfix =V29c7NFAainfix =avalueV27c7ac2Lamk sparse_arrayamk arrayV9V26amk arrayV11V25amk arrayV13V24V23V16FAainfix &lt;c7V9Aainfix &lt;=c0c7Iainfix =agetV20agetV19V30V30Aainfix &lt;agetV19V30V0Aainfix &lt;=c0agetV19V30Iainfix &lt;V30V18Aainfix &lt;=c0V30FAainfix =V2V4Aainfix =V0V2Aainfix &lt;=V0amaxlenAainfix &lt;=V18V0Aainfix &lt;=c0V18Aainfix =avalueV22V31avalueV8V31Iainfix =V31c5NFAainfix =avalueV22c5ac1Lamk sparse_arrayamk arrayV0V21amk arrayV2V20amk arrayV4V19V18V7FAainfix &lt;c5V0Aainfix &lt;=c0c5Aainfix =avalueV17c7adefaultAainfix &lt;c7V9Aainfix &lt;=c0c7Aainfix =avalueV8c5adefaultAainfix &lt;c5V0Aainfix &lt;=c0c5Iainfix =agetV12agetV14V32V32Aainfix &lt;agetV14V32V9Aainfix &lt;=c0agetV14V32Iainfix &lt;V32V15Aainfix &lt;=c0V32FAainfix =V11V13Aainfix =V9V11Aainfix &lt;=V9amaxlenAainfix &lt;=V15V9Aainfix &lt;=c0V15Aainfix =V9c20Aainfix =V16adefaultAainfix =V15c0Lamk sparse_arrayamk arrayV9V10amk arrayV11V12amk arrayV13V14V15V16FAainfix &lt;=c20amaxlenAainfix &lt;=c0c20Iainfix =agetV3agetV5V33V33Aainfix &lt;agetV5V33V0Aainfix &lt;=c0agetV5V33Iainfix &lt;V33V6Aainfix &lt;=c0V33FAainfix =V2V4Aainfix =V0V2Aainfix &lt;=V0amaxlenAainfix &lt;=V6V0Aainfix &lt;=c0V6Aainfix =V0c10Aainfix =V7adefaultAainfix =V6c0Lamk sparse_arrayamk arrayV0V1amk arrayV2V3amk arrayV4V5V6V7FAainfix &lt;=c10amaxlenAainfix &lt;=c0c10">
<label
name="expl:parameter harness"/>
......
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