Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 26b7cbf9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

binary heaps: cleaned

parent 6a95dc42
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
examples/programs/vacid_0_binary_heaps/proofs/why3session.xml
+ 408
− 792
View file @ 26b7cbf9
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="examples/programs/vacid_0_binary_heaps/proofs/why3session.xml">
name="proofs/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -56,13 +56,13 @@
expanded="false">
<theory
name="WP TestHarness"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="2" loccnumb="7" loccnume="18"
verified="true"
expanded="false">
<goal
name="WP_parameter testHarness"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="parameter testHarness"
sum="6ff5feea4c21bb589b93174c3cada2c3"
......@@ -77,7 +77,7 @@
expanded="false">
<goal
name="WP_parameter testHarness.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="precondition"
sum="a53a222192825bedaf0bbfe68632e441"
......@@ -100,7 +100,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -108,7 +108,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -124,7 +124,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.30"/>
<result status="valid" time="3.16"/>
</proof>
<proof
prover="9"
......@@ -137,7 +137,7 @@
</goal>
<goal
name="WP_parameter testHarness.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="precondition"
sum="69da9041861124c8756e46a221481341"
......@@ -184,7 +184,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="6.90"/>
<result status="valid" time="6.70"/>
</proof>
<proof
prover="9"
......@@ -197,7 +197,7 @@
</goal>
<goal
name="WP_parameter testHarness.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="precondition"
sum="1d71a5288b3a272778794d9a2d86d6e6"
......@@ -249,7 +249,7 @@
</goal>
<goal
name="WP_parameter testHarness.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="precondition"
sum="b11a88e1fb495eae651e783d3aad626c"
......@@ -301,7 +301,7 @@
</goal>
<goal
name="WP_parameter testHarness.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="precondition"
sum="0a106269cd9cf3ff25941bc6c130657e"
......@@ -332,7 +332,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -353,7 +353,7 @@
</goal>
<goal
name="WP_parameter testHarness.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="08d823c5b7c119a9cb915fc2b46b2094"
......@@ -368,7 +368,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -376,12 +376,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter testHarness.7"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="b1b3cc7069aae35bb6d220c7cefa8d94"
......@@ -401,7 +401,7 @@
</goal>
<goal
name="WP_parameter testHarness.8"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="85be482096780dedf8e28254f104a7d7"
......@@ -445,7 +445,7 @@
</goal>
<goal
name="WP_parameter testHarness.9"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="c270911410758ef949ea7cd52cdaf88a"
......@@ -460,7 +460,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
......@@ -468,7 +468,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -476,12 +476,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.47"/>
<result status="valid" time="0.46"/>
</proof>
</goal>
<goal
name="WP_parameter testHarness.10"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="3db05dc8a8b3fdc4d9e5fb139a776499"
......@@ -517,7 +517,7 @@
</goal>
<goal
name="WP_parameter testHarness.11"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="183c2668a47704a1fa2a2d9772f71bd7"
......@@ -545,7 +545,7 @@
</goal>
<goal
name="WP_parameter testHarness.12"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../test_harness.mlw"
locfile="proofs/../test_harness.mlw"
loclnum="15" loccnumb="4" loccnume="15"
expl="assertion"
sum="083bebe31b6eb9a8cc4873a7a2435938"
......@@ -581,13 +581,13 @@
expanded="false">
<theory
name="Elements"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="1" loccnumb="7" loccnume="15"
verified="true"
expanded="false">
<goal
name="Elements_singleton"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="19" loccnumb="6" loccnume="24"
sum="c943ed821ea5a2c5048cfd0956dbcae4"
proved="true"
......@@ -604,7 +604,7 @@
</goal>
<goal
name="Elements_union"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="23" loccnumb="6" loccnume="20"
sum="abd6baefd84cabded06935ab9c02fe7a"
proved="true"
......@@ -617,12 +617,12 @@
edited="elements_Elements_Elements_union_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="Elements_add1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="27" loccnumb="6" loccnume="19"
sum="f654669372089a77ecc2f309333e729a"
proved="true"
......@@ -635,7 +635,7 @@
edited="elements_Elements_Elements_add1_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.49"/>
</proof>
<proof
prover="9"
......@@ -643,12 +643,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.52"/>
<result status="valid" time="0.51"/>
</proof>
</goal>
<goal
name="Elements_remove_last"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="31" loccnumb="6" loccnume="26"
sum="569c81c80e0fbe28f0176bfb192166da"
proved="true"
......@@ -680,16 +680,16 @@
</proof>
<proof
prover="4"
timelimit="11"
timelimit="12"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="5.58"/>
<result status="valid" time="5.06"/>
</proof>
</goal>
<goal
name="Occ_elements"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="35" loccnumb="6" loccnume="18"
sum="e4f018fd40e706aa1f8212411ca88262"
proved="true"
......@@ -707,7 +707,7 @@
</goal>
<goal
name="Elements_set_outside"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="39" loccnumb="6" loccnume="26"
sum="631e5ec678cf665b673419965eb6fa00"
proved="true"
......@@ -720,12 +720,12 @@
edited="elements_Elements_Elements_set_outside_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.64"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal
name="Elements_set_inside"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="43" loccnumb="6" loccnume="25"
sum="8ac96634e8d8d7f754de49584f95b247"
proved="true"
......@@ -738,12 +738,12 @@
edited="elements_Elements_Elements_set_inside_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.59"/>
<result status="valid" time="0.54"/>
</proof>
</goal>
<goal
name="Elements_set_inside2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../elements.why"
locfile="proofs/../elements.why"
loclnum="48" loccnumb="6" loccnume="26"
sum="2fc8184354c7170e0e79faa6a339b425"
proved="true"
......@@ -774,13 +774,13 @@
expanded="false">
<theory
name="Bag_integers"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../bag_of_integers.why"
locfile="proofs/../bag_of_integers.why"
loclnum="1" loccnumb="7" loccnume="19"
verified="true"
expanded="false">
<goal
name="Min_bag_union1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../bag_of_integers.why"
locfile="proofs/../bag_of_integers.why"
loclnum="16" loccnumb="6" loccnume="20"
sum="166a5014079365e4b9bc2250c48e06a9"
proved="true"
......@@ -792,15 +792,15 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
timelimit="30"
timelimit="32"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="15.77"/>
<result status="valid" time="15.28"/>
</proof>
<proof
prover="0"
......@@ -824,7 +824,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
......@@ -832,7 +832,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.21"/>
<result status="valid" time="1.18"/>
</proof>
<proof
prover="4"
......@@ -845,7 +845,7 @@
</goal>
<goal
name="Min_bag_union2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../bag_of_integers.why"
locfile="proofs/../bag_of_integers.why"
loclnum="19" loccnumb="6" loccnume="20"
sum="7f61ef5ba47f082a2852d60d6fe94e25"
proved="true"
......@@ -865,7 +865,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.64"/>
<result status="valid" time="0.63"/>
</proof>
<proof
prover="1"
......@@ -897,7 +897,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.79"/>
<result status="valid" time="0.73"/>
</proof>
</goal>
</theory>
......@@ -908,13 +908,13 @@
expanded="false">
<theory
name="WP Implementation"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="2" loccnumb="7" loccnume="21"
verified="true"
expanded="false">
<goal
name="Is_heap_min"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="13" loccnumb="6" loccnume="17"
sum="90d9dd8526d185c49a5266ba72cfa636"
proved="true"
......@@ -927,12 +927,12 @@
edited="heap_implem_WP_Implementation_Is_heap_min_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.64"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal
name="WP_parameter create"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="20" loccnumb="4" loccnume="10"
expl="normal postcondition"
sum="a90359ca1f094b943b45eaf87eb66b2d"
......@@ -955,7 +955,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="7.20"/>
<result status="valid" time="7.16"/>
</proof>
<proof
prover="1"
......@@ -971,7 +971,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
......@@ -979,7 +979,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
<result status="valid" time="0.46"/>
</proof>
<proof
prover="4"
......@@ -992,7 +992,7 @@
</goal>
<goal
name="WP_parameter insert"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="9d56132a02c117a2f4a7e0acbfb4481f"
......@@ -1007,7 +1007,7 @@
expanded="false">
<goal
name="WP_parameter insert.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="loop invariant init"
sum="e32dd95354e54f0a333d07bc0ead1af7"
......@@ -1038,7 +1038,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="9"
......@@ -1046,12 +1046,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter insert.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="assertion"
sum="867e0346e23306b979fb5b5963e6b19d"
......@@ -1060,58 +1060,26 @@
shape="ais_heapaTuple2V6V7Iainfix &lt;V3V2Aainfix &lt;c0V3Iainfix =aTuple2V6V7aTuple2V5ainfix +V2c1FIainfix =V5amixfix [&lt;-]V4V3V0FIainfix &gt;=V0agetV4adivainfix -V3c1c2Iainfix &gt;V3c0Iainfix =aelementsV4c0ainfix +V2c1aaddamixfix []V4V3aelementsV1c0V2Aainfix &gt;amixfix []V4V3V0Aais_heap_arrayV4c0ainfix +V2c1Iainfix &lt;V3V2Aainfix =aelementsV4c0V2aelementsV1c0V2Aais_heap_arrayV4c0V2Iainfix =V3V2Aainfix &lt;=V3V2Aainfix &lt;=c0V3FFIais_heapaTuple2V1V2FF">
<label
name="expl:parameter insert"/>
<proof
prover="10"
timelimit="20"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="20.20"/>
</proof>
<proof
prover="1"
timelimit="20"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="20.03"/>
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.81"/>
<result status="valid" time="2.79"/>
</proof>
<proof
prover="2"
timelimit="28"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="14.58"/>
</proof>
<proof
prover="11"
timelimit="20"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="20.05"/>
</proof>
<proof
prover="9"
timelimit="10"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.22"/>
<result status="valid" time="13.55"/>
</proof>
</goal>
<goal
name="WP_parameter insert.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="assertion"
sum="233f94a622107f807656251bb60c0d30"
......@@ -1126,7 +1094,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
......@@ -1155,7 +1123,7 @@
</goal>
<goal
name="WP_parameter insert.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="normal postcondition"
sum="d537329f9a4f1f1e23a7208aac7a2eee"
......@@ -1170,7 +1138,7 @@
expanded="false">
<goal
name="WP_parameter insert.4.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="3c738372b107962914c161ad4f4a8594"
......@@ -1185,36 +1153,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
</proof>
<proof
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.04"/>
</proof>
<proof
prover="11"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.11"/>
</proof>
<proof
prover="9"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal
name="WP_parameter insert.4.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="bf7ae4fc99e5be3c555e1fbd3956ad60"
......@@ -1245,14 +1189,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter insert.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="loop invariant preservation"
sum="6d7f5b8a38bc419bf82f42db88911f20"
......@@ -1267,7 +1211,7 @@
expanded="false">
<goal
name="WP_parameter insert.5.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="3bc49de605de727650c81647ef88111b"
......@@ -1306,12 +1250,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter insert.5.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="ee584d193542fbb717ddb2afa21122e0"
......@@ -1342,7 +1286,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -1358,7 +1302,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.11"/>
<result status="valid" time="1.10"/>
</proof>
<proof
prover="9"
......@@ -1374,12 +1318,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.23"/>
<result status="valid" time="0.22"/>
</proof>
</goal>
<goal
name="WP_parameter insert.5.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="56834e67db9d2bc3fee1bba4b6068302"
......@@ -1410,7 +1354,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.08"/>
</proof>
<proof
prover="9"
......@@ -1418,20 +1362,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
timelimit="18"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="17.94"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter insert.5.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="c1c23eeae5e9a1edc5b969aad5a6702f"
......@@ -1462,7 +1398,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="9"
......@@ -1470,20 +1406,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
timelimit="18"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="17.94"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter insert.5.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="27a11b4808c270f0611b165b5b702006"
......@@ -1498,7 +1426,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.13"/>
<result status="valid" time="1.12"/>
</proof>
<proof
prover="1"
......@@ -1506,20 +1434,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.75"/>
</proof>
<proof
prover="9"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.03"/>
<result status="valid" time="0.78"/>
</proof>
</goal>
<goal
name="WP_parameter insert.5.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="74ac692940a2ee8749b869c5e2a29c32"
......@@ -1534,7 +1454,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
......@@ -1555,7 +1475,7 @@
</goal>
<goal
name="WP_parameter insert.5.7"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="3ba18c168948761f0ecc070b4597df35"
......@@ -1578,7 +1498,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.10"/>
</proof>
<proof
prover="9"
......@@ -1593,7 +1513,7 @@
</goal>
<goal
name="WP_parameter insert.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="loop variant decreases"
sum="c9f69fcf70cac46c8c95fa51ce80e3b3"
......@@ -1616,7 +1536,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
......@@ -1624,7 +1544,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -1632,7 +1552,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.09"/>
</proof>
<proof
prover="8"
......@@ -1661,7 +1581,7 @@
</goal>
<goal
name="WP_parameter insert.7"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="assertion"
sum="df2a01ec47a68700d7429c0728dc5646"
......@@ -1684,7 +1604,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -1692,7 +1612,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -1713,7 +1633,7 @@
</goal>
<goal
name="WP_parameter insert.8"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="assertion"
sum="a6e6013d3a510cac6f180db407bccf61"
......@@ -1728,7 +1648,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
......@@ -1752,12 +1672,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter insert.9"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="normal postcondition"
sum="bd56262023b58a61bcd6d5b7d60c92a5"
......@@ -1772,7 +1692,7 @@
expanded="false">
<goal
name="WP_parameter insert.9.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="cbd9ac9c115affc81ab628bc1285bd26"
......@@ -1787,7 +1707,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.29"/>
<result status="valid" time="0.28"/>
</proof>
<proof
prover="0"
......@@ -1795,12 +1715,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.30"/>
<result status="valid" time="0.29"/>
</proof>
</goal>
<goal
name="WP_parameter insert.9.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="28" loccnumb="4" loccnume="10"
expl="parameter insert"
sum="a204de0630ef09be5eb89b722c30856f"
......@@ -1815,7 +1735,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
......@@ -1823,7 +1743,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.23"/>
<result status="valid" time="0.21"/>
</proof>
<proof
prover="1"
......@@ -1839,7 +1759,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.70"/>
<result status="valid" time="3.68"/>
</proof>
<proof
prover="9"
......@@ -1847,7 +1767,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
......@@ -1864,7 +1784,7 @@
</goal>
<goal
name="WP_parameter extractMin"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="a6407744c4633b1f4bdbb8f97b60ca5e"
......@@ -1879,7 +1799,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="9b52055e46d636c5bb73d411f8527f92"
......@@ -1894,7 +1814,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -1910,7 +1830,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -1918,12 +1838,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="fbe7ef6c91b231c9cf9e2f938267513c"
......@@ -1939,12 +1859,12 @@
edited="heap_implem_WP_Implementation_WP_parameter_extractMin_3.v"
obsolete="false"
archived="false">
<result status="valid" time="0.64"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop invariant init"
sum="543d33e06e66f6a01aa0bb8f193afb1b"
......@@ -1959,7 +1879,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.3.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="a999e5818a6213f68f47d9edef0cf480"
......@@ -1990,7 +1910,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -2011,7 +1931,7 @@
</goal>
<goal
name="WP_parameter extractMin.3.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="c884ed705a2ffad83ba2f99d35605bde"
......@@ -2034,7 +1954,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -2042,7 +1962,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -2063,7 +1983,7 @@
</goal>
<goal
name="WP_parameter extractMin.3.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="d92877a34fe77d1fee778f6656a473f2"
......@@ -2099,7 +2019,7 @@
</goal>
<goal
name="WP_parameter extractMin.3.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="ef869bf6cf48ac7f697589b94ca0d252"
......@@ -2130,7 +2050,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -2162,7 +2082,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -2175,7 +2095,7 @@
</goal>
<goal
name="WP_parameter extractMin.3.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="00fe3f76bb0be590b828a9f11c6eb4f9"
......@@ -2198,7 +2118,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.15"/>
<result status="valid" time="0.14"/>
</proof>
<proof
prover="0"
......@@ -2206,7 +2126,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="9"
......@@ -2214,12 +2134,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.17"/>
<result status="valid" time="1.09"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.3.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="c85239a1674b00d09ee3b68c1311e0d3"
......@@ -2273,7 +2193,7 @@
</goal>
<goal
name="WP_parameter extractMin.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="f974122f70788665fb77ed0df8c4dfc7"
......@@ -2288,12 +2208,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.54"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="0751c9c28be04f537d04e6574f6c82bf"
......@@ -2308,7 +2228,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
......@@ -2329,7 +2249,7 @@
</goal>
<goal
name="WP_parameter extractMin.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="18d79b75be44b95633ce3b26248b1994"
......@@ -2344,20 +2264,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.19"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.03"/>
<result status="valid" time="0.18"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.7"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="3fa8477822025b495b4710bbf3bd2dc5"
......@@ -2372,7 +2284,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.7.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="756a1e9731e6d268870cfc3a7b6332a5"
......@@ -2400,7 +2312,7 @@
</goal>
<goal
name="WP_parameter extractMin.7.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="f4fb1b548991e064286aa50492392986"
......@@ -2423,7 +2335,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.83"/>
<result status="valid" time="0.79"/>
</proof>
<proof
prover="1"
......@@ -2447,12 +2359,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.22"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.7.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="c2cc016975c966aeba0f90e0e804cfac"
......@@ -2475,14 +2387,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.14"/>
<result status="valid" time="1.06"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter extractMin.8"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="065671c7ca80b7b80cc816bed8c88e1d"
......@@ -2497,7 +2409,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.8.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="6b7e68de54b3f5adf0d8a047139cc759"
......@@ -2520,7 +2432,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -2573,7 +2485,7 @@
</goal>
<goal
name="WP_parameter extractMin.8.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="74a277702780086f07bddf603ca8ff29"
......@@ -2604,7 +2516,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -2649,7 +2561,7 @@
</goal>
<goal
name="WP_parameter extractMin.8.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="492cc0be36a4f4f4e18192713bc5f948"
......@@ -2672,7 +2584,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -2704,7 +2616,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
......@@ -2712,7 +2624,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -2727,7 +2639,7 @@
</goal>
<goal
name="WP_parameter extractMin.9"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="7594a96570e4830624ec71d5737338b6"
......@@ -2742,12 +2654,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.73"/>
<result status="valid" time="0.72"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.10"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="cc564be5248d63adac7f5c7dbe9ed60f"
......@@ -2767,7 +2679,7 @@
</goal>
<goal
name="WP_parameter extractMin.11"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="c47e16130b8ca8b7289c05fc141d1bbc"
......@@ -2782,7 +2694,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.22"/>
</proof>
<proof
prover="1"
......@@ -2790,12 +2702,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.12"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="0e0c5ee432634b98ea272f4ead00a714"
......@@ -2810,7 +2722,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.12.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="d07ebee0fd693f0e41f36d6df2850a82"
......@@ -2825,7 +2737,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
......@@ -2833,7 +2745,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="9"
......@@ -2846,7 +2758,7 @@
</goal>
<goal
name="WP_parameter extractMin.12.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="60a6b8335411cc7d9bc98a1ef6a48098"
......@@ -2869,7 +2781,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.89"/>
<result status="valid" time="0.86"/>
</proof>
<proof
prover="1"
......@@ -2877,7 +2789,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="9"
......@@ -2898,7 +2810,7 @@
</goal>
<goal
name="WP_parameter extractMin.12.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="22bed695f3cacba9812e71b54738e41d"
......@@ -2915,14 +2827,6 @@
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="0"
timelimit="16"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="16.09"/>
</proof>
<proof
prover="1"
timelimit="3"
......@@ -2944,7 +2848,7 @@
</goal>
<goal
name="WP_parameter extractMin.13"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="c695e1309645ce40ccaa267af9c26ac2"
......@@ -2967,7 +2871,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -2983,7 +2887,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -2999,7 +2903,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -3020,7 +2924,7 @@
</goal>
<goal
name="WP_parameter extractMin.14"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop invariant preservation"
sum="0506243cbe85053ef5119c8f96680bc4"
......@@ -3035,7 +2939,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.14.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="6fdd6a23ef7221f77d2c918525d53981"
......@@ -3074,12 +2978,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.14.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="36e3126ac767ac786b9510e983f88d72"
......@@ -3142,7 +3046,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -3155,7 +3059,7 @@
</goal>
<goal
name="WP_parameter extractMin.14.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="152cf809c8e6dea50beabfe4cadd3aef"
......@@ -3164,90 +3068,18 @@
shape="ais_heap_arrayV5c0ainfix -V1c1Iainfix =V6V4FIainfix =V5amixfix [&lt;-]V3V2amixfix []V3V4FIainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3V4NIainfix =V4ainfix +ainfix *c2V2c2FIainfix &gt;amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2Iainfix &lt;ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix &gt;=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix &lt;V2ainfix -V1c1Iainfix &lt;amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix &gt;V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix &lt;V2ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V2FFIainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Iainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<proof
prover="7"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.90"/>
</proof>
<proof
prover="10"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.11"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.11"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.11"/>
</proof>
<proof
prover="2"
timelimit="50"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="25.50"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.05"/>
</proof>
<proof
prover="11"
timelimit="30"
timelimit="52"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.15"/>
</proof>
<proof
prover="9"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="6.79"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="29.90"/>
<result status="valid" time="23.96"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.14.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="4868748b9c79e7f405ff4128dfb06a07"
......@@ -3291,7 +3123,7 @@
</goal>
<goal
name="WP_parameter extractMin.14.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="be2190b08a19c9694ed03998a5bb0f34"
......@@ -3306,7 +3138,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.33"/>
<result status="valid" time="0.32"/>
</proof>
<proof
prover="1"
......@@ -3327,7 +3159,7 @@
</goal>
<goal
name="WP_parameter extractMin.14.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="bdbb97fc4e5dcc455e7f167615b9030e"
......@@ -3350,7 +3182,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="0.70"/>
</proof>
<proof
prover="9"
......@@ -3365,7 +3197,7 @@
</goal>
<goal
name="WP_parameter extractMin.15"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop variant decreases"
sum="2441976491e2901d302e503ff5677f2c"
......@@ -3388,7 +3220,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="0"
......@@ -3404,12 +3236,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.16"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="5027a0d78ec49842ad190409b0d2d973"
......@@ -3429,7 +3261,7 @@
</goal>
<goal
name="WP_parameter extractMin.17"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="42b639236dcaa3cca5470869c4d0a82d"
......@@ -3449,7 +3281,7 @@
</goal>
<goal
name="WP_parameter extractMin.18"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="3d588bffc22819ddaebc297a4ab45328"
......@@ -3466,18 +3298,10 @@
archived="false">
<result status="valid" time="0.21"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.12"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.19"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="9b4e70c5e33fcf17f58e8b165d177f3c"
......@@ -3492,7 +3316,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.19.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="a16e9f9e4ac22688e430dfdad03c60e3"
......@@ -3528,7 +3352,7 @@
</goal>
<goal
name="WP_parameter extractMin.19.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="785df395dbf992906f51f277bbeca863"
......@@ -3543,7 +3367,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.13"/>
</proof>
<proof
prover="7"
......@@ -3551,7 +3375,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.83"/>
<result status="valid" time="0.84"/>
</proof>
<proof
prover="1"
......@@ -3559,7 +3383,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="9"
......@@ -3575,12 +3399,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.22"/>
<result status="valid" time="0.21"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.19.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="6a0328089c9bf5c53cdea5e0242334e7"
......@@ -3611,14 +3435,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.19"/>
<result status="valid" time="1.14"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter extractMin.20"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="0366b51e26555309f9125982af816c75"
......@@ -3633,7 +3457,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.20.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="6590f6e88d982f54fd9afb96c07fa2db"
......@@ -3656,7 +3480,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -3696,7 +3520,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -3709,7 +3533,7 @@
</goal>
<goal
name="WP_parameter extractMin.20.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="15ca6bc382ab68dd299787d8116ebf7f"
......@@ -3732,7 +3556,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
......@@ -3748,7 +3572,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -3772,7 +3596,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -3785,7 +3609,7 @@
</goal>
<goal
name="WP_parameter extractMin.20.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="ae08fd661d7d62c04159f92dce1fafaf"
......@@ -3808,7 +3632,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -3863,7 +3687,7 @@
</goal>
<goal
name="WP_parameter extractMin.21"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop invariant preservation"
sum="0130bcb0bbcdc924f498c518dbd3232d"
......@@ -3878,7 +3702,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.21.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="77fc9d772bb964fb4bc3924726e20b51"
......@@ -3922,7 +3746,7 @@
</goal>
<goal
name="WP_parameter extractMin.21.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="ca154bc10d68f1ffcf5f5d8d15b5edcf"
......@@ -3945,7 +3769,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
......@@ -3953,7 +3777,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
......@@ -3961,7 +3785,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -3977,7 +3801,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="9"
......@@ -3998,99 +3822,27 @@
</goal>
<goal
name="WP_parameter extractMin.21.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="c201920e3bbb92ee8d41f434e66e6dcf"
proved="true"
expanded="false"
shape="ais_heap_arrayV4c0ainfix -V1c1Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [&lt;-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix &gt;amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2NIainfix &lt;ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix &gt;=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix &lt;V2ainfix -V1c1Iainfix &lt;amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix &gt;V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix &lt;V2ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V2FFIainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Iainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<proof
prover="7"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.17"/>
</proof>
<proof
prover="10"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.13"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.04"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.05"/>
</proof>
<proof
prover="2"
timelimit="60"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="26.04"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.02"/>
</proof>
<proof
prover="11"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.06"/>
</proof>
<proof
prover="9"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="5.77"/>
</proof>
expanded="false"
shape="ais_heap_arrayV4c0ainfix -V1c1Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [&lt;-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix &gt;amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2NIainfix &lt;ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix &gt;=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix &lt;V2ainfix -V1c1Iainfix &lt;amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix &gt;V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix &lt;V2ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V2FFIainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Iainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<proof
prover="4"
timelimit="30"
prover="2"
timelimit="60"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="29.91"/>
<result status="valid" time="22.62"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.21.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="f88c9faf6b062fe3f43dd0b3c189c2b9"
......@@ -4134,7 +3886,7 @@
</goal>
<goal
name="WP_parameter extractMin.21.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="f360a4cd541b34cd63e7c64089a79971"
......@@ -4149,7 +3901,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.09"/>
</proof>
<proof
prover="1"
......@@ -4165,12 +3917,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.21.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="5cf8d4418786dc409e4ce089d907ee6f"
......@@ -4185,7 +3937,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.34"/>
<result status="valid" time="0.32"/>
</proof>
<proof
prover="1"
......@@ -4193,7 +3945,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="9"
......@@ -4208,7 +3960,7 @@
</goal>
<goal
name="WP_parameter extractMin.22"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop variant decreases"
sum="aeade6cdc17e2b2867fda32592e30e4c"
......@@ -4231,7 +3983,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
......@@ -4252,7 +4004,7 @@
</goal>
<goal
name="WP_parameter extractMin.23"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="c7a4305f24cb4fc6451e49d14e3ba936"
......@@ -4267,12 +4019,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.05"/>
<result status="valid" time="1.00"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.24"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="f47c1c09a1a5dc93070265c622e55a44"
......@@ -4287,7 +4039,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="0"
......@@ -4303,12 +4055,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.25"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="dedf6bed1501b3f88b4106ef01cc4485"
......@@ -4323,20 +4075,20 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.18"/>
</proof>
<proof
prover="1"
timelimit="11"
timelimit="12"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="5.73"/>
<result status="valid" time="5.19"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.26"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="745c89fa456c1f15c717a5b6aa6ad1e6"
......@@ -4351,20 +4103,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.91"/>
</proof>
<proof
prover="9"
timelimit="19"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="9.81"/>
<result status="valid" time="0.93"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.27"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="cebc044ad35cb60608be1123f2f1365d"
......@@ -4387,7 +4131,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -4427,7 +4171,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -4435,12 +4179,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.28"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop invariant preservation"
sum="31b6e6e0c5590c0dfeb529844038baaa"
......@@ -4455,7 +4199,7 @@
expanded="false">
<goal
name="WP_parameter extractMin.28.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="270fd74295295beb0995d21155e0039c"
......@@ -4478,7 +4222,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
......@@ -4494,12 +4238,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.28.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="02d1684f07bd77066e286e820d7d0630"
......@@ -4514,7 +4258,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="7"
......@@ -4530,7 +4274,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
......@@ -4538,7 +4282,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
......@@ -4562,7 +4306,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
......@@ -4575,7 +4319,7 @@
</goal>
<goal
name="WP_parameter extractMin.28.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="f68e2498b8078aff8f91ab33279c887a"
......@@ -4584,90 +4328,18 @@
shape="ais_heap_arrayV4c0ainfix -V1c1Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [&lt;-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix &lt;=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix &lt;ainfix +ainfix *c2V2c2ainfix -V1c1NIainfix &gt;=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix &lt;V2ainfix -V1c1Iainfix &lt;amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix &gt;V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix &gt;ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix &lt;V2ainfix -V1c1Iainfix &gt;ainfix -V1c1c0Aainfix &lt;=c0V2FFIainfix &gt;anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix &gt;ainfix -V1c1c0Iainfix &gt;V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<label
name="expl:parameter extractMin"/>
<proof
prover="10"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.12"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.61"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.12"/>
</proof>
<proof
prover="0"
timelimit="60"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="60.09"/>
</proof>
<proof
prover="2"
timelimit="300"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="114.24"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="30.08"/>
</proof>
<proof
prover="11"
timelimit="60"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="60.08"/>
</proof>
<proof
prover="9"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="7.89"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="29.91"/>
<result status="valid" time="115.00"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.28.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="843ca4346f62b24acf1cef7fcbde0fc1"
......@@ -4711,7 +4383,7 @@
</goal>
<goal
name="WP_parameter extractMin.28.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="2a14c2eacdeab016704427cd75c95c96"
......@@ -4726,7 +4398,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="0"
......@@ -4734,12 +4406,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.28.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="parameter extractMin"
sum="50a02a512eb5f428714533b1c57e8196"
......@@ -4754,7 +4426,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="0"
......@@ -4762,7 +4434,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.30"/>
<result status="valid" time="0.31"/>
</proof>
<proof
prover="9"
......@@ -4770,14 +4442,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter extractMin.29"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="loop variant decreases"
sum="bb998c04f54c6f52fb755b6be87d68ea"
......@@ -4816,12 +4488,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.30"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="9dde311a11aab34a79815f15e36c09f7"
......@@ -4860,12 +4532,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.31"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="3288d35acdca0e7bcbb32824d5464caf"
......@@ -4888,7 +4560,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
......@@ -4920,7 +4592,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
......@@ -4941,7 +4613,7 @@
</goal>
<goal
name="WP_parameter extractMin.32"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="552342ef61d3d21eb95de0f733a55a99"
......@@ -4972,7 +4644,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -4996,7 +4668,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -5017,7 +4689,7 @@
</goal>
<goal
name="WP_parameter extractMin.33"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="assertion"
sum="c98fb9b3df138db9c2ea9bcbe7bd7e66"
......@@ -5040,7 +4712,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -5080,7 +4752,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -5093,7 +4765,7 @@
</goal>
<goal
name="WP_parameter extractMin.34"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="2f33ee779dd1a6a5c0298998dfe61194"
......@@ -5164,12 +4836,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter extractMin.35"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_implem.mlw"
locfile="proofs/../heap_implem.mlw"
loclnum="61" loccnumb="4" loccnume="14"
expl="normal postcondition"
sum="57187484d917803113cc08b19830e5ff"
......@@ -5184,7 +4856,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.15"/>
</proof>
<proof
prover="1"
......@@ -5192,7 +4864,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.17"/>
</proof>
<proof
prover="0"
......@@ -5200,7 +4872,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.09"/>
</proof>
<proof
prover="9"
......@@ -5208,7 +4880,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.09"/>
<result status="valid" time="1.06"/>
</proof>
</goal>
</transf>
......@@ -5221,7 +4893,7 @@
expanded="false">
<theory
name="WP AbstractHeap"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../abstract_heap.mlw"
locfile="proofs/../abstract_heap.mlw"
loclnum="2" loccnumb="7" loccnume="19"
verified="true"
expanded="false">
......@@ -5233,13 +4905,13 @@
expanded="false">
<theory
name="WP HeapSort"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="2" loccnumb="7" loccnume="15"
verified="true"
expanded="false">
<goal
name="Min_of_sorted"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="15" loccnumb="6" loccnume="19"
sum="5f48b906bd6ff1c9198e09d700985e5e"
proved="true"
......@@ -5252,12 +4924,12 @@
edited="heapsort_WP_HeapSort_Min_of_sorted_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="0.68"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="dd41a24caf4cda99ed56362bff789d74"
......@@ -5272,7 +4944,7 @@
expanded="false">
<goal
name="WP_parameter heapSort.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="precondition"
sum="fe210e1138ec2e99b6c06f667161c687"
......@@ -5295,7 +4967,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -5316,7 +4988,7 @@
</goal>
<goal
name="WP_parameter heapSort.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="normal postcondition"
sum="2732b65a1e775a0397b2607bd1f9d632"
......@@ -5355,12 +5027,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop initialization"
sum="ffd53fedf78a7c42d454fc05a5d6f595"
......@@ -5375,7 +5047,7 @@
expanded="false">
<goal
name="WP_parameter heapSort.3.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="f3f62814b0e2d9c080dc1f4178a5df5e"
......@@ -5406,7 +5078,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -5419,7 +5091,7 @@
</goal>
<goal
name="WP_parameter heapSort.3.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="729077201d51677f0e49f45344bbc121"
......@@ -5444,18 +5116,10 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.97"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.3.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="80b3fea2074fdd33ce6df0921c1e0285"
......@@ -5486,15 +5150,15 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="17"
timelimit="18"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="8.68"/>
<result status="valid" time="9.01"/>
</proof>
<proof
prover="9"
......@@ -5507,7 +5171,7 @@
</goal>
<goal
name="WP_parameter heapSort.3.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="56edb7b29d1042b7e19a022f41836195"
......@@ -5551,7 +5215,7 @@
</goal>
<goal
name="WP_parameter heapSort.3.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="1ee4380c6b8d9b90ea8855f191f5544e"
......@@ -5571,7 +5235,7 @@
</goal>
<goal
name="WP_parameter heapSort.3.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="parameter heapSort"
sum="7aa79d771c2fb46c9238b0605d31d16a"
......@@ -5602,7 +5266,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -5617,7 +5281,7 @@
</goal>
<goal
name="WP_parameter heapSort.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="fc5b58d9abe96fc422a560fa07c9900b"
......@@ -5632,7 +5296,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -5656,12 +5320,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.65"/>
<result status="valid" time="3.69"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="normal postcondition"
sum="b6594d6ca24759f9dd6d896c9bfe1206"
......@@ -5713,7 +5377,7 @@
</goal>
<goal
name="WP_parameter heapSort.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop initialization"
sum="2a7f55ed5c7efdc40240735cb0f6c108"
......@@ -5736,7 +5400,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -5746,14 +5410,6 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="10"
......@@ -5762,18 +5418,10 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.97"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.7"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="518a3bc8c99a509ac31a5682ac436580"
......@@ -5788,7 +5436,7 @@
expanded="false">
<goal
name="WP_parameter heapSort.7.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="d729e23b0241537ed4f352358ac23622"
......@@ -5808,7 +5456,7 @@
</goal>
<goal
name="WP_parameter heapSort.7.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="64a42c228cf2429332cbdd6f50fe4014"
......@@ -5823,7 +5471,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -5839,7 +5487,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
......@@ -5847,7 +5495,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.93"/>
<result status="valid" time="0.91"/>
</proof>
<proof
prover="9"
......@@ -5863,12 +5511,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.77"/>
<result status="valid" time="0.80"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.7.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="ad44d2ce0e7ee0bffc85d92830951610"
......@@ -5883,12 +5531,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.7.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="6c788274f473644b6440c381d622b2b1"
......@@ -5932,7 +5580,7 @@
</goal>
<goal
name="WP_parameter heapSort.7.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="158298ef52eafc7c65c1846757df3b9e"
......@@ -5963,7 +5611,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -5973,20 +5621,12 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.97"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter heapSort.8"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="normal postcondition"
sum="ab52bc5d0f26dd1253cfaf9267fcbfd5"
......@@ -6009,7 +5649,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -6038,7 +5678,7 @@
</goal>
<goal
name="WP_parameter heapSort.9"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop initialization"
sum="accac1b657e88cc9e9d69eb0cc0bb7d5"
......@@ -6061,7 +5701,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -6071,14 +5711,6 @@
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="8"
timelimit="116"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="115.80"/>
</proof>
<proof
prover="9"
timelimit="10"
......@@ -6090,7 +5722,7 @@
</goal>
<goal
name="WP_parameter heapSort.10"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="568450193c5d0d1836a1511758dfe710"
......@@ -6105,7 +5737,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.71"/>
<result status="valid" time="3.72"/>
</proof>
<transf
name="split_goal"
......@@ -6113,7 +5745,7 @@
expanded="false">
<goal
name="WP_parameter heapSort.10.1"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="f68231b94caee6897bc4d575c0268644"
......@@ -6133,7 +5765,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="3a2fc5e8edcab3e20ee10dc000cfa04a"
......@@ -6153,7 +5785,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.3"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="42e6f096ff4d573f0924674f6d3d1093"
......@@ -6168,12 +5800,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="7.12"/>
<result status="valid" time="7.20"/>
</proof>
</goal>
<goal
name="WP_parameter heapSort.10.4"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="b46473c4eb9e3d3413c37c3d75f85744"
......@@ -6193,7 +5825,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.5"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="8e7b0731fbcc9949df693f58dca8c220"
......@@ -6213,7 +5845,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.6"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="1bc815e9a0a0f3d55fbf78f9254da694"
......@@ -6233,7 +5865,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.7"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="93e2f824cb0ffd0aa56e5e3aa68d7b1e"
......@@ -6243,12 +5875,12 @@
<label
name="expl:parameter heapSort"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
prover="10"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="11"
......@@ -6261,7 +5893,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.8"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="b210722cfbe7ca149ef8dfc09ef3c1ed"
......@@ -6281,7 +5913,7 @@
</goal>
<goal
name="WP_parameter heapSort.10.9"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="for loop preservation"
sum="fad8525b2f58b10b8efc013e9ab395c5"
......@@ -6303,7 +5935,7 @@
</goal>
<goal
name="WP_parameter heapSort.11"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heapsort.mlw"
locfile="proofs/../heapsort.mlw"
loclnum="22" loccnumb="4" loccnume="12"
expl="normal postcondition"
sum="ce5476b6e75a4e80f0b81436cc23141c"
......@@ -6334,7 +5966,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="9"
......@@ -6342,15 +5974,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.19"/>
</proof>
<proof
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="9.97"/>
<result status="valid" time="1.17"/>
</proof>
</goal>
</transf>
......@@ -6363,13 +5987,13 @@
expanded="false">
<theory
name="Model"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_model.why"
locfile="proofs/../heap_model.why"
loclnum="1" loccnumb="7" loccnume="12"
verified="true"
expanded="false">
<goal
name="Model_empty"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_model.why"
locfile="proofs/../heap_model.why"
loclnum="13" loccnumb="6" loccnume="17"
sum="cdd521c7a28461970bb283be71e5744e"
proved="true"
......@@ -6389,7 +6013,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -6397,7 +6021,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
......@@ -6421,7 +6045,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.17"/>
<result status="valid" time="0.16"/>
</proof>
<proof
prover="4"
......@@ -6434,7 +6058,7 @@
</goal>
<goal
name="Model_singleton"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_model.why"
locfile="proofs/../heap_model.why"
loclnum="16" loccnumb="6" loccnume="21"
sum="1b8270a6adf23495c1c92caaf776c0e1"
proved="true"
......@@ -6446,7 +6070,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="7"
......@@ -6454,7 +6078,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="1"
......@@ -6494,12 +6118,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="6.92"/>
<result status="valid" time="7.07"/>
</proof>
</goal>
<goal
name="Model_set"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_model.why"
locfile="proofs/../heap_model.why"
loclnum="18" loccnumb="6" loccnume="15"
sum="d89d58476bbb20c2cf6449d58ea621ce"
proved="true"
......@@ -6512,12 +6136,12 @@
edited="heap_model_Model_Model_set_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.68"/>
<result status="valid" time="0.64"/>
</proof>
</goal>
<goal
name="Model_add_last"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap_model.why"
locfile="proofs/../heap_model.why"
loclnum="24" loccnumb="6" loccnume="20"
sum="122cbb51c94bf71bdc7ffb7516574350"
proved="true"
......@@ -6556,13 +6180,13 @@
expanded="false">
<theory
name="Heap"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="3" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
<goal
name="Parent_inf"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="12" loccnumb="6" loccnume="16"
sum="c5cd55f39c7235e7a0937923b90446bc"
proved="true"
......@@ -6590,7 +6214,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
......@@ -6611,7 +6235,7 @@
</goal>
<goal
name="Left_sup"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="13" loccnumb="6" loccnume="14"
sum="b73b1a83065e251cea6e29cefaa410a3"
proved="true"
......@@ -6639,7 +6263,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
......@@ -6660,7 +6284,7 @@
</goal>
<goal
name="Right_sup"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="14" loccnumb="6" loccnume="15"
sum="472ace84d040f29bb301365d201d258f"
proved="true"
......@@ -6709,7 +6333,7 @@
</goal>
<goal
name="Parent_right"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="15" loccnumb="6" loccnume="18"
sum="0339c9d2ae772e7c27be7a099e40ebed"
proved="true"
......@@ -6729,7 +6353,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -6737,7 +6361,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
......@@ -6758,7 +6382,7 @@
</goal>
<goal
name="Parent_left"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="16" loccnumb="6" loccnume="17"
sum="73828f0db6207075d1c6679f244b0692"
proved="true"
......@@ -6778,7 +6402,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -6786,7 +6410,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
......@@ -6794,7 +6418,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="9"
......@@ -6807,7 +6431,7 @@
</goal>
<goal
name="Inf_parent"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="17" loccnumb="6" loccnume="16"
sum="0dd86f1172c417c1dcfa6f9ea329da59"
proved="true"
......@@ -6835,7 +6459,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
......@@ -6856,7 +6480,7 @@
</goal>
<goal
name="Child_parent"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="18" loccnumb="6" loccnume="18"
sum="5fcbdbf8a5b622d7d032c083fde63db1"
proved="true"
......@@ -6876,7 +6500,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.66"/>
<result status="valid" time="1.63"/>
</proof>
<proof
prover="0"
......@@ -6884,7 +6508,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.59"/>
<result status="valid" time="0.58"/>
</proof>
<proof
prover="6"
......@@ -6905,7 +6529,7 @@
</goal>
<goal
name="Parent_pos"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="20" loccnumb="6" loccnume="16"
sum="f217cd783a9f7402baf6efd2ebf9ea1d"
proved="true"
......@@ -6957,12 +6581,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="6.98"/>
<result status="valid" time="7.46"/>
</proof>
</goal>
<goal
name="Is_heap_when_no_element"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="39" loccnumb="6" loccnume="29"
sum="25fa611e98a5b08e901c5196525ff9f2"
proved="true"
......@@ -6982,7 +6606,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="5.99"/>
<result status="valid" time="5.67"/>
</proof>
<proof
prover="1"
......@@ -7019,7 +6643,7 @@
</goal>
<goal
name="Is_heap_sub"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="42" loccnumb="6" loccnume="17"
sum="9b583ba23cf83ca004a0d39d6585d084"
proved="true"
......@@ -7057,18 +6681,10 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="1.28"/>
</proof>
</goal>
<goal
name="Is_heap_sub2"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="47" loccnumb="6" loccnume="18"
sum="06fe5b717c5000a1abbb21dbaae3598a"
proved="true"
......@@ -7088,7 +6704,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -7109,7 +6725,7 @@
</goal>
<goal
name="Is_heap_when_node_modified"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="52" loccnumb="6" loccnume="32"
sum="e36ba5577d42e573e8d472eed6bb033c"
proved="true"
......@@ -7129,7 +6745,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.31"/>
<result status="valid" time="0.32"/>
</proof>
<proof
prover="0"
......@@ -7137,7 +6753,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.32"/>
<result status="valid" time="0.33"/>
</proof>
<proof
prover="9"
......@@ -7150,7 +6766,7 @@
</goal>
<goal
name="Is_heap_add_last"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="60" loccnumb="6" loccnume="22"
sum="dfa860e6891f54734375f5e440745e53"
proved="true"
......@@ -7170,7 +6786,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="9"
......@@ -7178,12 +6794,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="8.26"/>
<result status="valid" time="8.28"/>
</proof>
</goal>
<goal
name="Parent_inf_el"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="65" loccnumb="6" loccnume="19"
sum="eaf8b2bcceeb7d355234bb712beb58ca"
proved="true"
......@@ -7211,7 +6827,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
......@@ -7227,12 +6843,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.22"/>
<result status="valid" time="4.46"/>
</proof>
</goal>
<goal
name="Left_sup_el"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="70" loccnumb="6" loccnume="17"
sum="5157ea71a452435423d7e846fd0e3f0d"
proved="true"
......@@ -7276,7 +6892,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.93"/>
<result status="valid" time="5.07"/>
</proof>
<proof
prover="9"
......@@ -7292,12 +6908,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.64"/>
<result status="valid" time="4.67"/>
</proof>
</goal>
<goal
name="Right_sup_el"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="76" loccnumb="6" loccnume="18"
sum="9bed3da1e08a3c76d3e899b0ab1e43c3"
proved="true"
......@@ -7317,7 +6933,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -7333,7 +6949,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
......@@ -7341,7 +6957,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.79"/>
<result status="valid" time="4.89"/>
</proof>
<proof
prover="9"
......@@ -7349,7 +6965,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -7357,12 +6973,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.93"/>
<result status="valid" time="4.90"/>
</proof>
</goal>
<goal
name="Is_heap_relation"
locfile="examples/programs/vacid_0_binary_heaps/proofs/../heap.why"
locfile="proofs/../heap.why"
loclnum="82" loccnumb="6" loccnume="22"
sum="783f759f706fbc29957ede2c5070b4eb"
proved="true"
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment