diff --git a/colibri2/core/egraph.ml b/colibri2/core/egraph.ml
index f13c98f25959fb3df42c66462f2e32d4e5f3f2a0..971590e17ef86b0155cf01c895dd3e070db594b7 100644
--- a/colibri2/core/egraph.ml
+++ b/colibri2/core/egraph.ml
@@ -618,7 +618,8 @@ module Delayed = struct
       (** node' is already registered *)
       else if Node.equal node (find t node0') then
         (** if node is the representant of node' then we have nothing to do *)
-        ()
+        Debug.dprintf0 debug_few
+          "[Egraph] @[    already equal@]"
       else
         (** merge node and node0' *)
         add_pending_merge t node0 node0'
diff --git a/colibri2/core/structures/nodes.ml b/colibri2/core/structures/nodes.ml
index 7ce6396cd7439556ddc0cabb27c364f06d2d4b50..a879c4d6fba9670a44db72d7af64dc268ac5e074 100644
--- a/colibri2/core/structures/nodes.ml
+++ b/colibri2/core/structures/nodes.ml
@@ -51,9 +51,7 @@ module Node = struct
   let used_names : (* next id to use *) int DStr.H.t = DStr.H.create 100
 
   (** remove the empty string *)
-  let () = DStr.H.add used_names "" 0
-
-  (* let () = DStr.H.add used_names "281" 0 *)
+  let () = List.iter (fun x -> DStr.H.add used_names x 0) [ "" ]
 
   let pp fmt x =
     Format.pp_print_char fmt '@';
diff --git a/colibri2/theories/ADT/adt_value.ml b/colibri2/theories/ADT/adt_value.ml
index 3115d5068014b2fe067b17b4171e9a79c2c43acb..77df372a243d561c6ce4456751b62be703032fcd 100644
--- a/colibri2/theories/ADT/adt_value.ml
+++ b/colibri2/theories/ADT/adt_value.ml
@@ -72,6 +72,11 @@ end
 let cases_of_adt adt =
   Case.S.of_list (List.init (IArray.length adt.MonoAdt.cases) ~f:(fun i -> i))
 
+let definition { MonoAdt.mono = { app = adt; _ }; _ } =
+  match Ground.Ty.definition adt with
+  | Abstract -> assert false
+  | Adt { cases; _ } -> cases
+
 let _ = MonoAdt.show
 
 type ts = { adt : MonoAdt.t; case : Case.t; fields : Value.t Field.M.t }
@@ -201,4 +206,12 @@ let init_ty d =
 
 let th_register d =
   init_check d;
-  init_ty d
+  init_ty d;
+  let pp d fmt c =
+    let c = value c in
+    let case = (definition c.adt).(c.case) in
+    Fmt.pf fmt "%a(%a)" Expr.Term.Const.pp case.cstr
+      Fmt.(list ~sep:comma (Interp.print_value_smt d))
+      (Field.M.values c.fields)
+  in
+  Interp.Register.print_value_smt key pp
diff --git a/colibri2/theories/bool/boolean.ml b/colibri2/theories/bool/boolean.ml
index 3afcb5a4622252de7ea8feb1ee9a0f653693a8fa..d522c3306ab6f72477703dacf2f0fa892cf43966 100644
--- a/colibri2/theories/bool/boolean.ml
+++ b/colibri2/theories/bool/boolean.ml
@@ -357,6 +357,8 @@ let th_register env =
   Ground.register_converter env converter;
   init_check env;
   init_ty env;
+  let pp _ fmt c = BoolValue.SD.pp fmt (BoolValue.value c) in
+  Interp.Register.print_value_smt dom pp;
   ()
 
 let () = Init.add_default_theory th_register
diff --git a/colibri2/theories/quantifier/quantifier.ml b/colibri2/theories/quantifier/quantifier.ml
index 3562b37124178cb1620523785045ca1c543074a1..95ce97533573b9c87a0a851c21bb5fe1fd677e90 100644
--- a/colibri2/theories/quantifier/quantifier.ml
+++ b/colibri2/theories/quantifier/quantifier.ml
@@ -368,11 +368,7 @@ let attach d th =
           in
           Debug.dprintf4 debug "[Quant] For %a adds %a"
             Ground.ClosedQuantifier.pp th
-            Fmt.(
-              list ~sep:semi
-                (Fmt.using
-                   (fun t -> t.Trigger.pats)
-                   (list ~sep:comma Pattern.pp)))
+            Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp))
             triggers;
           List.iter (InvertedPath.add_trigger d) triggers
       (* Todo match with current terms *))
diff --git a/colibri2/theories/quantifier/uninterp.ml b/colibri2/theories/quantifier/uninterp.ml
index 2e6b6b9a88d7287d0bca1ba178081ba58b35352e..5d04a3db83dacecbbf8e71a5bf7617aa0aeb5d7a 100644
--- a/colibri2/theories/quantifier/uninterp.ml
+++ b/colibri2/theories/quantifier/uninterp.ml
@@ -388,6 +388,8 @@ let th_register env =
       | { app = { builtin = Expr.Base; _ }; args; _ }
         when IArray.length args >= 1 ->
           On_uninterpreted_domain.compute d t
-      | _ -> NA)
+      | _ -> NA);
+  let pp _ fmt c = USModel.US.SD.pp fmt (USModel.US.value c) in
+  Interp.Register.print_value_smt USModel.US.key pp
 
 let () = Init.add_default_theory th_register
diff --git a/common/float_interval.mlw b/common/float_interval.mlw
index 962cdbcd623e2d02677113b3ab8d3a78a239f1af..3bc0db45e7c80ed041f6b6201522a0ee23ef606c 100644
--- a/common/float_interval.mlw
+++ b/common/float_interval.mlw
@@ -37,13 +37,21 @@ module GenericFloat
   constant max_real : real (* defined when cloning *)
 
   predicate in_range (x:real) = -. max_real <=. x <=. max_real
+
+  predicate is_float (x:real)
+  function round mode real : real
+  
+  axiom round_to_float: forall r m. is_float (round m r)
+  axiom round_float: forall r m. is_float r -> round m r = r
   
   axiom max_real_not_zero: max_real <> 0.
+  axiom max_real_round: is_float max_real
 
   type finite = abstract {
     r : real
   }
   invariant { in_range r }
+  invariant { is_float r }
   invariant { r <> 0. }
   by { r = max_real }
 
@@ -75,8 +83,6 @@ module GenericFloat
 
   (** {3 Operators} *)
 
-  val function sub mode t t : t
-  val function mul mode t t : t
   val function div mode t t : t
     (** The four basic operations, rounded in the given mode *)
 
@@ -98,8 +104,6 @@ module GenericFloat
   val function sqrt mode   t   : t   (** Square root *)
 
   let function (.-_) (x:t)   : t = neg x
-  let function (.-)  (x y:t) : t = sub RNE x y
-  let function (.*)  (x y:t) : t = mul RNE x y
   let function (./)  (x y:t) : t = div RNE x y
     (** Notations for operations in the default mode RNE *)
 
@@ -137,16 +141,9 @@ module GenericFloat
      match f with
      | NaN -> false
      | Zero neg -> notb neg
-     | Finite r -> 0. <=. r
+     | Finite r -> 0. <=. r (* r <> 0 in any case *)
      | Infinity neg -> notb neg
      end
-  predicate is_negative (f:t) =
-     match f with
-     | NaN -> false
-     | Zero neg -> neg
-     | Finite r -> r <=. 0.
-     | Infinity neg -> neg
-     end
 
   type classify =
    | Is_normal
@@ -238,12 +235,6 @@ module GenericFloat
   let predicate is_minus_infinity (x:t) = match x with Infinity neg -> neg | _ -> false end
   predicate is_plus_zero      (x:t) = match x with Zero neg -> notb neg | _ -> false end
   predicate is_minus_zero     (x:t) = match x with Zero neg -> neg | _ -> false end
-  predicate is_not_nan        (x:t) = match x with NaN -> false | _ -> true end
-
-  axiom is_not_nan: forall x:t. is_not_nan x <-> not (is_nan x)
-
-  axiom is_not_finite: forall x:t.
-    not (is_finite x) <-> (is_infinite x \/ is_nan x)
 
   (** {3 Conversions from other sorts} *)
 
@@ -309,7 +300,6 @@ module GenericFloat
   (*                                                                       *)
   (* Note that this means round (+INF) > 0 is not true.                    *)
   (* Note also this means round (2*INF) > round (INF) is not true either.  *)
-  function round mode real : real
 
   constant max_int  : int
 
@@ -323,10 +313,10 @@ module GenericFloat
 
   predicate in_int_range (i:int) = - max_int <= i <= max_int
 
-  axiom max_real_round : forall m. round m max_real = max_real
-
   axiom minus_max_real_round : forall m. round m (-. max_real) = -. max_real
 
+  axiom zero_round : forall m. round m 0. = 0.
+
   goal is_finite: forall x:t. is_finite x <-> in_range (to_real x)
 
   (* used as a condition to propagate is_finite *)
@@ -356,6 +346,9 @@ module GenericFloat
   axiom Round_up_neg:
     forall x:real. round RTP (-.x) = -. round RTN x
 
+  lemma round_sign:
+    forall m:mode, x:real[round m x,sign x]. round m x <> 0. -> sign (round m x) = sign x
+
   (* The biggest representable integer whose predecessor (i.e. -1) is  representable *)
   constant pow2sb : int (* defined when cloning *)
   axiom pow2sb: pow2sb = pow2 sb
@@ -375,9 +368,7 @@ module GenericFloat
   (** Comparison predicates *)
 
   predicate same_sign (x y : t) =
-    (is_positive x /\ is_positive y) \/ (is_negative x /\ is_negative y)
-  predicate diff_sign (x y : t) =
-    (is_positive x /\ is_negative y) \/ (is_negative x /\ is_positive y)
+    (is_positive x = is_positive y)
 
   goal feq_eq: forall x y.
     is_finite x -> is_finite y -> not (is_zero x) -> x .= y -> x = y
@@ -399,7 +390,7 @@ module GenericFloat
     is_finite x /\ is_finite y -> (x .= y <-> to_real x = to_real y)
 
   goal eq_special: forall x y. x .= y ->
-       (is_not_nan x  /\ is_not_nan y
+       (not (is_nan x)  /\ not (is_nan y)
     /\ ((is_finite x /\ is_finite y)
         \/ (is_infinite x /\ is_infinite y /\ same_sign x y)))
 
@@ -409,6 +400,9 @@ module GenericFloat
   goal le_finite: forall x y [le x y].
     is_finite x /\ is_finite y -> (le x y <-> to_real x <=. to_real y)
 
+  lemma le_trans:
+    forall x y z:t. le x y /\ le y z -> le x z
+
   goal le_lt_trans:
     forall x y z:t. x .<= y /\ y .< z -> x .< z
 
@@ -419,46 +413,41 @@ module GenericFloat
     forall x y:t. x .<= y /\ x .>= y -> x .= y
 
   goal not_lt_ge: forall x y:t.
-    not (x .< y) /\ is_not_nan x /\ is_not_nan y -> x .>= y
+    not (x .< y) /\ not (is_nan x) /\ (is_nan y) -> x .>= y
 
   goal not_gt_le: forall x y:t.
-    not (x .> y) /\ is_not_nan x /\ is_not_nan y -> x .<= y
+    not (x .> y) /\ not (is_nan x) /\ not (is_nan y) -> x .<= y
 
   goal le_special: forall x y [le x y]. le x y ->
       ((is_finite x /\ is_finite y)
-   \/ ((is_minus_infinity x /\ is_not_nan y)
-   \/  (is_not_nan x /\ is_plus_infinity y)))
+   \/ ((is_minus_infinity x /\ not (is_nan y))
+   \/  (not (is_nan x) /\ is_plus_infinity y)))
 
   goal lt_special: forall x y [lt x y]. lt x y ->
       ((is_finite x /\ is_finite y)
-   \/ ((is_minus_infinity x /\ is_not_nan y /\ not (is_minus_infinity y))
-   \/  (is_not_nan x /\ not (is_plus_infinity x) /\ is_plus_infinity y)))
+   \/ ((is_minus_infinity x /\ not (is_nan y) /\ not (is_minus_infinity y))
+   \/  (not (is_nan x) /\ not (is_plus_infinity x) /\ is_plus_infinity y)))
 
   goal lt_lt_finite: forall x y z. lt x y -> lt y z -> is_finite y
 
   (*  lemmas on sign *)
-  axiom positive_to_real: forall x[is_positive x|to_real x >=. 0.0].
+  goal positive_to_real: forall x[is_positive x|to_real x >=. 0.0].
     is_finite x -> is_positive x -> to_real x >=. 0.0
-  axiom to_real_positive: forall x[is_positive x].
+  goal to_real_positive: forall x[is_positive x].
     is_finite x -> to_real x >. 0.0 -> is_positive x
 
-  axiom negative_to_real: forall x [is_negative x|to_real x <=. 0.0].
-    is_finite x -> is_negative x -> to_real x <=. 0.0
-  axiom to_real_negative: forall x [is_negative x].
-    is_finite x -> to_real x <. 0.0 -> is_negative x
-
-  axiom negative_xor_positive: forall x.
-    not (is_positive x /\ is_negative x)
-  axiom negative_or_positive: forall x.
-    is_not_nan x -> is_positive x \/ is_negative x
+  goal negative_to_real: forall x [is_positive x|to_real x <=. 0.0].
+    is_finite x -> not (is_positive x) -> to_real x <=. 0.0
+  goal to_real_negative: forall x [is_positive x].
+    is_finite x -> to_real x <. 0.0 -> not (is_positive x)
 
   goal diff_sign_trans:
-    forall x y z:t. (diff_sign x y /\ diff_sign y z) -> same_sign x z
+    forall x y z:t. (not (same_sign x y) /\ (not (same_sign y z))) -> same_sign x z
 
   goal diff_sign_product:
     forall x y:t.
       (is_finite x /\ is_finite y /\ to_real x *. to_real y <. 0.0) ->
-        diff_sign x y
+        (not (same_sign x y))
 
   goal same_sign_product:
     forall x y:t.
@@ -466,7 +455,7 @@ module GenericFloat
         to_real x *. to_real y >=. 0.0
 
   predicate product_sign (z x y: t) =
-    (same_sign x y -> is_positive z) /\ (diff_sign x y -> is_negative z)
+    (same_sign x y <-> is_positive z)
 
   (** {3 Overflow} *)
 
@@ -487,18 +476,10 @@ module GenericFloat
   (* This predicate is used to tell what is the sign of zero in the
      axioms specifying add and sub *)
   predicate sign_zero_result (m:mode) (x:t) =
-    is_zero x ->
-    match m with
-    | RTN -> is_negative x
-    | _   -> is_positive x
-    end
+    is_zero x -> ((m <> RTN) <-> (is_positive x))
 
   (** {3 binary operations} *)
-  let function is_RTN mode =
-     match mode with
-     | RTN -> true
-     | _ -> false
-     end
+  function is_RTN (mode:mode) : bool = mode = RTN
 
   function add (mode:mode) (x:t) (y:t) : t =
     match x, y with
@@ -512,7 +493,7 @@ module GenericFloat
     | _, Infinity _ -> y
     | Finite x, Finite y ->
        let r = (round mode (x +. y)) in
-       if r = 0. then Zero (is_RTN mode)
+       if r = 0. then (* x +. y must be 0 *) Zero (is_RTN mode)
        else if in_range r then
          Finite (mk_finite r)
        else
@@ -547,7 +528,15 @@ module GenericFloat
     no_overflow m (to_real x +. to_real y) /\
     to_real (add m x y) = round m (to_real x +. to_real y)
 
-  axiom sub_finite: forall m:mode, x y:t [sub m x y].
+  function sub (mode:mode) (x:t) (y:t) : t = add mode x (neg y)
+
+  val sub (mode:mode) (x y:t) : t
+    ensures { result = sub mode x y }
+
+  let function (.-)  (x y:t) : t = sub RNE x y
+
+
+  goal sub_finite: forall m:mode, x y:t [sub m x y].
     is_finite x -> is_finite y -> no_overflow m (to_real x -. to_real y) ->
     is_finite (sub m x y) /\
     to_real (sub m x y) = round m (to_real x -. to_real y)
@@ -562,7 +551,41 @@ module GenericFloat
     no_overflow m (to_real x -. to_real y) /\
     to_real (sub m x y) = round m (to_real x -. to_real y)
 
-  axiom mul_finite: forall m:mode, x y:t [mul m x y].
+  function mul (mode:mode) (x:t) (y:t) : t =
+    match x, y with
+    | NaN, _ -> NaN
+    | _, NaN -> NaN
+    | Zero z1, Zero z2 -> Zero (z1 <> z2)
+    | Zero _, Infinity _ -> NaN
+    | Infinity _, Zero _ -> NaN
+    | Zero b, _ -> if is_positive y then x else Zero (notb b)
+    | _, Zero b -> if is_positive x then y else Zero (notb b)
+    | Infinity z1, Infinity z2 -> Infinity (z1 <> z2)
+    | Infinity b, _ -> if is_positive y then x else Infinity (notb b)
+    | _, Infinity b -> if is_positive x then y else Infinity (notb b)
+    | Finite x, Finite y ->
+       let r = (round mode (x *. y)) in
+       if r = 0. then Zero (sign (x *. y))
+       else if in_range r then
+         Finite (mk_finite r)
+       else
+       match mode with
+        | RTN -> if sign r then Infinity true
+                           else Finite (mk_finite max_real)
+        | RTP -> if sign r then Finite (mk_finite (-. max_real))
+                           else Infinity false
+        | RTZ -> if sign r then Finite (mk_finite (-. max_real))
+                           else Finite (mk_finite max_real)
+        | (RNA | RNE) -> Infinity (sign r)
+      end
+    end
+
+  val mul (mode:mode) (x y:t) : t
+    ensures { result = mul mode x y }
+
+  let function (.*)  (x y:t) : t = mul RNE x y
+
+  goal mul_finite: forall m:mode, x y:t [mul m x y].
     is_finite x -> is_finite y -> no_overflow m (to_real x *. to_real y) ->
     is_finite (mul m x y) /\
     to_real (mul m x y) = round m (to_real x *. to_real y)
@@ -577,7 +600,7 @@ module GenericFloat
     no_overflow m (to_real x *. to_real y) /\
     to_real (mul m x y) = round m (to_real x *. to_real y)
 
-  axiom div_finite: forall m:mode, x y:t [div m x y].
+  goal div_finite: forall m:mode, x y:t [div m x y].
     is_finite x -> is_finite y ->
     not is_zero y -> no_overflow m (to_real x /. to_real y) ->
     is_finite (div m x y) /\
@@ -594,7 +617,7 @@ module GenericFloat
     no_overflow m (to_real x /. to_real y) /\
     to_real (div m x y) = round m (to_real x /. to_real y)
 
-  axiom neg_finite: forall x:t [neg x].
+  goal neg_finite: forall x:t [neg x].
     is_finite x ->
     is_finite (neg x) /\
     to_real (neg x) = -. to_real x
@@ -615,9 +638,9 @@ module GenericFloat
     is_finite x /\
     to_real (abs x) = Abs.abs (to_real x)
 
-  axiom abs_universal : forall x:t [abs x]. not (is_negative (abs x))
+  goal abs_universal : forall x:t [abs x]. is_positive (abs x)
 
-  axiom fma_finite: forall m:mode, x y z:t [fma m x y z].
+  goal fma_finite: forall m:mode, x y z:t [fma m x y z].
     is_finite x -> is_finite y -> is_finite z ->
     no_overflow m (to_real x *. to_real y +. to_real z) ->
     is_finite (fma m x y z) /\
@@ -635,7 +658,7 @@ module GenericFloat
 
   use real.Square as S
 
-  axiom sqrt_finite: forall m:mode, x:t [sqrt m x].
+  goal sqrt_finite: forall m:mode, x:t [sqrt m x].
     is_finite x -> to_real x >=. 0. ->
     is_finite (sqrt m x) /\
     to_real (sqrt m x) = round m (S.sqrt (to_real x))
@@ -646,9 +669,9 @@ module GenericFloat
     to_real (sqrt m x) = round m (S.sqrt (to_real x))
 
   predicate same_sign_real (x:t) (r:real) =
-    (is_positive x /\ r >. 0.0) \/ (is_negative x /\ r <. 0.0)
+    (is_positive x /\ r >. 0.0) \/ ((not (is_positive x)) /\ r <. 0.0)
 
-  axiom same_sign_real_round: forall x m r[same_sign_real x (round m r)]. same_sign_real x (round m r) -> same_sign_real x r
+  (* axiom same_sign_real_round: forall x m r[same_sign_real x (round m r)]. same_sign_real x (round m r) -> same_sign_real x r *)
 
   goal add_special: forall m:mode, x y:t [add m x y].
     let r = add m x y in
@@ -661,7 +684,7 @@ module GenericFloat
     (is_infinite x /\ is_infinite y /\ same_sign x y
       -> is_infinite r /\ same_sign r x)
     /\
-    (is_infinite x /\ is_infinite y /\ diff_sign x y -> is_nan r)
+    (is_infinite x /\ is_infinite y /\ (not (same_sign x y)) -> is_nan r)
     /\
     (is_finite x /\ is_finite y /\ not no_overflow m (to_real x +. to_real y)
       -> same_sign_real r (round m (to_real x +. to_real y)) /\ overflow_value m r)
@@ -669,26 +692,26 @@ module GenericFloat
     (is_finite x /\ is_finite y
       -> if same_sign x y then same_sign r x else sign_zero_result m r)
 
-  axiom sub_special: forall m:mode, x y:t [sub m x y].
+  goal sub_special: forall m:mode, x y:t [sub m x y].
     let r = sub m x y in
     (is_nan x \/ is_nan y -> is_nan r)
     /\
-    (is_finite x /\ is_infinite y -> is_infinite r /\ diff_sign r y)
+    (is_finite x /\ is_infinite y -> is_infinite r /\ (not (same_sign r y)))
     /\
     (is_infinite x /\ is_finite y -> is_infinite r /\ same_sign r x)
     /\
     (is_infinite x /\ is_infinite y /\ same_sign x y -> is_nan r)
     /\
-    (is_infinite x /\ is_infinite y /\ diff_sign x y
+    (is_infinite x /\ is_infinite y /\ (not (same_sign x y))
       -> is_infinite r /\ same_sign r x)
     /\
     (is_finite x /\ is_finite y /\ not no_overflow m (to_real x -. to_real y)
       -> same_sign_real r (to_real x -. to_real y) /\ overflow_value m r)
     /\
     (is_finite x /\ is_finite y
-      -> if diff_sign x y then same_sign r x else sign_zero_result m r)
+      -> if same_sign x y then  sign_zero_result m r else same_sign r x)
 
-  axiom mul_special: forall m:mode, x y:t [mul m x y].
+  goal mul_special: forall m:mode, x y:t [mul m x y].
     let r = mul m x y in
        (is_nan x \/ is_nan y -> is_nan r)
     /\ (is_zero x /\ is_infinite y -> is_nan r)
@@ -702,7 +725,7 @@ module GenericFloat
          -> overflow_value m r)
     /\ (not is_nan r -> product_sign r x y)
 
-  axiom div_special: forall m:mode, x y:t [div m x y].
+  goal div_special: forall m:mode, x y:t [div m x y].
     let r = div m x y in
        (is_nan x \/ is_nan y -> is_nan r)
     /\ (is_finite x /\ is_infinite y -> is_zero r)
@@ -716,17 +739,17 @@ module GenericFloat
     /\ (is_zero x /\ is_zero y -> is_nan r)
     /\ (not is_nan r -> product_sign r x y)
 
-  axiom neg_special: forall x:t [neg x].
+  goal neg_special: forall x:t [neg x].
        (is_nan x -> is_nan (neg x))
     /\ (is_infinite x -> is_infinite (neg x))
-    /\ (not is_nan x -> diff_sign x (neg x))
+    /\ (not is_nan x -> (not (same_sign x (neg x))))
 
-  axiom abs_special: forall x:t [abs x].
+  goal abs_special: forall x:t [abs x].
        (is_nan x -> is_nan (abs x))
     /\ (is_infinite x -> is_infinite (abs x))
     /\ (not is_nan x -> is_positive (abs x))
 
-  axiom fma_special: forall m:mode, x y z:t [fma m x y z].
+  goal fma_special: forall m:mode, x y z:t [fma m x y z].
     let r = fma m x y z in
        (is_nan x \/ is_nan y \/ is_nan z -> is_nan r)
     /\ (is_zero x /\ is_infinite y -> is_nan r)
@@ -755,9 +778,9 @@ module GenericFloat
     /\ (is_finite x /\ is_finite y /\ is_finite z
         -> if product_sign z x y then same_sign r z
            else (to_real x *. to_real y +. to_real z = 0.0 ->
-                 if m = RTN then is_negative r else is_positive r))
+                 if m = RTN then not (is_positive r) else is_positive r))
 
-  axiom sqrt_special: forall m:mode, x:t [sqrt m x].
+  goal sqrt_special: forall m:mode, x:t [sqrt m x].
     let r = sqrt m x in
        (is_nan x -> is_nan r)
     /\ (is_plus_infinity x -> is_plus_infinity r)
@@ -768,15 +791,15 @@ module GenericFloat
 
   (* exact arithmetic with integers *)
 
-  axiom of_int_add_exact: forall m n, i j.
+  goal of_int_add_exact: forall m n, i j.
     in_safe_int_range i -> in_safe_int_range j ->
     in_safe_int_range (i + j) -> eq (of_int m (i + j)) (add n (of_int m i) (of_int m j))
 
-  axiom of_int_sub_exact: forall m n, i j.
+  goal of_int_sub_exact: forall m n, i j.
     in_safe_int_range i -> in_safe_int_range j ->
     in_safe_int_range (i - j) -> eq (of_int m (i - j)) (sub n (of_int m i) (of_int m j))
 
-  axiom of_int_mul_exact: forall m n, i j.
+  goal of_int_mul_exact: forall m n, i j.
     in_safe_int_range i -> in_safe_int_range j ->
     in_safe_int_range (i * j) -> eq (of_int m (i * j)) (mul n (of_int m i) (of_int m j))
 
@@ -854,7 +877,7 @@ module GenericFloat
   (** truncate *)
 
   axiom truncate_neg: forall x:t.
-    is_finite x -> is_negative x -> roundToIntegral RTZ x = roundToIntegral RTP x
+    is_finite x -> not (is_positive) x -> roundToIntegral RTZ x = roundToIntegral RTP x
 
   axiom truncate_pos: forall x:t.
     is_finite x -> is_positive x -> roundToIntegral RTZ x = roundToIntegral RTN x
@@ -899,7 +922,7 @@ module GenericFloat
 
   axiom RNA_down_tie:
     forall x:t. (x .- (roundToIntegral RTN x)) .= ((roundToIntegral RTP x) .- x) ->
-      is_negative x -> roundToIntegral RNA x = roundToIntegral RTN x
+      (not is_positive x) -> roundToIntegral RNA x = roundToIntegral RTN x
 
   axiom RNA_up_tie:
     forall x:t. ((roundToIntegral RTP x) .- x) .= (x .- (roundToIntegral RTN x)) ->
@@ -939,13 +962,13 @@ module Float_interval
   predicate valid (x:t) =
     match x with
     | Inan -> true
-    | Intv l h _ -> F.(l .<= h) /\ F.is_not_nan l /\ F.is_not_nan h
+    | Intv l h _ -> F.(le l h) /\ not (F.is_nan l) /\ not (F.is_nan h)
     end
 
   predicate mem (x:F.t) (i:t) =
     match i with
     | Inan -> F.is_nan x
-    | Intv l h b -> if F.is_nan x then b else F.(l .<= x .<= h)
+    | Intv l h b -> if F.is_nan x then b else F.(le l  x /\ le x h)
     end
 (*
   type classify =
@@ -980,23 +1003,34 @@ module Float_interval
       
   goal G1: forall f. F.is_plus_infinity f -> f = F.Infinity false
 
-  lemma G2: forall m f1 f2 f3.
+  (*lemma G2: forall m f1 f2 f3.
     not F.(is_nan (add m f1 f3)) -> not F.(is_nan (add m f2 f3)) -> F.(le f1 f2) ->
      F.(le (add m f1 f3) (add m f2 f3))
+   *)
 
   let ghost monotone_add (m:F.mode) (f1:F.t) (f2:F.t) (f3:F.t) =
-    requires { F.(is_not_nan (add m f1 f3)) }
-    requires { F.(is_not_nan (add m f2 f3)) }
+    requires { F.(not (is_nan (add m f1 f3))) }
+    requires { F.(not (is_nan (add m f2 f3))) }
     requires { F.(le f1 f2) }
     ensures  { F.(le (add m f1 f3) (add m f2 f3)) } ()
 
   let ghost monotone_add2 (m:F.mode) (f3:F.t) (f1:F.t) (f2:F.t) =
-    requires { F.(is_not_nan (add m f3 f1)) }
-    requires { F.(is_not_nan (add m f3 f2)) }
+    requires { F.(not (is_nan (add m f3 f1))) }
+    requires { F.(not (is_nan (add m f3 f2))) }
     requires { F.(le f1 f2) }
     ensures  { F.(le (add m f3 f1) (add m f3 f2)) } ()
 
+   let ghost le_trans (f1 f2 f3:F.t)
+     requires { F.le f1 f2 }
+     requires { F.le f2 f3 }
+     ensures { F.le f1 f3 } = ()
 
+  let ghost monotone_add3 (m:F.mode) (l1:F.t) (l2:F.t) (h1:F.t) (h2:F.t) =
+    requires { F.(not (is_nan (add m l1 l2))) }
+    requires { F.(not (is_nan (add m h1 h2))) }
+    requires { F.(le l1 h1) }
+    requires { F.(le l2 h2) }
+    ensures  { F.(le (add m l1 l2) (add m h1 h2)) } ()
 
   let cadd (m : F.mode) (i1 i2: t) : t
      requires { valid i1 }
@@ -1009,8 +1043,8 @@ module Float_interval
         let sum2 = F.add m h1 h2 in
         if F.is_nan sum1 then
           if F.is_nan sum2 then begin
-            assert { F.diff_sign l1 l2 };
-            assert { F.diff_sign h1 h2 };
+            assert { not (F.same_sign l1 l2) };
+            assert { not (F.same_sign h1 h2) };
             assert { F.same_sign l1 h1 };
             assert { F.same_sign l2 h2 };
             assert { F.is_infinite l1};
@@ -1020,7 +1054,7 @@ module Float_interval
             Inan
             end
           else begin
-            assert { F.diff_sign l1 l2 };
+            assert { not (F.same_sign l1 l2) };
             assert { F.is_infinite l1};
             assert { F.is_infinite l2};
             assert { F.is_plus_infinity l1 \/ F.is_plus_infinity l2 };
@@ -1040,8 +1074,8 @@ module Float_interval
 (*  let ghost add_nan (m:mode) (f1:F.t) (f2:F.t) F.is_not_nan f1 -> F.is_not_nan f2 -> F.is_nan (F.add m f1 f2) -> F.diff_sign f1 f2 /\ F.is_infinite f1 /\ F.is_infinite f2 *)
 
   let ghost add_nan (m:F.mode) (f1:F.t) (f2:F.t)
-    requires { F.is_not_nan f1 }
-    requires { F.is_not_nan f2 }
+    requires { not (F.is_nan f1) }
+    requires { not (F.is_nan f2) }
     requires { F.is_nan (F.add m f1 f2) }
     ensures { match f1, f2 with
      | F.Infinity neg1, F.Infinity neg2 -> neg1 <> neg2
@@ -1049,15 +1083,14 @@ module Float_interval
      end } = ()
 
   let ghost add_not_nan (m:F.mode) (f1:F.t) (f2:F.t)
-    requires { F.is_not_nan (F.add m f1 f2) }
+    requires { not (F.is_nan (F.add m f1 f2)) }
     ensures { match f1, f2 with
      | F.NaN, _ | _, F.NaN -> false
      | F.Infinity neg1, F.Infinity neg2 -> neg1 = neg2
      | _ -> true
      end } = ()
 
-
-  goal add_not_nan: forall m f1 f2[F.is_nan (F.add m f1 f2)]. F.is_not_nan f1 -> F.is_not_nan f2 -> F.is_not_nan (F.add m f1 f2) ->
+  goal add_not_nan: forall m f1 f2[F.is_nan (F.add m f1 f2)]. not (F.is_nan f1) -> not (F.is_nan f2) -> not (F.is_nan (F.add m f1 f2)) ->
                          (F.same_sign f1 f2 /\ F.is_infinite f1 /\ F.is_infinite f2) \/ F.is_finite f1 \/ F.is_finite f2
 
   let cadd2 (m : F.mode) (i1 i2: t) : t
@@ -1102,19 +1135,27 @@ module Float_interval
         | False, False ->begin
             add_not_nan m l1 l2;
             add_not_nan m h1 h2;
-            let lemma sum1_le  (f1:F.t) (f2:F.t) =
+            let r =
+             Intv sum1 sum2 (orb (orb (orb b1 b2)
+               F.(andb (F.is_plus_infinity h1) (F.is_minus_infinity l2)))
+               F.(andb (F.is_plus_infinity h2) (F.is_minus_infinity l1)))
+            in
+            let lemma mem  (f1:F.t) (f2:F.t) =
               requires { mem f1 i1 }
               requires { mem f2 i2 }
-              requires { F.is_not_nan (F.add m l1 l2) }
-              requires { F.is_not_nan (F.add m f1 f2) }
-              ensures  { F.le (F.add m l1 l2) (F.add m f1 f2) }
-               add_not_nan m f1 f2;
-               monotone_add m l1 f1 f2;
-               monotone_add2 m l1 l2 f2;
+              ensures  { mem (F.add m f1 f2) r }
+              if F.is_nan (F.add m f1 f2) then
+                 add_nan m f1 f2
+              else begin
+               monotone_add3 m l1 l2 f1 f2;
+               monotone_add3 m f1 f2 h1 h2;
+             end
+            in
+            let lemma valid  () =
+              ensures  { valid r }
+               monotone_add3 m l1 l2 h1 h2;
             in
-            Intv sum1 sum2 (orb (orb (orb b1 b2)
-            F.(andb (F.is_plus_infinity h1) (F.is_minus_infinity l2)))
-            F.(andb (F.is_plus_infinity h2) (F.is_minus_infinity l1)))
+            r
            end
       end
       end
diff --git a/common/float_interval/why3session.xml b/common/float_interval/why3session.xml
index 94c561372187f2d385b52fa1b1d8ff75d8eaa9e1..a5d5080a976e314e0e4fa4c36c8d3d4cffd1b3a7 100644
--- a/common/float_interval/why3session.xml
+++ b/common/float_interval/why3session.xml
@@ -3,170 +3,452 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="Colibri2" version="n/a" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="n/a" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="whyml">
 <path name=".."/><path name="float_interval.mlw"/>
 <theory name="GenericFloat">
  <goal name="finite&#39;vc" expl="VC for finite" proved="true">
  <proof prover="0"><result status="valid" time="0.06"/></proof>
  </goal>
- <goal name="is_finite" proved="true">
- <proof prover="0"><result status="valid" time="0.11"/></proof>
+ <goal name="is_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="round_sign">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.07"/></proof>
+ <proof prover="1" obsolete="true"><result status="unknown" time="0.15" steps="41497"/></proof>
+ <transf name="introduce_premises" >
+  <goal name="round_sign.0">
+  <transf name="instantiate" arg1="Round_monotonic" arg2="m,0.,x">
+   <goal name="round_sign.0.0">
+   <transf name="instantiate" arg1="Round_monotonic" arg2="m,x,0.">
+    <goal name="round_sign.0.0.0">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
+    <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="12145"/></proof>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="feq_eq">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
  </goal>
- <goal name="feq_eq" proved="true">
- <proof prover="0"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_feq">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
  </goal>
- <goal name="eq_feq" proved="true">
- <proof prover="0"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_refl">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
  </goal>
- <goal name="eq_refl" proved="true">
- <proof prover="0"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_sym">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
  </goal>
- <goal name="eq_sym" proved="true">
- <proof prover="0"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_trans">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
  </goal>
- <goal name="eq_trans" proved="true">
- <proof prover="0"><result status="valid" time="0.08"/></proof>
+ <goal name="eq_zero">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
  </goal>
- <goal name="eq_zero" proved="true">
- <proof prover="0"><result status="valid" time="0.03"/></proof>
+ <goal name="eq_to_real_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.16"/></proof>
  </goal>
- <goal name="eq_to_real_finite" proved="true">
- <proof prover="0"><result status="valid" time="0.16"/></proof>
+ <goal name="eq_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
  </goal>
- <goal name="eq_special" proved="true">
- <proof prover="0"><result status="valid" time="0.18"/></proof>
+ <goal name="lt_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
  </goal>
- <goal name="lt_finite" proved="true">
- <proof prover="0"><result status="valid" time="0.18"/></proof>
+ <goal name="le_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
  </goal>
- <goal name="le_finite" proved="true">
- <proof prover="0"><result status="valid" time="0.10"/></proof>
+ <goal name="le_trans">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
  </goal>
- <goal name="le_lt_trans" proved="true">
- <proof prover="0"><path name="float_interval-GenericFloat-le_lt_trans_2.psmt2"/><undone/></proof>
- <transf name="introduce_premises" proved="true" >
-  <goal name="le_lt_trans.0" proved="true">
+ <goal name="le_lt_trans">
+ <proof prover="0" obsolete="true"><path name="float_interval-GenericFloat-le_lt_trans_2.psmt2"/><result status="failure" time="0.00"/></proof>
+ <transf name="introduce_premises" >
+  <goal name="le_lt_trans.0">
   <proof prover="0" obsolete="true"><path name="float_interval-GenericFloat-le_lt_trans_1.psmt2"/><result status="unknown" time="0.00" steps="0"/></proof>
-  <transf name="destruct_term" proved="true" arg1="x">
-   <goal name="le_lt_trans.0.0" proved="true">
-   <proof prover="0"><result status="valid" time="0.11"/></proof>
+  <transf name="destruct_term" arg1="x">
+   <goal name="le_lt_trans.0.0">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
    </goal>
-   <goal name="le_lt_trans.0.1" proved="true">
-   <proof prover="0"><result status="valid" time="0.07"/></proof>
+   <goal name="le_lt_trans.0.1">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
    </goal>
-   <goal name="le_lt_trans.0.2" proved="true">
-   <proof prover="0"><result status="valid" time="0.12"/></proof>
+   <goal name="le_lt_trans.0.2">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
    </goal>
-   <goal name="le_lt_trans.0.3" proved="true">
-   <proof prover="0"><result status="valid" time="0.13"/></proof>
+   <goal name="le_lt_trans.0.3">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="lt_le_trans" proved="true">
- <proof prover="0"><result status="valid" time="0.15"/></proof>
+ <goal name="lt_le_trans">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.27"/></proof>
+ </goal>
+ <goal name="le_ge_asym">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.15"/></proof>
+ </goal>
+ <goal name="not_lt_ge">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ </goal>
+ <goal name="not_gt_le">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="le_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
  </goal>
- <goal name="le_ge_asym" proved="true">
- <proof prover="0"><result status="valid" time="0.13"/></proof>
+ <goal name="lt_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.19"/></proof>
  </goal>
- <goal name="not_lt_ge" proved="true">
- <proof prover="0"><result status="valid" time="0.10"/></proof>
+ <goal name="lt_lt_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
  </goal>
- <goal name="not_gt_le" proved="true">
- <proof prover="0"><result status="valid" time="0.11"/></proof>
+ <goal name="positive_to_real">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
  </goal>
- <goal name="le_special" proved="true">
- <proof prover="0"><result status="valid" time="0.18"/></proof>
+ <goal name="to_real_positive">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
  </goal>
- <goal name="lt_special" proved="true">
- <proof prover="0"><result status="valid" time="0.19"/></proof>
+ <goal name="negative_to_real">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
  </goal>
- <goal name="lt_lt_finite" proved="true">
- <proof prover="0"><result status="valid" time="0.09"/></proof>
+ <goal name="to_real_negative">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
  </goal>
- <goal name="diff_sign_trans" proved="true">
- <proof prover="0"><result status="valid" time="0.12"/></proof>
+ <goal name="diff_sign_trans">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.12"/></proof>
  </goal>
- <goal name="diff_sign_product" proved="true">
- <proof prover="0"><result status="valid" time="0.16"/></proof>
+ <goal name="diff_sign_product">
+ <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
  </goal>
- <goal name="same_sign_product" proved="true">
- <proof prover="0"><result status="valid" time="0.16"/></proof>
+ <goal name="same_sign_product">
+ <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
  </goal>
- <goal name="add_finite" proved="true">
- <proof prover="0"><result status="valid" time="0.13"/></proof>
+ <goal name="add_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
  </goal>
- <goal name="add_finite_rev" proved="true">
- <proof prover="0"><result status="valid" time="0.20"/></proof>
+ <goal name="add_finite_rev">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.20"/></proof>
  </goal>
- <goal name="add_finite_rev_n" proved="true">
- <proof prover="0"><result status="valid" time="0.40"/></proof>
+ <goal name="add_finite_rev_n">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.42"/></proof>
+ </goal>
+ <goal name="sub_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.24"/></proof>
  </goal>
  <goal name="sub_finite_rev">
- <proof prover="0"><result status="unknown" time="0.19"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="sub_finite_rev_n">
- <proof prover="0"><result status="unknown" time="0.19"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.55"/></proof>
+ </goal>
+ <goal name="mul_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.19"/></proof>
  </goal>
  <goal name="mul_finite_rev">
- <proof prover="0"><result status="unknown" time="0.20"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.14"/></proof>
  </goal>
  <goal name="mul_finite_rev_n">
- <proof prover="0"><result status="timeout" time="5.00"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.39"/></proof>
+ </goal>
+ <goal name="div_finite">
+ <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
  </goal>
  <goal name="div_finite_rev">
- <proof prover="0"><result status="unknown" time="0.12"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
  </goal>
  <goal name="div_finite_rev_n">
- <proof prover="0"><result status="unknown" time="0.12"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
  </goal>
- <goal name="neg_finite_rev" proved="true">
- <proof prover="0"><result status="valid" time="0.09"/></proof>
+ <goal name="neg_finite">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.12"/></proof>
+ </goal>
+ <goal name="neg_finite_rev">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="abs_finite_rev">
- <proof prover="0"><result status="unknown" time="0.12"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
+ </goal>
+ <goal name="abs_universal">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+ </goal>
+ <goal name="fma_finite">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
  </goal>
- <goal name="fma_finite_rev" proved="true">
- <proof prover="0" timelimit="20"><result status="valid" time="0.16"/></proof>
+ <goal name="fma_finite_rev">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
  </goal>
  <goal name="fma_finite_rev_n">
- <proof prover="0"><result status="unknown" time="0.11"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.11"/></proof>
+ </goal>
+ <goal name="sqrt_finite">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
  </goal>
  <goal name="sqrt_finite_rev">
- <proof prover="0"><result status="timeout" time="5.00"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
  </goal>
  <goal name="add_special">
- <proof prover="0"><result status="unknown" time="0.72"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.45"/></proof>
+ <proof prover="1" obsolete="true"><result status="unknown" time="0.24" steps="64795"/></proof>
+ </goal>
+ <goal name="sub_special">
+ <transf name="split_vc" >
+  <goal name="sub_special.0">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+  </goal>
+  <goal name="sub_special.1">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+  </goal>
+  <goal name="sub_special.2">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+  </goal>
+  <goal name="sub_special.3">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+  </goal>
+  <goal name="sub_special.4">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+  </goal>
+  <goal name="sub_special.5">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+  </goal>
+  <goal name="sub_special.6">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+  </goal>
+  <goal name="sub_special.7">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+  </goal>
+  <goal name="sub_special.8">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.61"/></proof>
+  </goal>
+  <goal name="sub_special.9">
+  <proof prover="0" obsolete="true"><result status="valid" time="1.16"/></proof>
+  </goal>
+  <goal name="sub_special.10">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.22"/></proof>
+  </goal>
+  <goal name="sub_special.11">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.19"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="mul_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.40"/></proof>
+ </goal>
+ <goal name="div_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.16"/></proof>
+ </goal>
+ <goal name="neg_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="abs_special">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.14"/></proof>
+ </goal>
+ <goal name="fma_special">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.23"/></proof>
+ <transf name="remove" arg1="zero1,one1,(-&#39;),(&gt;&#39;),(&lt;=&#39;),(&gt;=&#39;),zero,one,(&gt;),(&lt;=),(&gt;=),(-),(/),(/.),inv,(&gt;=.),(&lt;.),(&gt;.),abs1,sqr,andb,orb,notb,xorb,implb,to_nearest,zeroF,neg,(.-_),(./),sign,classify,le,lt,eq,ge,gt,(.&lt;=),(.&lt;),(.&gt;=),(.&gt;),(.=),is_normal,is_subnormal,is_zero,is_nan,is_finite,is_plus_infinity,is_minus_infinity,is_plus_zero,is_minus_zero,emax,in_int_range,no_overflow,in_safe_int_range,same_sign,product_sign,overflow_value,sign_zero_result,is_RTN,add,(.+),sub,(.-),mul,(.* ),same_sign_real,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Abs_sum,Abs_prod,triangular_inequality,Zero1,One,Add,Sub,Mul,Neg,Injective,Monotonic,Truncate_int,Truncate_down_pos,Truncate_up_neg,Truncate_monotonic,Truncate_monotonic_int1,Floor_int,Ceil_int,Floor_down,Ceil_up,Floor_monotonic,Ceil_monotonic,Sqrt_positive,Sqrt_square,Square_sqrt,Sqrt_mul,Sqrt_le,Power_0,Power_s,Power_1,Power_sum,pow2pos,pow2_0,pow2_1,pow2_2,pow2_3,pow2_4,pow2_5,pow2_6,pow2_7,pow2_8,pow2_9,pow2_10,pow2_11,pow2_12,pow2_13,pow2_14,pow2_15,pow2_16,pow2_17,pow2_18,pow2_19,pow2_20,pow2_21,pow2_22,pow2_23,pow2_24,pow2_25,pow2_26,pow2_27,pow2_28,pow2_29,pow2_30,pow2_31,pow2_32,pow2_33,pow2_34,pow2_35,pow2_36,pow2_37,pow2_38,pow2_39,pow2_40,pow2_41,pow2_42,pow2_43,pow2_44,pow2_45,pow2_46,pow2_47,pow2_48,pow2_49,pow2_50,pow2_51,pow2_52,pow2_53,pow2_54,pow2_55,pow2_56,pow2_57,pow2_58,pow2_59,pow2_60,pow2_61,pow2_62,pow2_63,pow2_64,eb_gt_1,sb_gt_1,round_to_float,round_float,max_real_not_zero,max_real_round,mk_finite_def,mk_finite_fed,zeroF_is_positive,zeroF_is_zero,zero_to_real,zero_of_int,max_real_bound,max_int,minus_max_real_round,zero_round,Bounded_real_no_overflow,Round_monotonic,Round_idempotent,Round_to_real,Round_down_le,Round_up_ge,Round_down_neg,Round_up_neg,round_sign,pow2sb,Exact_rounding_for_integers,le_trans,abs_finite">
+  <goal name="fma_special.0">
+  <proof prover="0" timelimit="1" obsolete="true"><path name="float_interval-GenericFloat-fma_special_1.psmt2"/><result status="valid" time="0.09"/></proof>
+  <transf name="split_vc" >
+   <goal name="fma_special.0.0">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.1">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="fma_special.0.2">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.3">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.03"/></proof>
+   </goal>
+   <goal name="fma_special.0.4">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.5">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="fma_special.0.6">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.7">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="fma_special.0.8">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.9">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.10">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.11">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="fma_special.0.12">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="fma_special.0.13">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.14">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.15">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.16">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.17">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.18">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.19">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
+   </goal>
+   <goal name="fma_special.0.20">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.06"/></proof>
+   </goal>
+   <goal name="fma_special.0.21">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.07"/></proof>
+   </goal>
+   <goal name="fma_special.0.22">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+   </goal>
+   <goal name="fma_special.0.23">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+   </goal>
+   <goal name="fma_special.0.24">
+   <proof prover="0" obsolete="true"><result status="unknown" time="0.06"/></proof>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ <transf name="split_vc" >
+  <goal name="fma_special.0">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
+  </goal>
+  <goal name="fma_special.1">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
+  </goal>
+  <goal name="fma_special.2">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.3">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.4">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+  </goal>
+  <goal name="fma_special.5">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.6">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+  </goal>
+  <goal name="fma_special.7">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+  </goal>
+  <goal name="fma_special.8">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.9">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+  </goal>
+  <goal name="fma_special.10">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.11">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.12">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.11"/></proof>
+  </goal>
+  <goal name="fma_special.13">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.14">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.15">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
+  </goal>
+  <goal name="fma_special.16">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.17">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+  </goal>
+  <goal name="fma_special.18">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.19">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
+  </goal>
+  <goal name="fma_special.20">
+  <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+  </goal>
+  <goal name="fma_special.21">
+  <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+  </goal>
+  <goal name="fma_special.22">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+  <goal name="fma_special.23">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
+  </goal>
+  <goal name="fma_special.24">
+  <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="sqrt_special">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+ </goal>
+ <goal name="of_int_add_exact">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+ </goal>
+ <goal name="of_int_sub_exact">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
+ </goal>
+ <goal name="of_int_mul_exact">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
  </goal>
  <goal name="Min_r">
- <proof prover="0"><result status="unknown" time="0.13"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.13"/></proof>
  </goal>
  <goal name="Min_l">
- <proof prover="0"><result status="unknown" time="0.12"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
  </goal>
  <goal name="Max_r">
- <proof prover="0"><result status="unknown" time="0.13"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.13"/></proof>
  </goal>
  <goal name="Max_l">
- <proof prover="0"><result status="unknown" time="0.14"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.14"/></proof>
  </goal>
 </theory>
 <theory name="Float_interval">
- <goal name="Test2" proved="true">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- <transf name="split_vc" proved="true" >
-  <goal name="Test2.0" proved="true">
-  <transf name="instantiate" proved="true" arg1="is_not_finite" arg2="f1">
-   <goal name="Test2.0.0" proved="true">
+ <goal name="Test2">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <transf name="split_vc" >
+  <goal name="Test2.0">
+  <transf name="instantiate" arg1="is_not_finite" arg2="f1">
+   <goal name="Test2.0.0">
    <proof prover="0"><result status="valid" time="0.05"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="Test" proved="true">
- <proof prover="0"><result status="valid" time="0.17"/></proof>
+ <goal name="Test">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.17"/></proof>
  <transf name="split_vc" >
   <goal name="Test.0">
   <transf name="instantiate" arg1="add_special" arg2="m, f1, f2">
@@ -177,24 +459,24 @@
   </goal>
  </transf>
  </goal>
- <goal name="G1" proved="true">
- <proof prover="0"><result status="valid" time="0.09"/></proof>
- <transf name="split_vc" proved="true" >
-  <goal name="G1.0" proved="true">
-  <transf name="unfold" proved="true" arg1="is_plus_infinity" arg2="in" arg3="H">
-   <goal name="G1.0.0" proved="true">
-   <transf name="destruct_term" proved="true" arg1="f">
-    <goal name="G1.0.0.0" proved="true">
-    <proof prover="0"><result status="valid" time="0.05"/></proof>
+ <goal name="G1">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <transf name="split_vc" >
+  <goal name="G1.0">
+  <transf name="unfold" arg1="is_plus_infinity" arg2="in" arg3="H">
+   <goal name="G1.0.0">
+   <transf name="destruct_term" arg1="f">
+    <goal name="G1.0.0.0">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
     </goal>
-    <goal name="G1.0.0.1" proved="true">
-    <proof prover="0"><result status="valid" time="0.04"/></proof>
+    <goal name="G1.0.0.1">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
     </goal>
-    <goal name="G1.0.0.2" proved="true">
-    <proof prover="0"><result status="valid" time="0.09"/></proof>
+    <goal name="G1.0.0.2">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
     </goal>
-    <goal name="G1.0.0.3" proved="true">
-    <proof prover="0"><result status="valid" time="0.05"/></proof>
+    <goal name="G1.0.0.3">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
     </goal>
    </transf>
    </goal>
@@ -202,226 +484,376 @@
   </goal>
  </transf>
  </goal>
- <goal name="G2" proved="true">
- <proof prover="0"><result status="valid" time="1.76"/></proof>
+ <goal name="monotone_add&#39;vc" expl="VC for monotone_add">
+ <proof prover="0" obsolete="true"><result status="valid" time="3.16"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="529404"/></proof>
  </goal>
- <goal name="monotone_add&#39;vc" expl="VC for monotone_add" proved="true">
- <proof prover="0"><result status="valid" time="0.31"/></proof>
+ <goal name="monotone_add2&#39;vc" expl="VC for monotone_add2">
+ <proof prover="0" obsolete="true"><result status="valid" time="3.05"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="619003"/></proof>
+ <transf name="remove" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),zero1,one1,(&gt;&#39;),(&lt;=&#39;),(&gt;=&#39;),(-&#39;),(/),(&gt;=.),(&lt;.),(&gt;.),abs1,sqr,andb,orb,notb,xorb,implb,to_nearest,zeroF,in_int_range,in_safe_int_range,same_sign,product_sign,overflow_value,sign_zero_result,is_RTN,add,(.+),same_sign_real,valid,mem,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Abs_le,Abs_pos,Abs_sum,Abs_prod,triangular_inequality,Zero1,One,Add,Sub,Mul,Neg,Injective,Monotonic,Truncate_int,Truncate_down_pos,Truncate_up_neg,Real_of_truncate,Truncate_monotonic,Truncate_monotonic_int1,Truncate_monotonic_int2,Floor_int,Ceil_int,Floor_down,Ceil_up,Ceil_monotonic,Sqrt_positive,Sqrt_square,Square_sqrt,Sqrt_mul,Sqrt_le,Power_0,Power_s,Power_1,Power_sum,pow2pos,pow2_0,pow2_1,pow2_2,pow2_3,pow2_4,pow2_5,pow2_6,pow2_7,pow2_8,pow2_9,pow2_10,pow2_11,pow2_12,pow2_13,pow2_14,pow2_15,pow2_16,pow2_17,pow2_18,pow2_19,pow2_20,pow2_21,pow2_22,pow2_23,pow2_24,pow2_25,pow2_26,pow2_27,pow2_28,pow2_29,pow2_30,pow2_31,pow2_32,pow2_33,pow2_34,pow2_35,pow2_36,pow2_37,pow2_38,pow2_39,pow2_40,pow2_41,pow2_42,pow2_43,pow2_44,pow2_45,pow2_46,pow2_47,pow2_48,pow2_49,pow2_50,pow2_51,pow2_52,pow2_53,pow2_54,pow2_55,pow2_56,pow2_57,pow2_58,pow2_59,pow2_60,pow2_61,pow2_62,pow2_63,pow2_64,eb_gt_1,sb_gt_1,round_to_float,round_float,max_real_not_zero,max_real_round,finite&#39;invariant,mk_finite_def,mk_finite_fed,Round_idempotent,Round_to_real,Round_down_le,Round_up_ge,Round_down_neg,Round_up_neg,round_sign,pow2sb,Exact_rounding_for_integers,le_trans,sub_finite,mul_finite,div_finite,neg_finite,abs_finite,abs_universal,fma_finite,sqrt_finite,sub_special,mul_special,div_special,neg_special,abs_special,fma_special,sqrt_special,of_int_add_exact,of_int_sub_exact,of_int_mul_exact,zeroF_is_int,of_int_is_int,big_float_is_int,roundToIntegral_is_int,eq_is_int,add_int,sub_int,mul_int,fma_int,neg_int,abs_int,is_int_of_int,is_int_to_int,is_int_is_finite,int_to_real,truncate_int,truncate_neg,truncate_pos,ceil_le,ceil_lest,ceil_to_int,floor_le,floor_lest,floor_to_int,RNA_down,RNA_up,RNA_down_tie,RNA_up_tie,to_int_roundToIntegral,to_int_monotonic,to_int_of_int,eq_to_int,neg_to_int,roundToIntegral_is_finite,Test2,Test">
+  <goal name="monotone_add2&#39;vc.0" expl="VC for monotone_add2">
+  <proof prover="0" timelimit="1" obsolete="true"><path name="float_interval-Float_interval-monotone_add2qtvc_1.psmt2"/><undone/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="le_trans&#39;vc" expl="VC for le_trans">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
  </goal>
- <goal name="monotone_add2&#39;vc" expl="VC for monotone_add2" proved="true">
- <proof prover="0" timelimit="100"><result status="valid" time="5.68"/></proof>
+ <goal name="monotone_add3&#39;vc" expl="VC for monotone_add3">
+ <proof prover="0" timelimit="100" obsolete="true"><result status="valid" time="5.72"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="555896"/></proof>
+ <transf name="remove" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),zero1,one1,(&gt;&#39;),(&lt;=&#39;),(&gt;=&#39;),(-&#39;),(/),(+.),(/.),(-._),abs1,andb,orb,notb,xorb,implb,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Abs_le,Abs_pos,Abs_sum,Abs_prod,triangular_inequality,Zero1,One,Add,Sub,Mul,Neg,Injective,Monotonic,Truncate_int,Truncate_down_pos,Truncate_up_neg,Truncate_monotonic_int2,Floor_int,Power_1,pow2_19,pow2_20,pow2_21,pow2_22,pow2_23,pow2_24,pow2_25,pow2_26,pow2_27,pow2_28,pow2_29,pow2_30,pow2_31,pow2_32,pow2_33,pow2_34,pow2_35,pow2_36,pow2_37,pow2_38,pow2_39,pow2_40,pow2_41,pow2_42,pow2_43,pow2_44,pow2_45,pow2_46,pow2_47,pow2_48,pow2_49,pow2_50,pow2_51,pow2_52,pow2_53,pow2_54,pow2_55,pow2_56,pow2_57,pow2_58,pow2_59,pow2_60,pow2_61,pow2_62,pow2_63,pow2_64">
+  <goal name="monotone_add3&#39;vc.0" expl="VC for monotone_add3">
+  <proof prover="0" timelimit="19" obsolete="true"><undone/></proof>
+  </goal>
+ </transf>
  </goal>
  <goal name="cadd&#39;vc" expl="VC for cadd">
  <transf name="split_vc" >
-  <goal name="cadd&#39;vc.0" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.88"/></proof>
+  <goal name="cadd&#39;vc.0" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.68"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.1" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="4.28"/></proof>
+  <goal name="cadd&#39;vc.1" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="3.30"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.2" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="2.38"/></proof>
+  <goal name="cadd&#39;vc.2" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="1.98"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.3" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.10"/></proof>
+  <goal name="cadd&#39;vc.3" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.4" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.84"/></proof>
+  <goal name="cadd&#39;vc.4" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.68"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.24"/></proof>
+  <goal name="cadd&#39;vc.5" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.6" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.58"/></proof>
+  <goal name="cadd&#39;vc.6" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.42"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.7" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.29"/></proof>
+  <goal name="cadd&#39;vc.7" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.23"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.8" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.87"/></proof>
+  <goal name="cadd&#39;vc.8" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.74"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.9" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.80"/></proof>
+  <goal name="cadd&#39;vc.9" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.61"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.10" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.23"/></proof>
+  <goal name="cadd&#39;vc.10" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.20"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.11" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.10"/></proof>
+  <goal name="cadd&#39;vc.11" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.12" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.53"/></proof>
+  <goal name="cadd&#39;vc.12" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.46"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.13" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.88"/></proof>
+  <goal name="cadd&#39;vc.13" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.68"/></proof>
   </goal>
-  <goal name="cadd&#39;vc.14" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="2.14"/></proof>
+  <goal name="cadd&#39;vc.14" expl="assertion">
+  <proof prover="0" obsolete="true"><result status="valid" time="2.28"/></proof>
   </goal>
   <goal name="cadd&#39;vc.15" expl="postcondition">
   <transf name="split_vc" >
-   <goal name="cadd&#39;vc.15.0" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.05"/></proof>
+   <goal name="cadd&#39;vc.15.0" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
    </goal>
-   <goal name="cadd&#39;vc.15.1" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.12"/></proof>
+   <goal name="cadd&#39;vc.15.1" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
    </goal>
-   <goal name="cadd&#39;vc.15.2" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.13"/></proof>
+   <goal name="cadd&#39;vc.15.2" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="cadd&#39;vc.15.3" expl="postcondition">
-   <proof prover="0"><result status="timeout" time="5.00"/></proof>
+   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+   <transf name="split_vc" >
+    <goal name="cadd&#39;vc.15.3.0" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.33"/></proof>
+    </goal>
+    <goal name="cadd&#39;vc.15.3.1" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="1.60"/></proof>
+    </goal>
+    <goal name="cadd&#39;vc.15.3.2" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+    <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="525585"/></proof>
+    </goal>
+    <goal name="cadd&#39;vc.15.3.3" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="add_nan&#39;vc" expl="VC for add_nan" proved="true">
- <proof prover="0"><result status="valid" time="0.11"/></proof>
+ <goal name="add_nan&#39;vc" expl="VC for add_nan">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
  </goal>
- <goal name="add_not_nan&#39;vc" expl="VC for add_not_nan" proved="true">
- <proof prover="0"><result status="valid" time="0.10"/></proof>
+ <goal name="add_not_nan&#39;vc" expl="VC for add_not_nan">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
  </goal>
- <goal name="add_not_nan" proved="true">
- <proof prover="0"><result status="valid" time="0.09"/></proof>
+ <goal name="add_not_nan">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="cadd2&#39;vc" expl="VC for cadd2">
  <proof prover="0" timelimit="100" obsolete="true"><result status="timeout" time="177.00"/></proof>
  <transf name="remove" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),zero1,one1,(&gt;&#39;),(&lt;=&#39;),(&gt;=&#39;),(-&#39;),(/),( *.),(&lt;=.),andb,orb,notb,xorb,implb,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Power_0,Power_s,Power_1,Power_sum,pow2_0,pow2_2,pow2_4,pow2_5,pow2_6">
   <goal name="cadd2&#39;vc.0" expl="VC for cadd2">
-  <proof prover="0"><result status="timeout" time="5.00"/></proof>
+  <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
   </goal>
  </transf>
  <transf name="split_vc" >
   <goal name="cadd2&#39;vc.0" expl="postcondition">
   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
   <transf name="split_vc" >
-   <goal name="cadd2&#39;vc.0.0" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.05"/></proof>
+   <goal name="cadd2&#39;vc.0.0" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
    </goal>
-   <goal name="cadd2&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.11"/></proof>
+   <goal name="cadd2&#39;vc.0.1" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
    </goal>
-   <goal name="cadd2&#39;vc.0.2" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.13"/></proof>
+   <goal name="cadd2&#39;vc.0.2" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="cadd2&#39;vc.0.3" expl="postcondition">
-   <proof prover="0"><result status="timeout" time="5.00"/></proof>
+   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="cadd2&#39;vc.1" expl="postcondition">
   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
   <transf name="split_vc" >
-   <goal name="cadd2&#39;vc.1.0" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.04"/></proof>
+   <goal name="cadd2&#39;vc.1.0" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
    </goal>
-   <goal name="cadd2&#39;vc.1.1" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.04"/></proof>
+   <goal name="cadd2&#39;vc.1.1" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
    </goal>
-   <goal name="cadd2&#39;vc.1.2" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.03"/></proof>
+   <goal name="cadd2&#39;vc.1.2" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="cadd2&#39;vc.1.3" expl="postcondition">
-   <proof prover="0"><result status="timeout" time="5.00"/></proof>
+   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
- <goal name="cadd3&#39;vc" expl="VC for cadd3" proved="true">
+ <goal name="cadd3&#39;vc" expl="VC for cadd3">
  <proof prover="0" timelimit="100" obsolete="true"><result status="timeout" time="100.00"/></proof>
- <transf name="split_vc" proved="true" >
-  <goal name="cadd3&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05"/></proof>
+ <transf name="split_vc" >
+  <goal name="cadd3&#39;vc.0" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.1" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.2" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.3" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.4" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.5" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.6" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05"/></proof>
+  <goal name="cadd3&#39;vc.7" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.06"/></proof>
+  <goal name="cadd3&#39;vc.8" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <goal name="cadd3&#39;vc.9" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05"/></proof>
+  <goal name="cadd3&#39;vc.10" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.06"/></proof>
+  <goal name="cadd3&#39;vc.11" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.6" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <goal name="cadd3&#39;vc.12" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.7" expl="precondition" proved="true">
+  <goal name="cadd3&#39;vc.13" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.14" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.66"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.15" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.58"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.16" expl="precondition">
   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
-  <transf name="split_vc" proved="true" >
-   <goal name="cadd3&#39;vc.7.0" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.05"/></proof>
+  <transf name="split_vc" >
+   <goal name="cadd3&#39;vc.16.0" expl="precondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
    </goal>
-   <goal name="cadd3&#39;vc.7.1" expl="postcondition">
-   <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+  </transf>
+  </goal>
+  <goal name="cadd3&#39;vc.17" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.18" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.19" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.19"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.20" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.17"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.21" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.22" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.23" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.32"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.24" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.27"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.25" expl="postcondition">
+  <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+  <transf name="instantiate" arg1="le_trans" arg2="(add m x2 x5)">
+   <goal name="cadd3&#39;vc.25.0" expl="postcondition">
+   <transf name="instantiate" arg1="Hinst" arg2="(add m x2 f2)">
+    <goal name="cadd3&#39;vc.25.0.0" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.53"/></proof>
+    </goal>
+   </transf>
    </goal>
-   <goal name="cadd3&#39;vc.7.2" expl="postcondition">
-   <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
+  </transf>
+  </goal>
+  <goal name="cadd3&#39;vc.26" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.27" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.28" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.29" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.30" expl="postcondition">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.31" expl="postcondition">
+  <proof prover="0" obsolete="true"><result status="timeout" time="10.00"/></proof>
+  <transf name="split_vc" >
+   <goal name="cadd3&#39;vc.31.0" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
    </goal>
-   <goal name="cadd3&#39;vc.7.3" expl="postcondition">
-   <proof prover="0" timelimit="20" obsolete="true"><result status="timeout" time="20.00"/></proof>
+   <goal name="cadd3&#39;vc.31.1" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
    <transf name="split_vc" >
-    <goal name="cadd3&#39;vc.7.3.0" expl="postcondition">
-    <proof prover="0" obsolete="true"><result status="timeout" time="10.00"/></proof>
+    <goal name="cadd3&#39;vc.31.1.0" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
     </goal>
-    <goal name="cadd3&#39;vc.7.3.1" expl="postcondition">
-    <proof prover="0" obsolete="true"><result status="timeout" time="10.00"/></proof>
+    <goal name="cadd3&#39;vc.31.3.0" expl="postcondition">
+    <proof prover="0"><result status="valid" time="2.73"/></proof>
     </goal>
-    <goal name="cadd3&#39;vc.7.3.2" expl="postcondition">
-    <proof prover="0" obsolete="true"><result status="timeout" time="10.00"/></proof>
+    <goal name="cadd3&#39;vc.31.3.1" expl="postcondition">
+    <proof prover="0"><result status="valid" time="4.04"/></proof>
     </goal>
-    <goal name="cadd3&#39;vc.7.3.3" expl="postcondition">
-    <proof prover="0" obsolete="true"><result status="timeout" time="10.00"/></proof>
+    <goal name="cadd3&#39;vc.31.3.2" expl="postcondition">
+    <proof prover="0"><result status="timeout" time="5.00"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="cadd3&#39;vc.31.2" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+   </goal>
+   <goal name="cadd3&#39;vc.31.3" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+   <transf name="split_vc" >
+    <goal name="cadd3&#39;vc.31.3.0" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.35"/></proof>
+    </goal>
+    <goal name="cadd3&#39;vc.31.3.1" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.56"/></proof>
+    </goal>
+    <goal name="cadd3&#39;vc.31.3.2" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="2.37"/></proof>
+    </goal>
+    <goal name="cadd3&#39;vc.31.3.3" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
-  <goal name="cadd3&#39;vc.8" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
-  </goal>
-  <goal name="cadd3&#39;vc.9" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05"/></proof>
-  </goal>
-  <goal name="cadd3&#39;vc.10" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05"/></proof>
-  </goal>
-  <goal name="cadd3&#39;vc.11" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <goal name="cadd3&#39;vc.32" expl="postcondition">
+  <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+  <transf name="split_vc" >
+   <goal name="cadd3&#39;vc.32.0" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+   </goal>
+   <goal name="cadd3&#39;vc.32.1" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+   <transf name="split_vc" >
+    <goal name="cadd3&#39;vc.32.1.0" expl="postcondition">
+    <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+    </goal>
+    <goal name="cadd3&#39;vc.32.3.2" expl="postcondition">
+    <proof prover="0"><result status="valid" time="0.08"/></proof>
+    </goal>
+    <goal name="cadd3&#39;vc.32.3.0" expl="postcondition">
+    <proof prover="0"><result status="valid" time="0.04"/></proof>
+    </goal>
+    <goal name="cadd3&#39;vc.32.3.1" expl="postcondition">
+    <proof prover="0"><result status="valid" time="0.19"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="cadd3&#39;vc.32.2" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+   </goal>
+   <goal name="cadd3&#39;vc.32.3" expl="postcondition">
+   <proof prover="0" obsolete="true"><result status="valid" time="0.15"/></proof>
+   </goal>
+  </transf>
   </goal>
-  <goal name="cadd3&#39;vc.12" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <goal name="cadd3&#39;vc.25" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.13" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <goal name="cadd3&#39;vc.39" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.14" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.06"/></proof>
+  <goal name="cadd3&#39;vc.22" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.15" expl="precondition" proved="true">
-  <proof prover="0" timelimit="100"><result status="valid" time="46.74"/></proof>
+  <goal name="cadd3&#39;vc.41" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.16" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <goal name="cadd3&#39;vc.33" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.17" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.06"/></proof>
+  <goal name="cadd3&#39;vc.35" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.18" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <goal name="cadd3&#39;vc.42" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.19" expl="precondition" proved="true">
+  <goal name="cadd3&#39;vc.18" expl="precondition">
   <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
-  <transf name="split_vc" proved="true" >
-   <goal name="cadd3&#39;vc.19.0" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.43"/></proof>
+  <transf name="split_vc" >
+   <goal name="cadd3&#39;vc.18.0" expl="precondition">
+   <proof prover="0"><undone/></proof>
    </goal>
    <goal name="cadd3&#39;vc.19.1" expl="postcondition">
    <proof prover="0"><undone/></proof>
@@ -434,34 +866,31 @@
    </goal>
   </transf>
   </goal>
-  <goal name="cadd3&#39;vc.20" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.11"/></proof>
+  <goal name="cadd3&#39;vc.26" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.21" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="100"><result status="valid" time="5.80"/></proof>
+  <goal name="cadd3&#39;vc.24" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
-  <goal name="cadd3&#39;vc.22" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="100"><result status="valid" time="89.44"/></proof>
-  <transf name="split_vc" proved="true" >
-   <goal name="cadd3&#39;vc.22.0" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.05"/></proof>
-   </goal>
-   <goal name="cadd3&#39;vc.22.1" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.10"/></proof>
-   </goal>
-   <goal name="cadd3&#39;vc.22.2" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.11"/></proof>
-   </goal>
-   <goal name="cadd3&#39;vc.22.3" expl="postcondition" proved="true">
-   <proof prover="0" timelimit="100"><result status="valid" time="58.99"/></proof>
+  <goal name="cadd3&#39;vc.32" expl="precondition">
+  <proof prover="0"><undone/></proof>
+  </goal>
+  <goal name="cadd3&#39;vc.30" expl="precondition">
+  <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+  <transf name="split_vc" >
+   <goal name="cadd3&#39;vc.30.0" expl="precondition">
+   <proof prover="0"><undone/></proof>
    </goal>
   </transf>
   </goal>
-  <goal name="cadd3&#39;vc.23" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="1.22"/></proof>
+  <goal name="cadd3&#39;vc.17" expl="precondition">
+  <proof prover="0"><undone/></proof>
   </goal>
  </transf>
  </goal>
+ <goal name="G2">
+ <proof prover="0"><undone/></proof>
+ </goal>
 </theory>
 </file>
 </why3session>