Commit 272de8d1 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

removed axiom; added a missing precondition; model is now sound again

parent fd2acc75
......@@ -486,10 +486,9 @@ let sbiw (dst: register) (k: int): unit
use bv.BV8
val bv8_to_int (x: BV8.t): int
let bv8_to_int (x: BV8.t): int
ensures { result = BV8.t'int x }
axiom bv8_nth_def: forall x y. (256 > x >= 0 /\ 8 > y >= 0) -> (BV8.nth (BV8.of_int x) y <-> mod (div x (pow2 y)) 2 = 1)
= any int ensures { result = BV8.t'int x }
(*
let add_ (dst src: register): unit
......@@ -563,7 +562,8 @@ let asr (dst: register): unit
ensures { ?cf = mod (old reg[dst]) 2 }
ensures { !cf = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf := BV8.nth (BV8.of_int (read reg dst)) 0;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.asr (BV8.of_int (read reg dst)) 1))
reg.data <- data_set reg.data dst (bv8_to_int (BV8.asr (BV8.of_int (read reg dst)) 1));
assert { forall b. BV8.nth b 0 <-> mod (BV8.t'int b) 2 = 1 }
let lsr (dst: register): unit
writes { reg, cf }
......@@ -573,7 +573,8 @@ let lsr (dst: register): unit
ensures { ?cf = mod (old reg[dst]) 2 }
ensures { !cf = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf := BV8.nth (BV8.of_int (read reg dst)) 0;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (read reg dst)) 1))
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (read reg dst)) 1));
assert { forall b. BV8.nth b 0 <-> mod (BV8.t'int b) 2 = 1 }
(* WIP: this will become the future definition, since 'lsl rX' is the same opcode as 'add rX, rX' *)
(*
......@@ -605,6 +606,7 @@ let bst (dst: register) (bit: int): unit
ensures { !tf = BV8.nth (BV8.of_int reg[dst]) bit }
= tf := BV8.nth (BV8.of_int (read reg dst)) bit
(* WIP note: we don't need multiple definitions of 'bitset'; the best one is probably this one *)
function bitset (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if v then
......@@ -624,6 +626,7 @@ function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
else
BV8.bw_xor w mask
(* WIP TODO: this can be moved to the 'by' part of bitset_correct2, if it doesn't impact any other proofs *)
lemma one_def:
BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b
......@@ -635,11 +638,9 @@ goal bitset_correct2:
forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
BV8.nth (bitset w b v) i = BV8.nth w i
(* WIP: this goal can be removed if the alternative definitions are not needed *)
goal bitset_equiv_def:
forall w, b, v. 0 <= b < 8 -> (bitset w b v) = (bitset' w b v)
goal bitsetx_equiv_def:
forall w, b, v. 0 <= b < 8 -> (bitset w b v) = (bitsetx w b v)
forall w, b, v. 0 <= b < 8 -> bitset w b v = bitsetx w b v = bitset' w b v
let bld (dst: register) (bit: int): unit
writes { reg }
......@@ -688,6 +689,7 @@ let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
end
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { valid_addr_space reg }
requires { w >= 0 }
ensures { 0 <= uint_sum (reg,lo) 0 w < pow2 (8*w) }
variant { w }
......
......@@ -2,19 +2,17 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.1" alternative="noBV" timelimit="60" steplimit="0" memlimit="12000"/>
<prover id="0" name="CVC4" version="1.4" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.6" alternative="noBV" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.4.1" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file>
<file proved="true">
<path name=".."/>
<path name="avrmodel.mlw"/>
<theory name="AVRint">
<theory name="AVRint" proved="true">
<goal name="VC prefix ?" expl="VC for prefix ?" proved="true">
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -78,10 +76,10 @@
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC ld_inc.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC ld_inc.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC ld_inc.3" expl="precondition" proved="true">
<proof prover="8"><result status="valid" time="0.04"/></proof>
......@@ -502,33 +500,55 @@
</goal>
</transf>
</goal>
<goal name="VC bv8_to_int" expl="VC for bv8_to_int" proved="true">
<proof prover="7"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC inc_" expl="VC for inc_" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC inc_.0" expl="precondition" proved="true">
<proof prover="8"><result status="valid" time="0.09"/></proof>
<proof prover="8"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC inc_.1" expl="postcondition" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.06" steps="135"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.21" steps="135"/></proof>
</goal>
<goal name="VC inc_.2" expl="postcondition" proved="true">
<proof prover="8"><result status="valid" time="0.65"/></proof>
<proof prover="8"><result status="valid" time="1.46"/></proof>
</goal>
</transf>
</goal>
<goal name="VC dec_" expl="VC for dec_" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.12" steps="164"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="164"/></proof>
</goal>
<goal name="VC eor" expl="VC for eor" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.12" steps="189"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.27" steps="189"/></proof>
</goal>
<goal name="VC clr" expl="VC for clr" proved="true">
<proof prover="8"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC com" expl="VC for com" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.09" steps="169"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.23" steps="169"/></proof>
</goal>
<goal name="VC asr" expl="VC for asr" proved="true">
<proof prover="4"><result status="valid" time="1.18"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC asr.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="77"/></proof>
</goal>
<goal name="VC asr.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="2.53"/></proof>
</goal>
<goal name="VC asr.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="145"/></proof>
</goal>
<goal name="VC asr.3" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.10" steps="73"/></proof>
</goal>
<goal name="VC asr.4" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC asr.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="74"/></proof>
</goal>
</transf>
</goal>
<goal name="VC lsr" expl="VC for lsr" proved="true">
<transf name="compute_specified" proved="true" >
......@@ -541,17 +561,20 @@
<goal name="VC lsr.0.0.0.0" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC lsr.0.0.0.1" expl="postcondition" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.16"/></proof>
<goal name="VC lsr.0.0.0.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="2.72"/></proof>
</goal>
<goal name="VC lsr.0.0.0.2" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof>
<proof prover="0" timelimit="1"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="VC lsr.0.0.0.3" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.13"/></proof>
<proof prover="7"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC lsr.0.0.0.4" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.05"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC lsr.0.0.0.5" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.20"/></proof>
</goal>
</transf>
</goal>
......@@ -568,7 +591,7 @@
<goal name="VC lsl.0.0" expl="VC for lsl" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="VC lsl.0.0.0" expl="VC for lsl" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.39"/></proof>
<proof prover="0" timelimit="1"><result status="valid" time="1.09"/></proof>
</goal>
</transf>
</goal>
......@@ -584,71 +607,30 @@
</transf>
</goal>
<goal name="one_def" proved="true">
<proof prover="8"><result status="valid" time="0.19"/></proof>
<proof prover="8"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="bitset_correct1" proved="true">
<proof prover="8"><result status="valid" time="0.19"/></proof>
<proof prover="8"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="bitset_correct2" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.24" steps="476"/></proof>
</goal>
<goal name="bitset_equiv_def">
<proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="8"><result status="unknown" time="0.16"/></proof>
<transf name="inline_all" >
<goal name="bitset_equiv_def.0">
<proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="8"><result status="unknown" time="0.17"/></proof>
<transf name="split_all_full" >
<goal name="bitset_equiv_def.0.0">
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="6" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="8" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<transf name="introduce_premises" >
<goal name="bitset_equiv_def.0.0.0">
<proof prover="2" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="8" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
</goal>
</transf>
</goal>
<goal name="bitset_equiv_def.0.1">
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="6" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="8" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<transf name="introduce_premises" >
<goal name="bitset_equiv_def.0.1.0">
<proof prover="2" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="8" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
</goal>
</transf>
</goal>
</transf>
<transf name="split_vc" >
<goal name="bitset_equiv_def.0.0">
<transf name="compute_specified" >
<goal name="bitset_equiv_def.0.0.0">
<proof prover="0" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="3" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="4" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="5" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="unknown" time="0.27"/></proof>
</goal>
</transf>
</goal>
</transf>
<transf name="split_vc" proved="true" >
<goal name="bitset_correct2.0" proved="true">
<proof prover="2"><result status="valid" time="0.63" steps="480"/></proof>
</goal>
</transf>
</goal>
<goal name="bitsetx_equiv_def" proved="true">
<proof prover="8"><result status="valid" time="0.19"/></proof>
<goal name="bitset_equiv_def" proved="true">
<transf name="split_vc" proved="true" >
<goal name="bitset_equiv_def.0" proved="true">
<proof prover="8" timelimit="13"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="bitset_equiv_def.1" proved="true">
<proof prover="8" timelimit="13"><result status="valid" time="0.43"/></proof>
</goal>
</transf>
</goal>
<goal name="VC bld" expl="VC for bld" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.22" steps="352"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.54" steps="437"/></proof>
</goal>
<goal name="VC uint_recursion" expl="VC for uint_recursion" proved="true">
<transf name="compute_specified" proved="true" >
......@@ -657,118 +639,46 @@
<goal name="VC uint_recursion.0.0" expl="assertion" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="VC uint_recursion.0.0.0" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.94"/></proof>
<proof prover="5"><result status="valid" time="4.43"/></proof>
</goal>
</transf>
</goal>
<goal name="VC uint_recursion.0.1" expl="variant decrease" proved="true">
<proof prover="7"><result status="valid" time="0.07"/></proof>
<proof prover="7"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC uint_recursion.0.2" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.09"/></proof>
<proof prover="7"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC uint_recursion.0.3" expl="postcondition" proved="true">
<proof prover="7" timelimit="5" memlimit="2000"><result status="valid" time="1.37"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="valid" time="2.40"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC uint_bound" expl="VC for uint_bound">
<proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<transf name="inline_all" >
<goal name="VC uint_bound.0" expl="VC for uint_bound">
<transf name="split_vc" >
<goal name="VC uint_bound.0.0" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC uint_bound.0.1" expl="assertion" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="VC uint_bound.0.1.0" expl="assertion" proved="true">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="77"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="1.53"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
<goal name="VC uint_bound.0.2" expl="variant decrease" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="VC uint_bound.0.2.0" expl="variant decrease" proved="true">
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="VC uint_bound.0.3" expl="precondition" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="VC uint_bound.0.3.0" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
<goal name="VC uint_bound.0.4" expl="assertion" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="VC uint_bound.0.4.0" expl="assertion" proved="true">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="81"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
<goal name="VC uint_bound.0.5" expl="postcondition">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
<proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
<transf name="split_vc" >
<goal name="VC uint_bound.0.5.0" expl="postcondition">
<proof prover="0" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="60.00"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="3" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="4" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="6" timelimit="60" memlimit="12000"><result status="timeout" time="60.00"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal" >
<goal name="VC uint_bound.0.5.0.0" expl="postcondition">
<proof prover="0" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="3" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="4" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="5" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
<goal name="VC uint_bound.0.5.1" expl="postcondition">
<proof prover="0" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="3" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="4" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal" >
<goal name="VC uint_bound.0.5.1.0" expl="postcondition">
<proof prover="0" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
<proof prover="3" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="4" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="5" timelimit="30" memlimit="4000"><result status="timeout" time="30.00"/></proof>
<proof prover="7" timelimit="5" memlimit="2000"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
<goal name="VC uint_bound" expl="VC for uint_bound" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC uint_bound.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.09" steps="74"/></proof>
</goal>
<goal name="VC uint_bound.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="2.98"/></proof>
<proof prover="5"><result status="valid" time="8.46"/></proof>
</goal>
<goal name="VC uint_bound.2" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.09" steps="76"/></proof>
</goal>
<goal name="VC uint_bound.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC uint_bound.4" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="76"/></proof>
</goal>
<goal name="VC uint_bound.5" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="83"/></proof>
</goal>
<goal name="VC uint_bound.6" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="2.46"/></proof>
</goal>
</transf>
</goal>
......@@ -871,7 +781,7 @@
<proof prover="2"><result status="valid" time="0.14" steps="74"/></proof>
</goal>
<goal name="VC init" expl="VC for init" proved="true">
<proof prover="5"><result status="valid" time="0.29"/></proof>
<proof prover="5"><result status="valid" time="0.54"/></proof>
</goal>
</theory>
</file>
......
No preview for this file type
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment