From 875f8b89ed1a56b3e6760ecef4548a16e15e92b5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 25 Oct 2021 16:14:41 +0200
Subject: [PATCH] Add limit on last effort
- Fix Interp when node has already a value
- Finish intersection of union of interval
---
src_colibri2/bin/dune | 1 +
src_colibri2/bin/options.ml | 86 +-
src_colibri2/core/colibri2_core.mli | 2 +
src_colibri2/core/interp.ml | 50 +-
src_colibri2/core/interp.mli | 2 +
src_colibri2/popop_lib/debug.ml | 2 +-
src_colibri2/solver/input.ml | 12 +-
src_colibri2/solver/scheduler.ml | 68 +-
src_colibri2/solver/scheduler.mli | 17 +-
src_colibri2/tests/tests_LRA.ml | 4 +-
src_colibri2/tests/tests_fp.ml | 2 +-
src_colibri2/tests/tests_lib.ml | 2 +-
src_colibri2/theories/ADT/adt_value.ml | 4 +-
src_colibri2/theories/LRA/dom_interval.ml | 17 +-
src_colibri2/theories/LRA/realValue.ml | 17 +-
src_colibri2/theories/LRA/realValue.mli | 4 +
src_common/union.mlw | 17 +-
src_common/union/why3session.xml | 2015 +++++++++------------
18 files changed, 1052 insertions(+), 1270 deletions(-)
diff --git a/src_colibri2/bin/dune b/src_colibri2/bin/dune
index efe704c10..630fce69e 100644
--- a/src_colibri2/bin/dune
+++ b/src_colibri2/bin/dune
@@ -7,6 +7,7 @@
cmdliner
fmt
gen
+ re
; dolmen deps
dolmen
dolmen.intf
diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
index 948cd7f66..50976d773 100644
--- a/src_colibri2/bin/options.ml
+++ b/src_colibri2/bin/options.ml
@@ -50,7 +50,22 @@ let gc_opts minor_heap_size major_heap_increment space_overhead max_overhead
let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
input_mode input header_check header_licenses header_lang_version type_check
type_strict debug context max_warn step_limit debug_flags show_steps
- check_status dont_print_result learning =
+ check_status dont_print_result learning limit_last_effort =
+ let last_effort_limit =
+ match limit_last_effort with
+ | None -> None
+ | Some (`Absolute_time f) -> Some (Colibri2_solver.Scheduler.Time f)
+ | Some (`Absolute_steps i) -> Some (Colibri2_solver.Scheduler.Steps i)
+ | Some (`Relative_time f) ->
+ Some (Colibri2_solver.Scheduler.Time (f *. time_limit))
+ | Some (`Relative_steps f) -> (
+ match step_limit with
+ | None -> None
+ | Some step_limit ->
+ Some
+ (Colibri2_solver.Scheduler.Steps
+ (int_of_float (f *. float step_limit))))
+ in
List.iter
Colibri2_popop_lib.Debug.(fun s -> set_flag (lookup_flag s))
debug_flags;
@@ -60,7 +75,7 @@ let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
( Colibri2_solver.Input.mk_state ~gc ~gc_opt ~bt ~colors ~time_limit
~size_limit ?input_lang ?input_mode ~input ~header_check ~header_licenses
~header_lang_version ~type_check ~type_strict ~debug ~context ~max_warn
- theories ~learning ?step_limit,
+ theories ~learning ?step_limit ?last_effort_limit,
show_steps,
check_status,
not dont_print_result )
@@ -136,13 +151,60 @@ let parse_time arg =
try
match arg.[l - 1] with
| 's' -> multiplier 1.
- | 'm' -> multiplier 60.
- | 'h' -> multiplier 3600.
- | 'd' -> multiplier 86400.
+ | 'm' -> multiplier (float nb_sec_minute)
+ | 'h' -> multiplier (float nb_sec_hour)
+ | 'd' -> multiplier (float nb_sec_day)
| '0' .. '9' -> `Ok (float_of_string arg)
| _ -> `Error "bad numeric argument"
with Failure _ -> `Error "bad numeric argument"
+let parse_limit_last_effort : _ Arg.parser =
+ let rint = Re.(group @@ rep1 digit) in
+ let rfloat =
+ Re.(group @@ seq [ rep1 digit; opt (seq [ char '.'; rep digit ]) ])
+ in
+ let relative unit = Re.(whole_string @@ seq [ rfloat; char '%'; str unit ]) in
+ let absolute_steps = Re.(whole_string @@ seq [ rint; str "steps" ]) in
+ let absolute_time = Re.(whole_string @@ seq [ rfloat; group (set "smhd") ]) in
+ let all =
+ Re.(
+ compile
+ @@ alt
+ [ relative "time"; relative "steps"; absolute_steps; absolute_time ])
+ in
+ fun arg ->
+ match Re.exec_opt all arg with
+ | None -> `Error "Bad last effort limit format"
+ | Some g -> (
+ match Re.Group.get_opt g 1 with
+ | Some s -> `Ok (`Relative_time (float_of_string s /. 100.))
+ | None -> (
+ match Re.Group.get_opt g 2 with
+ | Some s -> `Ok (`Relative_steps (float_of_string s /. 100.))
+ | None -> (
+ match Re.Group.get_opt g 3 with
+ | Some s -> `Ok (`Absolute_steps (int_of_string s))
+ | None -> (
+ match Re.Group.get_opt g 4 with
+ | Some s ->
+ let coef =
+ match Re.Group.get g 5 with
+ | "s" -> 1.
+ | "m" -> float nb_sec_minute
+ | "h" -> float nb_sec_hour
+ | "d" -> float nb_sec_day
+ | _ -> assert false
+ in
+ `Ok (`Absolute_time (float_of_string s *. coef))
+ | None -> `Error "Bad last effort limit format"))))
+
+let print_limit_last_effort : _ Arg.printer =
+ fun fmt -> function
+ | `Relative_time f -> Fmt.pf fmt "%f%%time" f
+ | `Relative_steps f -> Fmt.pf fmt "%f%%steps" f
+ | `Absolute_time f -> Fmt.pf fmt "%fs" f
+ | `Absolute_steps i -> Fmt.pf fmt "%isteps" i
+
let size_string f =
let n = int_of_float f in
let aux n div = (n / div, n mod div) in
@@ -177,6 +239,8 @@ let c_time = (parse_time, print_time)
let c_size = (parse_size, print_size)
+let c_limit_last_effort = (parse_limit_last_effort, print_limit_last_effort)
+
(* Gc Options parsing *)
(* ************************************************************************* *)
@@ -381,9 +445,19 @@ let state theories =
value & flag
& info ~env:(env_var ~doc "COLIBRI2_LEARNING") [ "learning" ] ~docs ~doc)
in
+ let last_effort_limit =
+ let doc =
+ "Deactivate last effort after the given time ( 90%steps, 90%time, \
+ 200steps, 200s )"
+ in
+ Arg.(
+ value
+ & opt (some c_limit_last_effort) None
+ & info [ "limit-last-effort" ] ~docs ~doc)
+ in
Term.(
const (mk_state theories)
$ gc $ gc_t $ bt $ colors $ time $ size $ in_lang $ in_mode $ input
$ header_check $ header_licenses $ header_lang_version $ typing $ strict
$ debug $ context $ max_warn $ step_limit $ debug_flags $ show_steps
- $ check_status $ dont_print_result $ learning)
+ $ check_status $ dont_print_result $ learning $ last_effort_limit)
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index c377ed961..bb76702dc 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -554,6 +554,8 @@ module Interp : sig
val map : 'a t -> f:('a -> 'b) -> 'b t
+ val filter_map : 'a t -> f:('a -> 'b option) -> 'b t
+
val unfold_with :
'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Base.Sequence.Step.t) -> 'c t
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 4ddca2101..4dffec901 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -107,6 +107,8 @@ module SeqLim = struct
let map (x : 'a t) ~f i = Sequence.map ~f (x i)
+ let filter_map (x : 'a t) ~f i = Sequence.filter_map ~f (x i)
+
let unfold_with x ~init ~f i = Sequence.unfold_with (x i) ~init ~f
let ( let+ ) x y i = Sequence.( >>| ) (x i) y
@@ -210,32 +212,34 @@ let node d n =
Fmt.(iter_bindings ~sep:comma Node.H.iter (pair Node.pp nop))
parent;
raise Impossible)
- else (
- Node.H.replace parent n' ();
- let r =
- try
- get_registered
- (fun n' -> raise (CantInterpretNode n'))
- Data.node
- (fun f d x -> f aux d x)
- d n'
- with CantInterpretNode _ as exn ->
- if Ground.Ty.S.is_empty (Ground.tys d n') then
- match Nodes.Only_for_solver.thterm n' with
- | None ->
- Fmt.epr "@.%a does not have type@." Node.pp n';
- raise exn
- | Some th -> (
- match Ground.of_thterm th with
+ else
+ match Egraph.get_value d n' with
+ | Some v -> fun _ -> Sequence.singleton v
+ | None ->
+ Node.H.replace parent n' ();
+ let r =
+ try
+ get_registered
+ (fun n' -> raise (CantInterpretNode n'))
+ Data.node
+ (fun f d x -> f aux d x)
+ d n'
+ with CantInterpretNode _ as exn ->
+ if Ground.Ty.S.is_empty (Ground.tys d n') then
+ match Nodes.Only_for_solver.thterm n' with
| None ->
Fmt.epr "@.%a does not have type@." Node.pp n';
raise exn
- | Some g -> ty (Egraph.ro d) (Ground.sem g).ty)
- else ty (Egraph.ro d) (Ground.Ty.S.choose (Ground.tys d n'))
- in
-
- Node.H.remove parent n';
- SeqLim.incr_depth d r)
+ | Some th -> (
+ match Ground.of_thterm th with
+ | None ->
+ Fmt.epr "@.%a does not have type@." Node.pp n';
+ raise exn
+ | Some g -> ty (Egraph.ro d) (Ground.sem g).ty)
+ else ty (Egraph.ro d) (Ground.Ty.S.choose (Ground.tys d n'))
+ in
+ Node.H.remove parent n';
+ SeqLim.incr_depth d r
in
aux d n
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index 01211721e..1f64312bb 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -40,6 +40,8 @@ module SeqLim : sig
val map : 'a t -> f:('a -> 'b) -> 'b t
+ val filter_map : 'a t -> f:('a -> 'b option) -> 'b t
+
val unfold_with :
'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Sequence.Step.t) -> 'c t
diff --git a/src_colibri2/popop_lib/debug.ml b/src_colibri2/popop_lib/debug.ml
index 136674beb..8fb130466 100644
--- a/src_colibri2/popop_lib/debug.ml
+++ b/src_colibri2/popop_lib/debug.ml
@@ -71,7 +71,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
let stack_trace = register_flag "stack_trace"
~desc:"Avoid@ catching@ exceptions@ in@ order@ to@ get@ the@ stack@ trace."
-let timestamp = register_info_flag "timestamp"
+let timestamp = register_flag "timestamp"
~desc:"Print@ a@ timestamp@ before@ debugging@ messages."
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index d9e85ca2a..434729d7e 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -47,8 +47,8 @@ let pp_status_colibri fmt = function
| `Unsat -> Fmt.pf fmt "unsat"
| `StepLimitReached -> Fmt.pf fmt "step limit reached"
-let create_ctx ?step_limit learning theories =
- let t = Scheduler.new_solver ~learning () in
+let create_ctx ?step_limit ?last_effort_limit learning theories =
+ let t = Scheduler.new_solver ~learning ?last_effort_limit () in
let ctx = Scheduler.get_context t in
Scheduler.init_theories t ~theories;
{
@@ -222,7 +222,9 @@ let hyp ~set_true st t =
let solve ~set_true st t =
let check st =
match
- Scheduler.check_sat ?limit:(Context.Ref.get st.step_limit) st.scheduler
+ Scheduler.check_sat
+ ?step_limit:(Context.Ref.get st.step_limit)
+ st.scheduler
with
| res -> st.state <- res
| exception Scheduler.ReachStepLimit -> st.state <- `StepLimitReached
@@ -433,7 +435,7 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
?input_lang ?input_mode ~input ?(header_check = false)
?(header_licenses = []) ?(header_lang_version = None) ?(type_check = true)
?(type_strict = true) ?(debug = false) ?(context = true)
- ?(max_warn = max_int) ?(learning = false) theories =
+ ?(max_warn = max_int) ?(learning = false) ?last_effort_limit theories =
(* Side-effects *)
let () = Gc.set gc_opt in
let () =
@@ -464,7 +466,7 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
type_check;
type_strict;
type_state = Dolmen_loop.Typer.new_state ();
- solve_state = create_ctx ?step_limit learning theories;
+ solve_state = create_ctx ?step_limit ?last_effort_limit learning theories;
export_lang = [];
}
in
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 53127a77b..083669326 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -62,6 +62,8 @@ exception Contradiction
exception ReachStepLimit
+type last_effort_limit = Time of float | Steps of int
+
module PrioMake (S : sig
type t
@@ -199,6 +201,7 @@ type t = {
context : Context.context;
mutable level : int;
solve_step : solve_step Context.Ref.t;
+ last_effort_limit : last_effort_limit option;
mutable steps : int;
mutable stepsl : int;
mutable last_todo : (Egraph.wt -> unit) * bp_kind;
@@ -230,7 +233,7 @@ let get_steps t = t.steps
* var_inc = t.var_inc
* } *)
-let new_solver ~learning () =
+let new_solver ~learning ?last_effort_limit () =
let context = Context.create () in
let creator = Context.creator context in
let daemon_count = ref (-1) in
@@ -251,6 +254,7 @@ let new_solver ~learning () =
stepsl = 0;
last_todo = ((fun _ -> ()), External);
last_effort_learnt = Context.Clicket.create creator;
+ last_effort_limit;
allow_learning = learning;
learning = false;
learning_htbl = ThTerm.H.create 32;
@@ -637,21 +641,28 @@ let run_one_step_propagation ~nodec t =
true
| None -> (
t.last_decision_made <- None;
- Debug.dprintf1 debug_queue "[Scheduler] LastEffort: %i"
- (PrioLastEffort.size t.lasteffort);
- (* if Context.TimeWheel.current_time t.lasteffort < max_last_effort then *)
- match PrioLastEffort.extract_min t.lasteffort with
- | Some att as o ->
- Debug.incr stats_lasteffort;
- t.last_effort_made <- o;
- protect_against_contradiction t
- (fun () ->
- let d = Backtrackable.get_delayed t.solver_state in
- Backtrackable.run_daemon d att.v)
- (fun () -> true)
- | None ->
- t.last_effort_made <- None;
- false
+ let last_effort_deactivated =
+ match t.last_effort_limit with
+ | Some (Steps step_limit) -> step_limit <= t.steps
+ | _ -> false
+ in
+ Debug.dprintf2 debug_queue "[Scheduler] LastEffort: %i%s"
+ (PrioLastEffort.size t.lasteffort)
+ (if last_effort_deactivated then " (deactivated)" else "");
+ if last_effort_deactivated then false
+ else
+ match PrioLastEffort.extract_min t.lasteffort with
+ | Some att as o ->
+ Debug.incr stats_lasteffort;
+ t.last_effort_made <- o;
+ protect_against_contradiction t
+ (fun () ->
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d att.v)
+ (fun () -> true)
+ | None ->
+ t.last_effort_made <- None;
+ false
(* else false *)))
let run_one_step_fix_model ~nodec t =
@@ -713,16 +724,16 @@ let rec flush t =
conflict_analysis t;
flush t
-let rec run_inf_step ~limit ~nodec t =
- if t.steps = limit then raise ReachStepLimit;
+let rec run_inf_step ~step_limit ~nodec t =
+ if t.steps = step_limit then raise ReachStepLimit;
flush t;
match run_one_step ~nodec t with
- | true -> run_inf_step ~limit ~nodec t
+ | true -> run_inf_step ~step_limit ~nodec t
| false -> Backtrackable.delayed_stop t.solver_state
-let run_inf_step ?(limit = -1) ?(nodec = false) t =
+let run_inf_step ?(step_limit = -1) ?(nodec = false) t =
try
- run_inf_step ~limit ~nodec t;
+ run_inf_step ~step_limit ~nodec t;
Debug.dprintf1 debug_pushpop "[Scheduler] sat(%i)" t.steps
with Contradiction as e ->
Debug.dprintf1 debug_pushpop "[Scheduler] unsat(%i)" t.steps;
@@ -748,25 +759,26 @@ let add_assertion t f =
Debug.dprintf0 debug "[Scheduler] Contradiction during assertion";
raise Contradiction
-let check_sat ?limit t =
+let check_sat ?step_limit t =
try
flush t;
- run_inf_step ?limit t;
+ run_inf_step ?step_limit t;
let d = Backtrackable.get_delayed t.solver_state in
if Backtrackable.get_unknown t.solver_state then `Unknown d else `Sat d
with Contradiction -> `Unsat
-let run_exn ?nodec ?limit ?(learning = false) ~theories f =
- let t = new_solver ~learning () in
+let run_exn ?nodec ?step_limit ?last_effort_limit ?(learning = false) ~theories
+ f =
+ let t = new_solver ~learning ?last_effort_limit () in
init_theories ~theories t;
let check = add_assertion t f in
flush t;
- run_inf_step ~nodec:(nodec = Some ()) ?limit t;
+ run_inf_step ~nodec:(nodec = Some ()) ?step_limit t;
let d = Backtrackable.get_delayed t.solver_state in
check d
-let run ?nodec ?limit ~theories f =
- try `Done (run_exn ?nodec ?limit ~theories f)
+let run ?nodec ?step_limit ?last_effort_limit ~theories f =
+ try `Done (run_exn ?nodec ?step_limit ?last_effort_limit ~theories f)
with Contradiction -> `Contradiction
let pop_to st bp = ignore (pop_to st bp)
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index 9f3d37d5e..ce31fa15d 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -18,9 +18,16 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+type last_effort_limit =
+ | Time of float
+ (* nb seconds *)
+ | Steps of int
+(* nb steps *)
+
val run_exn :
?nodec:unit ->
- ?limit:int ->
+ ?step_limit:int ->
+ ?last_effort_limit:last_effort_limit ->
?learning:bool ->
theories:(Egraph.wt -> unit) list ->
(Egraph.wt -> Egraph.wt -> 'a) ->
@@ -34,21 +41,23 @@ val run_exn :
val run :
?nodec:unit ->
- ?limit:int ->
+ ?step_limit:int ->
+ ?last_effort_limit:last_effort_limit ->
theories:(Egraph.wt -> unit) list ->
(Egraph.wt -> Egraph.wt -> 'a) ->
[> `Contradiction | `Done of 'a ]
type t
-val new_solver : learning:bool -> unit -> t
+val new_solver :
+ learning:bool -> ?last_effort_limit:last_effort_limit -> unit -> t
val init_theories : theories:(Egraph.wt -> unit) list -> t -> unit
val add_assertion : t -> (Egraph.wt -> unit) -> unit
val check_sat :
- ?limit:int -> t -> [> `Unsat | `Sat of Egraph.wt | `Unknown of Egraph.wt ]
+ ?step_limit:int -> t -> [> `Unsat | `Sat of Egraph.wt | `Unknown of Egraph.wt ]
val get_steps : t -> int
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 957dfff4b..d26a54428 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -35,9 +35,9 @@ let theories =
LRA.th_register;
]
-let run f = Scheduler.run_exn ~limit:3000 ~nodec:() ~theories f
+let run f = Scheduler.run_exn ~step_limit:3000 ~nodec:() ~theories f
-let run_dec f = Scheduler.run_exn ~limit:3000 ?nodec:None ~theories f
+let run_dec f = Scheduler.run_exn ~step_limit:3000 ?nodec:None ~theories f
let ( $$ ) f x = f x
diff --git a/src_colibri2/tests/tests_fp.ml b/src_colibri2/tests/tests_fp.ml
index 3dc6f9b67..68fd770d0 100644
--- a/src_colibri2/tests/tests_fp.ml
+++ b/src_colibri2/tests/tests_fp.ml
@@ -29,7 +29,7 @@ let theories = [ Boolean.th_register; Equality.th_register; Fp.th_register ]
let ( $$ ) f x = f x
-let run f = Scheduler.run_exn ~limit:3000 ~nodec:() ~theories f
+let run f = Scheduler.run_exn ~step_limit:3000 ~nodec:() ~theories f
let recognize_float32 _ =
run @@ fun env ->
diff --git a/src_colibri2/tests/tests_lib.ml b/src_colibri2/tests/tests_lib.ml
index 4e2cccfd7..c760ecddb 100644
--- a/src_colibri2/tests/tests_lib.ml
+++ b/src_colibri2/tests/tests_lib.ml
@@ -65,7 +65,7 @@ exception ReachStepLimit
exception Contradiction
-let run_exn = Colibri2_solver.Scheduler.run_exn ~limit:3000
+let run_exn = Colibri2_solver.Scheduler.run_exn ~step_limit:3000
let check_file ?limit ~theories filename =
let st =
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index ceb39eed2..2cfdb6f60 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -174,12 +174,12 @@ let init_ty d =
let i =
List.count args ~f:(fun ty -> Ground.Ty.equal ty adt.mono)
in
- (c, i))
+ (c, i + List.length args))
in
let cases =
List.sort ~compare:(fun (_, i) (_, j) -> Int.compare i j) cases
in
- Debug.dprintf2 debug "cases:%a"
+ Debug.dprintf4 debug "Order cases for %a:%a" MonoAdt.pp adt
Fmt.(list ~sep:semi (pair ~sep:comma Case.pp Int.pp))
cases;
let cases = List.map cases ~f:fst in
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 8785b5256..8d400b089 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -241,4 +241,19 @@ let init env =
let v = RealValue.value value in
let s = D.singleton v in
Egraph.set_dom d dom (RealValue.node value) s);
- Ground.register_converter env converter
+ Ground.register_converter env converter;
+ Interp.Register.node env (fun _ d n ->
+ match Egraph.get_dom d dom n with
+ | None -> None
+ | Some inter ->
+ Some
+ (if D.is_integer inter then
+ Interp.SeqLim.of_seq d
+ (Base.Sequence.filter_map RealValue.int_sequence ~f:(fun z ->
+ let q = Q.of_bigint z in
+ if D.mem q inter then Some RealValue.(nodevalue (cst' q))
+ else None))
+ else
+ Interp.SeqLim.filter_map (RealValue.q_sequence d) ~f:(fun q ->
+ if D.mem q inter then Some RealValue.(nodevalue (cst' q))
+ else None)))
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index d4002abf0..d77a2f428 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -65,6 +65,11 @@ let zero = cst Q.zero
let one = cst Q.one
+let positive_int_sequence =
+ let open Base.Sequence.Generator in
+ let rec loop i = yield i >>= fun () -> loop (Z.succ i) in
+ run (loop Z.one)
+
let int_sequence_without_zero =
let open Base.Sequence.Generator in
let rec loop i =
@@ -75,6 +80,11 @@ let int_sequence_without_zero =
let int_sequence = Base.Sequence.shift_right int_sequence_without_zero Z.zero
+let q_sequence d =
+ let open Interp.SeqLim in
+ let+ num = of_seq d int_sequence and* den = of_seq d positive_int_sequence in
+ Q.make num den
+
let init_ty d =
Interp.Register.ty d (fun d ty ->
match ty with
@@ -83,12 +93,7 @@ let init_ty d =
(Interp.SeqLim.map (Interp.SeqLim.of_seq d int_sequence)
~f:(fun i -> nodevalue (cst' (Q.of_bigint i))))
| { app = { builtin = Expr.Real; _ }; _ } ->
- let seq =
- let open Interp.SeqLim in
- let+ num = of_seq d int_sequence
- and* den = of_seq d int_sequence_without_zero in
- Q.make num den
- in
+ let seq = q_sequence d in
let seq =
Interp.SeqLim.unfold_with seq ~init:Q.S.empty ~f:(fun s v ->
if Q.S.mem v s then Skip s
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index c2862ae8a..2cefb591c 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -33,3 +33,7 @@ val cst : Q.t -> Node.t
val zero : Node.t
val init : Egraph.wt -> unit
+
+val int_sequence : Z.t Base.Sequence.t
+
+val q_sequence : _ Egraph.t -> Q.t Interp.SeqLim.t
diff --git a/src_common/union.mlw b/src_common/union.mlw
index 4ce3e88ae..0f1cd7f28 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -198,7 +198,7 @@ module Union
| OffSin q l ->
x = q \/ mem_off x l
| OffEnd q b l ->
- not (cmp x b q) /\ mem_on x l
+ cmp q b x /\ mem_on x l
| OffInf -> false
end
@@ -361,7 +361,7 @@ module Union
| (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.Eq -> smaller_lt_bound_on qv qu lu; lt_bound_is_not_mem_off qv lv; 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
@@ -383,12 +383,14 @@ module Union
| _, OffInf -> OffInf
| OnInf, u -> u
| OnSin qu lu, OffSin qv lv ->
+ lt_bound_is_not_mem_off 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)
+ | Ord.Gt -> smaller_lt_bound_on qv qu lu; assert { lt_bound_on qv u }; OffSin qv (inter_on_off u lv)
end
| OnEnd qu bu lu, OffEnd qv bv lv ->
+ lt_bound_is_not_mem_off qu lu;
match Q.compare qu qv with
| Ord.Eq ->
match bu, bv with
@@ -408,11 +410,11 @@ module Union
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
+ | Large -> lt_bound_is_not_mem_off qu lu; OffSin qv (inter_off_off lu lv)
+ | Strict -> lt_bound_is_not_mem_off qv lv; lt_bound_is_not_mem_off qu lu; 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
+ | Ord.Gt -> lt_bound_is_not_mem_off qv lv; lt_bound_is_not_mem_off qu lu; inter_off_off u lv
end
end
with inter_off_off (u:off) (v:off) : off
@@ -431,6 +433,8 @@ module Union
match u, v with
| _, OffInf | OffInf, _ -> OffInf
| OffSin qu lu, OffSin qv lv ->
+ lt_bound_is_not_mem_off qv lv;
+ lt_bound_is_not_mem_off qu lu;
match Q.compare qu qv with
| Ord.Eq -> OffSin qu (inter_off_off lu lv)
| Ord.Lt -> inter_off_off lu v
@@ -450,6 +454,7 @@ module Union
end
| (OffSin qu lu) as u, (OffEnd qv bv lv) as v
| (OffEnd qv bv lv) as v, (OffSin qu lu) as u ->
+ lt_bound_is_not_mem_off qu lu;
match Q.compare qu qv with
| Ord.Eq -> match bv with
| Large -> OffSin qv (inter_on_off lv lu)
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index 3f1523462..0662568ac 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -3,9 +3,9 @@
"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">
+<file format="whyml" proved="true">
<path name=".."/><path name="union.mlw"/>
-<theory name="Union">
+<theory name="Union" proved="true">
<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>
@@ -34,8 +34,8 @@
</goal>
</transf>
</goal>
- <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 name="lt_bound_is_not_mem_off'vc" expl="VC for lt_bound_is_not_mem_off" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="singleton'vc" expl="VC for singleton" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -46,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="2.71"/></proof>
+ <proof prover="3"><result status="valid" time="2.49"/></proof>
</goal>
</transf>
</goal>
@@ -62,1546 +62,1193 @@
<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">
- <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="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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.9" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.10" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <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.01"/></proof>
- </goal>
- <goal name="inter'vc.18" expl="variant decrease" proved="true">
- <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.02"/></proof>
- </goal>
- <goal name="inter'vc.20" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.21" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="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.01"/></proof>
- </goal>
- <goal name="inter'vc.26" expl="precondition" proved="true">
- <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.01"/></proof>
- </goal>
- <goal name="inter'vc.28" expl="precondition" proved="true">
- <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="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <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.01"/></proof>
- </goal>
- <goal name="inter'vc.36" expl="variant decrease" proved="true">
- <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>
- </goal>
- <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="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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.01"/></proof>
- </goal>
- <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">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.27"/></proof>
- </goal>
- <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>
- </goal>
- <goal name="inter'vc.53" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.54" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.55" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.56" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.57" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.31"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <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="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.01"/></proof>
- </goal>
- <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="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.70" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.44"/></proof>
- </goal>
- <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.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="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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">
+ <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">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.80" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.47"/></proof>
- </goal>
- <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="precondition" proved="true">
+ <goal name="inter'vc.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.85" expl="precondition" proved="true">
+ <goal name="inter'vc.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.86" expl="variant decrease" proved="true">
+ <goal name="inter'vc.3" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.87" expl="precondition" proved="true">
+ <goal name="inter'vc.4" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.88" expl="precondition" proved="true">
+ <goal name="inter'vc.5" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.89" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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.92" expl="postcondition" proved="true">
+ <goal name="inter'vc.6" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.93" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <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">
+ <goal name="inter'vc.7" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.96" expl="precondition" proved="true">
+ <goal name="inter'vc.8" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.97" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <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">
+ <goal name="inter'vc.9" expl="precondition" 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.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">
+ <goal name="inter'vc.10" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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.105" 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.11" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.107" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="inter'vc.108" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.109" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.27"/></proof>
- </goal>
- <goal name="inter'vc.110" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.111" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.112" expl="precondition" proved="true">
+ <goal name="inter'vc.12" 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.114" expl="precondition" proved="true">
+ <goal name="inter'vc.13" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.115" expl="precondition" proved="true">
+ <goal name="inter'vc.14" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.116" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="inter'vc.117" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
- </goal>
- <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.120" expl="postcondition" proved="true">
+ <goal name="inter'vc.15" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <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.121.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <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.121.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
- </goal>
- <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">
+ <goal name="inter'vc.16" expl="variant decrease" 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">
+ <goal name="inter'vc.17" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.129" expl="variant decrease" proved="true">
+ <goal name="inter'vc.18" expl="precondition" 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">
+ <goal name="inter'vc.19" 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">
+ <goal name="inter'vc.20" expl="precondition" 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">
+ <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.136" expl="variant decrease" proved="true">
+ <goal name="inter'vc.22" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.137" expl="precondition" proved="true">
+ <goal name="inter'vc.23" 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.140.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.112.0" expl="postcondition">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.112.5" expl="postcondition">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.112.2" expl="postcondition">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.112.7" expl="postcondition">
- <proof prover="3"><result status="valid" time="0.24"/></proof>
- </goal>
- <goal name="inter'vc.112.6" expl="postcondition">
- <proof prover="3"><result status="highfailure" time="4.27"/></proof>
- </goal>
- <goal name="inter'vc.112.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <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.141" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.24" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.25" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.142" expl="postcondition" proved="true">
+ <goal name="inter'vc.26" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.143" expl="variant decrease" proved="true">
+ <goal name="inter'vc.27" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.144" expl="precondition" proved="true">
+ <goal name="inter'vc.28" expl="precondition" proved="true">
+ <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.145" expl="precondition" proved="true">
+ <goal name="inter'vc.30" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.146" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.31" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.147" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.32" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.148" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.33" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.149" expl="postcondition" proved="true">
+ <goal name="inter'vc.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.150" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.35" expl="precondition" proved="true">
+ <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.01"/></proof>
</goal>
- <goal name="inter'vc.151" expl="precondition" proved="true">
+ <goal name="inter'vc.37" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.152" expl="precondition" proved="true">
+ <goal name="inter'vc.38" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.153" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.39" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.154" expl="postcondition" proved="true">
+ <goal name="inter'vc.40" expl="precondition" 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 name="inter'vc.41" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.156" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.42" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.157" expl="variant decrease" proved="true">
+ <goal name="inter'vc.43" 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.44" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.159" expl="precondition" proved="true">
+ <goal name="inter'vc.45" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.46" 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 name="inter'vc.47" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.161" expl="postcondition" proved="true">
+ <goal name="inter'vc.48" expl="precondition" 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 name="inter'vc.49" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.163" expl="postcondition" proved="true">
+ <goal name="inter'vc.50" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.164" expl="precondition" proved="true">
+ <goal name="inter'vc.51" expl="precondition" 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.52" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.166" expl="variant decrease" proved="true">
+ <goal name="inter'vc.53" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.54" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.167" expl="precondition" proved="true">
+ <goal name="inter'vc.55" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.56" 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.57" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.58" 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 name="inter'vc.59" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.170" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
+ <goal name="inter'vc.60" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.77"/></proof>
</goal>
- <goal name="inter'vc.171" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.31"/></proof>
+ <goal name="inter'vc.61" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.45"/></proof>
+ </goal>
+ <goal name="inter'vc.61.0.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.00"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.1.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.07"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.46"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1.5" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.1.5.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.40"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.1.7.0" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="inter'vc.61.1.7.0.0" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="H3" arg2="x">
+ <goal name="inter'vc.61.1.7.0.0.0" expl="postcondition" proved="true">
+ <transf name="case" proved="true" arg1="(x <. x5)">
+ <goal name="inter'vc.61.1.7.0.0.0.0" expl="true case (postcondition)" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.7.0.0.0.1" expl="false case (postcondition)" proved="true">
+ <transf name="case" proved="true" arg1="(x = x5)">
+ <goal name="inter'vc.61.1.7.0.0.0.1.0" expl="false case (true case. postcondition)" proved="true">
+ <transf name="cut" proved="true" arg1="(x = x2)">
+ <goal name="inter'vc.61.1.7.0.0.0.1.0.0" expl="false case (true case. postcondition)" proved="true">
+ <transf name="cut" proved="true" arg1="(not (cmp x Strict x5))">
+ <goal name="inter'vc.61.1.7.0.0.0.1.0.0.0" expl="false case (true case. postcondition)" proved="true">
+ <transf name="cut" proved="true" arg1="(not (mem_off x o2))">
+ <goal name="inter'vc.61.1.7.0.0.0.1.0.0.0.0" expl="false case (true case. postcondition)" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.7.0.0.0.1.0.0.0.1" expl="asserted formula" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1.7.0.0.0.1.0.0.1" expl="asserted formula" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1.7.0.0.0.1.0.1" expl="asserted formula" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1.7.0.0.0.1.1" expl="false case (postcondition)" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.1.7.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.25"/></proof>
+ </goal>
+ <goal name="inter'vc.61.1.7.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.60"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.07"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.61.2.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.71"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.25"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.58"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.61.2.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.03"/></proof>
+ </goal>
+ <goal name="inter'vc.61.2.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.63"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.172" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.62" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
- <goal name="inter'vc.173" expl="variant decrease" proved="true">
+ <goal name="inter'vc.63" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.174" expl="precondition" proved="true">
+ <goal name="inter'vc.64" expl="variant decrease" 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 name="inter'vc.65" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.176" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.66" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.177" expl="postcondition" proved="true">
+ <goal name="inter'vc.67" expl="variant decrease" 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 name="inter'vc.68" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.179" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.69" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.180" expl="postcondition" proved="true">
+ <goal name="inter'vc.70" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.181" expl="postcondition" proved="true">
+ <goal name="inter'vc.71" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.182" expl="postcondition" proved="true">
+ <goal name="inter'vc.72" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.183" expl="variant decrease" proved="true">
+ <goal name="inter'vc.73" 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">
+ <goal name="inter'vc.74" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.185" expl="precondition" proved="true">
+ <goal name="inter'vc.75" 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">
+ <goal name="inter'vc.76" expl="precondition" 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">
+ <goal name="inter'vc.77" expl="variant decrease" 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 name="inter'vc.78" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.191" expl="precondition" proved="true">
+ <goal name="inter'vc.79" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.192" expl="precondition" proved="true">
+ <goal name="inter'vc.80" 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 name="inter'vc.81" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.194" expl="postcondition" proved="true">
+ <goal name="inter'vc.82" expl="variant decrease" 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 name="inter'vc.83" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.197" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.84" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.198" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.85" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.199" expl="precondition" proved="true">
+ <goal name="inter'vc.86" 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 name="inter'vc.87" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.201" expl="postcondition" proved="true">
+ <goal name="inter'vc.88" expl="precondition" 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 name="inter'vc.89" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.203" expl="postcondition" proved="true">
+ <goal name="inter'vc.90" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.204" expl="variant decrease" proved="true">
+ <goal name="inter'vc.91" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.205" expl="precondition" proved="true">
+ <goal name="inter'vc.92" expl="variant decrease" 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 name="inter'vc.93" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.207" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.94" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.208" expl="postcondition" proved="true">
+ <goal name="inter'vc.95" expl="precondition" 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 name="inter'vc.96" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.210" expl="postcondition" proved="true">
+ <goal name="inter'vc.97" expl="precondition" 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 name="inter'vc.98" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.212" expl="precondition" proved="true">
+ <goal name="inter'vc.99" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.213" expl="variant decrease" proved="true">
+ <goal name="inter'vc.100" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.214" expl="precondition" proved="true">
+ <goal name="inter'vc.101" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.215" expl="precondition" proved="true">
+ <goal name="inter'vc.102" expl="variant decrease" 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">
+ <goal name="inter'vc.103" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.221" expl="precondition" proved="true">
+ <goal name="inter'vc.104" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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">
+ <goal name="inter'vc.105" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.225" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.106" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.226" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.107" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.227" expl="variant decrease" proved="true">
+ <goal name="inter'vc.108" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.228" expl="precondition" proved="true">
+ <goal name="inter'vc.109" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.229" expl="precondition" proved="true">
+ <goal name="inter'vc.110" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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">
+ <goal name="inter'vc.111" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.232" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.28"/></proof>
+ <goal name="inter'vc.112" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.233" expl="postcondition" proved="true">
+ <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.234" 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.235" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.115" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.236" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.116" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.237" expl="precondition" proved="true">
+ <goal name="inter'vc.117" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.238" expl="precondition" proved="true">
+ <goal name="inter'vc.118" 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 name="inter'vc.119" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.240" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <goal name="inter'vc.120" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.241" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <goal name="inter'vc.121" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.242" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.122" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.243" expl="postcondition" proved="true">
+ <goal name="inter'vc.123" expl="precondition" 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>
+ <goal name="inter'vc.124" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.244.0" expl="postcondition" proved="true">
+ <goal name="inter'vc.124.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.244.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.124.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.124.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.244.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.124.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.124.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.124.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.124.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.124.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
+ </goal>
+ <goal name="inter'vc.124.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.124.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.37"/></proof>
+ </goal>
+ <goal name="inter'vc.124.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.0.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.4.1" expl="postcondition" proved="true">
+ <transf name="case" proved="true" arg1="(x = x3)">
+ <goal name="inter'vc.125.0.4.1.0" expl="true case (postcondition)" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.4.1.1" expl="false case (postcondition)" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.0.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.4.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.21"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.0.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.0.6.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.6.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.6.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.56"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.6.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.63"/></proof>
+ </goal>
+ <goal name="inter'vc.125.0.6.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.0.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.63"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.1.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.37"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.40"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.42"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.1.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.36"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.1.6.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.43"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.6.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.36"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.6.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.36"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.6.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.34"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.6.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.34"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.1.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.1.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.29"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.7.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.27"/></proof>
+ </goal>
+ <goal name="inter'vc.125.1.7.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.64"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.47"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.125.2.6.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.94"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.6.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.36"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.6.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.36"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.6.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.34"/></proof>
+ </goal>
+ <goal name="inter'vc.125.2.6.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.38"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.125.2.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.25"/></proof>
+ </goal>
+ </transf>
</goal>
</transf>
</goal>
- <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 name="inter'vc.126" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
- <goal name="inter'vc.253" expl="precondition" proved="true">
+ <goal name="inter'vc.127" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.254" expl="precondition" proved="true">
+ <goal name="inter'vc.128" 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">
+ <goal name="inter'vc.129" expl="variant decrease" 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">
+ <goal name="inter'vc.130" 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">
+ <goal name="inter'vc.131" expl="precondition" 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.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">
+ <goal name="inter'vc.132" 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">
+ <goal name="inter'vc.133" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.268" expl="precondition" proved="true">
+ <goal name="inter'vc.134" 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">
+ <goal name="inter'vc.135" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.273" expl="variant decrease" proved="true">
+ <goal name="inter'vc.136" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.274" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.275" expl="precondition" proved="true">
+ <goal name="inter'vc.137" 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.277" expl="postcondition" proved="true">
+ <goal name="inter'vc.138" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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">
+ <goal name="inter'vc.139" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <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.281" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.282" expl="precondition" proved="true">
+ <goal name="inter'vc.140" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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.285" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="inter'vc.286" expl="postcondition" proved="true">
+ <goal name="inter'vc.141" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.287" expl="variant decrease" proved="true">
+ <goal name="inter'vc.142" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.288" expl="precondition" proved="true">
+ <goal name="inter'vc.143" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <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.291" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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">
+ <goal name="inter'vc.144" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.294" expl="variant decrease" proved="true">
+ <goal name="inter'vc.145" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.295" expl="precondition" proved="true">
+ <goal name="inter'vc.146" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.296" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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">
+ <goal name="inter'vc.147" expl="precondition" 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.301" expl="postcondition" proved="true">
+ <goal name="inter'vc.148" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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 name="inter'vc.149" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.304" expl="variant decrease" proved="true">
+ <goal name="inter'vc.150" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.305" expl="precondition" proved="true">
+ <goal name="inter'vc.151" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.306" expl="precondition" proved="true">
+ <goal name="inter'vc.152" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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">
+ <goal name="inter'vc.153" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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">
+ <goal name="inter'vc.154" expl="variant decrease" 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.314" expl="termination">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="inter'vc.315" expl="postcondition" proved="true">
+ <goal name="inter'vc.155" expl="precondition" 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">
+ <goal name="inter'vc.156" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.318" expl="variant decrease" proved="true">
+ <goal name="inter'vc.157" 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.320" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <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">
+ <goal name="inter'vc.158" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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">
+ <goal name="inter'vc.159" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.327" expl="precondition" proved="true">
+ <goal name="inter'vc.160" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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.330" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="inter'vc.331" expl="postcondition" proved="true">
+ <goal name="inter'vc.161" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.332" expl="variant decrease" proved="true">
+ <goal name="inter'vc.162" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.333" expl="precondition" proved="true">
+ <goal name="inter'vc.163" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.334" expl="precondition" proved="true">
+ <goal name="inter'vc.164" expl="variant decrease" 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">
+ <goal name="inter'vc.165" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.339" expl="variant decrease" proved="true">
+ <goal name="inter'vc.166" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.340" expl="precondition" proved="true">
+ <goal name="inter'vc.167" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.341" expl="precondition" proved="true">
+ <goal name="inter'vc.168" 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">
+ <goal name="inter'vc.169" expl="precondition" 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.346" expl="variant decrease" proved="true">
+ <goal name="inter'vc.170" 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">
+ <goal name="inter'vc.171" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.348" expl="precondition" proved="true">
+ <goal name="inter'vc.172" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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 name="inter'vc.173" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
- <goal name="inter'vc.351" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.174" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.0.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.44"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="inter'vc.174.0.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.45"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.45"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.1.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.97"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.36"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.35"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.4.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.94"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.1.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.1.6.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.10"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.6.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.96"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.6.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.1.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.1.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.58"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.7.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.35"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.7.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.35"/></proof>
+ </goal>
+ <goal name="inter'vc.174.1.7.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.35"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.52"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.2.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.57"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.34"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.38"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.4.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.35"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.2.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.2.6.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.58"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.6.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.6.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.75"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.174.2.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.174.2.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.90"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.7.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.35"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.7.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.34"/></proof>
+ </goal>
+ <goal name="inter'vc.174.2.7.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.94"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.352" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.175" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
- <goal name="inter'vc.353" expl="precondition" proved="true">
+ <goal name="inter'vc.176" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.354" expl="precondition" proved="true">
+ <goal name="inter'vc.177" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.355" expl="postcondition" proved="true">
+ <goal name="inter'vc.178" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.356" expl="precondition" proved="true">
+ <goal name="inter'vc.179" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.357" expl="precondition" proved="true">
+ <goal name="inter'vc.180" 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">
+ <goal name="inter'vc.181" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.360" expl="precondition" proved="true">
+ <goal name="inter'vc.182" 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">
+ <goal name="inter'vc.183" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.363" expl="precondition" proved="true">
+ <goal name="inter'vc.184" 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">
+ <goal name="inter'vc.185" 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">
+ <goal name="inter'vc.186" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.368" expl="precondition" proved="true">
+ <goal name="inter'vc.187" 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">
+ <goal name="inter'vc.188" 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">
+ <goal name="inter'vc.189" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.373" expl="precondition" proved="true">
+ <goal name="inter'vc.190" 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">
+ <goal name="inter'vc.191" 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 name="inter'vc.192" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.192.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.192.0.0" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.192.0.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
- <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 name="inter'vc.192.0.1" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.192.0.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.34"/></proof>
</goal>
</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 name="inter'vc.192.0.2" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.192.0.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.176.0.0" expl="postcondition">
- <proof prover="3"><undone/></proof>
+ <goal name="inter'vc.192.0.3" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x">
+ <goal name="inter'vc.192.0.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.37"/></proof>
+ </goal>
+ </transf>
</goal>
</transf>
</goal>
- <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>
+ <goal name="inter'vc.192.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.376.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
+ <goal name="inter'vc.192.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <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 name="inter'vc.192.1.1" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x1">
+ <goal name="inter'vc.192.1.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.87"/></proof>
</goal>
</transf>
</goal>
- <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 name="inter'vc.192.1.2" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x1">
+ <goal name="inter'vc.192.1.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.88"/></proof>
</goal>
</transf>
</goal>
- <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 name="inter'vc.192.1.3" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures1" arg2="x1">
+ <goal name="inter'vc.192.1.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.73"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.376.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <goal name="inter'vc.192.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.01"/></proof>
+ </goal>
+ <goal name="inter'vc.192.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.93"/></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>
--
GitLab