diff --git a/dolmen b/dolmen
index 6dd449152f9dc61e281b396fbd7aa3ebf6b0ea4d..57c66b6b6de28af0a7b9d0fe429bfacdca05f8d9 160000
--- a/dolmen
+++ b/dolmen
@@ -1 +1 @@
-Subproject commit 6dd449152f9dc61e281b396fbd7aa3ebf6b0ea4d
+Subproject commit 57c66b6b6de28af0a7b9d0fe429bfacdca05f8d9
diff --git a/src/bin/main.ml b/src/bin/main.ml
index 71a2d564492aa6d2957d5c72c940269db3d8f80f..d4f909723946a673a18f6c218200b5bb0898d28d 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -1,13 +1,13 @@
(* This file is free software, copied from dolmen. See file "LICENSE" for more information *)
-let handle_exn st exn =
+let handle_exn st _bt exn =
let _st = Errors.exn st exn in
exit 125
let finally st e =
match e with
| None -> st
- | Some exn -> handle_exn st exn
+ | Some (bt,exn) -> handle_exn st bt exn
let debug_pre_pipe st c =
if st.Loop.State.debug then
@@ -73,7 +73,9 @@ let () =
in
let st, g =
try Loop.Parser.parse [] st
- with exn -> handle_exn st exn
+ with exn ->
+ let bt = Printexc.get_raw_backtrace () in
+ handle_exn st bt exn
in
let st =
let open Loop.Pipeline in
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
index 5dcb50293cff7fcb80e4ca4798d0309312b49d2b..c4c384b08591bc028549d22c03a24ceda92b5767 100644
--- a/src_colibri2/bin/main.ml
+++ b/src_colibri2/bin/main.ml
@@ -46,7 +46,9 @@ let () =
| `Error `Parse | `Error `Term | `Error `Exn -> exit 2
| `Ok opt -> opt
in
- Colibri2_solver.Input.read ?limit:step_limit ~show_steps
- ~set_true:Colibri2_theories_bool.Boolean.set_true
- ~handle_exn:Colibri2_solver.Input.handle_exn_with_exit st ~check_status
- ~show_check_sat_result
+ try
+ Colibri2_solver.Input.read ?limit:step_limit ~show_steps
+ ~set_true:Colibri2_theories_bool.Boolean.set_true
+ ~handle_exn:Colibri2_solver.Input.handle_exn_with_exit st ~check_status
+ ~show_check_sat_result
+ with _exn -> Format.eprintf "here@."
diff --git a/src_colibri2/popop_lib/debug.ml b/src_colibri2/popop_lib/debug.ml
index 61ff438d466a846b4c9470ac86f843abf3f44c94..136674beb5291efa6cfbbfbd9b214a24f7e4d359 100644
--- a/src_colibri2/popop_lib/debug.ml
+++ b/src_colibri2/popop_lib/debug.ml
@@ -113,7 +113,7 @@ let real_dprintf ?nobox ?ct s =
if Option.is_some ct then
let b = Base.Backtrace.get ~at_most_num_frames:7 () in
let l = match (Base.Backtrace.to_string_list b) with
- | _::_::_::l -> l
+ | _::_::l -> l
| l -> l
in Fmt.(pf !formatter "@.%a" (vbox ~indent:1 (list ~sep:cut (box lines))) l)
)
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 12ade1adc93c3b114b8bcec44dad32e5d809faff..d3ed0f98a08990a1001f6f656f47935a00e75888 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -175,19 +175,21 @@ let print_exn st = function
| e ->
State.error st "@[<hv>Unhandled exception:@ %s@]" (Printexc.to_string e)
-let handle_exn_with_exit st exn =
- if st.State.debug then Format.eprintf "%s@." (Printexc.to_string exn);
+let handle_exn_with_exit st bt exn =
+ if st.State.debug then (
+ Printexc.print_raw_backtrace stderr bt;
+ Format.eprintf "%s@." (Printexc.to_string exn));
let () = print_exn st exn in
exit 2
-let handle_exn_with_error _ exn = raise exn
+let handle_exn_with_error _ bt exn = Printexc.raise_with_backtrace exn bt
let finally ~handle_exn st e =
match (st.State.solve_state.state, e) with
| `StepLimitReached, None -> raise Scheduler.ReachStepLimit
| _, None -> st
- | _, Some exn ->
- handle_exn st exn;
+ | _, Some (bt, exn) ->
+ handle_exn st bt exn;
assert false
let debug_pre_pipe st c =
@@ -370,7 +372,8 @@ let read ?show_check_sat_result ?show_steps ?limit ?check_status ~set_true
let st, g =
try Parser.parse [] st
with exn ->
- handle_exn st exn;
+ let bt = Printexc.get_raw_backtrace () in
+ handle_exn st bt exn;
assert false
in
let st =
diff --git a/src_colibri2/tests/solve/all/sat/dune.inc b/src_colibri2/tests/solve/all/sat/dune.inc
index aca73444f0d4e5534f76b17b6ead8815ff6700e6..4e0cd3e0bba21ec1769c54205e80729a14233335 100644
--- a/src_colibri2/tests/solve/all/sat/dune.inc
+++ b/src_colibri2/tests/solve/all/sat/dune.inc
@@ -4,3 +4,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat
--dont-print-result %{dep:div_abs2.smt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
diff --git a/src_colibri2/tests/solve/all/sat/union-Union-is_singletonqtvc_2.psmt2 b/src_colibri2/tests/solve/all/sat/union-Union-is_singletonqtvc_2.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..6ee8d7ada9f5043db5999639b83993bf5b13c754
--- /dev/null
+++ b/src_colibri2/tests/solve/all/sat/union-Union-is_singletonqtvc_2.psmt2
@@ -0,0 +1,10 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+
+(assert (>= 0.0 0.0))
+
+
+(check-sat)
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 43d61242135cc4bfdaf88344c3d912ba3083c383..857492e6d430d352e4e82554a51515d413431615 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -17,5 +17,8 @@
--dont-print-result %{dep:mul_abs.smt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_abs.smt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_1.psmt2 b/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_1.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..1a5337dd9031e64d714535fbafc36a2c602b36b9
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_1.psmt2
@@ -0,0 +1,89 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+(declare-fun prime_to_one_another (Int Int) Bool)
+
+(declare-sort t 0)
+
+(declare-fun num (t) Int)
+
+(declare-fun den (t) Int)
+
+;; t'invariant
+ (assert
+ (forall ((self t))
+ (! (and (< 0 (den self)) (prime_to_one_another (num self) (den self))) :pattern (
+ (den self)) :pattern ((num self)) )))
+
+
+(define-fun real ((q t)) Real (/ (to_real (num q)) (to_real (den q))))
+
+(declare-fun make (Int Int) t)
+
+;; make_def
+ (assert
+ (forall ((num1 Int) (den1 Int))
+ (=> (not (= den1 0))
+ (= (real (make num1 den1)) (/ (to_real num1) (to_real den1))))))
+
+(declare-datatypes ((t2 0))
+(((Strict) (Large))))
+(declare-datatypes ((t0 0))
+(((Singleton (Singleton_proj_1 t)(Singleton_proj_2 t0))
+ (Inter
+ (Inter_proj_1 t)(Inter_proj_2 t2)(Inter_proj_3 t)(Inter_proj_4 t2)(Inter_proj_5 t0))
+ (FiniteInf (FiniteInf_proj_1 t)(FiniteInf_proj_2 t2)) (End))))
+(declare-datatypes ((t3 0))
+(((InfFinite (InfFinite_proj_1 t)(InfFinite_proj_2 t2)(InfFinite_proj_3 t0))
+ (Finite (Finite_proj_1 t0)) (Inf))))
+(declare-fun length0 (t0) Int)
+
+;; length0'def
+ (assert
+ (forall ((l t0))
+ (ite ((_ is Singleton) l) (let (
+ (x (Singleton_proj_2 l))) (= (length0 l) (+
+ (length0 x) 1))) (ite ((_ is Inter) l) (let (
+ (x1 (Inter_proj_5 l))) (=
+ (length0
+ l) (+
+ (length0
+ x1) 2)))
+ (ite ((_ is FiniteInf) l) (=
+ (length0 l) 1) (= (length0 l) 0))))))
+
+;; length0_positive
+ (assert (forall ((l t0)) (>= (length0 l) 0)))
+
+(define-fun length ((l t3)) Int (ite ((_ is InfFinite) l) (let (
+ (x8 (InfFinite_proj_3 l))) (+
+ (length0 x8) 1))
+ (ite ((_ is Finite) l) (let ((x9 (Finite_proj_1 l)))
+ (length0 x9)) 0)))
+
+(declare-sort tqt 0)
+
+(declare-fun a12 (tqt) t3)
+
+(declare-fun u () tqt)
+
+(declare-fun x28 () t)
+
+(declare-fun x29 () t2)
+
+(declare-fun x30 () t)
+
+(declare-fun x31 () t2)
+
+(declare-fun x32 () t0)
+
+;; H
+ (assert (= (a12 u) (Finite (Inter x28 x29 x30 x31 x32))))
+
+(assert
+;; is_singletonqtvc
+ ;; File "colibrics/src_common/union.mlw", assert in is singleton Finite Inter case
+ (not (>= (length (a12 u)) 2)))
+(check-sat)
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 60cbf361ba62c7852ee914f5eb11687dcbf1dcc9..fc74437694abef8d76ba755998606eecbc69df50 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -214,8 +214,8 @@ let converter d (f : Ground.t) =
cmp
(function
| Uncomparable | Le -> None
- | Eq | Lt -> Some false
- | Ge | Gt -> Some true)
+ | Lt -> Some false
+ | Eq | Ge | Gt -> Some true)
`Ge a b
| { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index ff7d8c648b2490e41edecd3177642249a2e764e1..5a9a95d3f6ad0676e3f4ac1771007e4883932c64 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -345,3 +345,9 @@ let init env =
Ground.register_converter env converter;
init_ty env;
Check.init env
+
+let () =
+ Colibri2_theories_quantifiers.Trigger.register_builtin_skipped_for_trigger
+ (function
+ | Expr.Leq | Expr.Geq | Expr.Lt | Expr.Gt -> true
+ | _ -> false)
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index a160ee26863b61d7141519e475b1fb7442bd7eab..d36a61b665743f0d9ca689b985038be536d8cbdf 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -41,6 +41,11 @@ end
include T
include Popop_stdlib.MkDatatype (T)
+let register_builtin_skipped_for_trigger, builtin_skipped_for_trigger =
+ let q = Base.Queue.create () in
+ ( Base.Queue.enqueue q,
+ fun builtin -> Base.Queue.exists q ~f:(fun p -> p builtin) )
+
let compute_top_triggers (cq : Ground.ClosedQuantifier.t) =
let cq' = Ground.ClosedQuantifier.sem cq in
let tyvs = cq'.ty_vars in
@@ -65,6 +70,9 @@ let compute_top_triggers (cq : Ground.ClosedQuantifier.t) =
_,
tl ) ->
List.fold_left aux pats tl
+ | Expr.App ({ term_descr = Cst { builtin; _ }; _ }, _, tl)
+ when builtin_skipped_for_trigger builtin ->
+ List.fold_left aux pats tl
| _ -> t :: pats
in
let pats = CCList.sort_uniq ~cmp:Expr.Term.compare (aux [] t) in
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index e0f388774b8ba321a6f11e5196d15d0b553e4380..990e197025200839e379becb2926cbb3356d0c11 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -64,3 +64,7 @@ val instantiate : Egraph.wt -> t -> Ground.Subst.t -> unit
val match_ : Egraph.wt -> t -> Node.t -> unit
(** [match_ d tri n] match the pattern of [tri] with [n] and instantiate [tri]
with the resulting substitutions *)
+
+val register_builtin_skipped_for_trigger : (Expr.builtin -> bool) -> unit
+(** The registered function tells when an application should be skipped when
+ looking for patterns in a term (top down) *)
diff --git a/src_common/union.mlw b/src_common/union.mlw
index c3ac49fb131bfd15d64c8a83f295fd8fdeb23f53..1a023d3f9cbc816eb87a47f8d0caa2f619f6ce91 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -137,10 +137,17 @@ module Union
| Finite (Singleton q End) -> (Some q,0., 1.)
| Finite End -> absurd
| Finite (Inter q b q' b' _) ->
+ assert { length u.a >= 2 };
+ assert { nth 0 u.a = q };
+ assert { nth 1 u.a = q' };
+ assert { (Q.real q) <. (Q.real q') };
(None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
| Finite (FiniteInf q _) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
- | Finite (Singleton q (Singleton q' _)) -> (None,ghost (Q.real q), ghost (Q.real q'))
+ | Finite (Singleton q (Singleton q' _)) ->
+ assert { (Q.real q) <. (Q.real q') };
+ (None,ghost (Q.real q), ghost (Q.real q'))
| Finite (Singleton _ (Inter q b q' b' _)) ->
+ assert { (Q.real q) <. (Q.real q') };
(None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
| Finite (Singleton _ (FiniteInf q _)) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
end
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index dc269199b6f0a4a57e3d567552a063f1940e07b6..bead75ff46fa09799b93f9caa03223cc37813917 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -23,103 +23,120 @@
<proof prover="3"><result status="valid" time="2.82"/></proof>
</goal>
<goal name="is_singleton'vc" expl="VC for is_singleton">
- <proof prover="3"><result status="highfailure" time="0.02"/></proof>
+ <proof prover="3" obsolete="true"><result status="highfailure" time="0.02"/></proof>
<transf name="split_vc" >
- <goal name="is_singleton'vc.0" expl="unreachable point" proved="true">
+ <goal name="is_singleton'vc.0" expl="assertion">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.1" expl="assertion">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.2" expl="unreachable point" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="is_singleton'vc.1" expl="postcondition">
- <proof prover="3"><result status="highfailure" time="0.05"/></proof>
+ <goal name="is_singleton'vc.3" expl="assertion">
+ </goal>
+ <goal name="is_singleton'vc.4" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.5" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.6" expl="assertion">
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.7" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="highfailure" time="0.05"/></proof>
<transf name="split_vc" >
- <goal name="is_singleton'vc.1.0" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.57"/></proof>
</goal>
- <goal name="is_singleton'vc.1.1" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="is_singleton'vc.1.2.0" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.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="is_singleton'vc.7.2.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.1" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.2.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.2" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.2.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.3" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.7.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.7.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.5" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.2.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.7.2.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="is_singleton'vc.1.2.7" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.2.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
- <goal name="is_singleton'vc.1.3" expl="postcondition">
- <proof prover="3"><result status="unknown" time="0.01"/></proof>
+ <goal name="is_singleton'vc.7.3" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="unknown" time="0.01"/></proof>
<transf name="split_vc" >
- <goal name="is_singleton'vc.1.3.0" expl="postcondition">
+ <goal name="is_singleton'vc.7.3.0" expl="postcondition">
<proof prover="3"><result status="unknown" time="0.04"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.1" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.3.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.2" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.3.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.3" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.3.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.4" expl="postcondition">
+ <goal name="is_singleton'vc.7.3.4" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.5" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.3.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.60"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.7.3.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="is_singleton'vc.1.3.7" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.3.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
- <goal name="is_singleton'vc.1.4" expl="postcondition">
- <proof prover="3"><result status="unknown" time="0.01"/></proof>
+ <goal name="is_singleton'vc.7.4" expl="postcondition">
+ <proof prover="3" obsolete="true"><result status="unknown" time="0.01"/></proof>
<transf name="split_vc" >
- <goal name="is_singleton'vc.1.4.0" expl="postcondition">
+ <goal name="is_singleton'vc.7.4.0" expl="postcondition">
<proof prover="3"><result status="unknown" time="0.04"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.1" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.4.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.2" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.4.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.3" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.4.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.62"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.4" expl="postcondition">
+ <goal name="is_singleton'vc.7.4.4" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.5" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.4.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.67"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.7.4.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="is_singleton'vc.1.4.7" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.7.4.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</transf>