Commit 47500c79 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update sessions

parent f82676b5
......@@ -47,7 +47,7 @@
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC binary_mult.11" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.73"/></proof>
<proof prover="3"><result status="valid" time="1.00"/></proof>
</goal>
<goal name="VC binary_mult.12" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -368,7 +368,7 @@ module AsciiCode
ensures { eq_sub_bv result b zeros lastbit }
ensures { validAscii result }
let c = count b in
let maskbit = lsl_check c (of_int 31) in
let maskbit = lsl_check c (31:t) in
assert { bw_and b maskbit = zeros };
assert { even (t'int c) ->
not (nth_bv c zeros)
......
......@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
......@@ -299,7 +300,7 @@
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC proof1.6.2" expl="VC for proof1" proved="true">
<proof prover="4"><result status="valid" time="1.00"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="96"/></proof>
</goal>
</transf>
......@@ -775,39 +776,29 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.09" steps="97"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.09" steps="81"/></proof>
</goal>
<goal name="VC ascii.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC ascii.2" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC ascii.2.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.08" steps="87"/></proof>
</goal>
<goal name="VC ascii.2.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
<proof prover="6"><result status="valid" time="0.18" steps="403"/></proof>
</goal>
<goal name="VC ascii.3" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC ascii.3.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="88"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="89"/></proof>
</goal>
<goal name="VC ascii.3.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.16" steps="321"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.04" steps="157"/></proof>
</goal>
<goal name="VC ascii.3.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.24" steps="280"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="111"/></proof>
</goal>
<goal name="VC ascii.3.3" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.09"/></proof>
......@@ -815,18 +806,16 @@
</transf>
</goal>
<goal name="VC ascii.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC ascii.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="1.58"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC ascii.6" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.52"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="362"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="374"/></proof>
</goal>
</transf>
</goal>
......
......@@ -29,15 +29,15 @@ module Bitwalker
(* *)
let function maxvalue (len : BV32.t) : BV64.t =
BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)
BV64.lsl_bv (1:BV64.t) (C32_64.toBig len)
let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
requires { BV32.t'int len < 64}
ensures { BV64.eq_sub x BV64.zeros (BV32.t'int len) (64 - BV32.t'int len)
<-> BV64.t'int x < BV64.t'int (maxvalue len) }
=
assert { BV32.ult len (BV32.of_int 64) };
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len))
assert { BV32.ult len (64:BV32.t) };
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (64:BV64.t) (C32_64.toBig len))
<-> BV64.ult x (maxvalue len) }
(** return `value` with the bit of index `left` from the left set to `flag` *)
......@@ -47,13 +47,13 @@ module Bitwalker
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - BV32.t'int left) }
=
assert { BV32.ult left (BV32.of_int 64) };
assert { BV32.ult left (64:BV32.t) };
begin
ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) left ->
ensures { forall i:BV32.t. i <> BV32.sub (63:BV32.t) left ->
BV64.nth_bv result (C32_64.toBig i) =
BV64.nth_bv value (C32_64.toBig i) }
ensures { flag = BV64.nth_bv result
(C32_64.toBig (BV32.sub (BV32.of_int 63) left)) }
(C32_64.toBig (BV32.sub (63:BV32.t) left)) }
let mask =
BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.sub_check (63:BV32.t) left))
......@@ -75,13 +75,13 @@ module Bitwalker
ensures { flag = BV64.nth result (63 - left) }
=
let ghost left_bv = BV64.of_int left in
assert { BV64.ult left_bv (BV64.of_int 64) };
assert { (BV64.sub (BV64.of_int 63) left_bv) = BV64.of_int (63 - left) };
assert { BV64.ult left_bv (64:BV64.t) };
assert { (BV64.sub (63:BV64.t) left_bv) = BV64.of_int (63 - left) };
begin
ensures { forall i:BV64.t. BV64.ule i (BV64.of_int 63) ->
i <> BV64.sub (BV64.of_int 63) left_bv ->
ensures { forall i:BV64.t. BV64.ule i (63:BV64.t) ->
i <> BV64.sub (63:BV64.t) left_bv ->
BV64.nth_bv result i = BV64.nth_bv value i }
ensures { flag = BV64.nth_bv result (BV64.sub (BV64.of_int 63) left_bv) }
ensures { flag = BV64.nth_bv result (BV64.sub (63:BV64.t) left_bv) }
let mask =
BV64.lsl_bv (1:BV64.t) (BV64.of_int (63 - left))
in
......@@ -99,11 +99,11 @@ module Bitwalker
requires { 0 <= BV32.t'int left < 8 }
ensures { result = BV8.nth byte (7 - BV32.t'int left) }
=
assert {BV32.ult left (BV32.of_int 8)};
assert {BV32.ult left (8:BV32.t)};
begin
ensures {
result = BV8.nth_bv
byte (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))}
byte (BV8.sub (7:BV8.t) (C8_32.toSmall left))}
let mask =
BV32.lsl_bv (1:BV32.t) (BV32.sub_check (7:BV32.t) left)
in
......@@ -140,7 +140,7 @@ module Bitwalker
let retval = ref BV64.zeros in
let i = ref BV32.zeros in
let lstart = BV32.sub_check (BV32.of_int 64) len in
let lstart = BV32.sub_check (64:BV32.t) len in
while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
......@@ -167,10 +167,10 @@ module Bitwalker
requires {BV32.t'int left < 64}
ensures {result = BV64.nth value (63 - BV32.t'int left)}
=
assert {BV32.ult left (BV32.of_int 64)};
assert {BV32.ult left (64:BV32.t)};
begin
ensures {result = BV64.nth_bv value
(BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
(BV64.sub (63:BV64.t) (C32_64.toBig left))}
let mask = BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.sub_check (63:BV32.t) left)) in
not (BV64.eq (BV64.bw_and value mask) BV64.zeros)
......@@ -192,13 +192,13 @@ module Bitwalker
BV8.nth result i = BV8.nth byte i }
ensures { BV8.nth result (7 - BV32.t'int left) = flag }
=
assert { BV32.ult left (BV32.of_int 8) };
assert { BV32.ult left (8:BV32.t) };
begin
ensures { forall i:BV32.t. BV32.ult i (BV32.of_int 8) ->
i <> BV32.sub (BV32.of_int 7) left ->
ensures { forall i:BV32.t. BV32.ult i (8:BV32.t) ->
i <> BV32.sub (7:BV32.t) left ->
BV8.nth_bv result (C8_32.toSmall i)
= BV8.nth_bv byte (C8_32.toSmall i) }
ensures { BV8.nth_bv result (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))
ensures { BV8.nth_bv result (BV8.sub (7:BV8.t) (C8_32.toSmall left))
= flag }
let mask = BV8.lsl_bv (1:BV8.t) (BV8.sub_check (7:BV8.t) (C8_32.toSmall left)) in
match flag with
......@@ -251,7 +251,7 @@ module Bitwalker
-2 (*error: value_too_big*)
else
let lstart = BV32.sub_check (BV32.of_int 64) len in
let lstart = BV32.sub_check (64:BV32.t) len in
let i = ref BV32.zeros in
while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
......
......@@ -3,6 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" proved="true">
......@@ -16,13 +19,15 @@
<goal name="VC nth_ultpre0" expl="VC for nth_ultpre0" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC nth_ultpre0.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="166"/></proof>
<proof prover="11"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC nth_ultpre0.1" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.08"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC nth_ultpre0.2" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.58"/></proof>
<proof prover="2"><result status="valid" time="0.10" steps="512"/></proof>
<proof prover="11"><result status="valid" time="0.65"/></proof>
</goal>
</transf>
</goal>
......@@ -35,16 +40,16 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke_64bit_bv.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC poke_64bit_bv.3" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC poke_64bit_bv.4" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke_64bit_bv.5" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.12"/></proof>
<proof prover="11"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
......@@ -60,10 +65,10 @@
<proof prover="12"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC poke_64bit.3" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC poke_64bit.4" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC poke_64bit.5" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
......@@ -79,7 +84,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek_8bit_bv.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC peek_8bit_bv.3" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.05"/></proof>
......@@ -123,10 +128,10 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.5" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC peek.6" expl="loop invariant init" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="185"/></proof>
</goal>
<goal name="VC peek.7" expl="loop invariant init" proved="true">
<proof prover="11"><result status="valid" time="0.02"/></proof>
......@@ -138,13 +143,13 @@
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC peek.10" expl="precondition" proved="true">
<proof prover="11"><result status="valid" time="0.08"/></proof>
<proof prover="11"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC peek.11" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.12" expl="precondition" proved="true">
<proof prover="11"><result status="valid" time="0.06"/></proof>
<proof prover="11"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC peek.13" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
......@@ -153,13 +158,13 @@
<proof prover="12"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC peek.15" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.16"/></proof>
<proof prover="11"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC peek.16" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="1.36"/></proof>
<proof prover="11"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="VC peek.17" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="651"/></proof>
</goal>
<goal name="VC peek.18" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......@@ -168,7 +173,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.20" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.06"/></proof>
<proof prover="11"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
......@@ -181,7 +186,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek_64bit.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC peek_64bit.3" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.41"/></proof>
......@@ -194,13 +199,13 @@
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke_8bit.1" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke_8bit.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke_8bit.3" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC poke_8bit.4" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.07"/></proof>
......@@ -232,17 +237,17 @@
<goal name="VC poke_8bit_array.5.0" expl="postcondition" proved="true">
<transf name="case" proved="true" arg1="(div i 8 = o)">
<goal name="VC poke_8bit_array.5.0.0" expl="true case (postcondition)" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="258"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="267"/></proof>
</goal>
<goal name="VC poke_8bit_array.5.0.1" expl="false case (postcondition)" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="176"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="181"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC poke_8bit_array.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="169"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="174"/></proof>
</goal>
</transf>
</goal>
......@@ -273,7 +278,7 @@
<proof prover="12"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC poke.8" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.18"/></proof>
<proof prover="11"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC poke.9" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
......@@ -288,19 +293,19 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.13" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.14" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC poke.15" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC poke.16" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="12"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC poke.17" expl="precondition" proved="true">
<proof prover="11"><result status="valid" time="0.04"/></proof>
<proof prover="11"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke.18" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.03"/></proof>
......@@ -309,48 +314,48 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.20" expl="precondition" proved="true">
<proof prover="11"><result status="valid" time="0.08"/></proof>
<proof prover="11"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC poke.21" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC poke.21.0" expl="assertion" proved="true">
<proof prover="11"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="202"/></proof>
</goal>
</transf>
</goal>
<goal name="VC poke.22" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC poke.22.0" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC poke.22.1" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC poke.22.2" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC poke.22.3" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.21"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC poke.23" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.03"/></proof>
<proof prover="12"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC poke.24" expl="loop variant decrease" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC poke.25" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.17"/></proof>
<proof prover="11"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC poke.26" expl="loop invariant preservation" proved="true">
<proof prover="12"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC poke.27" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.14"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="736"/></proof>
</goal>
<goal name="VC poke.28" expl="loop invariant preservation" proved="true">
<proof prover="12"><result status="valid" time="0.14"/></proof>
<proof prover="11"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC poke.29" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
......@@ -359,13 +364,13 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.31" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.69"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="194"/></proof>
</goal>
<goal name="VC poke.32" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.33" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.39"/></proof>
<proof prover="11"><result status="valid" time="0.76"/></proof>
</goal>
</transf>
</goal>
......@@ -406,7 +411,7 @@
<goal name="VC pokethenpeek" expl="VC for pokethenpeek" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC pokethenpeek.0" expl="assertion" proved="true">
<proof prover="11"><result status="valid" time="0.17"/></proof>
<proof prover="11"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC pokethenpeek.1" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
......@@ -430,10 +435,10 @@
<proof prover="12"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC pokethenpeek.8" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.32"/></proof>
<proof prover="3"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC pokethenpeek.9" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="149"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="153"/></proof>
</goal>
</transf>
</goal>
......
......@@ -176,74 +176,74 @@
<goal name="VC maximum_subarray" expl="VC for maximum_subarray" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC maximum_subarray.0" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.00" steps="49"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="41"/></proof>
</goal>
<goal name="VC maximum_subarray.1" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC maximum_subarray.2" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC maximum_subarray.3" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC maximum_subarray.4" expl="index in array bounds" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC maximum_subarray.5" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="VC maximum_subarray.6" expl="loop variant decrease" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC maximum_subarray.7" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="139"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="135"/></proof>
</goal>
<goal name="VC maximum_subarray.8" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="60"><result status="valid" time="9.68" steps="5320"/></proof>
<proof prover="5" timelimit="60"><result status="valid" time="11.72" steps="6103"/></proof>
</goal>
<goal name="VC maximum_subarray.9" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.00" steps="31"/></proof>
<proof prover="5"><result status="valid" time="0.00" steps="30"/></proof>
</goal>
<goal name="VC maximum_subarray.10" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="37"/></proof>
</goal>
<goal name="VC maximum_subarray.11" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="22"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="21"/></proof>
</goal>
<goal name="VC maximum_subarray.12" expl="loop variant decrease" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC maximum_subarray.13" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC maximum_subarray.14" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="120"><result status="valid" time="51.58" steps="35058"/></proof>
<proof prover="5" timelimit="120"><result status="valid" time="34.65" steps="23080"/></proof>
</goal>
<goal name="VC maximum_subarray.15" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="136"/></proof>