diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index f4611fd2572f033c9bb30e1b82a7150785bb22df..9d739358ec0804e3dd9d1b848b9ee056948d9f16 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -1225,11 +1225,16 @@ module Debug : sig
     Info flags are set by --debug-all and must not change the behaviour. *)
 
   val dprintf0 :
-    ?nobox:unit -> flag -> (unit, Format.formatter, unit) format -> unit
+    ?nobox:unit ->
+    ?ct:unit ->
+    flag ->
+    (unit, Format.formatter, unit) format ->
+    unit
   (** Print only if the flag is set *)
 
   val dprintf1 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ('a -> unit, Format.formatter, unit) format ->
     'a ->
@@ -1238,6 +1243,7 @@ module Debug : sig
 
   val dprintf2 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ('b -> 'a -> unit, Format.formatter, unit) format ->
     'b ->
@@ -1247,6 +1253,7 @@ module Debug : sig
 
   val dprintf3 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ('c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
     'c ->
@@ -1257,6 +1264,7 @@ module Debug : sig
 
   val dprintf4 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ('d -> 'c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
     'd ->
@@ -1268,6 +1276,7 @@ module Debug : sig
 
   val dprintf5 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ('e -> 'd -> 'c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
     'e ->
@@ -1280,6 +1289,7 @@ module Debug : sig
 
   val dprintf6 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ('f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
     'f ->
@@ -1293,6 +1303,7 @@ module Debug : sig
 
   val dprintf7 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
       Format.formatter,
@@ -1310,6 +1321,7 @@ module Debug : sig
 
   val dprintf8 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
       Format.formatter,
@@ -1328,6 +1340,7 @@ module Debug : sig
 
   val dprintf9 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
       Format.formatter,
@@ -1347,6 +1360,7 @@ module Debug : sig
 
   val dprintf10 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
       Format.formatter,
@@ -1367,6 +1381,7 @@ module Debug : sig
 
   val dprintf11 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
       Format.formatter,
@@ -1388,6 +1403,7 @@ module Debug : sig
 
   val dprintf12 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'l ->
       'k ->
@@ -1422,6 +1438,7 @@ module Debug : sig
 
   val dprintf13 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'm ->
       'l ->
@@ -1458,6 +1475,7 @@ module Debug : sig
 
   val dprintf14 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'n ->
       'm ->
@@ -1496,6 +1514,7 @@ module Debug : sig
 
   val dprintf15 :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'o ->
       'n ->
@@ -1536,6 +1555,7 @@ module Debug : sig
 
   val dprintfn :
     ?nobox:unit ->
+    ?ct:unit ->
     flag ->
     ( 'o ->
       'n ->
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 25ddc34a665f6939957846e96201fbc2b3181173..7f32eb13351b20adcc7dfc46539f9b2ec964fdc4 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -963,8 +963,9 @@ module Delayed = struct
     set_value_pending d node nodevalue
 
   let set_dom d dom node v =
-    Debug.dprintf4 debug_few
-      "[Egraph] @[set_dom for %a with %a@]"
+    Debug.dprintf6 debug_few
+      "[Egraph] @[set_dom %a for %a with %a@]"
+      DomKind.pp dom
       Node.pp node (print_dom dom) v;
     set_dom_pending d dom node (Some v)
 
diff --git a/src_colibri2/popop_lib/debug.ml b/src_colibri2/popop_lib/debug.ml
index 8105a1b88c91628c6066936e66de15983dba45d0..61ff438d466a846b4c9470ac86f843abf3f44c94 100644
--- a/src_colibri2/popop_lib/debug.ml
+++ b/src_colibri2/popop_lib/debug.ml
@@ -99,7 +99,7 @@ let get_debug_formatter () = !formatter
 
 let () = set_debug_formatter Format.err_formatter
 
-let real_dprintf ?nobox s =
+let real_dprintf ?nobox ?ct s =
   let box = match nobox with None -> true | Some () -> false in
   if box then begin
     Format.pp_print_cut !formatter ();
@@ -109,60 +109,83 @@ let real_dprintf ?nobox s =
     (fun fmt -> if box then begin
          Format.pp_close_box fmt ();
          Format.pp_print_flush fmt ();
-       end
+       end;
+       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
+         in Fmt.(pf !formatter "@.%a" (vbox ~indent:1 (list ~sep:cut (box lines))) l)
     )
     !formatter s
+[@@ inline never]
 
-let dprintf0 ?nobox flag s =
-  if !flag then real_dprintf ?nobox s
+let dprintf0 ?nobox ?ct flag s =
+  if !flag then real_dprintf ?nobox ?ct s
+[@@ inline always]
 
-let dprintf1 ?nobox flag s a1 =
-  if !flag then real_dprintf ?nobox s a1
+let dprintf1 ?nobox ?ct flag s a1 =
+  if !flag then real_dprintf ?nobox ?ct s a1
+[@@ inline always]
 
-let dprintf2 ?nobox flag s a1 a2 =
-  if !flag then real_dprintf ?nobox s a1 a2
+let dprintf2 ?nobox ?ct flag s a1 a2 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2
+[@@ inline always]
 
-let dprintf3 ?nobox flag s a1 a2 a3 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3
+let dprintf3 ?nobox ?ct flag s a1 a2 a3 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3
+[@@ inline always]
 
-let dprintf4 ?nobox flag s a1 a2 a3 a4 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4
+let dprintf4 ?nobox ?ct flag s a1 a2 a3 a4 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4
+[@@ inline always]
 
-let dprintf5 ?nobox flag s a1 a2 a3 a4 a5 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5
+let dprintf5 ?nobox ?ct flag s a1 a2 a3 a4 a5 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5
+[@@ inline always]
 
-let dprintf6 ?nobox flag s a1 a2 a3 a4 a5 a6 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6
+let dprintf6 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6
+[@@ inline always]
 
-let dprintf7 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7
+let dprintf7 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7
+[@@ inline always]
 
-let dprintf8 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8
+let dprintf8 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8
+[@@ inline always]
 
-let dprintf9 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9
+let dprintf9 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9
+[@@ inline always]
 
-let dprintf10 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
+let dprintf10 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
+[@@ inline always]
 
-let dprintf11 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
+let dprintf11 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
+[@@ inline always]
 
-let dprintf12 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
+let dprintf12 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
+[@@ inline always]
 
-let dprintf13 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13
+let dprintf13 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13
+[@@ inline always]
 
-let dprintf14 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14
+let dprintf14 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14
+[@@ inline always]
 
-let dprintf15 ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
+let dprintf15 ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
+[@@ inline always]
 
-let dprintfn ?nobox flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 =
-  if !flag then real_dprintf ?nobox s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
+let dprintfn ?nobox ?ct flag s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 =
+  if !flag then real_dprintf ?nobox ?ct s a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15
   else
     (* ifprintf take too many times for computing the format *)
     let rec aux = fun _ -> Obj.magic aux in
diff --git a/src_colibri2/popop_lib/debug.mli b/src_colibri2/popop_lib/debug.mli
index 55580a1e05a6e4a036a3c4d9e0affa198f1efa5a..54cbd4d25a90d2060665b1c48dccf1a4c5e4afe9 100644
--- a/src_colibri2/popop_lib/debug.mli
+++ b/src_colibri2/popop_lib/debug.mli
@@ -55,95 +55,95 @@ val set_debug_formatter : Format.formatter -> unit
 val get_debug_formatter : unit -> Format.formatter
 (** Get the formatter used when printing debug material *)
 
-val dprintf0 : ?nobox:unit -> flag -> (unit,
+val dprintf0 : ?nobox:unit -> ?ct:unit -> flag -> (unit,
   Format.formatter, unit) format -> unit
 (** Print only if the flag is set *)
 
-val dprintf1 : ?nobox:unit -> flag -> ('a -> unit,
+val dprintf1 : ?nobox:unit -> ?ct:unit -> flag -> ('a -> unit,
   Format.formatter, unit) format -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf2 : ?nobox:unit -> flag -> ('b -> 'a -> unit,
+val dprintf2 : ?nobox:unit -> ?ct:unit -> flag -> ('b -> 'a -> unit,
   Format.formatter, unit) format ->
   'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf3 : ?nobox:unit -> flag -> ('c -> 'b -> 'a -> unit,
+val dprintf3 : ?nobox:unit -> ?ct:unit -> flag -> ('c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf4 : ?nobox:unit -> flag -> ('d -> 'c -> 'b -> 'a -> unit,
+val dprintf4 : ?nobox:unit -> ?ct:unit -> flag -> ('d -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf5 : ?nobox:unit -> flag -> ('e -> 'd -> 'c -> 'b -> 'a -> unit,
+val dprintf5 : ?nobox:unit -> ?ct:unit -> flag -> ('e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf6 : ?nobox:unit -> flag ->
+val dprintf6 : ?nobox:unit -> ?ct:unit -> flag ->
   ('f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf7 : ?nobox:unit -> flag ->
+val dprintf7 : ?nobox:unit -> ?ct:unit -> flag ->
   ('g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf8 : ?nobox:unit -> flag ->
+val dprintf8 : ?nobox:unit -> ?ct:unit -> flag ->
   ('h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf9 : ?nobox:unit -> flag ->
+val dprintf9 : ?nobox:unit -> ?ct:unit -> flag ->
   ('i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf10 : ?nobox:unit -> flag ->
+val dprintf10 : ?nobox:unit -> ?ct:unit -> flag ->
   ('j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf11 : ?nobox:unit -> flag ->
+val dprintf11 : ?nobox:unit -> ?ct:unit -> flag ->
   ('k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf12 : ?nobox:unit -> flag ->
+val dprintf12 : ?nobox:unit -> ?ct:unit -> flag ->
   ('l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf13 : ?nobox:unit -> flag ->
+val dprintf13 : ?nobox:unit -> ?ct:unit -> flag ->
   ('m -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf14 : ?nobox:unit -> flag ->
+val dprintf14 : ?nobox:unit -> ?ct:unit -> flag ->
   ('n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintf15 : ?nobox:unit -> flag ->
+val dprintf15 : ?nobox:unit -> ?ct:unit -> flag ->
   ('o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
   Format.formatter, unit) format ->
   'o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit
 (** Print only if the flag is set *)
 
-val dprintfn : ?nobox:unit -> flag ->
+val dprintfn : ?nobox:unit -> ?ct:unit -> flag ->
   ('o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> 'z,
   Format.formatter, unit) format ->
   'o -> 'n -> 'm -> 'l -> 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> 'z
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 2f46a03e276c2a8f0751f49aae1c0e29c1fd3f78..e3dbfbd530a2b7c02cf113663ec962257fb92cea 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -161,7 +161,7 @@ let new_solver ~learning () =
   in
   let sched_daemon att =
     incr daemon_count;
-    Debug.dprintf0 debug "[Scheduler] New waiting daemon";
+    (* Debug.dprintf0 debug "[Scheduler] New waiting daemon"; *)
     match get_event_priority att with
     | Immediate -> assert false (* absurd *)
     | Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
@@ -170,7 +170,7 @@ let new_solver ~learning () =
         Context.Ref.set t.fixing_model (att :: Context.Ref.get t.fixing_model)
   and sched_decision dec =
     incr dec_count;
-    Debug.dprintf1 debug "[Scheduler] New possible decisions prio:%i" !dec_count;
+    (* Debug.dprintf1 debug "[Scheduler] New possible decisions prio:%i" !dec_count; *)
     t.choices <-
       Prio.insert t.decprio (Att.Decision (!dec_count, dec)) t.choices
   in
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index f7aa4779b9b28bcbd36c2d3c2ecc5e65492ef68f..2df700bb6e2661f8ccd3eccef6bec9bbd796cb88 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -22,7 +22,7 @@ let dir = Sys.argv.(1)
 
 let result = if Array.length Sys.argv >= 3 then Some Sys.argv.(2) else None
 
-let cmd = "%{bin:colibri2} --size=10M --time=30s --max-steps 3500"
+let cmd = "%{bin:colibri2} --size=15M --time=30s --max-steps 3500"
 
 let print_test cout file =
   match result with
diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune.inc b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
index a63167f0516d0604ff19723247bde91df3d2f69d..98b899ea73a26e035e0584d4b0ce4aaedad0905e 100644
--- a/src_colibri2/tests/solve/all/steplimitreached/dune.inc
+++ b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
@@ -1,3 +1,3 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status steplimitreached 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status steplimitreached 
 --dont-print-result %{dep:bag-BagImpl-addqtvc.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status steplimitreached --learning --dont-print-result %{dep:bag-BagImpl-addqtvc.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status steplimitreached --learning --dont-print-result %{dep:bag-BagImpl-addqtvc.psmt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 8a470e8f41631aa1b4faa594a48387da1cf0a2cd..0b55ae9be6c6f5798936b861fe65579fa5085103 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -1,12 +1,12 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index 9a3098f1bed7ae73d9df3a42047d9765d4bafd0f..3a8a918a67df7e466836bcb7c234e24ee7fcdd91 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,33 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:anomaly_agetooold2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:assertion_fail.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:assertion_fail.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:assertion_fail.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:fuzzing1.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing1.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing1.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:fuzzing2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:par8-1-c.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:par8-1-c.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:par8-1-c.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-3.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:pigeon-4.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-4.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-4.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:quinn.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:quinn.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:quinn.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_v3_c2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_v3_c2.cnf})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_v3_c2.cnf})))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index 33634441266451e5d7912d9b29154467bb4f83e2..a4da599a19b005f9759869cda3cddbc91e8a27fd 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,18 +1,18 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:modus_ponens.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:modus_ponens.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:modus_ponens.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-1.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-1.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-1.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-3.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-4.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-4.cnf})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-4.cnf})))
diff --git a/src_colibri2/tests/solve/models/dune.inc b/src_colibri2/tests/solve/models/dune.inc
index ff2aa261caace0ce331feaf9636f1c0dc0c42fcf..0ffbe69bc24028ef9b0cf0b7c4e79d4a40ddf5d4 100644
--- a/src_colibri2/tests/solve/models/dune.inc
+++ b/src_colibri2/tests/solve/models/dune.inc
@@ -1,2 +1,2 @@
-(rule (action (with-stdout-to get_value.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 %{dep:get_value.smt2}))))
+(rule (action (with-stdout-to get_value.smt2.res (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 %{dep:get_value.smt2}))))
 (rule (alias runtest) (action (diff get_value.smt2.oracle get_value.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
index 48f0c472b8b8532231719bc3b27ade36cb3ca8b5..8e7e09be40b1350daabfd7868cad647e76b43834 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,18 +1,18 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:enum.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:tree1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:tree2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:tree3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree3.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree3.smt2})))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index 0879b8f097646a2d3482d13052461b9e038108db..76424e820adb599eb4103225c0826c56eaddfbc3 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,24 +1,24 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:enum2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:parlist0.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:parlist0.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:parlist0.psmt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/dune.inc b/src_colibri2/tests/solve/smt_fp/dune.inc
index 43a2e25af1e4cfe582d32fa8fe29372adc07f0da..3df67fbfaa78aeed8624cc20b8b429a4cdd6f680 100644
--- a/src_colibri2/tests/solve/smt_fp/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/dune.inc
@@ -1,2 +1,2 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:rm_universal.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:rm_universal.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:rm_universal.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:rm_universal.smt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index f0216026c8d36e97ea490cf09e2b42bc28de066b..a37aae0c7467a9349b619a24789a534a76c4ae72 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -1,45 +1,45 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:exists_eq_not_fp_eq.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists_eq_not_fp_eq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists_eq_not_fp_eq.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:inf_pos_neg_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:inf_pos_neg_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:inf_pos_neg_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:infm_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infm_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infm_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:infp_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infp_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infp_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:recognize_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:recognize_rounding_mode.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_rounding_mode.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_rounding_mode.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:rm_instanciation.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:rm_instanciation.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:rm_instanciation.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_add_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_add_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_add_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_mul_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_mul_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_mul_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:to_fp_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_fp_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_fp_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zero_pos_neg_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_pos_neg_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_pos_neg_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zerom_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerom_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerom_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zerop_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerop_eq_float32.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerop_eq_float32.smt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
index 5d8594119d983e5c74dfa5044d3723bcca6d6187..df78d2aeadad850713c9ff0c4205176e2eba52aa 100644
--- a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -1,12 +1,12 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:eq_fp_eq.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_fp_eq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_fp_eq.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:inf_pos_neg_neq.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:inf_pos_neg_neq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:inf_pos_neg_neq.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:propagate_le_ge.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:propagate_le_ge.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:propagate_le_ge.smt2})))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index 2c2e89ded6d45c4ab64d12a0fa8452bac48de0bf..c2743209c79e5a0af1b4f715e7ddb0361c8f8466 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,99 +1,102 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_CombiRepr_normalize.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_CombiRepr_normalize.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_CombiRepr_normalize.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_conflict_add_disequality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conflict_add_disequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conflict_add_disequality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_conpoly.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conpoly.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conpoly.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_decide_must_test_is_dis_equal.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_decide_must_test_is_dis_equal.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_decide_must_test_is_dis_equal.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_init_always_merge_itself.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_always_merge_itself.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_always_merge_itself.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_init_and_propa_must_be_ordered.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_and_propa_must_be_ordered.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_and_propa_must_be_ordered.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_case1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_case_4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_case_4_bis.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4_bis.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4_bis.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_itself_last_case.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_last_case.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_last_case.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_must_use_find.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_must_use_find.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_must_use_find.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_mult_explication.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_explication.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_explication.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_mult_not_linear_in_conflict.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_not_linear_in_conflict.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_not_linear_in_conflict.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_normalize_use_find_def.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_normalize_use_find_def.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_normalize_use_find_def.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_own_repr.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_own_repr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_own_repr.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_propacl.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_propacl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_propacl.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_subst_and_conflict_add.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_subst_and_conflict_add.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_subst_and_conflict_add.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_zero_dom.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_zero_dom.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_zero_dom.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:attach_only_when_dom_present.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:attach_only_when_dom_present.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:attach_only_when_dom_present.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:init_not_repr.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:init_not_repr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:init_not_repr.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:sem_invariant_in_learnt_dec.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:sem_invariant_in_learnt_dec.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:sem_invariant_in_learnt_dec.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_add_pexp_cl.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_add_pexp_cl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_add_pexp_cl.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_arith_homogeneous_dist_sign.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_arith_homogeneous_dist_sign.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_arith_homogeneous_dist_sign.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_merge_itself_repr_inside.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_merge_itself_repr_inside.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_merge_itself_repr_inside.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_set_pending_merge_expsameexp.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_set_pending_merge_expsameexp.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_set_pending_merge_expsameexp.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_subst_eventdom_find.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_subst_eventdom_find.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_subst_eventdom_find.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:to_real2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real2.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:zero_should_not_be_simplified.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_should_not_be_simplified.smt2})))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/zero_should_not_be_simplified.smt2 b/src_colibri2/tests/solve/smt_lra/sat/zero_should_not_be_simplified.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..04165ac26b0adb32064b9d750fa86de6ea05985a
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/sat/zero_should_not_be_simplified.smt2
@@ -0,0 +1,23 @@
+(set-logic ALL)
+(declare-fun v0 () Real)
+(assert 
+ (let ((?n12 0.0)) 
+ (let ((?n13 0.0)) 
+ (let ((?n15 0.0)) 
+ (let ((?n26 true)) 
+ (let ((?n28 true)) 
+ (let ((?n29 false)) 
+ (let ((?n30 0.0)) 
+ (let ((?n31 (* 0.0 ?n13))) 
+ (let ((?n32 (= ?n30 ?n31))) 
+ (let ((?n33 (ite ?n32 v0 ?n15))) 
+ (let ((?n34 (ite ?n29 ?n33 ?n12))) 
+ (let ((?n37 0.0)) 
+ (let ((?n38 (= ?n34 ?n37))) 
+ (let ((?n42 true)) 
+ (let ((?n43 (xor ?n38 ?n42))) 
+ (let ((?n44 (xor ?n28 ?n43))) 
+ (let ((?n45 (or ?n26 ?n44))) ?n45
+))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 32098dbe065e4c8236e9953029f2e4dee7575d88..148c56f234b5deb1bad0a638588d467da421fd0f 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -1,33 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:arith_ExpMult_by_zero.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_ExpMult_by_zero.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_ExpMult_by_zero.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:arith_merge_case2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_merge_case2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_merge_case2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:repr_and_poly.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_and_poly.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_and_poly.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:repr_fourier.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_fourier.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_fourier.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:solver_merge_itself_repr_empty.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_merge_itself_repr_empty.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_merge_itself_repr_empty.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:solver_set_sem_merge_sign.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_set_sem_merge_sign.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_set_sem_merge_sign.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:to_real2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real2.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real2.smt2})))
diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
index b0533db1e786e849483d576da545bf09427eb908..c73a28514ac43c5079afe957dbae5b47804a2ca1 100644
--- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -1,21 +1,21 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
index fdc03088e9ccf54610f6b382332c93ed58aa07bb..e25ae6b8c2aa2a031c4271477e527e4d1a5499d4 100644
--- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -1,30 +1,30 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ceil.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_pos_lt_to_real.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt_to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt_to_real.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:floor.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:floor.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:floor.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos_zero_le.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_zero_le.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_pos_zero_le.smt2})))
diff --git a/src_colibri2/tests/solve/smt_quant/dune.inc b/src_colibri2/tests/solve/smt_quant/dune.inc
index 94c44726ffa9cfb365197972f70c954968c1bf33..7ff5d8dec7552006dcfca2c9198ccdf8fa613f12 100644
--- a/src_colibri2/tests/solve/smt_quant/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/dune.inc
@@ -1,6 +1,6 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall0.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall3.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall4.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall4.smt2})))
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
index d888d22476695e087a41697346133e75a6296291..d33efa7a088a3f513006663b225c230b89037e1d 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
@@ -1,3 +1,3 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:exists.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists.smt2})))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index fcea32050f0ee3ba5b20f8dcfcf30ba4fd2de59e..517624de8395acfd45a3e1d50c99aa837e6ae91b 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,33 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:exists.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:exists2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall5.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall5.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall5.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall6.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall6.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall6.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall7.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall7.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall7.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall8.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall8.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall8.smt2})))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index 9872a6d3060efdca446859d6b939b45fa4cf283c..1ab95cb3d0d149b7b713ddcd730c5553dd02d7d1 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,63 +1,63 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:bad_conflict.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bad_conflict.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bad_conflict.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:bcp_dont_like_duplicate.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bcp_dont_like_duplicate.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bcp_dont_like_duplicate.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:bool_not_propa.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bool_not_propa.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bool_not_propa.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:boolexpup.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:boolexpup.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:boolexpup.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:clause_normalization.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clause_normalization.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clause_normalization.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:clmerge.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clmerge.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clmerge.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:conflict_complete_needed_cl.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:conflict_complete_needed_cl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:conflict_complete_needed_cl.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:directdom_not.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:directdom_not.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:directdom_not.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:dis_dom_before_first_age.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dis_dom_before_first_age.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dis_dom_before_first_age.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:dom_merge_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dom_merge_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dom_merge_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:equality_condis.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_condis.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_condis.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:equality_get_sem.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_get_sem.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_get_sem.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:exp_sem_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exp_sem_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exp_sem_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:explimit_cl_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:explimit_cl_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:explimit_cl_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:implication.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:implication.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:implication.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:intmap_set_disjoint.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:intmap_set_disjoint.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:intmap_set_disjoint.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:is_equal_not_propagated.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:is_equal_not_propagated.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:is_equal_not_propagated.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:ite_sem_bool.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ite_sem_bool.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ite_sem_bool.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:substupfalse_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:substupfalse_equality.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:substupfalse_equality.smt2})))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 7003c0e59b3715b4f75dcb76be45ff7b7648a64b..e29ac13dd0c6f2ef96e2ee757bc02792782d5fd6 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,39 +1,39 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:NEQ004_size4__decide_eq_us.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:NEQ004_size4__decide_eq_us.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:NEQ004_size4__decide_eq_us.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:deltaed0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:deltaed0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:deltaed0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:diff_to_value_for_bool.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_to_value_for_bool.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_to_value_for_bool.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:diff_value_substupfalse.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_value_substupfalse.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_value_substupfalse.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:distinct.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:eq_diamond2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_diamond2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_diamond2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:equality_norm_set.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:equality_norm_set.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:equality_norm_set.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:fundef.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fundef.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fundef.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:many_distinct.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:many_distinct.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:many_distinct.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:polyeq_genequality_deltaed.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality_deltaed.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality_deltaed.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:xor.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:xor.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:xor.smt2})))
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index 0551468dd3241f2e8e59170cfaa87cbcebd5edf2..7c14b026c2471385a06a017f2f33485ebef30c1b 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -113,4 +113,4 @@ let init env =
           Egraph.set_dom d dom (Float32.node value) s
         end
     )
-  
\ No newline at end of file
+  
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index e9613f9ba0bfa29b6c97cbab8d0b70af5379cfcd..60cbf361ba62c7852ee914f5eb11687dcbf1dcc9 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -22,29 +22,40 @@ open Colibri2_popop_lib
 open Colibri2_core
 open Colibri2_stdlib.Std
 
-let debug = Debug.register_info_flag
-  ~desc:"for intervals for the arithmetic theory"
-  "LRA.interval"
+let debug =
+  Debug.register_info_flag ~desc:"for intervals for the arithmetic theory"
+    "LRA.interval"
 
 module D = Colibri2_theories_LRA_stages.Interval_domain
 
-let dom = Dom.Kind.create (module struct type t = D.t let name = "ARITH" end)
+let dom =
+  Dom.Kind.create
+    (module struct
+      type t = D.t
 
-include (Dom.Lattice(struct
-    include D
-    let key = dom
-    let inter _ d1 d2 = inter d1 d2
-    let is_singleton _ d =
-      Option.map (fun x -> RealValue.nodevalue @@ RealValue.index x) (is_singleton d)
-  end
-))
+      let name = "ARITH"
+    end)
+
+include Dom.Lattice (struct
+  include D
+
+  let key = dom
+
+  let inter _ d1 d2 = inter d1 d2
+
+  let is_singleton _ d =
+    Option.map
+      (fun x -> RealValue.nodevalue @@ RealValue.index x)
+      (is_singleton d)
+end)
 
 let is_zero_or_positive d n =
   match Egraph.get_dom d dom n with
   | None -> false
-  | Some p -> match D.is_comparable D.zero p with
-    | D.Le | D.Lt -> true
-    | D.Ge | D.Gt | D.Uncomparable -> false
+  | Some p -> (
+      match D.is_comparable D.zero p with
+      | D.Le | D.Lt | D.Eq -> true
+      | D.Ge | D.Gt | D.Uncomparable -> false)
 
 let is_not_zero d n =
   match Egraph.get_dom d dom n with
@@ -54,59 +65,57 @@ let is_not_zero d n =
 let is_strictly_positive d n =
   match Egraph.get_dom d dom n with
   | None -> false
-  | Some p -> match D.is_comparable D.zero p with
-    | D.Lt -> true
-    | D.Le | D.Ge | D.Gt | D.Uncomparable -> false
+  | Some p -> (
+      match D.is_comparable D.zero p with
+      | D.Lt -> true
+      | D.Eq | D.Le | D.Ge | D.Gt | D.Uncomparable -> false)
 
 let is_strictly_negative d n =
   match Egraph.get_dom d dom n with
   | None -> false
-  | Some p -> match D.is_comparable D.zero p with
-    | D.Gt -> true
-    | D.Le | D.Ge | D.Lt | D.Uncomparable -> false
+  | Some p -> (
+      match D.is_comparable D.zero p with
+      | D.Gt -> true
+      | D.Eq | D.Le | D.Ge | D.Lt | D.Uncomparable -> false)
 
-let is_integer d n =
+let assume_negative d n = upd_dom d n (D.lt Q.zero)
+
+let assume_positive d n = upd_dom d n (D.gt Q.zero)
+
+let zero_is d n =
   match Egraph.get_dom d dom n with
-  | None -> false
-  | Some p -> D.is_integer p
+  | None -> D.Uncomparable
+  | Some p -> D.is_comparable D.zero p
 
+let is_integer d n =
+  match Egraph.get_dom d dom n with None -> false | Some p -> D.is_integer p
 
 module ChoLRA = struct
   let make_decision node v env =
-    Debug.dprintf4 Debug.decision
-      "[LRA] decide %a on %a" D.pp v Node.pp node;
+    Debug.dprintf4 Debug.decision "[LRA] decide %a on %a" D.pp v Node.pp node;
     set_dom env node v
 
   let choose_decision node env =
     let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
-      match D.split_heuristic v with
-      | Singleton _ -> Choice.DecNo
-      | Splitted (v1,v2) ->
-        DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
-      | NotSplitted ->
-        DecTodo [make_decision node (D.singleton (D.choose v))]
-
-  let choice n = {
-    Choice.prio = 1;
-    choice = choose_decision n;
-    print_cho = "Decision made by dom_interval.ml";
+    match D.split_heuristic v with
+    | Singleton _ -> Choice.DecNo
+    | Splitted (v1, v2) ->
+        DecTodo (List.map (make_decision node) (Shuffle.shufflel [ v1; v2 ]))
+    | NotSplitted -> DecTodo [ make_decision node (D.singleton (D.choose v)) ]
+
+  let choice n =
+    {
+      Choice.prio = 1;
+      choice = choose_decision n;
+      print_cho = "Decision made by dom_interval.ml";
     }
-
 end
 
 let choice = ChoLRA.choice
 
-let neg_cmp = function
-  | `Lt -> `Ge
-  | `Le -> `Gt
-  | `Ge -> `Lt
-  | `Gt -> `Le
+let neg_cmp = function `Lt -> `Ge | `Le -> `Gt | `Ge -> `Lt | `Gt -> `Le
 
-let com_cmp = function
-  | `Lt -> `Gt
-  | `Le -> `Ge
-  | `Ge -> `Le
-  | `Gt -> `Lt
+let com_cmp = function `Lt -> `Gt | `Le -> `Ge | `Ge -> `Le | `Gt -> `Lt
 
 let backward = function
   | `Lt -> D.lt'
@@ -115,7 +124,7 @@ let backward = function
   | `Ge -> D.ge'
 
 (** {2 Initialization} *)
-let converter d (f:Ground.t) =
+let converter d (f : Ground.t) =
   let r = Ground.node f in
   let reg n = Egraph.register d n in
   let open Monad in
@@ -124,67 +133,103 @@ let converter d (f:Ground.t) =
   let set = updd upd_dom in
   let get = getd dom in
   let cmp test cmp a b =
-    reg a; reg b;
-    attach d (
-      setb r (let* va = get a and+ vb = get b in
-              test (D.is_comparable va vb)) &&
-      set b  (let+ va = get a and+ vr = getb r in
-              backward (if vr then (com_cmp cmp) else (com_cmp (neg_cmp cmp))) va) &&
-      set a  (let+ vb = get b and+ vr = getb r in
-              backward (if vr then cmp else (neg_cmp cmp)) vb)
-    );
+    reg a;
+    reg b;
+    attach d
+      (setb r
+         (let* va = get a and+ vb = get b in
+          test (D.is_comparable va vb))
+      && set b
+           (let+ va = get a and+ vr = getb r in
+            backward (if vr then com_cmp cmp else com_cmp (neg_cmp cmp)) va)
+      && set a
+           (let+ vb = get b and+ vr = getb r in
+            backward (if vr then cmp else neg_cmp cmp) vb))
   in
   match Ground.sem f with
-  | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
+  | { app = { builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
     when Ground.Ty.equal ty Ground.Ty.real ->
-    (* Egraph.register_decision d (ChoLRA.choice r) *) (* not useful for now *)
-    ()
-  | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
+      (* Egraph.register_decision d (ChoLRA.choice r) *)
+      (* not useful for now *)
+      ()
+  | { app = { builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
     when Ground.Ty.equal ty Ground.Ty.int ->
-    upd_dom d r D.integers
-  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
-    let (a,b) = IArray.extract2_exn args in
-    reg a; reg b;
-    attach d (
-      set r (let+ va = get a and+ vb = get b in D.add va vb) &&
-      set a (let+ vb = get b and+ vr = get r in D.minus vr vb) &&
-      set b (let+ va = get a and+ vr = get r in D.minus vr va)
-    );
-  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
-    let (a,b) = IArray.extract2_exn args in
-    reg a; reg b;
-    attach d (
-      set r (let+ va = get a and+ vb = get b in D.minus va vb) &&
-      set a (let+ vb = get b and+ vr = get r in D.add vr vb) &&
-      set b (let+ va = get a and+ vr = get r in D.minus va vr)
-    );
-  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
-    let a = IArray.extract1_exn args in
-    reg a;
-    attach d (
-      set r (let+ va = get a in D.mult_cst Q.minus_one va) &&
-      set a (let+ vr = get r in D.mult_cst Q.minus_one vr)
-    );
-  | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false) `Lt a b
-  | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some true | Gt -> Some false) `Le a b
-  | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp (function | Uncomparable | Le -> None | Lt -> Some false  | Ge | Gt -> Some true) `Ge a b
-  | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some false  | Gt -> Some true) `Gt a b
+      upd_dom d r D.integers
+  | { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      attach d
+        (set r
+           (let+ va = get a and+ vb = get b in
+            D.add va vb)
+        && set a
+             (let+ vb = get b and+ vr = get r in
+              D.minus vr vb)
+        && set b
+             (let+ va = get a and+ vr = get r in
+              D.minus vr va))
+  | { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      attach d
+        (set r
+           (let+ va = get a and+ vb = get b in
+            D.minus va vb)
+        && set a
+             (let+ vb = get b and+ vr = get r in
+              D.add vr vb)
+        && set b
+             (let+ va = get a and+ vr = get r in
+              D.minus va vr))
+  | { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      attach d
+        (set r
+           (let+ va = get a in
+            D.mult_cst Q.minus_one va)
+        && set a
+             (let+ vr = get r in
+              D.mult_cst Q.minus_one vr))
+  | { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp
+        (function
+          | Uncomparable | Le -> None
+          | Lt -> Some true
+          | Eq | Ge | Gt -> Some false)
+        `Lt a b
+  | { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp
+        (function
+          | Uncomparable | Ge -> None
+          | Eq | Lt | Le -> Some true
+          | Gt -> Some false)
+        `Le a b
+  | { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp
+        (function
+          | Uncomparable | Le -> None
+          | Eq | Lt -> Some false
+          | Ge | Gt -> Some true)
+        `Ge a b
+  | { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp
+        (function
+          | Uncomparable | Ge -> None
+          | Eq | Lt | Le -> Some false
+          | Gt -> Some true)
+        `Gt a b
   | _ -> ()
 
 let init env =
-  Daemon.attach_reg_value env
-    RealValue.key
-    (fun d value ->
-       let v = RealValue.value value in
-       let s = D.singleton v in
-       Egraph.set_dom d dom (RealValue.node value) s
-    );
+  Daemon.attach_reg_value env RealValue.key (fun d value ->
+      let v = RealValue.value value in
+      let s = D.singleton v in
+      Egraph.set_dom d dom (RealValue.node value) s);
   Ground.register_converter env converter
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
index 4a7f75404698ceb723de8b98028a1fcce513e116..fa4cd42d3038c849ef084502c515955ec7fb0e1a 100644
--- a/src_colibri2/theories/LRA/dom_interval.mli
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -18,14 +18,28 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-val init: Egraph.wt -> unit
+val init : Egraph.wt -> unit
 
-module D: sig type t end
+module D : sig
+  type t
+
+  type is_comparable = Gt | Lt | Ge | Le | Eq | Uncomparable
+end
 
 val dom : D.t Dom.Kind.t
 
-val is_zero_or_positive: _ Egraph.t -> Node.t -> bool
-val is_not_zero: _ Egraph.t -> Node.t -> bool
-val is_strictly_positive: _ Egraph.t -> Node.t -> bool
-val is_strictly_negative: _ Egraph.t -> Node.t -> bool
-val is_integer: _ Egraph.t -> Node.t -> bool
+val is_zero_or_positive : _ Egraph.t -> Node.t -> bool
+
+val is_not_zero : _ Egraph.t -> Node.t -> bool
+
+val is_strictly_positive : _ Egraph.t -> Node.t -> bool
+
+val is_strictly_negative : _ Egraph.t -> Node.t -> bool
+
+val is_integer : _ Egraph.t -> Node.t -> bool
+
+val zero_is : _ Egraph.t -> Node.t -> D.is_comparable
+
+val assume_positive : Egraph.wt -> Node.t -> unit
+
+val assume_negative : Egraph.wt -> Node.t -> unit
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 73396151e323e93dc4f721a317d8306806b37be4..4b22129c30aeca2db6aef6e80bbd913c676444ec 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -34,7 +34,10 @@ end
 
 module ThE = ThTerm.Register (T)
 
-let node_of_polynome t = ThE.node (ThE.index t)
+let node_of_polynome p =
+  match Polynome.is_cst p with
+  | None -> ThE.node (ThE.index p)
+  | Some q -> RealValue.node (RealValue.index q)
 
 include Pivot.Total (struct
   include Polynome
@@ -55,10 +58,14 @@ include Pivot.Total (struct
 
   let set d cl p =
     match is_one_node p with
-    | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
+    | None -> (
+        match Polynome.is_cst p with
+        | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
+        | Some q ->
+            Egraph.set_value d cl (RealValue.nodevalue (RealValue.index q)))
     | Some cl' -> Egraph.merge d cl cl'
 
-  let solve p1 p2 =
+  let solve p1 p2 : _ Pivot.solve_total =
     let diff = sub p1 p2 in
     (* 0 = other - repr = p1 - p2 = diff *)
     Debug.dprintf2 debug "[Arith] @[solve 0=%a@]" pp diff;
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 63fd43051d9d8bf28a5be8b9b6666eb63af1b1c2..be0975b674dc60581170c8cb16c5f036c9ed3bfa 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -27,30 +27,65 @@ let debug =
     ~desc:"for the arithmetic theory of product of variable" "LRA.product"
 
 module T = struct
-  include Product
+  module T = struct
+    type t = { abs : Product.t; sign : Sign_product.t }
+    [@@deriving eq, ord, hash, show]
+
+    let name = "SARITH_PROD"
+  end
 
-  let name = "SARITH_PROD"
+  include T
+  include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
 end
 
 module ThE = ThTerm.Register (T)
 
-let node_of_product t = ThE.node (ThE.index t)
+let node_of_product abs sign =
+  let t = { T.abs; sign } in
+  ThE.node (ThE.index t)
+
+let set d cl abs sign =
+  if Sign_product.equal Sign_product.zero sign then
+    Egraph.merge d cl RealValue.zero
+  else
+    let aux () =
+      Egraph.set_thterm d cl (ThE.thterm (ThE.index { abs; sign }))
+    in
+    match Product.is_one_node abs with
+    | None -> aux ()
+    | Some cl' -> (
+        match Sign_product.is_one_node sign with
+        | Some cl'' when Egraph.is_equal d cl' cl'' -> Egraph.merge d cl cl'
+        | _ -> aux ())
+
+module rec SolveAbs : sig
+  val assume_equality : Egraph.wt -> Node.t -> Product.t -> unit
+
+  val init : Egraph.wt -> unit
+
+  val get_repr : _ Egraph.t -> Node.t -> Product.t option
 
-include Pivot.WithUnsolved (struct
-  let name = "ARITH_PROD"
+  val iter_eqs : _ Egraph.t -> Node.t -> f:(Product.t -> unit) -> unit
+
+  val attach_repr_change :
+    _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+
+  val attach_eqs_change :
+    _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+end = Pivot.WithUnsolved (struct
+  let name = "ARITH_ABS"
 
   include Product
 
-  let of_one_node n = Product.monome n Q.one
+  let pp fmt p = Fmt.pf fmt "|%a|" pp p
+
+  let of_one_node _ n = Product.monome n Q.one
 
   let subst p n q =
     let p, c = subst p n q in
     if Q.is_zero c then None else Some p
 
-  let set d cl p =
-    match Product.is_one_node p with
-    | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
-    | Some cl' -> Egraph.merge d cl cl'
+  let set d cl abs = SolveSign.iter_eqs d cl ~f:(fun sign -> set d cl abs sign)
 
   type data = Q.t
 
@@ -78,7 +113,8 @@ include Pivot.WithUnsolved (struct
 
   let attach_info_change d f = Events.attach_any_dom d Dom_interval.dom f
 
-  let solve (_, notz1, unk1, p1) (_, notz2, unk2, p2) =
+  let solve (_, notz1, unk1, p1) (_, notz2, unk2, p2) :
+      _ Pivot.solve_with_unsolved =
     let exception Solved of Node.t * Product.t in
     try
       (if
@@ -108,46 +144,118 @@ include Pivot.WithUnsolved (struct
         if Q.equal q Q.one && not (Node.M.mem n unk2) then
           let p = Product.div p2 (Product.remove n p1) in
           raise (Solved (n, p)));
-      None
-    with Solved (n, p) -> Some (n, p)
+      Unsolved
+    with Solved (n, p) -> Subst (n, p)
+end)
+
+and SolveSign : sig
+  val assume_equality : Egraph.wt -> Node.t -> Sign_product.t -> unit
+
+  val init : Egraph.wt -> unit
+
+  val get_repr : _ Egraph.t -> Node.t -> Sign_product.t option
+
+  val iter_eqs : _ Egraph.t -> Node.t -> f:(Sign_product.t -> unit) -> unit
+
+  val attach_repr_change :
+    _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+
+  val attach_eqs_change :
+    _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+
+  val reshape :
+    Egraph.wt -> Node.t -> f:(Sign_product.t -> Sign_product.t) -> unit
+end = Pivot.WithUnsolved (struct
+  let name = "ARITH_SIGN"
+
+  include Sign_product
+
+  let of_one_node d n =
+    if Dom_interval.is_not_zero d n then Sign_product.of_one_node_non_zero n
+    else Sign_product.of_one_node n
+
+  let attach_info_change d f = Events.attach_any_dom d Dom_interval.dom f
+
+  let set d cl sign = SolveAbs.iter_eqs d cl ~f:(fun abs -> set d cl abs sign)
+
+  type info = Sign_product.presolve * Sign_product.t
+
+  let info _ m : info = (Sign_product.presolve m, m)
+
+  let solve ((info1, p1) : info) ((_, p2) : info) : _ Pivot.solve_with_unsolved
+      =
+    match info1 with
+    | Zero -> Unsolved
+    | NonZero -> (
+        (* all non_zero *)
+        let p = Sign_product.mul p2 p1 in
+        match Sign_product.extract p with
+        | Plus_one -> AlreadyEqual
+        | Minus_one -> Contradiction
+        | Zero -> Contradiction
+        | Var (n, p) -> Subst (n, p)
+        | NoNonZero -> Unsolved)
+    | OneNonZero n ->
+        if not (Node.M.mem n (Sign_product.nodes p2)) then
+          let p = Sign_product.mul p2 (Sign_product.remove n p1) in
+          Subst (n, p)
+        else Unsolved
+    | Other -> Unsolved
 end)
 
 let factorize res a coef b d _ =
-  match (get_repr d a, get_repr d b) with
-  | Some pa, Some pb ->
-      let common =
-        Node.M.inter
-          (fun _ a b -> Q.none_zero (Q.min (Q.floor a) (Q.floor b)))
-          pa.poly pb.poly
-      in
-      if not (Node.M.is_empty common) then (
-        let cst, l =
-          List.fold_left
-            (fun (cst, acc) (p, v) ->
-              let p =
-                Product.of_map
-                  (Node.M.diff
-                     (fun _ a b -> Q.none_zero (Q.sub a b))
-                     p.Product.poly common)
-              in
-              match Product.classify p with
-              | ONE -> (Q.add v cst, acc)
-              | NODE n -> (cst, (n, v) :: acc)
-              | PRODUCT ->
-                  let n = node_of_product p in
-                  Egraph.register d n;
-                  (cst, (n, v) :: acc))
-            (Q.zero, [])
-            [ (pa, Q.one); (pb, coef) ]
-        in
-        let p = Polynome.of_list cst l in
-        let n = Dom_polynome.node_of_polynome p in
-        Debug.dprintf10 debug "[Factorize] %a = %a + %a * %a into %a" Node.pp
-          res Node.pp a Q.pp coef Node.pp b Polynome.pp p;
-        Egraph.register d n;
-        Dom_polynome.assume_equality d n p;
-        assume_equality d res (Product.of_map (Node.M.add n Q.one common)))
-  | _ -> ()
+  if
+    (not (Egraph.is_equal d RealValue.zero res))
+    && (not (Egraph.is_equal d RealValue.zero a))
+    && not (Egraph.is_equal d RealValue.zero b)
+  then
+    match
+      ( SolveAbs.get_repr d a,
+        SolveAbs.get_repr d b,
+        SolveSign.get_repr d a,
+        SolveSign.get_repr d b )
+    with
+    | Some pa, Some pb, Some sa, Some sb ->
+        let common_abs = Product.common pa pb in
+        let common_sign = Sign_product.common sa sb in
+        if
+          not
+            (Product.equal Product.one common_abs
+            && Sign_product.equal Sign_product.one common_sign)
+        then (
+          let cst, l =
+            List.fold_left
+              (fun (cst, acc) (abs, sign, v) ->
+                let abs = Product.div abs common_abs in
+                let sign = Sign_product.mul sign common_sign in
+                match (Product.classify abs, Sign_product.classify sign) with
+                | ONE, PLUS_ONE -> (Q.add v cst, acc)
+                | ONE, MINUS_ONE -> (Q.sub v cst, acc)
+                | NODE n, NODE n' when Egraph.is_equal d n n' ->
+                    (cst, (n, v) :: acc)
+                | _ ->
+                    let n = node_of_product abs sign in
+                    Egraph.register d n;
+                    (cst, (n, v) :: acc))
+              (Q.zero, [])
+              [ (pa, sa, Q.one); (pb, sb, coef) ]
+          in
+          let p = Polynome.of_list cst l in
+          let n = Dom_polynome.node_of_polynome p in
+          let pp_coef fmt coef =
+            if Q.equal Q.one coef then Fmt.pf fmt "+" else Fmt.pf fmt "-"
+          in
+          Debug.dprintf10 debug "[Factorize] %a = %a %a %a into %a" Node.pp res
+            Node.pp a pp_coef coef Node.pp b Polynome.pp p;
+          Egraph.register d n;
+          Dom_polynome.assume_equality d n p;
+          let abs = Product.mul (Product.monome n Q.one) common_abs in
+          let sign =
+            Sign_product.mul (Sign_product.of_one_node n) common_sign
+          in
+          SolveAbs.assume_equality d res abs;
+          SolveSign.assume_equality d res sign)
+    | _ -> ()
 
 (** {2 Initialization} *)
 let converter d (f : Ground.t) =
@@ -158,33 +266,52 @@ let converter d (f : Ground.t) =
       let a, b = IArray.extract2_exn args in
       reg a;
       reg b;
-      assume_equality d res (Product.of_list [ (a, Q.one); (b, Q.one) ])
+      SolveAbs.assume_equality d res
+        (Product.of_list [ (a, Q.one); (b, Q.one) ]);
+      SolveSign.assume_equality d res
+        (Sign_product.mul
+           (Sign_product.of_one_node a)
+           (Sign_product.of_one_node b))
   | { app = { builtin = Expr.Div }; tyargs = []; args; _ } ->
       let num, den = IArray.extract2_exn args in
       reg num;
       reg den;
       Daemon.attach_dom d den Dom_interval.dom (fun d _ ->
-          if Dom_interval.is_not_zero d den then
-            assume_equality d num
-              (Product.of_list [ (res, Q.one); (den, Q.one) ]))
+          if Dom_interval.is_not_zero d den then (
+            (* num = res * den *)
+            SolveAbs.assume_equality d num
+              (Product.of_list [ (res, Q.one); (den, Q.one) ]);
+            SolveSign.assume_equality d num
+              (Sign_product.mul
+                 (Sign_product.of_one_node res)
+                 (Sign_product.of_one_node den))))
   | { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
       let a, b = IArray.extract2_exn args in
       reg a;
       reg b;
       List.iter
-        (fun node -> attach_repr_change d ~node (factorize res a Q.one b))
+        (fun node ->
+          SolveAbs.attach_repr_change d ~node (factorize res a Q.one b);
+          SolveSign.attach_repr_change d ~node (factorize res a Q.one b))
         [ a; b ]
   | { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
       let a, b = IArray.extract2_exn args in
       reg a;
       reg b;
       List.iter
-        (fun node -> attach_repr_change d ~node (factorize res a Q.minus_one b))
+        (fun node ->
+          SolveAbs.attach_repr_change d ~node (factorize res a Q.minus_one b);
+          SolveSign.attach_repr_change d ~node (factorize res a Q.minus_one b))
         [ a; b ]
   | _ -> ()
 
+let reshape_non_zero d n =
+  let q = Sign_product.of_one_node_non_zero n in
+  SolveSign.reshape d n ~f:(fun p ->
+      Option.value ~default:p (Sign_product.subst p n q))
+
 let init env =
-  init env;
+  SolveAbs.init env;
   Dom_polynome.attach_repr_change env (fun d n ->
       match Dom_polynome.get_repr d n with
       | None -> ()
@@ -195,9 +322,9 @@ let init env =
               let p1 = Product.of_list [ (cl, Q.one) ] in
               Debug.dprintf4 debug "[Polynome->Product] propagate %a is %a"
                 Node.pp n Node.pp cl;
-              assume_equality d n p1));
-  attach_eqs_change env (fun d n ->
-      iter_eqs d n ~f:(fun p ->
+              SolveAbs.assume_equality d n p1));
+  SolveAbs.attach_eqs_change env (fun d n ->
+      SolveAbs.iter_eqs d n ~f:(fun p ->
           if Node.M.is_num_elt 1 p.poly then
             let cl, q = Node.M.choose p.poly in
             if Q.equal q Q.one then (
@@ -205,4 +332,21 @@ let init env =
               Debug.dprintf4 debug "[Product->Polynome] propagate %a is %a"
                 Node.pp n Node.pp cl;
               Dom_polynome.assume_equality d n p1)));
+  DaemonWithFilter.attach_any_dom env Dom_interval.dom (fun d n ->
+      match Dom_interval.zero_is d n with
+      | Eq -> Some (fun d -> SolveSign.assume_equality d n Sign_product.zero)
+      | Lt -> Some (fun d -> SolveSign.assume_equality d n Sign_product.one)
+      | Gt ->
+          Some (fun d -> SolveSign.assume_equality d n Sign_product.minus_one)
+      | Le | Ge | Uncomparable ->
+          if Dom_interval.is_not_zero d n then
+            Some (fun d -> reshape_non_zero d n)
+          else None);
+  SolveSign.attach_eqs_change env (fun d n ->
+      SolveSign.iter_eqs d n ~f:(fun s ->
+          match Sign_product.classify s with
+          | Sign_product.PLUS_ONE -> Dom_interval.assume_positive d n
+          | Sign_product.MINUS_ONE -> Dom_interval.assume_negative d n
+          | Sign_product.ZERO -> Egraph.merge d n RealValue.zero
+          | _ -> ()));
   Ground.register_converter env converter
diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli
index 05faec2a015f19ad0ba96957d6361d25207e4656..3b2f1ac3c9651de225e5acc6f72582c879efc8cb 100644
--- a/src_colibri2/theories/LRA/dom_product.mli
+++ b/src_colibri2/theories/LRA/dom_product.mli
@@ -18,10 +18,16 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-val assume_equality : Egraph.wt -> Node.t -> Product.t -> unit
+(* val assume_equality : Egraph.wt -> Node.t -> Product.t -> unit *)
 
-val node_of_product : Product.t -> Node.t
+val node_of_product : Product.t -> Sign_product.t -> Node.t
 
-val get_repr : _ Egraph.t -> Node.t -> Product.t option
+module SolveAbs : sig
+  val get_repr : _ Egraph.t -> Node.t -> Product.t option
+end
+
+module SolveSign : sig
+  val get_repr : _ Egraph.t -> Node.t -> Sign_product.t option
+end
 
 val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 0ff795e9cee0f7ea421ec19ef4cf7f0370dd61b6..7f4daa6c18f9452d9d4bbde1bb3269430a2ed407 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -43,54 +43,59 @@ let divide d (p : Polynome.t) =
     let l =
       List.fold_left
         (fun acc (e, q) ->
-          match Dom_product.get_repr d e with
-          | None when Egraph.is_equal d RealValue.zero e -> acc
-          | None -> raise Exit
-          | Some p -> (p, q) :: acc)
+          match
+            ( Dom_product.SolveAbs.get_repr d e,
+              Dom_product.SolveSign.get_repr d e )
+          with
+          | None, _ when Egraph.is_equal d RealValue.zero e -> acc
+          | None, _ | _, None -> raise Exit
+          | Some abs, Some sign -> (abs, sign, q) :: acc)
         [] l
     in
-    Debug.dprintf4 debug "@[eq:%a@ %a@]" Polynome.pp p
-      Fmt.(list ~sep:(any "+") (using CCPair.swap (pair Q.pp Product.pp)))
-      l;
+    (* Debug.dprintf4 debug "@[eq:%a@ %a@]" Polynome.pp p
+     *   Fmt.(list ~sep:(any "+") (using CCPair.swap (pair Q.pp Product.pp)))
+     *   l; *)
     match l with
     | [] -> raise Exit
-    | (hd, _) :: _ ->
+    | (hd, __, _) :: _ ->
         let common =
           List.fold_left
-            (fun acc (p, _) ->
+            (fun acc (abs, _, _) ->
               Node.M.inter
                 (fun _ a b -> if Q.equal a b then Some a else None)
-                acc p.Product.poly)
+                acc abs.Product.poly)
             hd.Product.poly l
         in
-        let common, pos =
+        let common =
           Node.M.fold_left
-            (fun (acc, pos) n v ->
-              if Dom_interval.is_strictly_positive d n then
-                (Node.M.add n v acc, pos)
-              else if Dom_interval.is_strictly_negative d n then
-                (Node.M.add n v acc, not pos)
-              else (acc, pos))
-            (Node.M.empty, true) common
+            (fun acc abs v ->
+              if Dom_interval.is_not_zero d abs then Node.M.add abs v acc
+              else acc)
+            Node.M.empty common
         in
         if Node.M.is_empty common then raise Exit;
-        Debug.dprintf4 debug "[Fourier] found possible division: %a / %a"
-          Polynome.pp p (Node.M.pp Q.pp) common;
+        let common = Product.of_map common in
+        Debug.dprintf4 debug "[Fourier] found possible division: %a / |%a|"
+          Polynome.pp p Product.pp common;
         let cst, l =
           List.fold_left
-            (fun (cst, acc) (p, v) ->
-              let p = Product.of_map (Node.M.set_diff p.Product.poly common) in
-
-              let v = if pos then v else Q.neg v in
-              match Product.classify p with
-              | ONE -> (Q.add v cst, acc)
-              | NODE n -> (cst, (n, v) :: acc)
-              | PRODUCT ->
-                  let n = Dom_product.node_of_product p in
-                  (Q.add Q.one cst, (n, v) :: acc))
+            (fun (cst, acc) (abs, sign, v) ->
+              let abs = Product.div abs common in
+              let pos, sign = Sign_product.extract_cst sign in
+              let v =
+                match pos with Zero -> Q.zero | Pos -> v | Neg -> Q.neg v
+              in
+              match (Product.classify abs, Sign_product.classify sign) with
+              | _, MINUS_ONE -> assert false
+              | ONE, PLUS_ONE -> (Q.add v cst, acc)
+              | NODE n, NODE n' when Egraph.is_equal d n n' ->
+                  (cst, (n, v) :: acc)
+              | _ ->
+                  let n = Dom_product.node_of_product abs sign in
+                  (cst, (n, v) :: acc))
             (Q.zero, []) l
         in
-        Some (Polynome.of_list cst l, common, pos)
+        Some (Polynome.of_list cst l, common)
   with Exit -> None
 
 let delta d eq =
@@ -188,7 +193,7 @@ let make_equations d (eqs, vars) g =
           Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly )
       in
       match divide d p_non_norm with
-      | Some (p', _, _) ->
+      | Some (p', _) ->
           let p' = Dom_polynome.normalize d p' in
           ( add_eq d eqs p' bound_non_norm Ground.S.empty,
             Node.M.union_merge (fun _ _ _ -> Some ()) vars p'.Polynome.poly )
diff --git a/src_colibri2/theories/LRA/pivot.ml b/src_colibri2/theories/LRA/pivot.ml
index 76b0c8f419f80081ed2f55b85b32e86225e6ba2a..5d5be6e4959f8d95ba7397a88465d3ee2df10028 100644
--- a/src_colibri2/theories/LRA/pivot.ml
+++ b/src_colibri2/theories/LRA/pivot.ml
@@ -21,6 +21,12 @@
 let debug =
   Debug.register_info_flag ~desc:"for the normalization by pivoting" "LRA.pivot"
 
+type 'a solve_with_unsolved =
+  | AlreadyEqual
+  | Contradiction
+  | Unsolved
+  | Subst of Node.t * 'a
+
 module WithUnsolved (P : sig
   type t
 
@@ -28,7 +34,7 @@ module WithUnsolved (P : sig
 
   include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
 
-  val of_one_node : Node.t -> t
+  val of_one_node : _ Egraph.t -> Node.t -> t
 
   val is_one_node : t -> Node.t option
 
@@ -47,7 +53,7 @@ module WithUnsolved (P : sig
   val attach_info_change :
     Egraph.wt -> (Egraph.rt -> Node.t -> Events.enqueue) -> unit
 
-  val solve : info -> info -> (Node.t * t) option
+  val solve : info -> info -> t solve_with_unsolved
 
   val set : Egraph.wt -> Node.t -> t -> unit
 end) : sig
@@ -64,6 +70,8 @@ end) : sig
 
   val attach_eqs_change :
     _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+
+  val reshape : Egraph.wt -> Node.t -> f:(P.t -> P.t) -> unit
 end = struct
   type t = {
     repr : P.t;
@@ -104,10 +112,11 @@ end = struct
                         is the reason why this module doesn't specifically wait for
                         representative change *)
                     Egraph.set_dom d dom used
-                      { repr = P.of_one_node used; eqs = P.S.empty };
+                      { repr = P.of_one_node d used; eqs = P.S.empty };
                     Some (Node.S.of_list [ cl'; used ])
                 | Some p ->
-                    assert (P.equal (P.of_one_node used) p.repr);
+                    assert (
+                      Option.equal Node.equal (P.is_one_node p.repr) (Some used));
                     assert false))
           used_in_poly d used)
       new_cls
@@ -150,7 +159,7 @@ end = struct
     P.normalize p ~f:(fun cl ->
         let cl = Egraph.find d cl in
         match Egraph.get_dom d dom cl with
-        | None -> P.of_one_node cl
+        | None -> P.of_one_node d cl
         | Some p -> p.repr)
 
   module Th = struct
@@ -162,12 +171,6 @@ end = struct
       | Some v', Some v -> equal v' v
       | _ -> false
 
-    let norm_dom cl = function
-      | None ->
-          let r = P.of_one_node cl in
-          { repr = r; eqs = P.S.empty }
-      | Some p -> p
-
     let add_itself d cl norm =
       add_used_t d cl norm;
       Egraph.set_dom d dom cl norm
@@ -254,7 +257,7 @@ end = struct
           add_used_product d cl (P.nodes eq);
           set_poly d cl p [ eq ]
       | Some p ->
-          assert (P.equal p.repr (P.of_one_node cl));
+          assert (Option.equal Node.equal (P.is_one_node p.repr) (Some cl));
           subst_doms d cl eq;
           assert (
             P.equal eq (Base.Option.value_exn (Egraph.get_dom d dom cl)).repr);
@@ -267,8 +270,10 @@ end = struct
       let criteria i1 i2 =
         let aux i1 i2 =
           match P.solve i1 i2 with
-          | None -> ()
-          | Some (n, p) -> raise (Solved (n, p))
+          | AlreadyEqual -> ()
+          | Contradiction -> Egraph.contradiction d
+          | Unsolved -> ()
+          | Subst (n, p) -> raise (Solved (n, p))
         in
         aux i1 i2;
         aux i2 i1
@@ -301,11 +306,31 @@ end = struct
         P.S.iter f p.eqs
 
   let assume_equality d n (p : P.t) =
+    Debug.dprintf5 debug "[Pivot %s] assume %a = %a" P.name Node.pp n P.pp p;
     let n = Egraph.find d n in
     let p = norm_product d p in
     Th.merge_one_new_eq d n p
 
-  module ChangePos = struct
+  let reshape d cl ~(f : P.t -> P.t) =
+    match Node.HC.find used_in_poly d cl with
+    | exception Not_found -> ()
+    | b ->
+        Node.S.iter
+          (fun cl' ->
+            match Egraph.get_dom d dom cl' with
+            | None -> assert false (* absurd: can't be used and absent *)
+            | Some q ->
+                let eqs =
+                  P.S.fold (fun p acc -> P.S.add (f p) acc) q.eqs P.S.empty
+                in
+                let q' = { repr = f q.repr; eqs } in
+                Egraph.set_dom d dom cl' q';
+                let l = Th.part d (q'.repr :: P.S.elements q'.eqs) in
+                let l = Base.List.cartesian_product l l in
+                ignore (Th.solve d l))
+          b
+
+  module ChangeInfo = struct
     type runable = Node.S.t
 
     let print_runable = Node.S.pp
@@ -336,9 +361,9 @@ end = struct
           | None -> Events.EnqAlready)
   end
 
-  let () = Events.register (module ChangePos)
+  let () = Events.register (module ChangeInfo)
 
-  let init d = ChangePos.init d
+  let init d = ChangeInfo.init d
 
   let attach_eqs_change d ?node f =
     match node with
diff --git a/src_colibri2/theories/LRA/pivot.mli b/src_colibri2/theories/LRA/pivot.mli
index 72186b9c1736954ff30113ededa139fe7080a552..54857e51a6b6b16fdd635408ee0afb1fde1b6c21 100644
--- a/src_colibri2/theories/LRA/pivot.mli
+++ b/src_colibri2/theories/LRA/pivot.mli
@@ -20,6 +20,12 @@
 
 (** Normalization of equations generic in the shape of the terms *)
 
+type 'a solve_with_unsolved =
+  | AlreadyEqual
+  | Contradiction
+  | Unsolved
+  | Subst of Node.t * 'a
+
 module WithUnsolved (P : sig
   type t
   (** Normalizable terms *)
@@ -28,7 +34,7 @@ module WithUnsolved (P : sig
 
   include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
 
-  val of_one_node : Node.t -> t
+  val of_one_node : _ Egraph.t -> Node.t -> t
   (** Build a value that represent one node *)
 
   val is_one_node : t -> Node.t option
@@ -36,7 +42,7 @@ module WithUnsolved (P : sig
 
   val subst : t -> Node.t -> t -> t option
   (** [subst p n q] substitute [n] by [q] in [p], if [n] is not in [p] None is
-        returned, otherwise the result of the substitution is returned *)
+      returned, otherwise the substitution is returned *)
 
   val normalize : t -> f:(Node.t -> t) -> t
   (** [norm p ~f] normalize [p] using [f] *)
@@ -59,9 +65,9 @@ module WithUnsolved (P : sig
        used for the computation of [info] changed. All unsolved equation which
        contains, [nodes t], the given node will be looked again. *)
 
-  val solve : info -> info -> (Node.t * t) option
+  val solve : info -> info -> t solve_with_unsolved
   (** [solve t1 t2] solve the equation [t1 = t2] by returning a substitution.
-        Return None if the equation can't be yet solved *)
+        Return Unsolved if the equation can't be yet solved *)
 
   val set : Egraph.wt -> Node.t -> t -> unit
   (** Called a new term equal to this node is found *)
@@ -81,6 +87,11 @@ end) : sig
 
   val attach_eqs_change :
     _ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+
+  val reshape : Egraph.wt -> Node.t -> f:(P.t -> P.t) -> unit
+  (** Apply the given function to all the normalized form which contains this node.
+      The resulting normalized form should contain the same or less nodes than before.
+  *)
 end
 
 type 'a solve_total = AlreadyEqual | Contradiction | Subst of Node.t * 'a
diff --git a/src_colibri2/theories/LRA/product.ml b/src_colibri2/theories/LRA/product.ml
index c971e576b0faca9c954ba11e49eb8ac4bb2630ca..87cef75a21c1dea5ab8e0afbcf0bfcbce4a64eb4 100644
--- a/src_colibri2/theories/LRA/product.ml
+++ b/src_colibri2/theories/LRA/product.ml
@@ -22,8 +22,7 @@ open Colibri2_popop_lib
 open Colibri2_core
 
 module T = struct
-  type t = { (* cst : Q.t; *) poly : Q.t Node.M.t}
-  [@@deriving eq,ord,hash]
+  type t = { (* cst : Q.t; *) poly : Q.t Node.M.t } [@@deriving eq, ord, hash]
 
   let pp_exposant fmt q =
     if Z.equal q.Q.den Z.one && Z.fits_int q.Q.num then
@@ -48,12 +47,12 @@ module T = struct
     else
       Fmt.pf fmt "@[%a@]"
         (* print_not_one v.cst *)
-        Fmt.(iter_bindings Node.M.iter (pair ~sep:nop Node.pp pp_exposant)) v.poly
-
+        Fmt.(iter_bindings Node.M.iter (pair ~sep:nop Node.pp pp_exposant))
+        v.poly
 end
 
 include T
-include Popop_stdlib.MkDatatype(T)
+include Popop_stdlib.MkDatatype (T)
 
 (** different invariant *)
 
@@ -61,48 +60,45 @@ let invariant p =
   (* not (Q.equal p.cst Q.zero && Node.M.is_empty p.poly) && *)
   Node.M.for_all (fun _ q -> not (Q.equal q Q.zero)) p.poly
 
-(** constructor *)
 (* let cst q = assert (not (Q.equal q Q.zero)); {cst = q; poly = Node.M.empty}
  * (\* let zero = cst Q.zero *\) *)
+
+(** constructor *)
 let one = { poly = Node.M.empty }
 (*
  * let is_cst p = if Node.M.is_empty p.poly then Some p.cst else None
  * (\* let is_zero p = Q.equal p.cst Q.zero && Node.M.is_empty p.poly *\)
  * let is_one p = Q.equal p.cst Q.one && Node.M.is_empty p.poly *)
 
-type extract = One  | Var of Q.t * Node.t * t
+type extract = One | Var of Q.t * Node.t * t
+
 let extract p =
-  if Node.M.is_empty p.poly then
-    (* if Q.equal p.cst Q.one then *) One
+  if Node.M.is_empty p.poly then (* if Q.equal p.cst Q.one then *) One
     (* else Cst p.cst *)
   else
-    let x,q = Shuffle.chooseb Node.M.choose Node.M.choose_rnd p.poly in
-    let p' = {(* p with  *)poly = Node.M.remove x p.poly} in
-    Var(q,x,p')
+    let x, q = Shuffle.chooseb Node.M.choose Node.M.choose_rnd p.poly in
+    let p' = { (* p with  *) poly = Node.M.remove x p.poly } in
+    Var (q, x, p')
 
 let remove n p = { poly = Node.M.remove n p.poly }
 
 type kind = ONE | NODE of Node.t | PRODUCT
+
 let classify p =
-  if Node.M.is_empty p.poly then
-    ONE
-  else
-  if Node.M.is_num_elt 1 p.poly then
-    let node,k = Node.M.choose p.poly in
-    if Q.equal Q.one k then NODE node
-    else PRODUCT
+  if Node.M.is_empty p.poly then ONE
+  else if Node.M.is_num_elt 1 p.poly then
+    let node, k = Node.M.choose p.poly in
+    if Q.equal Q.one k then NODE node else PRODUCT
   else PRODUCT
 
-
 let monome x c =
-  if Q.equal Q.zero c then one
-  else {poly = Node.M.singleton x c}
+  if Q.equal Q.zero c then one else { poly = Node.M.singleton x c }
 
-let is_one_node p = (** cst = 0 and one empty monome *)
+let is_one_node p =
+  (* cst = 0 and one empty monome *)
   if (* Q.equal Q.zero p.cst && *) Node.M.is_num_elt 1 p.poly then
-    let node,k = Node.M.choose p.poly in
-    if Q.equal Q.one k then Some node
-    else None
+    let node, k = Node.M.choose p.poly in
+    if Q.equal Q.one k then Some node else None
   else None
 
 (* let mult_cst c p1 =
@@ -113,9 +109,9 @@ let power_cst c p1 =
   if Q.equal Q.zero c then one
   else if Q.equal Q.one c then p1
   else
-  let poly_mult c m = Node.M.map (fun c1 -> Q.mul c c1) m in
-  if Q.equal Q.zero c then one
-  else {(* cst = Q.mul c p1.cst; *) poly = poly_mult c p1.poly}
+    let poly_mult c m = Node.M.map (fun c1 -> Q.mul c c1) m in
+    if Q.equal Q.zero c then one
+    else { (* cst = Q.mul c p1.cst; *) poly = poly_mult c p1.poly }
 
 (** Warning Node.M.union can be used only for defining an operation [op]
     that verifies [op 0 p = p] and [op p 0 = p] *)
@@ -123,76 +119,88 @@ let mul p1 p2 =
   let poly_add m1 m2 =
     Node.M.union (fun _ c1 c2 -> Q.none_zero (Q.add c1 c2)) m1 m2
   in
-  {(* cst = Q.mul p1.cst p2.cst; *) poly = poly_add p1.poly p2.poly}
+  { (* cst = Q.mul p1.cst p2.cst; *) poly = poly_add p1.poly p2.poly }
 
 let div p1 p2 =
   let poly_sub m1 m2 =
-    Node.M.union_merge (fun _ c1 c2 ->
-      match c1 with
-      | None -> Some (Q.neg c2)
-      | Some c1 -> Q.none_zero (Q.sub c1 c2))
-      m1 m2 in
-  {(* cst = Q.div p1.cst p2.cst; *) poly = poly_sub p1.poly p2.poly}
+    Node.M.union_merge
+      (fun _ c1 c2 ->
+        match c1 with
+        | None -> Some (Q.neg c2)
+        | Some c1 -> Q.none_zero (Q.sub c1 c2))
+      m1 m2
+  in
+  { (* cst = Q.div p1.cst p2.cst; *) poly = poly_sub p1.poly p2.poly }
 
 let x_m_yc p1 p2 c =
   assert (not (Q.equal c Q.zero));
   let f a b = Q.add a (Q.mul c b) in
   let poly m1 m2 =
-    Node.M.union_merge (fun _ c1 c2 ->
-      match c1 with
-      | None -> Some (Q.mul c c2)
-      | Some c1 -> Q.none_zero (f c1 c2))
-      m1 m2 in
-  {(* cst = Q.mul p1.cst (Q. p2.cst; *) poly = poly p1.poly p2.poly}
-
+    Node.M.union_merge
+      (fun _ c1 c2 ->
+        match c1 with
+        | None -> Some (Q.mul c c2)
+        | Some c1 -> Q.none_zero (f c1 c2))
+      m1 m2
+  in
+  { (* cst = Q.mul p1.cst (Q. p2.cst; *) poly = poly p1.poly p2.poly }
 
 let xc_m_yc p1 c1 p2 c2 =
   let c1_iszero = Q.equal c1 Q.zero in
   let c2_iszero = Q.equal c2 Q.zero in
   if c1_iszero && c2_iszero then one
-  else if c1_iszero
-  then p2
-  else if c2_iszero
-  then p1
+  else if c1_iszero then p2
+  else if c2_iszero then p1
   else
     let f e1 e2 = Q.add (Q.mul c1 e1) (Q.mul c2 e2) in
     let poly m1 m2 =
-      Node.M.merge (fun _ e1 e2 ->
-          match e1, e2 with
+      Node.M.merge
+        (fun _ e1 e2 ->
+          match (e1, e2) with
           | None, None -> assert false
           | None, Some e2 -> Some (Q.mul c2 e2)
           | Some e1, None -> Some (Q.mul c1 e1)
-          | Some e1, Some e2 ->
-            Q.none_zero (f e1 e2))
-        m1 m2 in
-    {(* cst = f p1.cst p2.cst; *) poly = poly p1.poly p2.poly}
+          | Some e1, Some e2 -> Q.none_zero (f e1 e2))
+        m1 m2
+    in
+    { (* cst = f p1.cst p2.cst; *) poly = poly p1.poly p2.poly }
 
 let subst_node p x y =
-  let poly,qo = Node.M.find_remove x p.poly in
+  let poly, qo = Node.M.find_remove x p.poly in
   match qo with
-  | None -> p, Q.zero
+  | None -> (p, Q.zero)
   | Some q ->
-    let poly = Node.M.change (function
-        | None -> qo
-        | Some q' -> Q.none_zero (Q.add q q')
-      ) y poly in
-    {poly}, q
+      let poly =
+        Node.M.change
+          (function None -> qo | Some q' -> Q.none_zero (Q.add q q'))
+          y poly
+      in
+      ({ poly }, q)
 
 let subst p x s =
-  let poly,q = Node.M.find_remove x p.poly in
-  match q with
-  | None -> p, Q.zero
-  | Some q -> x_m_yc {poly} s q, q
+  let poly, q = Node.M.find_remove x p.poly in
+  match q with None -> (p, Q.zero) | Some q -> (x_m_yc { poly } s q, q)
 
 let fold f acc p = Node.M.fold_left f acc p.poly
+
 let iter f p = Node.M.iter f p.poly
 
-let of_list (* cst  *)l =
-  let fold acc (node,q) = Node.M.change (function
-      | None -> Some q
-      | Some q' -> Q.none_zero (Q.add q q')) node acc in
-  {(* cst; *)poly= List.fold_left fold Node.M.empty l}
+let of_list (* cst  *) l =
+  let fold acc (node, q) =
+    Node.M.change
+      (function None -> Some q | Some q' -> Q.none_zero (Q.add q q'))
+      node acc
+  in
+  { (* cst; *) poly = List.fold_left fold Node.M.empty l }
 
 let of_map m =
-  assert ( Node.M.for_all (fun _ v -> Q.sign v <> 0) m );
+  assert (Node.M.for_all (fun _ v -> Q.sign v <> 0) m);
   { poly = m }
+
+let common pa pb =
+  {
+    poly =
+      Node.M.inter
+        (fun _ a b -> Q.none_zero (Q.min (Q.floor a) (Q.floor b)))
+        pa.poly pb.poly;
+  }
diff --git a/src_colibri2/theories/LRA/product.mli b/src_colibri2/theories/LRA/product.mli
index dfca11762cac524ef13d534df3469072cad08f74..32c5916cf3f6f2a293eba5fe6227ca6259bb2fc2 100644
--- a/src_colibri2/theories/LRA/product.mli
+++ b/src_colibri2/theories/LRA/product.mli
@@ -19,45 +19,55 @@
 (*************************************************************************)
 
 open Colibri2_popop_lib
+
 open Colibri2_core
 (** Polynome *)
 
-type t = private { (* cst : Q.t;  *)poly : Q.t Node.M.t}
+type t = private { (* cst : Q.t;  *) poly : Q.t Node.M.t }
+
 include Popop_stdlib.Datatype with type t := t
 
-val invariant: t -> bool
+val invariant : t -> bool
 
-val one: t
+val one : t
 
-val monome: Node.t -> Q.t  -> t
-val is_one_node: t -> Node.t option
+val monome : Node.t -> Q.t -> t
 
-val remove: Node.t -> t -> t
+val is_one_node : t -> Node.t option
+
+val remove : Node.t -> t -> t
 
 type extract =
-  | One            (** p = 1 *)
-  | Var of Q.t * Node.t * t (** p = x^q * p' *)
+  | One  (** p = 1 *)
+  | Var of Q.t * Node.t * t  (** p = x^q * p' *)
 
 val extract : t -> extract
 
 type kind = ONE | NODE of Node.t | PRODUCT
+
 val classify : t -> kind
 
-val power_cst: Q.t -> t -> t
+val power_cst : Q.t -> t -> t
 
-val of_list: (Node.t * Q.t) list -> t
+val of_list : (Node.t * Q.t) list -> t
 
-val mul: t -> t -> t
-val div: t -> t -> t
+val mul : t -> t -> t
 
-val x_m_yc: t -> t -> Q.t -> t
+val div : t -> t -> t
 
-val xc_m_yc: t -> Q.t -> t -> Q.t -> t
+val x_m_yc : t -> t -> Q.t -> t
 
-val subst: t -> Node.t -> t -> t * Q.t
-val subst_node: t -> Node.t -> Node.t -> t * Q.t
+val xc_m_yc : t -> Q.t -> t -> Q.t -> t
 
-val fold: ('a -> Node.t -> Q.t -> 'a) -> 'a -> t -> 'a
-val iter: (Node.t -> Q.t -> unit) -> t -> unit
+val subst : t -> Node.t -> t -> t * Q.t
+
+val subst_node : t -> Node.t -> Node.t -> t * Q.t
+
+val fold : ('a -> Node.t -> Q.t -> 'a) -> 'a -> t -> 'a
+
+val iter : (Node.t -> Q.t -> unit) -> t -> unit
 
 val of_map : Q.t Node.M.t -> t
+
+val common : t -> t -> t
+(** Return the common part *)
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 3e9d7818b661a8b79fdddfe80bd2c93b4a5cf989..1656d81f4ea5a9c13e81390053db86fb32490167 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -22,238 +22,298 @@ open Colibri2_core
 open Colibri2_popop_lib
 open Colibri2_stdlib.Std
 
-module RealValue = Value.Register(struct
-    include Q
-    let name = "Q"
-  end)
+module RealValue = Value.Register (struct
+  include Q
+
+  let name = "Q"
+end)
 
 include RealValue
 
-let () = Interp.Register.print_value_smt RealValue.key
-    (fun _ fmt v ->
-       let v = RealValue.value v in
-       if Z.equal v.den Z.one then
-         Z.pp_print fmt v.num
-       else
-         Fmt.pf fmt "(/ %a %a)" Z.pp_print v.num Z.pp_print v.den
-    )
+let () =
+  Interp.Register.print_value_smt RealValue.key (fun _ fmt v ->
+      let v = RealValue.value v in
+      if Z.equal v.den Z.one then Z.pp_print fmt v.num
+      else Fmt.pf fmt "(/ %a %a)" Z.pp_print v.num Z.pp_print v.den)
 
 let cst' c = index ~basename:(Format.asprintf "%aR" Q.pp c) c
+
 let cst c = node (cst' c)
 
 let zero = cst Q.zero
+
 let one = cst Q.one
 
 let int_sequence_without_zero =
   let open Base.Sequence.Generator in
   let rec loop i =
-    yield i >>= fun () -> yield (Z.neg i) >>= (fun () -> loop (Z.succ i))
+    yield i >>= fun () ->
+    yield (Z.neg i) >>= fun () -> loop (Z.succ i)
   in
   run (loop Z.one)
 
-let int_sequence =
-  Base.Sequence.shift_right int_sequence_without_zero Z.zero
+let int_sequence = Base.Sequence.shift_right int_sequence_without_zero Z.zero
 
 let init_ty d =
   Interp.Register.ty d (fun d ty ->
       match ty with
-      | {app={builtin = Expr.Int;_};_} ->
-        Some (Interp.SeqLim.map (Interp.SeqLim.of_seq d int_sequence)
-                ~f:(fun i -> nodevalue (cst' (Q.of_bigint i)))
-             )
-      | {app={builtin = Expr.Real;_};_} ->
-        let seq =
-          let open Interp.SeqLim in
-          let+ num = of_seq d int_sequence
-          and* den = of_seq d int_sequence_without_zero in
-          (Q.make num den)
-        in
-        let seq = Interp.SeqLim.unfold_with seq ~init:Q.S.empty
-            ~f:(fun s v -> if Q.S.mem v s then Skip s
-                 else Yield(nodevalue (cst' v),Q.S.add v s)) in
-        Some seq
+      | { app = { builtin = Expr.Int; _ }; _ } ->
+          Some
+            (Interp.SeqLim.map (Interp.SeqLim.of_seq d int_sequence)
+               ~f:(fun i -> nodevalue (cst' (Q.of_bigint i))))
+      | { app = { builtin = Expr.Real; _ }; _ } ->
+          let seq =
+            let open Interp.SeqLim in
+            let+ num = of_seq d int_sequence
+            and* den = of_seq d int_sequence_without_zero in
+            Q.make num den
+          in
+          let seq =
+            Interp.SeqLim.unfold_with seq ~init:Q.S.empty ~f:(fun s v ->
+                if Q.S.mem v s then Skip s
+                else Yield (nodevalue (cst' v), Q.S.add v s))
+          in
+          Some seq
       | _ -> None)
 
 module Check = struct
   let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+
   let compute_ground d t =
-      let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
-      let (!<) v = `Some (RealValue.nodevalue (RealValue.index v)) in
-      let (!<<) b =
-        let r = if b then Boolean.values_true else Boolean.values_false in
-        `Some r
-      in
-      match Ground.sem t with
-      | { app = {builtin = Expr.Coercion};
-          tyargs =
-            ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
-            | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
-            );
-          args } ->
+    let ( !> ) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
+    let ( !< ) v = `Some (RealValue.nodevalue (RealValue.index v)) in
+    let ( !<< ) b =
+      let r = if b then Boolean.values_true else Boolean.values_false in
+      `Some r
+    in
+    match Ground.sem t with
+    | {
+     app = { builtin = Expr.Coercion };
+     tyargs =
+       ( [
+           { app = { builtin = Expr.Int | Expr.Rat; _ }; _ };
+           { app = { builtin = Expr.Real; _ }; _ };
+         ]
+       | [
+           { app = { builtin = Expr.Int; _ }; _ };
+           { app = { builtin = Expr.Rat; _ }; _ };
+         ] );
+     args;
+    } ->
         let a = IArray.extract1_exn args in
-        !< (!> a)
-      | { app = {builtin = Expr.Integer s}; tyargs = []; args; ty = _ } ->
-        assert ( IArray.is_empty args);
-        !< (Q.of_string s)
-      | { app = {builtin = Expr.Decimal s}; tyargs = []; args; ty = _ } ->
-        assert ( IArray.is_empty args);
-        !< (Q.of_string_decimal s)
-      | { app = {builtin = Expr.Rational s}; tyargs = []; args; ty = _ } ->
-        assert ( IArray.is_empty args);
-        !< (Q.of_string_decimal s)
-      | { app = {builtin = Expr.Add}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !< (Q.add !>a !>b)
-      | { app = {builtin = Expr.Sub}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !< (Q.sub !>a !>b)
-      | { app = {builtin = Expr.Minus}; tyargs = []; args; ty = _ } ->
+        !<(!>a)
+    | { app = { builtin = Expr.Integer s }; tyargs = []; args; ty = _ } ->
+        assert (IArray.is_empty args);
+        !<(Q.of_string s)
+    | { app = { builtin = Expr.Decimal s }; tyargs = []; args; ty = _ } ->
+        assert (IArray.is_empty args);
+        !<(Q.of_string_decimal s)
+    | { app = { builtin = Expr.Rational s }; tyargs = []; args; ty = _ } ->
+        assert (IArray.is_empty args);
+        !<(Q.of_string_decimal s)
+    | { app = { builtin = Expr.Add }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<(Q.add !>a !>b)
+    | { app = { builtin = Expr.Sub }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<(Q.sub !>a !>b)
+    | { app = { builtin = Expr.Minus }; tyargs = []; args; ty = _ } ->
         let a = IArray.extract1_exn args in
-        !< (Q.neg !>a)
-      | { app = {builtin = Expr.Mul}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !< (Q.mul !>a !>b)
-      | { app = {builtin = Expr.Div}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        if Q.is_zero !>b then `Uninterp
-        else !< (Q.div !>a !>b)
-      | { app = {builtin = Expr.Lt}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !<< (Q.lt !>a !>b)
-      | { app = {builtin = Expr.Leq}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !<< (Q.leq !>a !>b)
-      | { app = {builtin = Expr.Gt}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !<< (Q.gt !>a !>b)
-      | { app = {builtin = Expr.Geq}; tyargs = []; args; ty = _ } ->
-        let a,b = IArray.extract2_exn args in
-        !<< (Q.geq !>a !>b)
-      | { app = {builtin = Expr.Floor}; tyargs = []; args; _ } ->
+        !<(Q.neg !>a)
+    | { app = { builtin = Expr.Mul }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<(Q.mul !>a !>b)
+    | { app = { builtin = Expr.Div }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        if Q.is_zero !>b then `Uninterp else !<(Q.div !>a !>b)
+    | { app = { builtin = Expr.Lt }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Q.lt !>a !>b)
+    | { app = { builtin = Expr.Leq }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Q.leq !>a !>b)
+    | { app = { builtin = Expr.Gt }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Q.gt !>a !>b)
+    | { app = { builtin = Expr.Geq }; tyargs = []; args; ty = _ } ->
+        let a, b = IArray.extract2_exn args in
+        !<<(Q.geq !>a !>b)
+    | { app = { builtin = Expr.Floor }; tyargs = []; args; _ } ->
         let a = IArray.extract1_exn args in
-        !< (Q.floor (!> a))
-      | _ -> `None
+        !<(Q.floor !>a)
+    | _ -> `None
 
   let init d =
     Interp.Register.check d (fun d t ->
-        let check r =
-          Value.equal r (interp d (Ground.node t))
-        in
+        let check r = Value.equal r (interp d (Ground.node t)) in
         match compute_ground d t with
         | `None -> NA
         | `Some v -> Interp.check_of_bool (check v)
-        | `Uninterp -> Interp.check_of_bool (Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.check d t)
-      );
+        | `Uninterp ->
+            Interp.check_of_bool
+              (Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain
+               .check d t));
     Interp.Register.compute d (fun d t ->
         match compute_ground d t with
         | `None -> NA
         | `Some v -> Value v
-        | `Uninterp -> Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.compute d t
-      )
+        | `Uninterp ->
+            Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain
+            .compute d t)
 
   let attach d g =
     let f d g =
       match compute_ground d g with
       | `None -> raise Impossible
       | `Some v -> Egraph.set_value d (Ground.node g) v
-      | `Uninterp -> Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate d g
+      | `Uninterp ->
+          Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain
+          .propagate d g
     in
     Interp.WatchArgs.create d f g
 end
 
-let wait_for_this_node_get_a_value d n =
-  Daemon.attach_value d n RealValue.key
+let wait_for_this_node_get_a_value d n = Daemon.attach_value d n RealValue.key
 
-      (** {2 Initialization} *)
-let converter d (f:Ground.t) =
+(** {2 Initialization} *)
+let converter d (f : Ground.t) =
   let r = Ground.node f in
   let reg n = Egraph.register d n in
-  let merge n = Egraph.register d n; Egraph.merge d r n in
+  let merge n =
+    Egraph.register d n;
+    Egraph.merge d r n
+  in
   let open Monad in
   let cmp cmp a b =
-        reg a; reg b;
-    attach d (
-      setv Boolean.dom r (let+ va = getv key a and+ vb = getv key b in cmp va vb)
-    );
+    reg a;
+    reg b;
+    attach d
+      (setv Boolean.dom r
+         (let+ va = getv key a and+ vb = getv key b in
+          cmp va vb))
   in
   let set = setv key in
   let get = getv key in
   match Ground.sem f with
-  | { app = {builtin = Expr.Coercion};
-      tyargs =
-        ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
-        | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
-        );
-      args } ->
-    let a = IArray.extract1_exn args in
-    merge a; Check.attach d f
-  | { app = {builtin = Expr.Integer s}; tyargs = []; args; _ } ->
-    assert ( IArray.is_empty args);
-    merge (cst (Q.of_string s))
-  | { app = {builtin = Expr.Decimal s}; tyargs = []; args; _ } ->
-assert ( IArray.is_empty args);
-    merge (cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Rational s}; tyargs = []; args; _ } ->
-assert ( IArray.is_empty args);
-    merge (cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    reg a; reg b; Check.attach d f;
-    attach d (
-      set r (let+ va = get a and+ vb = get b in Q.add va vb) &&
-      set a (let+ vb = get b and+ vr = get r in Q.sub vr vb) &&
-      set b (let+ va = get a and+ vr = get r in Q.sub vr va)
-    );
-  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    reg a; reg b; Check.attach d f;
-    attach d (
-      set r (let+ va = get a and+ vb = get b in Q.sub va vb) &&
-      set a (let+ vb = get b and+ vr = get r in Q.add vr vb) &&
-      set b (let+ va = get a and+ vr = get r in Q.sub va vr)
-    )
-  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } ->
-  let a,b = IArray.extract2_exn args in
-  reg a; reg b; Check.attach d f;
-  attach d (
-    set r (let+ va = get a and+ vb = get b in Q.mul va vb) &&
-    set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.div vr vb)) &&
-    set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
-  )
-  | { app = {builtin = Expr.Div}; tyargs = []; args; _ } ->
-  let a,b = IArray.extract2_exn args in
-  reg a; reg b; Check.attach d f;
-  attach d (
-    set r (let* va = get a and+ vb = get b in if Q.is_zero vb then None else Some (Q.div va vb)) &&
-    set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.mul vr vb)) &&
-    (* if va is 0, and vr is not 0, b can't be not zero because vr would be 0. So b is 0. *)
-    set b (let* va = get a and+ vr = get r in if Q.is_zero vr then None else Some (Q.div va vr))
-  );
-  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
-    let a = IArray.extract1_exn args in
-    reg a; Check.attach d f;
-    attach d (
-      set r (let+ va = get a in Q.neg va) &&
-      set a (let+ vr = get r in Q.neg vr)
-    );
-  | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp Q.lt a b; Check.attach d f;
-  | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp Q.le a b; Check.attach d f;
-  | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp Q.gt a b; Check.attach d f;
-  | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
-    let a,b = IArray.extract2_exn args in
-    cmp Q.ge a b; Check.attach d f;
-  | { app = {builtin = Expr.Floor}; tyargs = []; args; _ } ->
-    let a = IArray.extract1_exn args in
-    reg a; Check.attach d f;
+  | {
+   app = { builtin = Expr.Coercion };
+   tyargs =
+     ( [
+         { app = { builtin = Expr.Int | Expr.Rat; _ }; _ };
+         { app = { builtin = Expr.Real; _ }; _ };
+       ]
+     | [
+         { app = { builtin = Expr.Int; _ }; _ };
+         { app = { builtin = Expr.Rat; _ }; _ };
+       ] );
+   args;
+  } ->
+      let a = IArray.extract1_exn args in
+      merge a;
+      Check.attach d f
+  | { app = { builtin = Expr.Integer s }; tyargs = []; args; _ } ->
+      assert (IArray.is_empty args);
+      merge (cst (Q.of_string s))
+  | { app = { builtin = Expr.Decimal s }; tyargs = []; args; _ } ->
+      assert (IArray.is_empty args);
+      merge (cst (Q.of_string_decimal s))
+  | { app = { builtin = Expr.Rational s }; tyargs = []; args; _ } ->
+      assert (IArray.is_empty args);
+      merge (cst (Q.of_string_decimal s))
+  | { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f;
+      attach d
+        (set r
+           (let+ va = get a and+ vb = get b in
+            Q.add va vb)
+        && set a
+             (let+ vb = get b and+ vr = get r in
+              Q.sub vr vb)
+        && set b
+             (let+ va = get a and+ vr = get r in
+              Q.sub vr va))
+  | { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f;
+      attach d
+        (set r
+           (let+ va = get a and+ vb = get b in
+            Q.sub va vb)
+        && set a
+             (let+ vb = get b and+ vr = get r in
+              Q.add vr vb)
+        && set b
+             (let+ va = get a and+ vr = get r in
+              Q.sub va vr))
+  | { app = { builtin = Expr.Mul }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f;
+      attach d
+        (set r
+           (let+ va = get a and+ vb = get b in
+            Q.mul va vb)
+        && set a
+             (let* vb = get b and+ vr = get r in
+              if Q.is_zero vb then None else Some (Q.div vr vb))
+        && set b
+             (let* va = get a and+ vr = get r in
+              if Q.is_zero va then None else Some (Q.div vr va)))
+  | { app = { builtin = Expr.Div }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      reg a;
+      reg b;
+      Check.attach d f;
+      attach d
+        (set r
+           (let* va = get a and+ vb = get b in
+            if Q.is_zero vb then None else Some (Q.div va vb))
+        && set a
+             (let* vb = get b and+ vr = get r in
+              if Q.is_zero vb then None else Some (Q.mul vr vb))
+        && (* if va is 0, and vr is not 0, b can't be not zero because vr would be 0. So b is 0. *)
+        set b
+          (let* va = get a and+ vr = get r in
+           if Q.is_zero vr then None else Some (Q.div va vr)))
+  | { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f;
+      attach d
+        (set r
+           (let+ va = get a in
+            Q.neg va)
+        && set a
+             (let+ vr = get r in
+              Q.neg vr))
+  | { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp Q.lt a b;
+      Check.attach d f
+  | { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp Q.le a b;
+      Check.attach d f
+  | { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp Q.gt a b;
+      Check.attach d f
+  | { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
+      let a, b = IArray.extract2_exn args in
+      cmp Q.ge a b;
+      Check.attach d f
+  | { app = { builtin = Expr.Floor }; tyargs = []; args; _ } ->
+      let a = IArray.extract1_exn args in
+      reg a;
+      Check.attach d f
   | _ -> ()
 
-
 let init env =
   Ground.register_converter env converter;
   init_ty env;
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index bf72dac0e0133877e5cb29ce40e9abbeb33dcaae..0584e07e7fdd511918420706958925140b16bf92 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -20,9 +20,10 @@
 
 include Value.S with type s = Q.t
 
-val cst': Q.t -> t
-val cst:  Q.t -> Node.t
+val cst' : Q.t -> t
 
-val zero: Node.t
+val cst : Q.t -> Node.t
 
-val init: Egraph.wt -> unit
+val zero : Node.t
+
+val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/sign_product.ml b/src_colibri2/theories/LRA/sign_product.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7ef561b8a77da8297dfa1eddf7775571daa39705
--- /dev/null
+++ b/src_colibri2/theories/LRA/sign_product.ml
@@ -0,0 +1,193 @@
+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+(** Product of node sign with one constant 1 or -1 *)
+
+module T = struct
+  type cst = Pos | Neg [@@deriving eq, ord, hash]
+
+  type power = Odd | Even | OddNonZero  (** the node can't be zero*)
+  [@@deriving eq, ord, hash]
+
+  type t = NZ of { poly : power Node.M.t; cst : cst } | Zero
+  [@@deriving eq, ord, hash]
+
+  let pp_exposant fmt q =
+    match q with
+    | OddNonZero -> ()
+    | Even -> Fmt.string fmt "²"
+    | Odd -> Fmt.string fmt "³"
+
+  let pp fmt = function
+    | Zero -> Fmt.pf fmt "0"
+    | NZ v ->
+        Fmt.pf fmt "@[%s%a@]"
+          (match v.cst with Pos -> "+" | Neg -> "-")
+          (* print_not_one v.cst *)
+          Fmt.(iter_bindings Node.M.iter (pair Node.pp pp_exposant))
+          v.poly
+end
+
+include T
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
+
+let of_one_node cl = NZ { poly = Node.M.singleton cl Odd; cst = Pos }
+
+let of_one_node_non_zero cl =
+  NZ { poly = Node.M.singleton cl OddNonZero; cst = Pos }
+
+let is_one_node = function
+  | Zero -> None
+  | NZ t ->
+      if Node.M.is_num_elt 1 t.poly && T.equal_cst t.cst Pos then
+        match Node.M.choose t.poly with
+        | _, Even -> None
+        | n, (Odd | OddNonZero) -> Some n
+      else None
+
+let one = NZ { cst = Pos; poly = Node.M.empty }
+
+let minus_one = NZ { cst = Neg; poly = Node.M.empty }
+
+let zero = Zero
+
+let mul_cst c1 c2 =
+  match (c1, c2) with Pos, Pos | Neg, Neg -> Pos | Neg, Pos | Pos, Neg -> Neg
+
+let mul p1 p2 =
+  match (p1, p2) with
+  | Zero, _ | _, Zero -> Zero
+  | NZ p1, NZ p2 ->
+      let poly m1 m2 =
+        Node.M.union
+          (fun _ c1 c2 ->
+            match (c1, c2) with
+            | Odd, Odd -> Some Even
+            | (OddNonZero | Odd), (OddNonZero | Odd) -> None
+            | Even, v | v, Even -> Some v)
+          m1 m2
+      in
+      NZ { cst = mul_cst p1.cst p2.cst; poly = poly p1.poly p2.poly }
+
+let subst p x s =
+  match p with
+  | Zero -> None
+  | NZ p -> (
+      let poly, q = Node.M.find_remove x p.poly in
+      match q with
+      | None -> None
+      | Some (Odd | OddNonZero) -> Some (mul (NZ { cst = p.cst; poly }) s)
+      | Some Even -> Some (mul (mul (NZ { cst = p.cst; poly }) s) s))
+
+let normalize p ~f =
+  match p with
+  | Zero -> Zero
+  | NZ p ->
+      let add acc cl v =
+        let q = f cl in
+        match v with Odd | OddNonZero -> mul acc q | Even -> mul (mul acc q) q
+      in
+      Node.M.fold_left add (NZ { cst = p.cst; poly = Node.M.empty }) p.poly
+
+type data = power
+
+let nodes = function Zero -> Node.M.empty | NZ p -> p.poly
+
+type extracted = Plus_one | Minus_one | Zero | Var of Node.t * t | NoNonZero
+
+let extract : t -> extracted = function
+  | Zero -> Zero
+  | NZ p -> (
+      if Node.M.is_empty p.poly then
+        match p.cst with Pos -> Plus_one | Neg -> Minus_one
+      else
+        match
+          Node.M.fold_left
+            (fun acc c v ->
+              match acc with
+              | Some _ -> acc
+              | None -> (
+                  match v with Odd | Even -> None | OddNonZero -> Some c))
+            None p.poly
+        with
+        | None -> NoNonZero
+        | Some x ->
+            let p' = NZ { p with poly = Node.M.remove x p.poly } in
+            Var (x, p'))
+
+type presolve = Zero | NonZero | OneNonZero of Node.t | Other
+
+let presolve : t -> presolve = function
+  | Zero -> Zero
+  | NZ p ->
+      Node.M.fold_left
+        (fun acc c -> function
+          | Odd | Even -> (
+              match acc with
+              | NonZero -> OneNonZero c
+              | OneNonZero _ | Zero | Other -> Other)
+          | OddNonZero -> acc)
+        NonZero p.poly
+
+type extract_cst = Pos | Neg | Zero
+
+let extract_cst : t -> extract_cst * t = function
+  | Zero -> (Zero, Zero)
+  | NZ t as t' -> (
+      match t.cst with Pos -> (Pos, t') | Neg -> (Neg, NZ { t with cst = Pos }))
+
+let remove n = function
+  | T.Zero -> T.Zero
+  | NZ p -> NZ { p with poly = Node.M.remove n p.poly }
+
+let common pa pb =
+  match (pa, pb) with
+  | T.Zero, T.Zero -> T.Zero
+  | Zero, p | p, Zero -> p
+  | NZ pa, NZ pb ->
+      NZ
+        {
+          poly =
+            Node.M.inter
+              (fun _ v1 v2 ->
+                match (v1, v2) with
+                | Odd, Odd -> Some Odd
+                | (Odd | OddNonZero), (Odd | OddNonZero) -> Some OddNonZero
+                | Odd, Even | Even, Odd -> Some Odd
+                | OddNonZero, Even | Even, OddNonZero -> Some OddNonZero
+                | Even, Even -> Some Even)
+              pa.poly pb.poly;
+          cst =
+            (match (pa.cst, pb.cst) with
+            | Neg, Neg -> Neg
+            | Pos, Pos | Neg, Pos | Pos, Neg -> Pos);
+        }
+
+type kind = PLUS_ONE | MINUS_ONE | ZERO | NODE of Node.t | PRODUCT
+
+let classify = function
+  | T.Zero -> ZERO
+  | T.NZ p ->
+      if Node.M.is_empty p.poly then
+        match p.cst with Pos -> PLUS_ONE | Neg -> MINUS_ONE
+      else if T.equal_cst Pos p.cst && Node.M.is_num_elt 1 p.poly then
+        let node, v = Node.M.choose p.poly in
+        match v with Even -> PRODUCT | Odd | OddNonZero -> NODE node
+      else PRODUCT
diff --git a/src_colibri2/theories/LRA/sign_product.mli b/src_colibri2/theories/LRA/sign_product.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9f3515e62e833a6581f52fa31615b331241049f7
--- /dev/null
+++ b/src_colibri2/theories/LRA/sign_product.mli
@@ -0,0 +1,76 @@
+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+(** Product of node sign with one constant 1 or -1 *)
+
+type t
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+val of_one_node : Node.t -> t
+(** Build a value that represent one node *)
+
+val of_one_node_non_zero : Node.t -> t
+(** Build a value that represent one node when it is known to be non-zero *)
+
+val is_one_node : t -> Node.t option
+(** Test if a value represents one node *)
+
+val subst : t -> Node.t -> t -> t option
+(** [subst p n q] substitute [n] by [q] in [p], if [n] is not in [p] None is
+      returned, otherwise the result of the substitution is returned *)
+
+val normalize : t -> f:(Node.t -> t) -> t
+(** [norm p ~f] normalize [p] using [f] *)
+
+type data
+(** An abstract type to avoid translating the map to sets in {!nodes} *)
+
+val nodes : t -> data Node.M.t
+(** [nodes t] returns the node which are present in [t] *)
+
+val mul : t -> t -> t
+
+type extracted = Plus_one | Minus_one | Zero | Var of Node.t * t | NoNonZero
+
+val extract : t -> extracted
+
+type extract_cst = Pos | Neg | Zero
+
+val extract_cst : t -> extract_cst * t
+
+val remove : Node.t -> t -> t
+
+val common : t -> t -> t
+(** Return the common part *)
+
+val one : t
+
+val minus_one : t
+
+val zero : t
+
+type kind = PLUS_ONE | MINUS_ONE | ZERO | NODE of Node.t | PRODUCT
+
+val classify : t -> kind
+
+type presolve = Zero | NonZero | OneNonZero of Node.t | Other
+
+val presolve : t -> presolve
diff --git a/src_colibri2/theories/LRA/stages/interval_sig.ml b/src_colibri2/theories/LRA/stages/interval_sig.ml
index 1715ca252c8d5844ba6d6e2f69f1997493b16561..cff021537f139003c2f8b2beb45221d6a4972ed1 100644
--- a/src_colibri2/theories/LRA/stages/interval_sig.ml
+++ b/src_colibri2/theories/LRA/stages/interval_sig.ml
@@ -23,76 +23,81 @@ open Colibri2_popop_lib
 module type S = sig
   include Popop_stdlib.Datatype
 
-  val is_distinct: t -> t -> bool
-  type is_comparable =
-    | Gt
-    | Lt
-    | Ge
-    | Le
-    | Uncomparable
-
-  val is_comparable: t -> t -> is_comparable
-  val is_included: t -> t -> bool
-
-  val mult_cst: Q.t -> t -> t
+  val is_distinct : t -> t -> bool
+
+  type is_comparable = Gt | Lt | Ge | Le | Eq | Uncomparable
+
+  val is_comparable : t -> t -> is_comparable
+
+  val is_included : t -> t -> bool
+
+  val mult_cst : Q.t -> t -> t
+
   val add_cst : Q.t -> t -> t
-  val add: t -> t -> t
-  val minus: t -> t -> t
 
-  val mem: Q.t -> t -> bool
+  val add : t -> t -> t
 
+  val minus : t -> t -> t
+
+  val mem : Q.t -> t -> bool
+
+  val singleton : Q.t -> t
   (** from Q.t *)
-  val singleton: Q.t -> t
-  val is_singleton: t -> Q.t option
 
-  val except: t -> Q.t -> t option
+  val is_singleton : t -> Q.t option
+
+  val except : t -> Q.t -> t option
+
+  type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
 
-  type split_heuristic =
-    | Singleton of Q.t
-    | Splitted of t * t
-    | NotSplitted
+  val split_heuristic : t -> split_heuristic
 
-  val split_heuristic: t -> split_heuristic
+  val absent : Q.t -> t -> bool
 
-  val absent: Q.t -> t -> bool
-  val is_integer: t -> bool
-  val integers: t
+  val is_integer : t -> bool
 
-  val gt: Q.t -> t
-  val ge: Q.t -> t
-  val lt: Q.t -> t
-  val le: Q.t -> t
+  val integers : t
+
+  val gt : Q.t -> t
+
+  val ge : Q.t -> t
+
+  val lt : Q.t -> t
+
+  val le : Q.t -> t
   (** > q, >= q, < q, <= q *)
 
-  val le': t -> t
-  val lt': t -> t
-  val ge': t -> t
-  val gt': t -> t
+  val le' : t -> t
 
-  val union: t -> t -> t
+  val lt' : t -> t
+
+  val ge' : t -> t
+
+  val gt' : t -> t
+
+  val union : t -> t -> t
   (** union set *)
 
-  val inter: t -> t -> t option
+  val inter : t -> t -> t option
   (** intersection set.
       if the two arguments are equals, return the second
   *)
 
+  val zero : t
 
-  val zero: t
-  val reals: t
+  val reals : t
 
+  val is_reals : t -> bool
   (** R *)
-  val is_reals: t -> bool
 
-  val choose: t -> Q.t
+  val choose : t -> Q.t
   (** Nothing smart in this choosing *)
 
-  val invariant: t -> bool
+  val invariant : t -> bool
 
   (* val choose_rnd : (int -> int) -> t -> Q.t
    * (\** choose an element randomly (but non-uniformly), the given function is
    *       the random generator *\)
    * 
    * val get_convexe_hull: t -> (Q.t * bound) option * (Q.t * bound) option *)
-
 end
diff --git a/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
index 69981140f7b9381b9a17cd76b713885f705bdd10..33178987e69acdb4aa9a968e78f6cdec55bdeb48 100644
--- a/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
+++ b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
@@ -24,75 +24,95 @@ open Base
 
 module T = struct
   type t = {
-    noninteger: bool;  (** true: maybe negative, false: never negative *)
-    sign: Sign_domain.t;
+    noninteger : bool;  (** true: maybe negative, false: never negative *)
+    sign : Sign_domain.t;
   }
   [@@deriving ord, eq, hash]
 
-
   let pp fmt t =
-    let prefix s = if t.noninteger then s else "â„•"^s in
-    Fmt.string fmt @@
-    match t.sign.neg, t.sign.zero, t.sign.pos with
-    | true, true, true  -> if t.noninteger then "ℝ" else "ℕ"
+    let prefix s = if t.noninteger then s else "â„•" ^ s in
+    Fmt.string fmt
+    @@
+    match (t.sign.neg, t.sign.zero, t.sign.pos) with
+    | true, true, true -> if t.noninteger then "ℝ" else "ℕ"
     | true, false, true -> prefix "≠0"
     | false, true, false -> prefix "=0"
     | true, true, false -> prefix "≤0"
-    | true, false, false  -> prefix "<0"
-    | false, false, false  -> prefix "∅"
+    | true, false, false -> prefix "<0"
+    | false, false, false -> prefix "∅"
     | false, false, true -> prefix ">0"
     | false, true, true -> prefix "≥0"
-
 end
 
 include T
-include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
 
 let invariant t = Sign_domain.invariant t.sign
 
-type split_heuristic =
-  | Singleton of Q.t
-  | Splitted of t * t
-  | NotSplitted
+type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
 
 let split_heuristic t =
   match Sign_domain.split_heuristic t.sign with
   | Singleton q -> Singleton q
-  | Splitted (t1,t2) -> Splitted ({ noninteger = t.noninteger; sign = t1 },
-                                  { noninteger = t.noninteger; sign = t2 })
+  | Splitted (t1, t2) ->
+      Splitted
+        ( { noninteger = t.noninteger; sign = t1 },
+          { noninteger = t.noninteger; sign = t2 } )
   | NotSplitted -> NotSplitted
 
 let absent q t =
-  (not t.noninteger && not (Q.is_integer q)) ||
-  Sign_domain.absent q t.sign
+  ((not t.noninteger) && not (Q.is_integer q)) || Sign_domain.absent q t.sign
+
+let le' t = { noninteger = true; sign = Sign_domain.le' t.sign }
 
-let le' t = { noninteger = true; sign = Sign_domain.le' t.sign; }
-let lt' t = { noninteger = true; sign = Sign_domain.lt' t.sign; }
-let ge' t = { noninteger = true; sign = Sign_domain.ge' t.sign; }
-let gt' t = { noninteger = true; sign = Sign_domain.gt' t.sign; }
+let lt' t = { noninteger = true; sign = Sign_domain.lt' t.sign }
+
+let ge' t = { noninteger = true; sign = Sign_domain.ge' t.sign }
+
+let gt' t = { noninteger = true; sign = Sign_domain.gt' t.sign }
 
 let is_distinct t1 t2 = Sign_domain.is_distinct t1.sign t2.sign
 
-type is_comparable = Sign_domain.is_comparable = Gt | Lt | Ge | Le | Uncomparable
+type is_comparable = Sign_domain.is_comparable =
+  | Gt
+  | Lt
+  | Ge
+  | Le
+  | Eq
+  | Uncomparable
 
 let is_comparable t1 t2 = Sign_domain.is_comparable t1.sign t2.sign
+
 let is_included t1 t2 =
-  (not t1.noninteger || t2.noninteger) &&
-  Sign_domain.is_included t1.sign t2.sign
-
-let mult_cst q t = { noninteger = t.noninteger && Q.is_not_zero q;
-                     sign = Sign_domain.mult_cst q t.sign }
-let add_cst q t = { noninteger = t.noninteger;
-                    sign = Sign_domain.add_cst q t.sign }
-let add t1 t2 = { noninteger = t1.noninteger || t2.noninteger;
-                  sign = Sign_domain.add t1.sign t2.sign }
-let minus t1 t2 = { noninteger = t1.noninteger || t2.noninteger;
-                    sign = Sign_domain.minus t1.sign t2.sign }
-let mem q t =
-  (Q.is_integer q || t.noninteger) &&
-  Sign_domain.mem q t.sign
-
-let singleton q = { noninteger = not (Q.is_integer q); sign = Sign_domain.singleton q }
+  ((not t1.noninteger) || t2.noninteger)
+  && Sign_domain.is_included t1.sign t2.sign
+
+let mult_cst q t =
+  {
+    noninteger = t.noninteger && Q.is_not_zero q;
+    sign = Sign_domain.mult_cst q t.sign;
+  }
+
+let add_cst q t =
+  { noninteger = t.noninteger; sign = Sign_domain.add_cst q t.sign }
+
+let add t1 t2 =
+  {
+    noninteger = t1.noninteger || t2.noninteger;
+    sign = Sign_domain.add t1.sign t2.sign;
+  }
+
+let minus t1 t2 =
+  {
+    noninteger = t1.noninteger || t2.noninteger;
+    sign = Sign_domain.minus t1.sign t2.sign;
+  }
+
+let mem q t = (Q.is_integer q || t.noninteger) && Sign_domain.mem q t.sign
+
+let singleton q =
+  { noninteger = not (Q.is_integer q); sign = Sign_domain.singleton q }
+
 let is_singleton t = Sign_domain.is_singleton t.sign
 
 let except t q =
@@ -101,25 +121,32 @@ let except t q =
   | Some sign -> Some { noninteger = t.noninteger; sign }
 
 let gt q = { noninteger = true; sign = Sign_domain.gt q }
+
 let ge q = { noninteger = true; sign = Sign_domain.ge q }
+
 let lt q = { noninteger = true; sign = Sign_domain.lt q }
+
 let le q = { noninteger = true; sign = Sign_domain.le q }
 
-let union t1 t2 = { noninteger = t1.noninteger || t2.noninteger;
-                    sign = Sign_domain.union t1.sign t2.sign
-                  }
+let union t1 t2 =
+  {
+    noninteger = t1.noninteger || t2.noninteger;
+    sign = Sign_domain.union t1.sign t2.sign;
+  }
 
 let inter t1 t2 =
   match Sign_domain.inter t1.sign t2.sign with
-  | Some sign ->
-    Some { noninteger = t1.noninteger && t2.noninteger; sign; }
+  | Some sign -> Some { noninteger = t1.noninteger && t2.noninteger; sign }
   | None -> None
 
 let zero = { noninteger = false; sign = Sign_domain.zero }
+
 let reals = { noninteger = true; sign = Sign_domain.reals }
+
 let integers = { noninteger = false; sign = Sign_domain.reals }
+
 let is_reals t = t.noninteger && Sign_domain.is_reals t.sign
 
 let choose t = Sign_domain.choose t.sign
 
-let is_integer t = not (t.noninteger)
+let is_integer t = not t.noninteger
diff --git a/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml b/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
index ce6a596796bdb474a2be414896d8aea88d495992..7d5db0e4f9ca73b288cba1e26a99804c1fe84044 100644
--- a/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
+++ b/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
@@ -19,55 +19,65 @@
 (*************************************************************************)
 
 (** Sign domain: abstraction of integer numerical values by their signs. *)
+
 (** From frama-c *)
 
 open Base
 
 module T = struct
   type t = {
-    pos: bool;  (** true: maybe positive, false: never positive *)
-    zero: bool; (** true: maybe zero, false: never zero *)
-    neg: bool;  (** true: maybe negative, false: never negative *)
+    pos : bool;  (** true: maybe positive, false: never positive *)
+    zero : bool;  (** true: maybe zero, false: never zero *)
+    neg : bool;  (** true: maybe negative, false: never negative *)
   }
   [@@deriving ord, eq, hash]
 
-
   let pp fmt t =
-    Fmt.string fmt @@
-    match t.neg, t.zero, t.pos with
-    | true, true, true  -> "ℝ"
+    Fmt.string fmt
+    @@
+    match (t.neg, t.zero, t.pos) with
+    | true, true, true -> "ℝ"
     | true, false, true -> "≠0"
     | false, true, false -> "=0"
     | true, true, false -> "≤0"
-    | true, false, false  -> "<0"
-    | false, false, false  -> "∅"
+    | true, false, false -> "<0"
+    | false, false, false -> "∅"
     | false, false, true -> ">0"
     | false, true, true -> "≥0"
-
 end
 
 include T
-include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
-
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
 
 let invariant t = t.neg || t.zero || t.pos
 
-let top =         { pos = true;  zero = true;  neg = true  }
-let pos_or_zero = { pos = true;  zero = true;  neg = false }
-let pos =         { pos = true;  zero = false; neg = false }
-let neg_or_zero = { pos = false; zero = true;  neg = true  }
-let neg =         { pos = false; zero = false; neg = true  }
-let zero =        { pos = false; zero = true;  neg = false }
-let one =         { pos = true; zero = false;  neg = false }
-let non_zero =    { pos = true;  zero = false; neg = true  }
+let top = { pos = true; zero = true; neg = true }
+
+let pos_or_zero = { pos = true; zero = true; neg = false }
+
+let pos = { pos = true; zero = false; neg = false }
+
+let neg_or_zero = { pos = false; zero = true; neg = true }
+
+let neg = { pos = false; zero = false; neg = true }
+
+let zero = { pos = false; zero = true; neg = false }
+
+let one = { pos = true; zero = false; neg = false }
+
+let non_zero = { pos = true; zero = false; neg = true }
+
 let ge_zero v = not v.neg
+
 let le_zero v = not v.pos
 
 (* Bottom is a special value (`Bottom) in Eva, and need not be part of
    the lattice. Here, we have a value which is equivalent to it, defined
    there only for commodity. *)
 let empty = { pos = false; zero = false; neg = false }
+
 let is_empty t = equal t empty
+
 let is_reals t = equal t top
 
 (* Inclusion: test inclusion of each field. *)
@@ -76,41 +86,37 @@ let is_included v1 v2 =
   bincl v1.pos v2.pos && bincl v1.zero v2.zero && bincl v1.neg v2.neg
 
 (* Join of the lattice: pointwise logical or. *)
-let join v1 v2 = {
-  pos  = v1.pos  || v2.pos;
-  zero = v1.zero || v2.zero;
-  neg  = v1.neg  || v2.neg;
-}
+let join v1 v2 =
+  { pos = v1.pos || v2.pos; zero = v1.zero || v2.zero; neg = v1.neg || v2.neg }
 
 (* Meet of the lattice (called 'narrow' in Eva for historical reasons).
    We detect the case where the values have incompatible concretization,
    and report this as `Bottom. *)
 let narrow v1 v2 =
-  let r = {
-    pos  = v1.pos  && v2.pos;
-    zero = v1.zero && v2.zero;
-    neg  = v1.neg  && v2.neg;
-  } in
+  let r =
+    {
+      pos = v1.pos && v2.pos;
+      zero = v1.zero && v2.zero;
+      neg = v1.neg && v2.neg;
+    }
+  in
   if is_empty r then None else Some r
 
 let mem q v =
   let c = Q.sign q in
-  c = 0 && v.zero || c < 0 && v.neg || c > 0 && v.pos
+  (c = 0 && v.zero) || (c < 0 && v.neg) || (c > 0 && v.pos)
 
 let absent q v =
   let c = Q.sign q in
-  c = 0 && not v.zero || c < 0 && not v.neg || c > 0 && not v.pos
+  (c = 0 && not v.zero) || (c < 0 && not v.neg) || (c > 0 && not v.pos)
 
 let reals = top
 
 (* [singleton] creates an abstract value corresponding to the singleton [i]. *)
 let singleton i =
-  if Q.lt i Q.zero then neg
-  else if Q.gt i Q.zero then pos
-  else zero
+  if Q.lt i Q.zero then neg else if Q.gt i Q.zero then pos else zero
 
-let is_singleton v =
-  if equal v zero then Some Q.zero else None
+let is_singleton v = if equal v zero then Some Q.zero else None
 
 (** {2 Forward transfer functions} *)
 
@@ -129,14 +135,15 @@ let add v1 v2 =
   let same_sign v1 v2 =
     (le_zero v1 && le_zero v2) || (ge_zero v1 && ge_zero v2)
   in
-  let zero = not (same_sign v1 v2) || (v1.zero && v2.zero) in
+  let zero = (not (same_sign v1 v2)) || (v1.zero && v2.zero) in
   { neg; pos; zero }
 
 let add_cst q v =
   let c = Q.sign q in
   if c = 0 then v
-  else if c > 0 then { neg = v.neg; zero = v.zero && v.neg ; pos = v.pos || v.zero || v.neg }
-  else { neg = v.neg || v.zero || v.pos; zero = v.zero && v.pos ; pos = v.pos }
+  else if c > 0 then
+    { neg = v.neg; zero = v.zero && v.neg; pos = v.pos || v.zero || v.neg }
+  else { neg = v.neg || v.zero || v.pos; zero = v.zero && v.pos; pos = v.pos }
 
 let mul v1 v2 =
   let pos = (v1.pos && v2.pos) || (v1.neg && v2.neg) in
@@ -144,20 +151,19 @@ let mul v1 v2 =
   let zero = v1.zero || v2.zero in
   { neg; pos; zero }
 
-let minus v1 v2 =
-  add v1 { neg = v2.pos; zero = v2.zero; pos = v2.neg }
+let minus v1 v2 = add v1 { neg = v2.pos; zero = v2.zero; pos = v2.neg }
 
 let mult_cst q v =
   let c = Q.sign q in
   if c = 0 then zero
   else if c > 0 then v
-  else  { neg = v.pos; zero = v.zero; pos = v.neg }
-
+  else { neg = v.pos; zero = v.zero; pos = v.neg }
 
 let div v1 v2 =
   let pos = (v1.pos && v2.pos) || (v1.neg && v2.neg) in
   let neg = (v1.pos && v2.neg) || (v1.neg && v2.pos) in
-  let zero = true in (* zero can appear with large enough v2 *)
+  let zero = true in
+  (* zero can appear with large enough v2 *)
   { neg; pos; zero }
 
 (* The implementation of the bitwise operators below relies on this table
@@ -194,8 +200,7 @@ let bitwise_xor v1 v2 =
     || (v1.neg && v2.neg)
   in
   let neg =
-    (v1.neg && (v2.pos || v2.zero)) ||
-    (v2.neg && (v1.pos || v1.zero))
+    (v1.neg && (v2.pos || v2.zero)) || (v2.neg && (v1.pos || v1.zero))
   in
   let zero = (v1.zero && v2.zero) || (v1.pos && v2.pos) || (v1.neg && v2.neg) in
   { neg; pos; zero }
@@ -284,46 +289,55 @@ let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
 let is_distinct a b =
   Bool.(a.neg <> b.neg) && Bool.(a.zero <> b.zero) && Bool.(a.pos <> b.pos)
 
-type is_comparable =
-  | Gt
-  | Lt
-  | Ge
-  | Le
-  | Uncomparable
+type is_comparable = Gt | Lt | Ge | Le | Eq | Uncomparable
 
 let is_comparable x y =
-  match x, y with
-  | {pos=false; zero=false;neg=false},_ | _, {pos=false; zero=false;neg=false}
-  | {pos=true; neg = true;_}, _ | _, {pos=true; neg = true;_} -> Uncomparable
-  | {pos=true; _ }, {pos = true; _}
-  | {neg=true; _ }, {neg = true; _} -> Uncomparable
-  | {neg=true; zero=false; pos = false }, {neg=false; zero=_; pos=_}
-  | {neg=true; zero=true; pos = false }, {neg=false; zero=false; pos=true}
-  | {neg=false; zero=true; pos = false }, {neg=false; zero=false; pos=true}
-    -> Lt
-  | {neg=true; zero=true; pos = false }, {neg=false; zero=true; pos=_}
-  | {neg=false; zero=true; pos = false }, {neg=false; zero=true; pos=_}
-    -> Le
-  | {neg=false; zero=_; pos=_}, {neg=true; zero=false; pos = false }
-  | {neg=false; zero=false; pos=true}, {neg=true; zero=true; pos = false }
-  | {neg=false; zero=false; pos=true}, {neg=false; zero=true; pos = false }
-    -> Gt
-  | {neg=false; zero=true; pos=_}, {neg=true; zero=true; pos = false }
-  | {neg=false; zero=true; pos=true}, {neg=false; zero=true; pos = false }
-    -> Ge
+  match (x, y) with
+  | { pos = false; zero = false; neg = false }, _
+  | _, { pos = false; zero = false; neg = false }
+  | { pos = true; neg = true; _ }, _
+  | _, { pos = true; neg = true; _ } ->
+      Uncomparable
+  | { pos = true; _ }, { pos = true; _ } | { neg = true; _ }, { neg = true; _ }
+    ->
+      Uncomparable
+  | ( { neg = false; zero = true; pos = false },
+      { neg = false; zero = true; pos = false } ) ->
+      Eq
+  | ( { neg = true; zero = false; pos = false },
+      { neg = false; zero = _; pos = _ } )
+  | ( { neg = true; zero = true; pos = false },
+      { neg = false; zero = false; pos = true } )
+  | ( { neg = false; zero = true; pos = false },
+      { neg = false; zero = false; pos = true } ) ->
+      Lt
+  | ( { neg = true; zero = true; pos = false },
+      { neg = false; zero = true; pos = _ } )
+  | ( { neg = false; zero = true; pos = false },
+      { neg = false; zero = true; pos = _ } ) ->
+      Le
+  | ( { neg = false; zero = _; pos = _ },
+      { neg = true; zero = false; pos = false } )
+  | ( { neg = false; zero = false; pos = true },
+      { neg = true; zero = true; pos = false } )
+  | ( { neg = false; zero = false; pos = true },
+      { neg = false; zero = true; pos = false } ) ->
+      Gt
+  | ( { neg = false; zero = true; pos = _ },
+      { neg = true; zero = true; pos = false } )
+  | ( { neg = false; zero = true; pos = true },
+      { neg = false; zero = true; pos = false } ) ->
+      Ge
 
 let is_included x y =
   (* <= is like implication on booleans *)
   Bool.(x.neg <= y.neg && x.zero <= y.zero && x.pos <= y.pos)
 
 let union = join
-let inter = narrow
 
+let inter = narrow
 
-type split_heuristic =
-  | Singleton of Q.t
-  | Splitted of t * t
-  | NotSplitted
+type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
 
 let split_heuristic _ = NotSplitted
 
@@ -333,56 +347,34 @@ let except t x =
     if is_empty t then None else Some t
   else Some t
 
-let choose t =
-  if t.zero then Q.zero
-  else if t.pos then Q.one
-  else Q.minus_one
+let choose t = if t.zero then Q.zero else if t.pos then Q.one else Q.minus_one
 
 let le q =
   let c = Q.sign q in
-  if c < 0 then neg
-  else if c = 0 then neg_or_zero
-  else top
+  if c < 0 then neg else if c = 0 then neg_or_zero else top
 
 let lt q =
   let c = Q.sign q in
-  if c <= 0 then neg
-  else top
+  if c <= 0 then neg else top
 
 let ge q =
   let c = Q.sign q in
-  if c < 0 then top
-  else if c = 0 then pos_or_zero
-  else pos
+  if c < 0 then top else if c = 0 then pos_or_zero else pos
 
 let gt q =
   let c = Q.sign q in
-  if c >= 0 then pos
-  else top
+  if c >= 0 then pos else top
 
 let le' v =
-  { neg = v.neg || v.zero || v.pos;
-    zero = v.zero || v.pos;
-    pos = v.pos
-  }
+  { neg = v.neg || v.zero || v.pos; zero = v.zero || v.pos; pos = v.pos }
 
-let lt' v =
-  { neg = v.neg || v.zero || v.pos;
-    zero = v.pos;
-    pos = v.pos
-  }
+let lt' v = { neg = v.neg || v.zero || v.pos; zero = v.pos; pos = v.pos }
 
 let ge' v =
-  { neg = v.neg;
-    zero = v.zero || v.neg ;
-    pos = v.pos || v.zero || v.neg;
-  }
+  { neg = v.neg; zero = v.zero || v.neg; pos = v.pos || v.zero || v.neg }
 
-let gt' v =
-  { neg = v.neg;
-    zero = v.neg ;
-    pos = v.pos || v.zero || v.neg;
-  }
+let gt' v = { neg = v.neg; zero = v.neg; pos = v.pos || v.zero || v.neg }
 
 let integers = reals
+
 let is_integer _ = false
diff --git a/src_common/interval.mlw b/src_common/interval.mlw
index a97b41139949b1accb3fc098ed9d91e9321d41dc..70bb62789babf34b5d3767a4a1210a009afcc1a0 100644
--- a/src_common/interval.mlw
+++ b/src_common/interval.mlw
@@ -116,6 +116,7 @@ module Convexe
   | Lt
   | Ge
   | Le
+  | Eq
   | Uncomparable
 
   use q.Ord as Ord
@@ -128,6 +129,7 @@ module Convexe
       | Gt -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 >. q2
       | Le -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <=. q2
       | Ge -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 >=. q2
+      | Eq -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 = q2
     end
     }
    =
@@ -163,6 +165,7 @@ module Convexe
        end
     | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
        match Q.compare v1' v2, Q.compare v1 v2' with
+       | Ord.Eq, Ord.Eq -> Eq
        | Ord.Eq, _ ->
          match b1', b2 with
          | Large, Large -> Le
diff --git a/src_common/interval__Convexe.ml b/src_common/interval__Convexe.ml
index d552b1acd86f9f4bbad3563ad8be2ba976bb29fb..2a6402b6d0e3492315af77134b4544012c73230d 100644
--- a/src_common/interval__Convexe.ml
+++ b/src_common/interval__Convexe.ml
@@ -74,6 +74,7 @@ type is_comparable =
   | Lt
   | Ge
   | Le
+  | Eq
   | Uncomparable
 
 let is_comparable (e1: t') (e2: t') : is_comparable =
@@ -117,6 +118,7 @@ let is_comparable (e1: t') (e2: t') : is_comparable =
     v2',
     b2')) ->
     begin match ((Q_extra.compare v1' v2), (Q_extra.compare v1 v2')) with
+    | (Ord.Eq, Ord.Eq) -> Eq
     | (Ord.Eq,
       _) ->
       begin match (b1', b2) with
diff --git a/src_common/q/why3session.xml b/src_common/q/why3session.xml
index 6ef2aa09b442a13a6d5ad85b6c0b3b0f1456d368..0d13e6466775d9fe18669fc6fe9687bc71f5f5f8 100644
--- a/src_common/q/why3session.xml
+++ b/src_common/q/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="3" name="Colibri2" version="0.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Colibri2" version="n/a" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="whyml" proved="true">
 <path name=".."/><path name="q.mlw"/>
 <theory name="QWithInf" proved="true">