From af9218d5910c170a62a56356d2e682c7ea344e8d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 21 Oct 2021 10:25:52 +0200
Subject: [PATCH] New union
---
dolmen | 2 +-
.../solve/all/unsat/ordered_is_ordered.psmt2 | 2 +-
src_colibri2/theories/quantifier/pattern.ml | 2 +-
.../theories/quantifier/quantifier.ml | 5 +-
src_colibri2/theories/quantifier/trigger.ml | 5 +-
src_common/union.mlw | 469 +++-
src_common/union/why3session.xml | 2195 +++++++++--------
src_common/union__Union.ml | 312 ++-
8 files changed, 1718 insertions(+), 1274 deletions(-)
diff --git a/dolmen b/dolmen
index 660c77c85..38294b2dc 160000
--- a/dolmen
+++ b/dolmen
@@ -1 +1 @@
-Subproject commit 660c77c855d8b7441f6aec56c84c54e46229bc15
+Subproject commit 38294b2dcb07477506b9a06e4a51d1fdb2c8c3e6
diff --git a/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2 b/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
index 16c96a949..b68bf6fca 100644
--- a/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
+++ b/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
@@ -1,7 +1,7 @@
;; produced by local colibri2.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
-(set-option :max-steps-colibri2 10000)
+(set-option :max-steps-colibri2 11000)
(declare-datatypes ((tuple2 2))
((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2))))))
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 3f9dd5ba2..a125a49ea 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -250,7 +250,7 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
in
let nodes =
IArray.foldi_non_empty_exn
- ~f:(fun i acc parg -> Node.S.inter acc (get_parents (i + 1) parg))
+ ~f:(fun i acc parg -> Node.S.inter acc (get_parents i parg))
~init:(get_parents 0) pargs
in
if Node.S.is_empty nodes then raise Not_found else nodes
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index ce157326d..937c2285f 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -298,8 +298,9 @@ let th_register d =
(* let delay = Events.Delayed_by 10 in *)
Daemon.attach_reg_sem d Ground.ClosedQuantifier.key quantifier_registered;
Ground.register_converter d (fun d g ->
- if not (application_useless d g) then add_info_on_ground_terms d g
- else Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g);
+ if application_useless d g then
+ Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g
+ else add_info_on_ground_terms d g);
Interp.Register.check_closed_quantifier d (fun d g ->
let n = Ground.ClosedQuantifier.node g in
let unknown =
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index 3824b3338..bb49bbe7e 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -356,12 +356,13 @@ let instantiate d tri subst =
Expr.Term.Var.M.map (Egraph.find_def d) subst.Ground.Subst.term;
}
in
- Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a"
+ Debug.dprintf9 debug
+ "[Quant] %a instantiation found %a, pat %a, checks:%a, eager:%b"
Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form
Fmt.(list ~sep:comma Pattern.pp)
tri.pats
Fmt.(list ~sep:comma Pattern.pp)
- tri.checks;
+ tri.checks tri.eager;
if
tri.eager
&& List.for_all
diff --git a/src_common/union.mlw b/src_common/union.mlw
index e719aa981..4ce3e88ae 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -6,113 +6,177 @@ module Union
use interval.Bound
use real.RealInfix
- type t0 =
- | Singleton Q.t t0
- | Inter Q.t Bound.t Q.t Bound.t t0
- | FiniteInf Q.t Bound.t
- | End
+ type on =
+ | OnSin Q.t on
+ | OnEnd Q.t Bound.t off
+ | OnInf
+
+ with off =
+ | OffSin Q.t off
+ | OffEnd Q.t Bound.t on
+ | OffInf
type t =
- | InfFinite Q.t Bound.t t0
- | Finite t0
- | Inf
+ | On on
+ | Off off
+
+ function length_on (l:on) : int =
+ match l with
+ | OnSin _ l ->
+ length_on l + 1
+ | OnEnd _ _ l ->
+ length_off l + 1
+ | OnInf -> 0
+ end
+
+ with length_off (l:off) : int =
+ match l with
+ | OffSin _ l ->
+ length_off l + 1
+ | OffEnd _ _ l ->
+ length_on l + 1
+ | OffInf -> 0
+ end
- function length0 (l:t0) : int =
+ let rec lemma pos_length_on (l:on)
+ ensures { length_on l >= 0 } =
match l with
- | Singleton _ l ->
- length0 l + 1
- | Inter _ _ _ _ l ->
- length0 l + 2
- | FiniteInf _ _ ->
- 1
- | End -> 0
+ | OnSin _ l -> pos_length_on l
+ | OnEnd _ _ l ->
+ pos_length_off l
+ | OnInf -> ()
end
- let rec lemma length0_positive (l:t0)
- ensures { length0 l >= 0 } =
+ with lemma pos_length_off (l:off)
+ ensures { length_off l >= 0 } =
match l with
- | Singleton _ l -> length0_positive l
- | Inter _ _ _ _ l ->
- length0_positive l
- | FiniteInf _ _ -> ()
- | End -> ()
+ | OffSin _ l -> pos_length_off l
+ | OffEnd _ _ l ->
+ pos_length_on l
+ | OffInf -> ()
end
function length (l:t) : int =
match l with
- | InfFinite _ _ l ->
- length0 l + 1
- | Finite l ->
- length0 l
- | Inf ->
- 0
+ | On l ->
+ length_on l + 1
+ | Off l ->
+ length_off l
end
- predicate lt_bound0 (x:Q.t) (l:t0) =
+ predicate lt_bound_on (x:Q.t) (l:on) =
match l with
- | Singleton q l ->
- x <. q /\ lt_bound0 x l
- | Inter q _ q' _ l ->
- x <. q /\ x <. q' /\ lt_bound0 x l
- | FiniteInf q _ ->
- x <. q
- | End -> true
+ | OnSin q l ->
+ x <. q /\ lt_bound_on x l
+ | OnEnd q _ l ->
+ x <. q /\ lt_bound_off x l
+ | OnInf -> true
end
- let rec ghost lt_bound0_transitive (x:Q.t) (y:Q.t) (l:t0) (m:t0)
- requires { forall q. lt_bound0 q l -> q <. x }
+ with lt_bound_off (x:Q.t) (l:off) =
+ match l with
+ | OffSin q l ->
+ x <. q /\ lt_bound_off x l
+ | OffEnd q _ l ->
+ x <. q /\ lt_bound_on x l
+ | OffInf -> true
+ end
+
+ let rec ghost lt_bound_on_on_transitive (x:Q.t) (y:Q.t) (l:on) (m:on)
+ requires { forall q. lt_bound_on q l -> q <. x }
+ requires { x <=. y }
+ requires { lt_bound_on y m }
+ ensures { forall q. lt_bound_on q l -> lt_bound_on q m }
+ variant { m } =
+ match m with
+ | OnSin _ m ->
+ lt_bound_on_on_transitive x y l m
+ | OnEnd _ _ m ->
+ lt_bound_on_off_transitive x y l m
+ | OnInf -> ()
+ end
+
+ with ghost lt_bound_on_off_transitive (x:Q.t) (y:Q.t) (l:on) (m:off)
+ requires { forall q. lt_bound_on q l -> q <. x }
+ requires { x <=. y }
+ requires { lt_bound_off y m }
+ ensures { forall q. lt_bound_on q l -> lt_bound_off q m }
+ variant { m } =
+ match m with
+ | OffSin _ m ->
+ lt_bound_on_off_transitive x y l m
+ | OffEnd _ _ m ->
+ lt_bound_on_on_transitive x y l m
+ | OffInf -> ()
+ end
+
+ let rec ghost smaller_lt_bound_on (x:Q.t) (y:Q.t) (m:on)
+ requires { x <=. y }
+ requires { lt_bound_on y m }
+ ensures { lt_bound_on x m }
+ variant { m } =
+ match m with
+ | OnSin _ m ->
+ smaller_lt_bound_on x y m
+ | OnEnd _ _ m ->
+ smaller_lt_bound_off x y m
+ | OnInf -> ()
+ end
+
+ with ghost smaller_lt_bound_off (x:Q.t) (y:Q.t) (m:off)
requires { x <=. y }
- requires { lt_bound0 y m }
- ensures { forall q. lt_bound0 q l -> lt_bound0 q m }
+ requires { lt_bound_off y m }
+ ensures { lt_bound_off x m }
variant { m } =
match m with
- | Singleton _ m ->
- lt_bound0_transitive x y l m
- | Inter _ _ _ _ m ->
- lt_bound0_transitive x y l m
- | FiniteInf _ _ -> ()
- | End -> ()
+ | OffSin _ m ->
+ smaller_lt_bound_off x y m
+ | OffEnd _ _ m ->
+ smaller_lt_bound_on x y m
+ | OffInf -> ()
end
+
predicate lt_bound (x:Q.t) (l:t) =
match l with
- | InfFinite q _ l ->
- x <. q \/ lt_bound0 x l
- | Finite l ->
- lt_bound0 x l
- | Inf ->
- true
+ | On l -> lt_bound_on x l
+ | Off l -> lt_bound_off x l
+ end
+
+ predicate ordered_on (l:on) =
+ match l with
+ | OnSin q l ->
+ lt_bound_on q l /\
+ ordered_on l
+ | OnEnd q _ l ->
+ lt_bound_off q l /\
+ ordered_off l
+ | OnInf -> true
end
- predicate ordered0 (l:t0) =
+ with ordered_off (l:off) =
match l with
- | Singleton q l ->
- lt_bound0 q l /\
- ordered0 l
- | Inter q _ q' _ l ->
- Q.(q < q') /\
- lt_bound0 q' l /\
- ordered0 l
- | FiniteInf _ _ -> true
- | End -> true
+ | OffSin q l ->
+ lt_bound_off q l /\
+ ordered_off l
+ | OffEnd q _ l ->
+ lt_bound_on q l /\
+ ordered_on l
+ | OffInf -> true
end
predicate ordered (l:t) =
match l with
- | InfFinite q _ l ->
- lt_bound0 q l /\
- ordered0 l
- | Finite l ->
- ordered0 l
- | Inf -> true
+ | On l -> ordered_on l
+ | Off l -> ordered_off l
end
type t' = { a: t }
invariant { ordered a }
invariant {
- a <> Finite End
+ a <> Off OffInf
}
- by { a = Inf }
+ by { a = On OnInf }
predicate cmp (x:real) (b:Bound.t) (y:real) =
match b with
@@ -120,66 +184,79 @@ module Union
| Bound.Strict -> x <. y
end
- predicate mem0 (x:real) (l:t0) =
+ predicate mem_on (x:real) (l:on) =
match l with
- | Singleton q l ->
- x = q \/ mem0 x l
- | Inter q b q' b' l ->
- (cmp q b x /\ cmp x b' q') \/ mem0 x l
- | FiniteInf q b ->
- cmp q b x
- | End -> false
+ | OnSin q l ->
+ x <. q \/ (q <. x /\ mem_on x l)
+ | OnEnd q b l ->
+ cmp x b q \/ mem_off x l
+ | OnInf -> true
end
- let rec lemma lt_bound0_is_not_mem0 (q:Q.t) (r:real) (l:t0)
- requires { lt_bound0 q l }
- requires { r <=. q }
- ensures { not (mem0 r l) }
- =
+ with mem_off (x:real) (l:off) =
match l with
- | Singleton _ l -> lt_bound0_is_not_mem0 q r l
- | Inter _ _ _ _ l ->
- lt_bound0_is_not_mem0 q r l
- | FiniteInf _ _ -> ()
- | End -> ()
+ | OffSin q l ->
+ x = q \/ mem_off x l
+ | OffEnd q b l ->
+ not (cmp x b q) /\ mem_on x l
+ | OffInf -> false
end
predicate mem (x:real) (l:t) =
match l with
- | InfFinite q b l ->
- cmp x b q \/ mem0 x l
- | Finite l ->
- mem0 x l
- | Inf ->
- true
+ | On l ->
+ mem_on x l
+ | Off l ->
+ mem_off x l
+ end
+
+ let rec ghost lt_bound_is_not_mem_off (q:Q.t) (l:off)
+ requires { lt_bound_off q l }
+ ensures { forall r. r <=. q -> not (mem_off r l) }
+ variant { l }
+ =
+ match l with
+ | OffSin _ l -> lt_bound_is_not_mem_off q l
+ | OffEnd _ _ _ -> ()
+ | OffInf -> ()
end
let singleton (q:Q.t) : t'
ensures { forall x:real. mem x result.a <-> x = q }
=
- { a = Finite (Singleton q End) }
-
- let is_singleton (u:t') : (option Q.t, ghost real, ghost real)
+ { a = Off (OffSin q OffInf) }
+
+ let is_singleton (u:t') : (option Q.t, ghost real, ghost real)
ensures {
- let (o,x1,x2) = result in
+ let (o,x1,x2) = result in
match o with
| Some q -> forall x:real. mem x u.a <-> x = q
| None -> x1 <> x2 /\ mem x1 u.a /\ mem x2 u.a
end
} =
match u.a with
- | Inf -> (None, ghost 0., ghost 1.)
- | InfFinite q _ _ -> (None, ghost (Q.real q)-.1., ghost (Q.real q)-.2.)
- | Finite (Singleton q End) -> (Some q,ghost 0., ghost 1.)
- | Finite End -> absurd
- | Finite (Inter q _ q' _ _) ->
- (None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
- | Finite (FiniteInf q _) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
- | Finite (Singleton q (Singleton q' _)) ->
- (None,ghost (Q.real q), ghost (Q.real q'))
- | Finite (Singleton _ (Inter q _ q' _ _)) ->
- (None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
- | Finite (Singleton _ (FiniteInf q _)) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
+ | Off (OffSin q OffInf) -> (Some q,ghost 0.,ghost 1.)
+ | Off (OffSin q (OffSin q' _)) -> (None,ghost Q.real q,ghost Q.real q')
+ | Off (OffSin _ (OffEnd q _ on)) ->
+ match on with
+ | OnSin q' _ -> (None,ghost (Q.real q*.0.3+.Q.real q'*.0.7),
+ ghost (Q.real q*.0.7+.Q.real q'*.0.3))
+ | OnEnd q' _ _ -> (None,ghost(Q.real q*.0.3+.Q.real q'*.0.7),
+ ghost(Q.real q*.0.7+.Q.real q'*.0.3))
+ | OnInf -> (None,ghost(Q.real q+.1.),ghost(Q.real q+.2.))
+ end
+ | Off (OffEnd q _ on) ->
+ match on with
+ | OnSin q' _ -> (None,ghost (Q.real q*.0.3+.Q.real q'*.0.7),
+ ghost (Q.real q*.0.7+.Q.real q'*.0.3))
+ | OnEnd q' _ _ -> (None,ghost(Q.real q*.0.3+.Q.real q'*.0.7),
+ ghost(Q.real q*.0.7+.Q.real q'*.0.3))
+ | OnInf -> (None,ghost(Q.real q+.1.),ghost(Q.real q+.2.))
+ end
+ | On (OnSin q _) -> (None, ghost (Q.real q-.1.), ghost (Q.real q-.2.))
+ | On (OnEnd q _ _) -> (None, ghost (Q.real q-.1.), ghost (Q.real q-.2.))
+ | On OnInf -> (None, ghost 0., ghost 1.)
+ | Off OffInf -> absurd
end
use q.Ord as Ord
@@ -236,6 +313,174 @@ module Union
| Ord.Gt, _, _ -> (v1,b1)
end
+
+ let inter (u:t') (v:t') : option t'
+ ensures {
+ forall x:real. (mem x u.a /\ mem x v.a) <->
+ match result with
+ | None -> false
+ | Some w -> mem x w.a
+ end
+ } =
+
+ let rec inter_on_on (u:on) (v:on) : on
+ requires { ordered_on u }
+ requires { ordered_on v }
+ ensures { ordered_on result }
+ ensures {
+ forall x:real. (mem_on x u /\ mem_on x v) <-> mem_on x result
+ }
+ ensures {
+ forall q.
+ (lt_bound_on q u) -> (lt_bound_on q v) ->
+ (lt_bound_on q result )
+ }
+ variant { length_on u + length_on v } =
+ match u, v with
+ | u, OnInf | OnInf, u -> u
+ | OnSin qu lu, OnSin qv lv ->
+ match Q.compare qu qv with
+ | Ord.Eq -> OnSin qu (inter_on_on lu lv)
+ | Ord.Lt -> smaller_lt_bound_on qu qv lv; OnSin qu (inter_on_on lu v)
+ | Ord.Gt -> smaller_lt_bound_on qv qu lu; OnSin qv (inter_on_on u lv)
+ end
+ | OnEnd qu bu lu, OnEnd qv bv lv ->
+ match Q.compare qu qv with
+ | Ord.Eq ->
+ let b = match bu, bv with
+ | Large, Large -> Large
+ | _ -> Strict
+ end
+ in
+ lt_bound_is_not_mem_off qu lv;
+ lt_bound_is_not_mem_off qu lu;
+ OnEnd qu b (inter_off_off lu lv)
+ | Ord.Lt -> smaller_lt_bound_off qu qv lv; OnEnd qu bu (inter_on_off v lu)
+ | Ord.Gt -> smaller_lt_bound_off qv qu lu; OnEnd qv bv (inter_on_off u lv)
+ end
+ | (OnSin qu lu) as u, (OnEnd qv bv lv) as v
+ | (OnEnd qv bv lv) as v, (OnSin qu lu) as u ->
+ match Q.compare qu qv with
+ | Ord.Eq -> smaller_lt_bound_on qv qu lu; OnEnd qv Strict (inter_on_off lu lv)
+ | Ord.Lt -> smaller_lt_bound_off qu qv lv; OnSin qu (inter_on_on lu v)
+ | Ord.Gt -> smaller_lt_bound_on qv qu lu; OnEnd qv bv (inter_on_off u lv)
+ end
+ end
+ with inter_on_off (u:on) (v:off) : off
+ requires { ordered_on u }
+ requires { ordered_off v }
+ ensures { ordered_off result }
+ ensures {
+ forall x:real. (mem_on x u /\ mem_off x v) <-> mem_off x result
+ }
+ ensures {
+ forall q.
+ (lt_bound_on q u) -> (lt_bound_off q v) ->
+ (lt_bound_off q result )
+ }
+ variant { length_on u + length_off v } =
+ match u, v with
+ | _, OffInf -> OffInf
+ | OnInf, u -> u
+ | OnSin qu lu, OffSin qv lv ->
+ match Q.compare qu qv with
+ | Ord.Eq -> inter_on_off lu lv
+ | Ord.Lt -> (inter_on_off lu v)
+ | Ord.Gt -> OffSin qv (inter_on_off u lv)
+ end
+ | OnEnd qu bu lu, OffEnd qv bv lv ->
+ match Q.compare qu qv with
+ | Ord.Eq ->
+ match bu, bv with
+ | Large, Large -> OffSin qu (inter_on_off lv lu)
+ | _ -> inter_on_off lv lu
+ end
+ | Ord.Lt -> inter_off_off lu v
+ | Ord.Gt -> smaller_lt_bound_off qv qu lu; OffEnd qv bv (inter_on_on u lv)
+ end
+ | (OnSin qu lu) as u, (OffEnd qv bv lv) as v ->
+ match Q.compare qu qv with
+ | Ord.Eq -> OffEnd qv Strict (inter_on_on lu lv)
+ | Ord.Lt -> inter_on_off lu v
+ | Ord.Gt -> smaller_lt_bound_on qv qu lu; OffEnd qv bv (inter_on_on u lv)
+ end
+ | (OnEnd qv bv lv) as v, (OffSin qu lu) as u ->
+ match Q.compare qu qv with
+ | Ord.Eq ->
+ match bv with
+ | Large -> OffSin qv (inter_off_off lu lv)
+ | Strict -> inter_off_off lu lv
+ end
+ | Ord.Lt -> smaller_lt_bound_off qu qv lv; OffSin qu (inter_on_off v lu)
+ | Ord.Gt -> inter_off_off u lv
+ end
+ end
+ with inter_off_off (u:off) (v:off) : off
+ requires { ordered_off u}
+ requires { ordered_off v }
+ ensures { ordered_off result }
+ ensures {
+ forall x:real. (mem_off x u /\ mem_off x v) <-> mem_off x result
+ }
+ ensures {
+ forall q.
+ (lt_bound_off q u) -> (lt_bound_off q v) ->
+ (lt_bound_off q result )
+ }
+ variant { length_off u + length_off v } =
+ match u, v with
+ | _, OffInf | OffInf, _ -> OffInf
+ | OffSin qu lu, OffSin qv lv ->
+ match Q.compare qu qv with
+ | Ord.Eq -> OffSin qu (inter_off_off lu lv)
+ | Ord.Lt -> inter_off_off lu v
+ | Ord.Gt -> inter_off_off u lv
+ end
+ | OffEnd qu bu lu, OffEnd qv bv lv ->
+ match Q.compare qu qv with
+ | Ord.Eq ->
+ let b = match bu, bv with
+ | Large, Large -> Large
+ | _ -> Strict
+ end
+ in
+ OffEnd qu b (inter_on_on lu lv)
+ | Ord.Lt -> inter_on_off lu v
+ | Ord.Gt -> inter_on_off lv u
+ end
+ | (OffSin qu lu) as u, (OffEnd qv bv lv) as v
+ | (OffEnd qv bv lv) as v, (OffSin qu lu) as u ->
+ match Q.compare qu qv with
+ | Ord.Eq -> match bv with
+ | Large -> OffSin qv (inter_on_off lv lu)
+ | Strict -> inter_on_off lv lu
+ end
+ | Ord.Lt -> inter_off_off lu v
+ | Ord.Gt -> inter_on_off lv u
+ end
+ end
+ in
+ let mk_off_option (l:off) : option t'
+ requires { ordered_off l }
+ ensures {
+ forall x:real. mem_off x l <->
+ match result with
+ | None -> false
+ | Some w -> mem x w.a
+ end
+ }
+ =
+ match l with
+ | OffInf -> None
+ | l -> Some { a = Off l }
+ end
+ in
+ match u.a,v.a with
+ | On u, On v -> Some { a = On (inter_on_on u v) }
+ | On u, Off v | Off v, On u -> mk_off_option (inter_on_off u v)
+ | Off u, Off v -> mk_off_option (inter_off_off u v)
+ end
+(*
let inter (u:t') (v:t') : option t'
ensures {
forall x:real. (mem x u.a /\ mem x v.a) <->
@@ -428,7 +673,7 @@ module Union
| Ord.Gt -> aux_option lu lv
end
end
-
+*)
end
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index 6b96b6d95..3f1523462 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -3,14 +3,26 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="3" name="Colibri2" version="n/a" timelimit="5" steplimit="0" memlimit="1000"/>
-<file format="whyml" proved="true">
+<file format="whyml">
<path name=".."/><path name="union.mlw"/>
-<theory name="Union" proved="true">
- <goal name="length0_positive'vc" expl="VC for length0_positive" proved="true">
+<theory name="Union">
+ <goal name="pos_length_on'vc" expl="VC for pos_length_on" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="pos_length_off'vc" expl="VC for pos_length_off" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="lt_bound_on_on_transitive'vc" expl="VC for lt_bound_on_on_transitive" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="lt_bound_on_off_transitive'vc" expl="VC for lt_bound_on_off_transitive" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="lt_bound0_transitive'vc" expl="VC for lt_bound0_transitive" proved="true">
- <proof prover="3"><result status="valid" time="0.65"/></proof>
+ <goal name="smaller_lt_bound_on'vc" expl="VC for smaller_lt_bound_on" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="smaller_lt_bound_off'vc" expl="VC for smaller_lt_bound_off" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="t''vc" expl="VC for t'" proved="true">
<transf name="split_vc" proved="true" >
@@ -22,8 +34,8 @@
</goal>
</transf>
</goal>
- <goal name="lt_bound0_is_not_mem0'vc" expl="VC for lt_bound0_is_not_mem0" proved="true">
- <proof prover="3"><result status="valid" time="0.29"/></proof>
+ <goal name="lt_bound_is_not_mem_off'vc" expl="VC for lt_bound_is_not_mem_off">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="singleton'vc" expl="VC for singleton" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -34,7 +46,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="is_singleton'vc.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.62"/></proof>
+ <proof prover="3"><result status="valid" time="2.71"/></proof>
</goal>
</transf>
</goal>
@@ -50,33 +62,248 @@
<goal name="max_bound_inf'vc" expl="VC for max_bound_inf" proved="true">
<proof prover="3"><result status="valid" time="0.13"/></proof>
</goal>
- <goal name="inter'vc" expl="VC for inter" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.0" expl="variant decrease" proved="true">
+ <goal name="inter'vc" expl="VC for inter">
+ <transf name="split_vc" >
+ <goal name="inter'vc.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.1" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.1" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.1.0" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.1.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.6" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.59.0.6.0" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.59.0.6.0.0" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.6.0.0.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.6.0.0.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.6.0.1" expl="postcondition">
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.6.0.1.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.6.0.1.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.6.0.2" expl="postcondition">
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.6.0.2.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.6.0.2.0.0" expl="postcondition">
+ <transf name="destruct_term" arg1="x2">
+ <goal name="inter'vc.59.0.6.0.2.0.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.6.0.2.0.0.1" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.6.1" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.6.1.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.6.1.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.6.2" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.6.2.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.6.2.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.7" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.59.0.7.0" expl="postcondition">
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.7.0.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.7.0.0.0" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="destruct_term" arg1="x4">
+ <goal name="inter'vc.59.0.7.0.0.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.7.0.0.0.1" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.7.1" expl="postcondition">
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.7.1.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.7.1.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.7.2" expl="postcondition">
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.59.0.7.2.0" expl="postcondition">
+ <transf name="instantiate" arg1="H4" arg2="x">
+ <goal name="inter'vc.59.0.7.2.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.4" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.59.0.4.0" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.4.1" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.4.2" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.59.0.3" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.5" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.0.2" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.1.1" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.1.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.6" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.7" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.4" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.3" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.93"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.5" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.1.2" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.1.2" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.1.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.6" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.7" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.4" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.3" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.5" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59.2.2" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.2" expl="precondition" proved="true">
+ <goal name="inter'vc.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.3" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.4" expl="precondition" proved="true">
+ <goal name="inter'vc.4" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.5" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.6" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.7" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.8" expl="precondition" proved="true">
+ <goal name="inter'vc.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.9" expl="variant decrease" proved="true">
@@ -88,84 +315,148 @@
<goal name="inter'vc.11" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.12" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.12" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.13" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.13" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.13.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.58.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.58.5" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.58.7" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.58.7.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.58.7.1" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="highfailure" time="4.17"/></proof>
+ </goal>
+ <goal name="inter'vc.58.7.2" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.58.6" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.58.6.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.58.6.1" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.58.6.2" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.58.2" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.58.4" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.58.4.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.58.4.1" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="highfailure" time="4.20"/></proof>
+ </goal>
+ <goal name="inter'vc.58.4.2" expl="postcondition">
+ <proof prover="3" obsolete="true"><path name="union-Union-interqtvc_6.psmt2"/><result status="timeout" time="5.00"/></proof>
+ <transf name="eliminate_let_fmla" >
+ <goal name="inter'vc.58.4.2.0" expl="postcondition">
+ <transf name="instantiate" arg1="H1" arg2="x2">
+ <goal name="inter'vc.58.4.2.0.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.58.3" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.61"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.14" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.14" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="inter'vc.15" expl="precondition" proved="true">
+ <goal name="inter'vc.15" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.16" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.17" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.18" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.19" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.20" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.21" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.22" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.21" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.23" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.22" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
+ </goal>
+ <goal name="inter'vc.23" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="inter'vc.24" expl="variant decrease" proved="true">
+ <goal name="inter'vc.24" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.25" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.26" expl="precondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.26.0" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.27" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.28" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.29" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.30" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.30" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.31" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.31" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="inter'vc.32" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.32" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="inter'vc.33" expl="variant decrease" proved="true">
+ <goal name="inter'vc.33" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.35" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.36" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.37" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -173,25 +464,25 @@
<goal name="inter'vc.38" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.39" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.39" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.40" expl="precondition" proved="true">
+ <goal name="inter'vc.40" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.41" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.41" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.42" expl="precondition" proved="true">
+ <goal name="inter'vc.42" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.43" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.44" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.45" expl="precondition" proved="true">
+ <goal name="inter'vc.45" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.46" expl="precondition" proved="true">
@@ -200,17 +491,17 @@
<goal name="inter'vc.47" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.48" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.48" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.49" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.49" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
- <goal name="inter'vc.50" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.50" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.27"/></proof>
</goal>
- <goal name="inter'vc.51" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.51" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.52" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -225,1174 +516,1092 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.56" expl="precondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.56.0" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.57" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.57" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.58" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.58" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
- <goal name="inter'vc.59" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.59" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.31"/></proof>
</goal>
- <goal name="inter'vc.60" expl="precondition" proved="true">
+ <goal name="inter'vc.60" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.61" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.61" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.62" expl="precondition" proved="true">
+ <goal name="inter'vc.62" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.63" expl="precondition" proved="true">
+ <goal name="inter'vc.63" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.64" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.65" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.65" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="inter'vc.66" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.67" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.67" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.68" expl="precondition" proved="true">
+ <goal name="inter'vc.68" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.69" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.70" expl="precondition" proved="true">
+ <goal name="inter'vc.69" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.71" expl="precondition" proved="true">
+ <goal name="inter'vc.70" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.72" expl="precondition" proved="true">
+ <goal name="inter'vc.71" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.72" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.73" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.44"/></proof>
</goal>
- <goal name="inter'vc.74" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.74" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.75" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.76" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.77" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.77" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.78" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.78" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.79" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.80" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.80" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.81" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.81" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
- <goal name="inter'vc.82" expl="precondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.82.0" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.82" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
</goal>
- <goal name="inter'vc.83" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.83" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.84" expl="variant decrease" proved="true">
+ <goal name="inter'vc.84" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.85" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.86" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.86" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.87" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.87" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.88" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.89" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.89" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.90" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.90" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
+ </goal>
+ <goal name="inter'vc.91" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.48"/></proof>
</goal>
- <goal name="inter'vc.91" expl="precondition" proved="true">
+ <goal name="inter'vc.92" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.92" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.93" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.93" expl="variant decrease" proved="true">
+ <goal name="inter'vc.94" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.95" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.94" expl="precondition" proved="true">
+ <goal name="inter'vc.96" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.95" expl="precondition" proved="true">
+ <goal name="inter'vc.97" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.96" expl="variant decrease" proved="true">
+ <goal name="inter'vc.98" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.99" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.100" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.101" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.97" expl="precondition" proved="true">
+ <goal name="inter'vc.102" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.103" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.98" expl="precondition" proved="true">
+ <goal name="inter'vc.104" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.99" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
+ <goal name="inter'vc.105" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.100" expl="precondition" proved="true">
+ <goal name="inter'vc.106" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.101" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.107" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.102" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.108" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="inter'vc.103" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.109" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.27"/></proof>
</goal>
- <goal name="inter'vc.104" expl="precondition" proved="true">
+ <goal name="inter'vc.110" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.105" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <goal name="inter'vc.111" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.106" expl="precondition" proved="true">
+ <goal name="inter'vc.112" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.113" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.107" expl="precondition" proved="true">
+ <goal name="inter'vc.114" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.108" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="inter'vc.109" expl="precondition" proved="true">
+ <goal name="inter'vc.115" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.110" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.116" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.111" expl="variant decrease" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.111.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.111.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.117" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="inter'vc.112" expl="precondition" proved="true">
+ <goal name="inter'vc.118" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.31"/></proof>
+ </goal>
+ <goal name="inter'vc.119" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.113" expl="precondition" proved="true">
+ <goal name="inter'vc.120" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.114" expl="postcondition" proved="true">
+ <goal name="inter'vc.121" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.114.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.47"/></proof>
+ <goal name="inter'vc.121.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.114.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.121.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.114.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.121.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.114.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.114.3.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.114.3.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.114.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.51"/></proof>
- </goal>
</transf>
</goal>
- <goal name="inter'vc.115" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.115.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.115.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.86"/></proof>
- </goal>
- <goal name="inter'vc.115.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.65"/></proof>
- </goal>
- <goal name="inter'vc.115.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.29"/></proof>
- </goal>
- <goal name="inter'vc.115.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.61"/></proof>
- </goal>
- <goal name="inter'vc.115.0.4" expl="postcondition" proved="true">
- <proof prover="3" timelimit="10"><result status="valid" time="9.90"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.115.1" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.115.1.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.10"/></proof>
- </goal>
- <goal name="inter'vc.115.1.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
- </goal>
- <goal name="inter'vc.115.1.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.115.1.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.25"/></proof>
- </goal>
- <goal name="inter'vc.115.1.4" expl="postcondition" proved="true">
- <proof prover="3" timelimit="10"><result status="valid" time="9.08"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.115.2" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.115.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.33"/></proof>
- </goal>
- <goal name="inter'vc.115.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
- </goal>
- <goal name="inter'vc.115.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
- </goal>
- <goal name="inter'vc.115.2.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
- </goal>
- <goal name="inter'vc.115.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.48"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
+ <goal name="inter'vc.122" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.123" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.124" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.126" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.127" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.128" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.129" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.130" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.131" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.132" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.133" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.134" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.135" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.116" expl="postcondition" proved="true">
+ <goal name="inter'vc.136" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.137" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.138" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.139" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.140" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.116.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.45"/></proof>
- </goal>
- <goal name="inter'vc.116.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
- </goal>
- <goal name="inter'vc.116.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <goal name="inter'vc.140.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.116.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <goal name="inter'vc.112.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.116.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.48"/></proof>
+ <goal name="inter'vc.112.5" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- </transf>
- </goal>
- <goal name="inter'vc.117" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.117.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <goal name="inter'vc.112.2" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.117.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
+ <goal name="inter'vc.112.7" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
- <goal name="inter'vc.117.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
+ <goal name="inter'vc.112.6" expl="postcondition">
+ <proof prover="3"><result status="highfailure" time="4.27"/></proof>
</goal>
- <goal name="inter'vc.117.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.117.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.112.4" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.117.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <goal name="inter'vc.112.3" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.118" expl="variant decrease" proved="true">
+ <goal name="inter'vc.141" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.142" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.119" expl="precondition" proved="true">
+ <goal name="inter'vc.143" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.144" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.145" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120" expl="precondition" proved="true">
+ <goal name="inter'vc.146" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.147" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.148" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.149" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.121" expl="precondition" proved="true">
+ <goal name="inter'vc.150" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.151" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.152" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.122" expl="precondition" proved="true">
+ <goal name="inter'vc.153" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.154" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.155" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.156" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.157" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.123" expl="precondition" proved="true">
+ <goal name="inter'vc.158" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.124" expl="precondition" proved="true">
+ <goal name="inter'vc.159" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.160" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.161" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.162" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.163" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.164" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.165" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.166" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.167" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.168" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.169" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.170" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
+ </goal>
+ <goal name="inter'vc.171" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.31"/></proof>
+ </goal>
+ <goal name="inter'vc.172" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.173" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.175" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.176" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.177" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.178" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.179" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.180" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.181" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.182" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.183" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.184" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.185" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.186" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.187" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.188" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.189" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.190" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.191" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.192" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.193" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.194" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.195" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.196" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.197" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.198" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.199" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.200" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.201" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.202" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.203" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.204" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.205" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.206" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.207" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.208" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.209" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.43"/></proof>
+ </goal>
+ <goal name="inter'vc.210" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.211" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.125" expl="precondition" proved="true">
+ <goal name="inter'vc.212" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.213" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.214" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.215" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.216" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.217" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
+ </goal>
+ <goal name="inter'vc.218" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="inter'vc.219" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="inter'vc.220" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.126" expl="precondition" proved="true">
+ <goal name="inter'vc.221" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.127" expl="precondition" proved="true">
+ <goal name="inter'vc.222" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.223" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.224" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.128" expl="precondition" proved="true">
+ <goal name="inter'vc.225" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.226" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.227" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.228" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.129" expl="precondition" proved="true">
+ <goal name="inter'vc.229" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.130" expl="precondition" proved="true">
+ <goal name="inter'vc.230" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.231" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.131" expl="precondition" proved="true">
+ <goal name="inter'vc.232" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.28"/></proof>
+ </goal>
+ <goal name="inter'vc.233" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.132" expl="precondition" proved="true">
+ <goal name="inter'vc.234" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.133" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.82"/></proof>
+ <goal name="inter'vc.235" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.134" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.134.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.134.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.134.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.04"/></proof>
- </goal>
- <goal name="inter'vc.134.0.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.50"/></proof>
- </goal>
- <goal name="inter'vc.134.0.5" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.0.5.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.93"/></proof>
- </goal>
- <goal name="inter'vc.134.0.5.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.85"/></proof>
- </goal>
- <goal name="inter'vc.134.0.5.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
- </goal>
- <goal name="inter'vc.134.0.5.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.49"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.0.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.0.7" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.0.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.64"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.0.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.52"/></proof>
- </goal>
- <goal name="inter'vc.134.0.9" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.41"/></proof>
- </goal>
- <goal name="inter'vc.134.0.10" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.0.11" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.13"/></proof>
- </goal>
- <goal name="inter'vc.134.0.12" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.0.12.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.84"/></proof>
- </goal>
- <goal name="inter'vc.134.0.12.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.94"/></proof>
- </goal>
- <goal name="inter'vc.134.0.12.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
- </goal>
- <goal name="inter'vc.134.0.12.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.42"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.0.13" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.0.13.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="6.93"/></proof>
- </goal>
- <goal name="inter'vc.134.0.13.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
- </goal>
- <goal name="inter'vc.134.0.13.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.1" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.1.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.1.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.1.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.1.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.64"/></proof>
- </goal>
- <goal name="inter'vc.134.1.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.09"/></proof>
- </goal>
- <goal name="inter'vc.134.1.5" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.1.5.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
- </goal>
- <goal name="inter'vc.134.1.5.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.56"/></proof>
- </goal>
- <goal name="inter'vc.134.1.5.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.55"/></proof>
- </goal>
- <goal name="inter'vc.134.1.5.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.1.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.1.7" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.1.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.41"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.1.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.134.1.9" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.81"/></proof>
- </goal>
- <goal name="inter'vc.134.1.10" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.1.11" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.1.11.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.96"/></proof>
- </goal>
- <goal name="inter'vc.134.1.11.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.38"/></proof>
- </goal>
- <goal name="inter'vc.134.1.11.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.16"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.1.12" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.1.12.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
- </goal>
- <goal name="inter'vc.134.1.12.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.63"/></proof>
- </goal>
- <goal name="inter'vc.134.1.12.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.52"/></proof>
- </goal>
- <goal name="inter'vc.134.1.12.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.1.13" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.1.13.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.22"/></proof>
- </goal>
- <goal name="inter'vc.134.1.13.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
- </goal>
- <goal name="inter'vc.134.1.13.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.2" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.134.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.2.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.73"/></proof>
- </goal>
- <goal name="inter'vc.134.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.134.2.5" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.2.5.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
- </goal>
- <goal name="inter'vc.134.2.5.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.57"/></proof>
- </goal>
- <goal name="inter'vc.134.2.5.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.50"/></proof>
- </goal>
- <goal name="inter'vc.134.2.5.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.2.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.2.7" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.2.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.2.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.13"/></proof>
- </goal>
- <goal name="inter'vc.134.2.9" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.2.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.15"/></proof>
- </goal>
- <goal name="inter'vc.134.2.9.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.56"/></proof>
- </goal>
- <goal name="inter'vc.134.2.9.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.41"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.2.10" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.134.2.11" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.05"/></proof>
- </goal>
- <goal name="inter'vc.134.2.12" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.2.12.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.16"/></proof>
- </goal>
- <goal name="inter'vc.134.2.12.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.34"/></proof>
- </goal>
- <goal name="inter'vc.134.2.12.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.56"/></proof>
- </goal>
- <goal name="inter'vc.134.2.12.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.134.2.13" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.134.2.13.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.82"/></proof>
- </goal>
- <goal name="inter'vc.134.2.13.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.134.2.13.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
+ <goal name="inter'vc.236" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.135" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.135.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.135.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.135.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.135.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.08"/></proof>
- </goal>
- <goal name="inter'vc.135.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.63"/></proof>
- </goal>
- <goal name="inter'vc.135.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.21"/></proof>
- </goal>
- <goal name="inter'vc.135.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.135.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.135.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
- </goal>
- <goal name="inter'vc.135.9" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.62"/></proof>
- </goal>
- <goal name="inter'vc.135.10" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.135.11" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.135.11.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
- </goal>
- <goal name="inter'vc.135.11.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.80"/></proof>
- </goal>
- <goal name="inter'vc.135.11.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.135.12" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.135.12.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.15"/></proof>
- </goal>
- <goal name="inter'vc.135.12.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.13"/></proof>
- </goal>
- <goal name="inter'vc.135.12.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
- </goal>
- <goal name="inter'vc.135.12.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.16"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.135.13" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.13"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.237" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.136" expl="postcondition" proved="true">
+ <goal name="inter'vc.238" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.239" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.240" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
+ </goal>
+ <goal name="inter'vc.241" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="inter'vc.242" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.243" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.244" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.136.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.136.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.244.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.136.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.136.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.20"/></proof>
- </goal>
- <goal name="inter'vc.136.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
- </goal>
- <goal name="inter'vc.136.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.35"/></proof>
- </goal>
- <goal name="inter'vc.136.6" expl="postcondition" proved="true">
+ <goal name="inter'vc.244.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.136.7" expl="postcondition" proved="true">
+ <goal name="inter'vc.244.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.136.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.62"/></proof>
- </goal>
- <goal name="inter'vc.136.9" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.66"/></proof>
- </goal>
- <goal name="inter'vc.136.10" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.136.11" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.136.12" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.16"/></proof>
- </goal>
- <goal name="inter'vc.136.13" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.31"/></proof>
- </goal>
</transf>
</goal>
- <goal name="inter'vc.137" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.245" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.246" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.247" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.248" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.249" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.250" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.251" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.252" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.253" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.254" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.255" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.256" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.257" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="inter'vc.258" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.259" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.260" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.261" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.262" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.263" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.264" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.138" expl="precondition" proved="true">
+ <goal name="inter'vc.265" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.266" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.267" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.268" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.269" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.270" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.271" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.272" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.139" expl="precondition" proved="true">
+ <goal name="inter'vc.273" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.140" expl="precondition" proved="true">
+ <goal name="inter'vc.274" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.141" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.14"/></proof>
+ <goal name="inter'vc.275" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.276" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.142" expl="precondition" proved="true">
+ <goal name="inter'vc.277" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.143" expl="precondition" proved="true">
+ <goal name="inter'vc.278" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.279" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.144" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
+ <goal name="inter'vc.280" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.145" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.281" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.146" expl="precondition" proved="true">
+ <goal name="inter'vc.282" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.147" expl="precondition" proved="true">
+ <goal name="inter'vc.283" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.284" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.148" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <goal name="inter'vc.285" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.149" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.286" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.150" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.287" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.151" expl="precondition" proved="true">
+ <goal name="inter'vc.288" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.152" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
+ <goal name="inter'vc.289" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.290" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter'vc.153" expl="precondition" proved="true">
+ <goal name="inter'vc.291" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.154" expl="unreachable point" proved="true">
+ <goal name="inter'vc.292" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.25"/></proof>
+ </goal>
+ <goal name="inter'vc.293" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.155" expl="precondition" proved="true">
+ <goal name="inter'vc.294" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.156" expl="precondition" proved="true">
+ <goal name="inter'vc.295" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.157" expl="precondition" proved="true">
+ <goal name="inter'vc.296" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.158" expl="precondition" proved="true">
+ <goal name="inter'vc.297" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.298" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.299" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.300" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.159" expl="precondition" proved="true">
+ <goal name="inter'vc.301" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.160" expl="precondition" proved="true">
+ <goal name="inter'vc.302" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.303" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.161" expl="precondition" proved="true">
+ <goal name="inter'vc.304" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.162" expl="precondition" proved="true">
+ <goal name="inter'vc.305" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.163" expl="precondition" proved="true">
+ <goal name="inter'vc.306" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.164" expl="precondition" proved="true">
+ <goal name="inter'vc.307" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.308" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.309" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.310" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.165" expl="precondition" proved="true">
+ <goal name="inter'vc.311" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.312" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.313" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.166" expl="precondition" proved="true">
+ <goal name="inter'vc.314" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.315" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.316" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.39"/></proof>
+ </goal>
+ <goal name="inter'vc.317" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.167" expl="unreachable point" proved="true">
+ <goal name="inter'vc.318" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.319" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.168" expl="precondition" proved="true">
+ <goal name="inter'vc.320" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.169" expl="precondition" proved="true">
+ <goal name="inter'vc.321" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.322" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.170" expl="precondition" proved="true">
+ <goal name="inter'vc.323" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.40"/></proof>
+ </goal>
+ <goal name="inter'vc.324" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.325" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.326" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.171" expl="precondition" proved="true">
+ <goal name="inter'vc.327" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.172" expl="precondition" proved="true">
+ <goal name="inter'vc.328" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.329" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.173" expl="precondition" proved="true">
+ <goal name="inter'vc.330" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.331" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.174" expl="precondition" proved="true">
+ <goal name="inter'vc.332" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.333" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.334" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.335" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.336" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.337" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.338" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.339" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.340" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.341" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.342" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.343" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.344" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.27"/></proof>
+ </goal>
+ <goal name="inter'vc.345" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.175" expl="precondition" proved="true">
+ <goal name="inter'vc.346" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.347" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.348" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.176" expl="precondition" proved="true">
+ <goal name="inter'vc.349" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.350" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.351" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.352" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.177" expl="precondition" proved="true">
+ <goal name="inter'vc.353" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.178" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.06"/></proof>
- </goal>
- <goal name="inter'vc.178.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.178.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.0.4" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.0.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.51"/></proof>
- </goal>
- <goal name="inter'vc.178.0.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.99"/></proof>
- </goal>
- <goal name="inter'vc.178.0.4.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.37"/></proof>
- </goal>
- <goal name="inter'vc.178.0.4.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.0.4.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.82"/></proof>
- </goal>
- <goal name="inter'vc.178.0.4.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.12"/></proof>
- </goal>
- <goal name="inter'vc.178.0.4.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.40"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.0.4.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.55"/></proof>
+ <goal name="inter'vc.354" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.355" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.356" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.357" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.358" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.359" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.360" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.361" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.362" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.363" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.364" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.365" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.366" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.367" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.368" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.369" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.370" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.371" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.372" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.373" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.374" expl="termination">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.375" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.376" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.376.0" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="inter'vc.376.0.0" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="instantiate" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.176.0.3.0" expl="postcondition">
+ <proof prover="3"><undone/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.178.0.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.0.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.16"/></proof>
- </goal>
- <goal name="inter'vc.178.0.7" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.0.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.49"/></proof>
+ <goal name="inter'vc.176.0.2" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="instantiate" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.176.0.2.0" expl="postcondition">
+ <proof prover="3"><undone/></proof>
</goal>
- <goal name="inter'vc.178.0.7.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.01"/></proof>
- </goal>
- <goal name="inter'vc.178.0.7.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.28"/></proof>
- </goal>
- <goal name="inter'vc.178.0.7.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.0.7.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.81"/></proof>
- </goal>
- <goal name="inter'vc.178.0.7.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.11"/></proof>
- </goal>
- <goal name="inter'vc.178.0.7.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.40"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.0.7.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.46"/></proof>
+ </transf>
+ </goal>
+ <goal name="inter'vc.176.0.1" expl="postcondition">
+ <transf name="instantiate" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.176.0.1.0" expl="postcondition">
+ <proof prover="3"><undone/></proof>
</goal>
</transf>
</goal>
+ <goal name="inter'vc.176.0.0" expl="postcondition">
+ <proof prover="3"><undone/></proof>
+ </goal>
</transf>
</goal>
- <goal name="inter'vc.178.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.376.1" expl="postcondition">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="inter'vc.376.2" expl="postcondition" proved="true">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.1.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.1.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.1.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.09"/></proof>
+ <goal name="inter'vc.376.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.19"/></proof>
</goal>
- <goal name="inter'vc.178.1.4" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.4.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.4.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.66"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.77"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.47"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.1.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.19"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.2" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.4.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.65"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.89"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.55"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.1.4.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.4.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.05"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.48"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.50"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.1.4.4" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.4.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.91"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.23"/></proof>
- </goal>
- <goal name="inter'vc.178.1.4.4.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.74"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.176.1.3" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="instantiate" arg1="Ensures1" arg2="x1">
+ <goal name="inter'vc.176.1.3.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.178.1.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.1.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.7.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.7.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.67"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.92"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.47"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.1.7.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.30"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.2" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.7.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.62"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.87"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.55"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.1.7.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.7.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.00"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.43"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.48"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.1.7.4" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.1.7.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.93"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.28"/></proof>
- </goal>
- <goal name="inter'vc.178.1.7.4.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.73"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.176.1.2" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="instantiate" arg1="Ensures1" arg2="x1">
+ <goal name="inter'vc.176.1.2.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
</goal>
- </transf>
- </goal>
- <goal name="inter'vc.178.2" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.178.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.2.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.84"/></proof>
- </goal>
- <goal name="inter'vc.178.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.47"/></proof>
- </goal>
- <goal name="inter'vc.178.2.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.2.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
- </goal>
- <goal name="inter'vc.178.2.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.30"/></proof>
+ <goal name="inter'vc.176.1.1" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <transf name="instantiate" arg1="Ensures1" arg2="x1">
+ <goal name="inter'vc.176.1.1.0" expl="postcondition">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
+ </goal>
+ </transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.178.3" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.178.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.178.3.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.54"/></proof>
- </goal>
- <goal name="inter'vc.178.3.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.28"/></proof>
- </goal>
- <goal name="inter'vc.178.3.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.178.3.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.16"/></proof>
- </goal>
- <goal name="inter'vc.178.3.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.36"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.376.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
+ <goal name="lt_bound_is_not_mem_on'vc" expl="VC for lt_bound_is_not_mem_on">
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ </goal>
</theory>
</file>
</why3session>
diff --git a/src_common/union__Union.ml b/src_common/union__Union.ml
index 2c9dcd2a9..38b000f8c 100644
--- a/src_common/union__Union.ml
+++ b/src_common/union__Union.ml
@@ -1,29 +1,45 @@
-type t0 =
- | Singleton of (Q.t) * t0
- | Inter of (Q.t) * Interval__Bound.t * (Q.t) * Interval__Bound.t * t0
- | FiniteInf of (Q.t) * Interval__Bound.t
- | End
+type on =
+ | OnSin of (Q.t) * on
+ | OnEnd of (Q.t) * Interval__Bound.t * off
+ | OnInf
+and off =
+ | OffSin of (Q.t) * off
+ | OffEnd of (Q.t) * Interval__Bound.t * on
+ | OffInf
type t =
- | InfFinite of (Q.t) * Interval__Bound.t * t0
- | Finite of t0
- | Inf
+ | On of on
+ | Off of off
type t' = t
-let singleton (q: Q.t) : t' = Finite (Singleton (q, End))
+let singleton (q: Q.t) : t' = Off (OffSin (q, OffInf))
let is_singleton (u: t') : (Q.t) option =
match u with
- | Inf -> None
- | InfFinite (q, _, _) -> None
- | Finite Singleton (q, End) -> Some q
- | Finite End -> assert false (* absurd *)
- | Finite Inter (q, _, q', _, _) -> None
- | Finite FiniteInf (q, _) -> None
- | Finite Singleton (q, Singleton (q', _)) -> None
- | Finite Singleton (_, Inter (q, _, q', _, _)) -> None
- | Finite Singleton (_, FiniteInf (q, _)) -> None
+ | Off OffSin (q, OffInf) -> Some q
+ | Off OffSin (q, OffSin (q', _)) -> None
+ | Off OffSin (_,
+ OffEnd (q,
+ _,
+ on)) ->
+ begin match on with
+ | OnSin (q', _) -> None
+ | OnEnd (q', _, _) -> None
+ | OnInf -> None
+ end
+ | Off OffEnd (q,
+ _,
+ on) ->
+ begin match on with
+ | OnSin (q', _) -> None
+ | OnEnd (q', _, _) -> None
+ | OnInf -> None
+ end
+ | On OnSin (q, _) -> None
+ | On OnEnd (q, _, _) -> None
+ | On OnInf -> None
+ | Off OffInf -> assert false (* absurd *)
let min_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
(b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
@@ -70,168 +86,140 @@ let max_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
| (Ord.Gt, _, _) -> (v1, b1)
let inter (u: t') (v: t') : t' option =
- let rec aux (u1: t0) (v1: t0) : t0 =
+ let rec inter_on_on (u1: on) (v1: on) : on =
match (u1, v1) with
- | ((End, _) | (_, End)) -> End
- | (Singleton (qu,
+ | ((u2, OnInf) | (OnInf, u2)) -> u2
+ | (OnSin (qu,
lu),
- Singleton (qv,
+ OnSin (qv,
lv)) ->
begin match (Q_extra.compare qu qv) with
- | Ord.Eq -> Singleton (qu, aux lu lv)
- | Ord.Lt -> aux lu v1
- | Ord.Gt -> aux u1 lv
+ | Ord.Eq -> OnSin (qu, inter_on_on lu lv)
+ | Ord.Lt -> OnSin (qu, inter_on_on lu v1)
+ | Ord.Gt -> OnSin (qv, inter_on_on u1 lv)
end
- | (FiniteInf (q,
- b),
- FiniteInf (q',
- b')) ->
- (let (q'', b'') = max_bound_inf q b q' b' in FiniteInf (q'', b''))
- | (((Singleton (qu, lu) as u2),
- (FiniteInf (qv, bv) as v2)) | ((FiniteInf (qv, bv) as v2),
- (Singleton (qu, lu) as u2))) ->
+ | (OnEnd (qu,
+ bu,
+ lu),
+ OnEnd (qv,
+ bv,
+ lv)) ->
begin match (Q_extra.compare qu qv) with
- | Ord.Lt -> aux lu v2
- | Ord.Gt -> u2
| Ord.Eq ->
- begin match bv with
- | Interval__Bound.Large -> u2
- | Interval__Bound.Strict -> lu
- end
+ (let b =
+ match (bu, bv) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ Interval__Bound.Large
+ | _ -> Interval__Bound.Strict in
+ OnEnd (qu, b, inter_off_off lu lv))
+ | Ord.Lt -> OnEnd (qu, bu, inter_on_off v1 lu)
+ | Ord.Gt -> OnEnd (qv, bv, inter_on_off u1 lv)
end
- | (((FiniteInf (q, b) as u3),
- (Inter (qv0, bv0, qv1, bv1, lv) as v3)) | ((Inter (qv0, bv0, qv1, bv1,
- lv) as v3),
- (FiniteInf (q, b) as u3))) ->
- begin match (Q_extra.compare q qv0) with
- | Ord.Lt -> v3
- | Ord.Gt ->
- begin match (Q_extra.compare q qv1) with
- | Ord.Lt -> Inter (q, b, qv1, bv1, lv)
- | Ord.Gt -> aux u3 lv
- | Ord.Eq ->
- begin match (b, bv1) with
- | (Interval__Bound.Large,
- Interval__Bound.Large) ->
- Singleton (q, lv)
- | _ -> lv
- end
- end
+ | (((OnSin (qu, lu) as u2),
+ (OnEnd (qv, bv, lv) as v2)) | ((OnEnd (qv, bv, lv) as v2),
+ (OnSin (qu, lu) as u2))) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq -> OnEnd (qv, Interval__Bound.Strict, inter_on_off lu lv)
+ | Ord.Lt -> OnSin (qu, inter_on_on lu v2)
+ | Ord.Gt -> OnEnd (qv, bv, inter_on_off u2 lv)
+ end
+ and inter_on_off (u3: on) (v3: off) : off =
+ match (u3, v3) with
+ | (_, OffInf) -> OffInf
+ | (OnInf, u4) -> u4
+ | (OnSin (qu,
+ lu),
+ OffSin (qv,
+ lv)) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq -> inter_on_off lu lv
+ | Ord.Lt -> inter_on_off lu v3
+ | Ord.Gt -> OffSin (qv, inter_on_off u3 lv)
+ end
+ | (OnEnd (qu,
+ bu,
+ lu),
+ OffEnd (qv,
+ bv,
+ lv)) ->
+ begin match (Q_extra.compare qu qv) with
| Ord.Eq ->
- begin match (b, bv0) with
- | (Interval__Bound.Strict,
+ begin match (bu, bv) with
+ | (Interval__Bound.Large,
Interval__Bound.Large) ->
- Inter (qv0, b, qv1, bv1, lv)
- | _ -> v3
+ OffSin (qu, inter_on_off lv lu)
+ | _ -> inter_on_off lv lu
end
+ | Ord.Lt -> inter_off_off lu v3
+ | Ord.Gt -> OffEnd (qv, bv, inter_on_on u3 lv)
end
- | (((Singleton (qu, lu) as u4),
- (Inter (qv0, bv0, qv1, bv1, lv) as v4)) | ((Inter (qv0, bv0, qv1, bv1,
- lv) as v4),
- (Singleton (qu, lu) as u4))) ->
- begin match (Q_extra.compare qu qv0) with
- | Ord.Lt -> aux lu v4
- | Ord.Gt ->
- begin match (Q_extra.compare qu qv1) with
- | Ord.Lt -> Singleton (qu, aux lu v4)
- | Ord.Gt -> aux u4 lv
- | Ord.Eq ->
- begin match bv1 with
- | Interval__Bound.Large -> Singleton (qu, aux lu lv)
- | _ -> aux lu lv
- end
- end
+ | ((OnSin (qu, lu) as u4),
+ (OffEnd (qv, bv, lv) as v4)) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq -> OffEnd (qv, Interval__Bound.Strict, inter_on_on lu lv)
+ | Ord.Lt -> inter_on_off lu v4
+ | Ord.Gt -> OffEnd (qv, bv, inter_on_on u4 lv)
+ end
+ | ((OnEnd (qv, bv, lv) as v5),
+ (OffSin (qu, lu) as u5)) ->
+ begin match (Q_extra.compare qu qv) with
| Ord.Eq ->
- begin match bv0 with
- | Interval__Bound.Large -> Singleton (qu, aux lu v4)
- | _ -> aux lu v4
+ begin match bv with
+ | Interval__Bound.Large -> OffSin (qv, inter_off_off lu lv)
+ | Interval__Bound.Strict -> inter_off_off lu lv
end
+ | Ord.Lt -> OffSin (qu, inter_on_off v5 lu)
+ | Ord.Gt -> inter_off_off u5 lv
+ end
+ and inter_off_off (u6: off) (v6: off) : off =
+ match (u6, v6) with
+ | ((_, OffInf) | (OffInf, _)) -> OffInf
+ | (OffSin (qu,
+ lu),
+ OffSin (qv,
+ lv)) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq -> OffSin (qu, inter_off_off lu lv)
+ | Ord.Lt -> inter_off_off lu v6
+ | Ord.Gt -> inter_off_off u6 lv
end
- | (Inter (qu0,
- bu0,
- qu1,
- bu1,
+ | (OffEnd (qu,
+ bu,
lu),
- Inter (qv0,
- bv0,
- qv1,
- bv1,
+ OffEnd (qv,
+ bv,
lv)) ->
- (let v' = v1 in let u' = u1 in
- let small_big (qu01: Q.t) (bu01: Interval__Bound.t) (qu11: Q.t)
- (bu11: Interval__Bound.t) (lu1: t0) (u5: t0) (qv01: Q.t)
- (bv01: Interval__Bound.t) (qv11: Q.t)
- (bv11: Interval__Bound.t) (lv1: t0) (v5: t0) : t0 =
- match (Q_extra.compare qu11 qv01) with
- | Ord.Eq ->
- begin match (bu11, bv01) with
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq ->
+ (let b =
+ match (bu, bv) with
| (Interval__Bound.Large,
Interval__Bound.Large) ->
- Singleton (qu11, aux lu1 v5)
- | _ -> aux lu1 v5
- end
- | Ord.Lt -> aux lu1 v5
- | Ord.Gt ->
- (let (qw0, bw0) = max_bound_inf qu01 bu01 qv01 bv01 in
- Inter (qw0, bw0, qu11, bu11, aux lu1 v5)) in
- match (Q_extra.compare qu1 qv1) with
- | Ord.Eq ->
- (let (qw01, bw01) = max_bound_inf qu0 bu0 qv0 bv0 in
- let b =
- match (bu1, bv1) with
- | (Interval__Bound.Large,
- Interval__Bound.Large) ->
- Interval__Bound.Large
- | _ -> Interval__Bound.Strict in
- Inter (qw01, bw01, qv1, b, aux lu lv))
- | Ord.Lt -> small_big qu0 bu0 qu1 bu1 lu u1 qv0 bv0 qv1 bv1 lv v1
- | Ord.Gt -> small_big qv0 bv0 qv1 bv1 lv v1 qu0 bu0 qu1 bu1 lu u1) in
- let aux_option (lu: t0) (lv: t0) : t' option =
- match aux lu lv with
- | End -> None
- | lw -> Some (Finite lw) in
+ Interval__Bound.Large
+ | _ -> Interval__Bound.Strict in
+ OffEnd (qu, b, inter_on_on lu lv))
+ | Ord.Lt -> inter_on_off lu v6
+ | Ord.Gt -> inter_on_off lv u6
+ end
+ | (((OffSin (qu, lu) as u7),
+ (OffEnd (qv, bv, lv) as v7)) | ((OffEnd (qv, bv, lv) as v7),
+ (OffSin (qu, lu) as u7))) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq ->
+ begin match bv with
+ | Interval__Bound.Large -> OffSin (qv, inter_on_off lv lu)
+ | Interval__Bound.Strict -> inter_on_off lv lu
+ end
+ | Ord.Lt -> inter_off_off lu v7
+ | Ord.Gt -> inter_on_off lv u7
+ end in
+ let mk_off_option (l: off) : t' option =
+ match l with
+ | OffInf -> None
+ | l1 -> Some (Off l1) in
match (u, v) with
- | (Inf, _) -> Some v
- | (_, Inf) -> Some u
- | (InfFinite (qu1,
- bu1,
- lu),
- InfFinite (qv1,
- bv1,
- lv)) ->
- begin match (Q_extra.compare qu1 qv1) with
- | Ord.Eq ->
- (let b =
- match (bu1, bv1) with
- | (Interval__Bound.Large,
- Interval__Bound.Large) ->
- Interval__Bound.Large
- | _ -> Interval__Bound.Strict in
- Some (InfFinite (qu1, b, aux lu lv)))
- | Ord.Lt ->
- Some (InfFinite (qu1, bu1,
- aux lu (Inter (qu1, Interval__Bound.Strict, qv1, bv1, lv))))
- | Ord.Gt ->
- Some (InfFinite (qv1, bv1,
- aux (Inter (qv1, Interval__Bound.Strict, qu1, bu1, lu)) lv))
- end
- | (Finite lu, Finite lv) -> aux_option lu lv
- | ((Finite lu, InfFinite (qv1, bv1, lv)) | (InfFinite (qv1, bv1, lv),
- Finite lu)) ->
- (let (qu0, bu0) =
- match lu with
- | End -> assert false (* absurd *)
- | Singleton (qu01, _) -> (qu01, Interval__Bound.Large)
- | Inter (qu01, bu01, _, _, _) -> (qu01, bu01)
- | FiniteInf (qu01, bu01) -> (qu01, bu01) in
- match (Q_extra.compare qu0 qv1) with
- | Ord.Eq ->
- begin match (bu0, bv1) with
- | (Interval__Bound.Large,
- Interval__Bound.Large) ->
- aux_option lu (Singleton (qv1, lv))
- | _ -> aux_option lu lv
- end
- | Ord.Lt -> aux_option lu (Inter (qu0, bu0, qv1, bv1, lv))
- | Ord.Gt -> aux_option lu lv)
+ | (On u8, On v8) -> Some (On (inter_on_on u8 v8))
+ | ((On u8, Off v8) | (Off v8, On u8)) -> mk_off_option (inter_on_off u8 v8)
+ | (Off u8, Off v8) -> mk_off_option (inter_off_off u8 v8)
--
GitLab