diff --git a/.gitignore b/.gitignore
index 664bfb8a35991957c996ca70113c2971f9ab1645..9a29e7203869e1ecc46d5ff7d20d8bf5ac626a96 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,3 +15,15 @@ why3shapes.gz
 # dependencies (remove it later & use submodules instead ?)
 dolmen/
 farith/
+
+
+# doc
+*.html
+*.css
+*.pdf
+
+# temporary files
+*.swp
+
+# debug files
+*debug_graph.tmp/
diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
index e9d69bae383b85b99d0bbf1bf2f0c9626c2ab0b0..d71a6cbd80b95b8ebf31fdf4b203b2fbc048e894 100644
--- a/src_colibri2/bin/options.ml
+++ b/src_colibri2/bin/options.ml
@@ -50,7 +50,7 @@ let gc_opts minor_heap_size major_heap_increment space_overhead max_overhead
 let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
     input_mode input header_check header_licenses header_lang_version type_check
     type_strict debug context max_warn step_limit debug_flags show_steps
-    check_status dont_print_result =
+    check_status dont_print_result learning =
   List.iter
     Colibri2_popop_lib.Debug.(fun s -> set_flag (lookup_flag s))
     debug_flags;
@@ -60,7 +60,7 @@ let mk_state theories gc gc_opt bt colors time_limit size_limit input_lang
   ( Colibri2_solver.Input.mk_state ~gc ~gc_opt ~bt ~colors ~time_limit
       ~size_limit ?input_lang ?input_mode ~input ~header_check ~header_licenses
       ~header_lang_version ~type_check ~type_strict ~debug ~context ~max_warn
-      theories,
+      theories ~learning,
     step_limit,
     show_steps,
     check_status,
@@ -376,9 +376,15 @@ let state theories =
     in
     Arg.(value & flag & info [ "dont-print-result" ] ~docs ~doc)
   in
+  let learning =
+    let doc = Format.asprintf "Activate learning." in
+    Arg.(
+      value & flag
+      & info ~env:(env_var ~doc "COLIBRI2_LEARNING") [ "learning" ] ~docs ~doc)
+  in
   Term.(
     const (mk_state theories)
     $ gc $ gc_t $ bt $ colors $ time $ size $ in_lang $ in_mode $ input
     $ header_check $ header_licenses $ header_lang_version $ typing $ strict
     $ debug $ context $ max_warn $ step_limit $ debug_flags $ show_steps
-    $ check_status $ dont_print_result)
+    $ check_status $ dont_print_result $ learning)
diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index 5cadadd935415498fd931d392040f86aaec1fa57..3faa8c1483498af7b715d7335b7b836a4195af5a 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -200,14 +200,15 @@ module Events = struct
     | FixingModel
 
   type enqueue = Events.enqueue =
-    | EnqRun : 'r Dem.t * 'r -> enqueue  (** Schedule a daemon run *)
-    | EnqLast : 'r Dem.t * 'r -> enqueue
+    | EnqRun : 'r Dem.t * 'r * ThTerm.t option -> enqueue
+        (** Schedule a daemon run *)
+    | EnqLast : 'r Dem.t * 'r * ThTerm.t option -> enqueue
         (** Same as EnqRun but remove the waiting event *)
     | EnqAlready : enqueue  (** Don't run but keep the waiting event *)
     | EnqStopped : enqueue  (** Stop and don't run *)
 
   type daemon_key = Events.Wait.daemon_key =
-    | DaemonKey : 'runable Dem.t * 'runable -> daemon_key
+    | DaemonKey : 'runable Dem.t * 'runable * ThTerm.t option -> daemon_key
 
   module type T = Egraph.Wait.Dem
   (** Basic daemons *)
@@ -252,7 +253,11 @@ module Choice = struct
     | DecNo
     | DecTodo of (Egraph.wt -> unit) list
 
-  and t = Egraph.choice = { choice : Egraph.wt -> choice_state; prio : int }
+  and t = Egraph.choice = {
+    choice : Egraph.wt -> choice_state;
+    prio : int;
+    print_cho : string;
+  }
 
   let register = Egraph.register_decision
 end
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index 68d557c6289365d970934355705fb255e74e7217..f4611fd2572f033c9bb30e1b82a7150785bb22df 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -774,6 +774,7 @@ module Daemon : sig
 
   val attach_dom :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     'a Dom.Kind.t ->
@@ -785,10 +786,15 @@ module Daemon : sig
      set. *)
 
   val attach_any_dom :
-    _ Egraph.t -> 'a Dom.Kind.t -> (Egraph.wt -> Node.t -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    'a Dom.Kind.t ->
+    (Egraph.wt -> Node.t -> unit) ->
+    unit
 
   val attach_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     ('a, 'b) Value.Kind.t ->
@@ -797,26 +803,45 @@ module Daemon : sig
 
   val attach_any_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     (Egraph.wt -> Node.t -> Value.t -> unit) ->
     unit
 
-  val attach_reg_any : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
+  val attach_reg_any :
+    _ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.wt -> Node.t -> unit) -> unit
 
   val attach_reg_node :
-    _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    Node.t ->
+    (Egraph.wt -> Node.t -> unit) ->
+    unit
 
   val attach_reg_sem :
-    _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    ('a, 'b) ThTerm.Kind.t ->
+    (Egraph.wt -> 'b -> unit) ->
+    unit
 
   val attach_reg_value :
-    _ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    ('a, 'b) Value.Kind.t ->
+    (Egraph.wt -> 'b -> unit) ->
+    unit
 
   val attach_repr :
-    _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    Node.t ->
+    (Egraph.wt -> Node.t -> unit) ->
+    unit
 
-  val attach_any_repr : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
+  val attach_any_repr :
+    _ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.wt -> Node.t -> unit) -> unit
 end
 
 module DaemonFixingModel : sig
@@ -827,6 +852,7 @@ module DaemonFixingModel : sig
 
   val attach_dom :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     'a Dom.Kind.t ->
@@ -835,10 +861,15 @@ module DaemonFixingModel : sig
   (** [attach_dom d ?direct n dom callback] The callback is *)
 
   val attach_any_dom :
-    _ Egraph.t -> 'a Dom.Kind.t -> (Egraph.wt -> Node.t -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    'a Dom.Kind.t ->
+    (Egraph.wt -> Node.t -> unit) ->
+    unit
 
   val attach_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     ('a, 'b) Value.Kind.t ->
@@ -847,26 +878,45 @@ module DaemonFixingModel : sig
 
   val attach_any_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     (Egraph.wt -> Node.t -> Value.t -> unit) ->
     unit
 
-  val attach_reg_any : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
+  val attach_reg_any :
+    _ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.wt -> Node.t -> unit) -> unit
 
   val attach_reg_node :
-    _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    Node.t ->
+    (Egraph.wt -> Node.t -> unit) ->
+    unit
 
   val attach_reg_sem :
-    _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    ('a, 'b) ThTerm.Kind.t ->
+    (Egraph.wt -> 'b -> unit) ->
+    unit
 
   val attach_reg_value :
-    _ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    ('a, 'b) Value.Kind.t ->
+    (Egraph.wt -> 'b -> unit) ->
+    unit
 
   val attach_repr :
-    _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    Node.t ->
+    (Egraph.wt -> Node.t -> unit) ->
+    unit
 
-  val attach_any_repr : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
+  val attach_any_repr :
+    _ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.wt -> Node.t -> unit) -> unit
 end
 
 module DaemonWithFilter : sig
@@ -877,6 +927,7 @@ module DaemonWithFilter : sig
 
   val attach_dom :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     'a Dom.Kind.t ->
@@ -886,12 +937,14 @@ module DaemonWithFilter : sig
 
   val attach_any_dom :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     'a Dom.Kind.t ->
     (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
     unit
 
   val attach_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     ('a, 'b) Value.Kind.t ->
@@ -900,40 +953,51 @@ module DaemonWithFilter : sig
 
   val attach_any_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ?direct:bool ->
     Node.t ->
     (Egraph.rt -> Node.t -> Value.t -> (Egraph.wt -> unit) option) ->
     unit
 
   val attach_reg_any :
-    _ Egraph.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
+    unit
 
   val attach_reg_node :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     Node.t ->
     (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
     unit
 
   val attach_reg_sem :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ('a, 'b) ThTerm.Kind.t ->
     (Egraph.rt -> 'b -> (Egraph.wt -> unit) option) ->
     unit
 
   val attach_reg_value :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     ('a, 'b) Value.Kind.t ->
     (Egraph.rt -> 'b -> (Egraph.wt -> unit) option) ->
     unit
 
   val attach_repr :
     _ Egraph.t ->
+    ?thterm:ThTerm.t ->
     Node.t ->
     (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
     unit
 
   val attach_any_repr :
-    _ Egraph.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
+    _ Egraph.t ->
+    ?thterm:ThTerm.t ->
+    (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
+    unit
 end
 
 module Monad : sig
@@ -960,7 +1024,7 @@ module Monad : sig
 
   val ( && ) : sequence -> sequence -> sequence
 
-  val attach : _ Egraph.t -> sequence -> unit
+  val attach : _ Egraph.t -> ?thterm:ThTerm.t -> sequence -> unit
 end
 
 module rec DaemonWithKey : sig
@@ -978,12 +1042,20 @@ module rec DaemonWithKey : sig
 
   module Register (S : S) : sig
     val attach_dom :
-      _ Egraph.t -> ?direct:bool -> Node.t -> 'a Dom.Kind.t -> S.Key.t -> unit
+      _ Egraph.t ->
+      ?thterm:ThTerm.t ->
+      ?direct:bool ->
+      Node.t ->
+      'a Dom.Kind.t ->
+      S.Key.t ->
+      unit
 
-    val attach_any_dom : _ Egraph.t -> 'a Dom.Kind.t -> S.Key.t -> unit
+    val attach_any_dom :
+      _ Egraph.t -> ?thterm:ThTerm.t -> 'a Dom.Kind.t -> S.Key.t -> unit
 
     val attach_value :
       _ Egraph.t ->
+      ?thterm:ThTerm.t ->
       ?direct:bool ->
       Node.t ->
       ('a, 'b) Value.Kind.t ->
@@ -991,20 +1063,32 @@ module rec DaemonWithKey : sig
       unit
 
     val attach_any_value :
-      _ Egraph.t -> ?direct:bool -> Node.t -> S.Key.t -> unit
+      _ Egraph.t ->
+      ?thterm:ThTerm.t ->
+      ?direct:bool ->
+      Node.t ->
+      S.Key.t ->
+      unit
 
-    val attach_reg_any : _ Egraph.t -> S.Key.t -> unit
+    val attach_reg_any : _ Egraph.t -> ?thterm:ThTerm.t -> S.Key.t -> unit
 
-    val attach_reg_node : _ Egraph.t -> Node.t -> S.Key.t -> unit
+    val attach_reg_node :
+      _ Egraph.t -> ?thterm:ThTerm.t -> Node.t -> S.Key.t -> unit
 
-    val attach_reg_sem : _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> S.Key.t -> unit
+    val attach_reg_sem :
+      _ Egraph.t ->
+      ?thterm:ThTerm.t ->
+      ('a, 'b) ThTerm.Kind.t ->
+      S.Key.t ->
+      unit
 
     val attach_reg_value :
-      _ Egraph.t -> ('a, 'b) Value.Kind.t -> S.Key.t -> unit
+      _ Egraph.t -> ?thterm:ThTerm.t -> ('a, 'b) Value.Kind.t -> S.Key.t -> unit
 
-    val attach_repr : _ Egraph.t -> Node.t -> S.Key.t -> unit
+    val attach_repr :
+      _ Egraph.t -> ?thterm:ThTerm.t -> Node.t -> S.Key.t -> unit
 
-    val attach_any_repr : _ Egraph.t -> S.Key.t -> unit
+    val attach_any_repr : _ Egraph.t -> ?thterm:ThTerm.t -> S.Key.t -> unit
   end
 end
 
@@ -1025,13 +1109,15 @@ and Events : sig
     | FixingModel
 
   type enqueue =
-    | EnqRun : 'r Dem.t * 'r -> enqueue  (** Schedule a daemon run *)
-    | EnqLast : 'r Dem.t * 'r -> enqueue
+    | EnqRun : 'r Dem.t * 'r * ThTerm.t option -> enqueue
+        (** Schedule a daemon run *)
+    | EnqLast : 'r Dem.t * 'r * ThTerm.t option -> enqueue
         (** Same as EnqRun but remove the waiting event *)
     | EnqAlready : enqueue  (** Don't run but keep the waiting event *)
     | EnqStopped : enqueue  (** Stop and don't run *)
 
-  type daemon_key = DaemonKey : 'runable Dem.t * 'runable -> daemon_key
+  type daemon_key =
+    | DaemonKey : 'runable Dem.t * 'runable * ThTerm.t option -> daemon_key
 
   (** {3 Basic daemons} *)
   module type T = sig
@@ -1103,7 +1189,8 @@ and Events : sig
   val attach_any_repr : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
   (** wakeup when a node is not its representative class anymore *)
 
-  val new_pending_daemon : _ Egraph.t -> 'a Dem.t -> 'a -> unit
+  val new_pending_daemon :
+    _ Egraph.t -> ?thterm:ThTerm.t -> 'a Dem.t -> 'a -> unit
   (** register an event for later (immediate or not). *)
 end
 
@@ -1112,7 +1199,7 @@ end
 module Choice : sig
   type choice_state = DecNo | DecTodo of (Egraph.wt -> unit) list
 
-  and t = { choice : Egraph.wt -> choice_state; prio : int }
+  and t = { choice : Egraph.wt -> choice_state; prio : int; print_cho : string }
 
   val register : Egraph.wt -> t -> unit
   (** register a decision that would be scheduled later. The
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index dbe78b2b920e2fc389220050293289a8c550c55e..065a46de4fd816aa5154a4a2abab539acba5ca54 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -28,14 +28,23 @@ module type Attach = sig
   type result
 
   val attach_dom :
-    ( ?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit,
+    ( ?thterm:Nodes.ThTerm.t ->
+      ?direct:bool ->
+      Node.t ->
+      'a DomKind.t ->
+      (Node.t -> result) env ->
+      unit,
       'b )
     arg
 
-  val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit, 'b) arg
+  val attach_any_dom :
+    ( ?thterm:Nodes.ThTerm.t -> 'a DomKind.t -> (Node.t -> result) env -> unit,
+      'b )
+    arg
 
   val attach_value :
-    ( ?direct:bool ->
+    ( ?thterm:Nodes.ThTerm.t ->
+      ?direct:bool ->
       Node.t ->
       ('a, 'b) ValueKind.t ->
       (Node.t -> 'b -> result) env ->
@@ -44,23 +53,41 @@ module type Attach = sig
     arg
 
   val attach_any_value :
-    ( ?direct:bool -> Node.t -> (Node.t -> Value.t -> result) env -> unit,
+    ( ?thterm:Nodes.ThTerm.t ->
+      ?direct:bool ->
+      Node.t ->
+      (Node.t -> Value.t -> result) env ->
+      unit,
       'b )
     arg
 
-  val attach_reg_any : ((Node.t -> result) env -> unit, 'b) arg
+  val attach_reg_any :
+    (?thterm:Nodes.ThTerm.t -> (Node.t -> result) env -> unit, 'b) arg
 
-  val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
+  val attach_reg_node :
+    (?thterm:Nodes.ThTerm.t -> Node.t -> (Node.t -> result) env -> unit, 'b) arg
 
   val attach_reg_sem :
-    (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit, 'r) arg
+    ( ?thterm:Nodes.ThTerm.t ->
+      ('a, 'b) ThTermKind.t ->
+      ('b -> result) env ->
+      unit,
+      'r )
+    arg
 
   val attach_reg_value :
-    (('a, 'b) ValueKind.t -> ('b -> result) env -> unit, 'r) arg
+    ( ?thterm:Nodes.ThTerm.t ->
+      ('a, 'b) ValueKind.t ->
+      ('b -> result) env ->
+      unit,
+      'r )
+    arg
 
-  val attach_repr : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
+  val attach_repr :
+    (?thterm:Nodes.ThTerm.t -> Node.t -> (Node.t -> result) env -> unit, 'b) arg
 
-  val attach_any_repr : ((Node.t -> result) env -> unit, 'b) arg
+  val attach_any_repr :
+    (?thterm:Nodes.ThTerm.t -> (Node.t -> result) env -> unit, 'b) arg
 end
 
 module type Simple =
@@ -96,34 +123,41 @@ module Simple = struct
 
     let () = Egraph.Wait.register_dem (module D)
 
-    let wrap_node f _ n = Events.EnqRun (D.key, fun d -> f d n)
+    let wrap_node thterm f _ n = Events.EnqRun (D.key, (fun d -> f d n), thterm)
 
-    let wrap_node_and_other f _ n v = Events.EnqRun (D.key, fun d -> f d n v)
+    let wrap_node_and_other thterm f _ n v =
+      Events.EnqRun (D.key, (fun d -> f d n v), thterm)
 
-    let wrap_other f _ v = Events.EnqRun (D.key, fun d -> f d v)
+    let wrap_other thterm f _ v = Events.EnqRun (D.key, (fun d -> f d v), thterm)
 
-    let attach_dom d ?direct n dom f =
-      Egraph.attach_dom d ?direct n dom (wrap_node f)
+    let attach_dom d ?thterm ?direct n dom f =
+      Egraph.attach_dom d ?direct n dom (wrap_node thterm f)
 
-    let attach_any_dom d dom f = Egraph.attach_any_dom d dom (wrap_node f)
+    let attach_any_dom d ?thterm dom f =
+      Egraph.attach_any_dom d dom (wrap_node thterm f)
 
-    let attach_value d ?direct n v f =
-      Egraph.attach_value d ?direct n v (wrap_node_and_other f)
+    let attach_value d ?thterm ?direct n v f =
+      Egraph.attach_value d ?direct n v (wrap_node_and_other thterm f)
 
-    let attach_any_value d ?direct n f =
-      Egraph.attach_any_value d ?direct n (wrap_node_and_other f)
+    let attach_any_value d ?thterm ?direct n f =
+      Egraph.attach_any_value d ?direct n (wrap_node_and_other thterm f)
 
-    let attach_reg_any d f = Egraph.attach_reg_any d (wrap_node f)
+    let attach_reg_any d ?thterm f =
+      Egraph.attach_reg_any d (wrap_node thterm f)
 
-    let attach_reg_node d n f = Egraph.attach_reg_node d n (wrap_node f)
+    let attach_reg_node d ?thterm n f =
+      Egraph.attach_reg_node d n (wrap_node thterm f)
 
-    let attach_reg_sem d th f = Egraph.attach_reg_sem d th (wrap_other f)
+    let attach_reg_sem d ?thterm th f =
+      Egraph.attach_reg_sem d th (wrap_other thterm f)
 
-    let attach_reg_value d th f = Egraph.attach_reg_value d th (wrap_other f)
+    let attach_reg_value d ?thterm th f =
+      Egraph.attach_reg_value d th (wrap_other thterm f)
 
-    let attach_repr d n f = Egraph.attach_repr d n (wrap_node f)
+    let attach_repr d ?thterm n f = Egraph.attach_repr d n (wrap_node thterm f)
 
-    let attach_any_repr d f = Egraph.attach_any_repr d (wrap_node f)
+    let attach_any_repr d ?thterm f =
+      Egraph.attach_any_repr d (wrap_node thterm f)
   end
 
   module FixingModel = Make (struct
@@ -162,43 +196,48 @@ module WithFilter = struct
 
   let () = Egraph.Wait.register_dem (module D)
 
-  let wrap_node f d n =
+  let wrap_node thterm f d n =
     match f d n with
     | None -> Events.EnqAlready
-    | Some g -> Events.EnqRun (D.key, g)
+    | Some g -> Events.EnqRun (D.key, g, thterm)
 
-  let wrap_node_and_other f d n v =
+  let wrap_node_and_other thterm f d n v =
     match f d n v with
     | None -> Events.EnqAlready
-    | Some g -> Events.EnqRun (D.key, g)
+    | Some g -> Events.EnqRun (D.key, g, thterm)
 
-  let wrap_other f d v =
+  let wrap_other thterm f d v =
     match f d v with
     | None -> Events.EnqAlready
-    | Some g -> Events.EnqRun (D.key, g)
+    | Some g -> Events.EnqRun (D.key, g, thterm)
 
-  let attach_dom d ?direct n dom f =
-    Egraph.attach_dom d ?direct n dom (wrap_node f)
+  let attach_dom d ?thterm ?direct n dom f =
+    Egraph.attach_dom d ?direct n dom (wrap_node thterm f)
 
-  let attach_any_dom d dom f = Egraph.attach_any_dom d dom (wrap_node f)
+  let attach_any_dom d ?thterm dom f =
+    Egraph.attach_any_dom d dom (wrap_node thterm f)
 
-  let attach_value d ?direct n v f =
-    Egraph.attach_value d ?direct n v (wrap_node_and_other f)
+  let attach_value d ?thterm ?direct n v f =
+    Egraph.attach_value d ?direct n v (wrap_node_and_other thterm f)
 
-  let attach_any_value d ?direct n f =
-    Egraph.attach_any_value d ?direct n (wrap_node_and_other f)
+  let attach_any_value d ?thterm ?direct n f =
+    Egraph.attach_any_value d ?direct n (wrap_node_and_other thterm f)
 
-  let attach_reg_any d f = Egraph.attach_reg_any d (wrap_node f)
+  let attach_reg_any d ?thterm f = Egraph.attach_reg_any d (wrap_node thterm f)
 
-  let attach_reg_node d n f = Egraph.attach_reg_node d n (wrap_node f)
+  let attach_reg_node d ?thterm n f =
+    Egraph.attach_reg_node d n (wrap_node thterm f)
 
-  let attach_reg_sem d th f = Egraph.attach_reg_sem d th (wrap_other f)
+  let attach_reg_sem d ?thterm th f =
+    Egraph.attach_reg_sem d th (wrap_other thterm f)
 
-  let attach_reg_value d th f = Egraph.attach_reg_value d th (wrap_other f)
+  let attach_reg_value d ?thterm th f =
+    Egraph.attach_reg_value d th (wrap_other thterm f)
 
-  let attach_repr d n f = Egraph.attach_repr d n (wrap_node f)
+  let attach_repr d ?thterm n f = Egraph.attach_repr d n (wrap_node thterm f)
 
-  let attach_any_repr d f = Egraph.attach_any_repr d (wrap_node f)
+  let attach_any_repr d ?thterm f =
+    Egraph.attach_any_repr d (wrap_node thterm f)
 end
 
 module Key = struct
@@ -249,42 +288,48 @@ module Key = struct
           let print_runable = S.Key.pp
         end)
 
-    let wrap k d =
+    let wrap thterm k d =
       match H.find h d k with
       | Stop -> Events.EnqStopped
       | Wait ->
           H.set h d k Scheduled;
-          Events.EnqRun (key, k)
+          Events.EnqRun (key, k, thterm)
       | Scheduled -> Events.EnqAlready
 
-    let wrap_node k d _ = wrap k d
+    let wrap_node thterm k d _ = wrap thterm k d
 
-    let wrap_node_and_other k d _ _ = wrap k d
+    let wrap_node_and_other thterm k d _ _ = wrap thterm k d
 
-    let wrap_other k d _ = wrap k d
+    let wrap_other thterm k d _ = wrap thterm k d
 
-    let attach_dom d ?direct n dom f =
-      Egraph.attach_dom d ?direct n dom (wrap_node f)
+    let attach_dom d ?thterm ?direct n dom f =
+      Egraph.attach_dom d ?direct n dom (wrap_node thterm f)
 
-    let attach_any_dom d dom f = Egraph.attach_any_dom d dom (wrap_node f)
+    let attach_any_dom d ?thterm dom f =
+      Egraph.attach_any_dom d dom (wrap_node thterm f)
 
-    let attach_value d ?direct n v f =
-      Egraph.attach_value d ?direct n v (wrap_node_and_other f)
+    let attach_value d ?thterm ?direct n v f =
+      Egraph.attach_value d ?direct n v (wrap_node_and_other thterm f)
 
-    let attach_any_value d ?direct v f =
-      Egraph.attach_any_value d ?direct v (wrap_node_and_other f)
+    let attach_any_value d ?thterm ?direct v f =
+      Egraph.attach_any_value d ?direct v (wrap_node_and_other thterm f)
 
-    let attach_reg_any d f = Egraph.attach_reg_any d (wrap_node f)
+    let attach_reg_any d ?thterm f =
+      Egraph.attach_reg_any d (wrap_node thterm f)
 
-    let attach_reg_node d n f = Egraph.attach_reg_node d n (wrap_node f)
+    let attach_reg_node d ?thterm n f =
+      Egraph.attach_reg_node d n (wrap_node thterm f)
 
-    let attach_reg_sem d th f = Egraph.attach_reg_sem d th (wrap_other f)
+    let attach_reg_sem d ?thterm th f =
+      Egraph.attach_reg_sem d th (wrap_other thterm f)
 
-    let attach_reg_value d th f = Egraph.attach_reg_value d th (wrap_other f)
+    let attach_reg_value d ?thterm th f =
+      Egraph.attach_reg_value d th (wrap_other thterm f)
 
-    let attach_repr d n f = Egraph.attach_repr d n (wrap_node f)
+    let attach_repr d ?thterm n f = Egraph.attach_repr d n (wrap_node thterm f)
 
-    let attach_any_repr d f = Egraph.attach_any_repr d (wrap_node f)
+    let attach_any_repr d ?thterm f =
+      Egraph.attach_any_repr d (wrap_node thterm f)
   end
 end
 
@@ -418,11 +463,11 @@ module Monad = struct
     | SetD (_, _, f) -> attach_aux compute d f
     | UpdD (_, _, f) -> attach_aux compute d f
 
-  let attach d seq =
+  let attach d ?thterm seq =
     let compute d =
       match compute_seq d D.Nil seq with
       | Nil -> Events.EnqAlready
-      | r -> Events.EnqRun (D.key, r)
+      | r -> Events.EnqRun (D.key, r, thterm)
     in
     let ft =
       { doms = DomKind.Vector.create 10; sems = ValueKind.Vector.create 10 }
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index b02bdb2f472831b9f9b9330b6c32505d2664a7eb..cc089afd200614853e031d0e3d3dcc19259cf65b 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -28,14 +28,23 @@ module type Attach = sig
   type result
 
   val attach_dom :
-    ( ?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit,
+    ( ?thterm:Nodes.ThTerm.t ->
+      ?direct:bool ->
+      Node.t ->
+      'a DomKind.t ->
+      (Node.t -> result) env ->
+      unit,
       'b )
     arg
 
-  val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit, 'b) arg
+  val attach_any_dom :
+    ( ?thterm:Nodes.ThTerm.t -> 'a DomKind.t -> (Node.t -> result) env -> unit,
+      'b )
+    arg
 
   val attach_value :
-    ( ?direct:bool ->
+    ( ?thterm:Nodes.ThTerm.t ->
+      ?direct:bool ->
       Node.t ->
       ('a, 'b) ValueKind.t ->
       (Node.t -> 'b -> result) env ->
@@ -44,23 +53,41 @@ module type Attach = sig
     arg
 
   val attach_any_value :
-    ( ?direct:bool -> Node.t -> (Node.t -> Value.t -> result) env -> unit,
+    ( ?thterm:Nodes.ThTerm.t ->
+      ?direct:bool ->
+      Node.t ->
+      (Node.t -> Value.t -> result) env ->
+      unit,
       'b )
     arg
 
-  val attach_reg_any : ((Node.t -> result) env -> unit, 'b) arg
+  val attach_reg_any :
+    (?thterm:Nodes.ThTerm.t -> (Node.t -> result) env -> unit, 'b) arg
 
-  val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
+  val attach_reg_node :
+    (?thterm:Nodes.ThTerm.t -> Node.t -> (Node.t -> result) env -> unit, 'b) arg
 
   val attach_reg_sem :
-    (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit, 'r) arg
+    ( ?thterm:Nodes.ThTerm.t ->
+      ('a, 'b) ThTermKind.t ->
+      ('b -> result) env ->
+      unit,
+      'r )
+    arg
 
   val attach_reg_value :
-    (('a, 'b) ValueKind.t -> ('b -> result) env -> unit, 'r) arg
+    ( ?thterm:Nodes.ThTerm.t ->
+      ('a, 'b) ValueKind.t ->
+      ('b -> result) env ->
+      unit,
+      'r )
+    arg
 
-  val attach_repr : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
+  val attach_repr :
+    (?thterm:Nodes.ThTerm.t -> Node.t -> (Node.t -> result) env -> unit, 'b) arg
 
-  val attach_any_repr : ((Node.t -> result) env -> unit, 'b) arg
+  val attach_any_repr :
+    (?thterm:Nodes.ThTerm.t -> (Node.t -> result) env -> unit, 'b) arg
 end
 
 module type Simple =
@@ -113,10 +140,7 @@ module Monad : sig
   val setd : 'a DomKind.t -> Node.t -> 'a option monad -> sequence
 
   val updd :
-    (Egraph.wt -> Node.t -> 'a -> unit) ->
-    Node.t ->
-    'a option monad ->
-    sequence
+    (Egraph.wt -> Node.t -> 'a -> unit) -> Node.t -> 'a option monad -> sequence
 
   val getv : ('a, _) ValueKind.t -> Node.t -> 'a option monad
 
@@ -130,5 +154,5 @@ module Monad : sig
 
   val ( && ) : sequence -> sequence -> sequence
 
-  val attach : _ Egraph.t -> sequence -> unit
+  val attach : _ Egraph.t -> ?thterm:Nodes.ThTerm.t -> sequence -> unit
 end
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 7a8c8e75e2d15ab2171140bde404188c9c355172..2c2f38b969e55b7a1093ca39fc329f6d006ad470 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -155,6 +155,7 @@ module Def = struct
   and choice = {
     choice: rw delayed_t -> choice_state;
     prio: int;
+    print_cho: string;
   }
 
   let nothing_todo t =
@@ -179,6 +180,7 @@ open Def
 type choice = Def.choice = {
   choice: rw delayed_t -> choice_state;
   prio: int;
+  print_cho: string;
 }
 type choice_state = Def.choice_state =
   | DecNo
@@ -193,9 +195,9 @@ end
 module Wait : Events.Wait.S with type delayed = rw delayed_t =
   Events.Wait.Make(WaitDef)
 
-let new_pending_daemon (type d) t (dem : d Events.Dem.t) runable =
+let new_pending_daemon (type d) t ?thterm (dem : d Events.Dem.t) runable =
   let module Dem = (val Wait.get_dem dem) in
-  let daemonkey = Events.Wait.DaemonKey (dem, runable) in
+  let daemonkey = Events.Wait.DaemonKey (dem, runable, thterm) in
   match Dem.delay with
   | Immediate -> Queue.push (RunDem daemonkey) t.todo_immediate_dem
   | _ -> t.sched_daemon daemonkey
@@ -332,7 +334,6 @@ module T = struct
   let is_registered t node =
     Node.M.mem node t.repr
 
-
 end
 open T
 
@@ -498,10 +499,10 @@ module Delayed = struct
     match apply (t:> ro t) e with
     | Events.EnqStopped -> None
     | EnqAlready -> Some e
-    | EnqRun (dem,runable) ->
+    | EnqRun (dem,runable,_) ->
       new_pending_daemon t dem runable;
       Some e
-    | EnqLast (dem,runable) ->
+    | EnqLast (dem,runable,_) ->
       new_pending_daemon t dem runable;
       None
 
@@ -875,7 +876,7 @@ module Delayed = struct
      - daemon not immediate
   *)
 
-  let rec do_pending_daemon delayed (Events.Wait.DaemonKey (dem,runable)) =
+  let rec do_pending_daemon delayed (Events.Wait.DaemonKey (dem,runable,_)) =
     let (module Dem) = Wait.get_dem dem in
     Dem.run delayed runable
 
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index c51486a2e7e03aa82e4eb6c9712477d02757fb64..5e51dd991fb5cf482450b5d5c5d2d417fa349efe 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -125,6 +125,7 @@ type choice_state =
 and choice = {
   choice: wt -> choice_state;
   prio: int;
+  print_cho: string;
 }
 
 val register_decision: wt -> choice -> unit
@@ -132,7 +133,7 @@ val register_decision: wt -> choice -> unit
     [choose_decision] of the [Cho] will be called at that time to know
     if the decision is still needed. *)
 
-val new_pending_daemon: _ t -> 'a Events.Dem.t -> 'a -> unit
+val new_pending_daemon: _ t -> ?thterm:Nodes.ThTerm.t -> 'a Events.Dem.t -> 'a -> unit
 (** register an event for later (immediate or not). *)
 
 val contradiction: _ t -> 'b
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 3fafbd9c4ec434f69327fed7bf7c25209775fc6d..2641ad0178b3526dfc033edb3aa440d08cc0a15e 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -37,14 +37,18 @@ end
 type delay = Immediate | Delayed_by of int | LastEffort of int | FixingModel
 
 type enqueue =
-  | EnqRun : 'r Dem.t * 'r -> enqueue  (** Schedule a daemon run *)
-  | EnqLast : 'r Dem.t * 'r -> enqueue
+  | EnqRun : 'r Dem.t * 'r * Nodes.ThTerm.t option -> enqueue
+      (** Schedule a daemon run *)
+  | EnqLast : 'r Dem.t * 'r * Nodes.ThTerm.t option -> enqueue
       (** Same as EnqRun but remove the waiting event *)
   | EnqAlready : enqueue  (** Don't run but keep the waiting event *)
   | EnqStopped : enqueue  (** Stop and don't run *)
 
 module Wait = struct
-  type daemon_key = DaemonKey : 'runable Dem.t * 'runable -> daemon_key
+  type daemon_key =
+    | DaemonKey :
+        'runable Dem.t * 'runable * Nodes.ThTerm.t option
+        -> daemon_key
 
   module type S = sig
     type delayed
@@ -106,7 +110,7 @@ module Wait = struct
     let get_dem = Registry.get
 
     let get_priority = function
-      | DaemonKey (dem, _) ->
+      | DaemonKey (dem, _, _) ->
           let module Dem = (val get_dem dem) in
           Dem.delay
 
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index 343cf612d3e992c5fa00b320318cd290d2ded32d..2f744c27eb2d1501bdd8a4083fbe73b6e31059a7 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -28,14 +28,18 @@ type delay =
   | FixingModel
 
 type enqueue =
-  | EnqRun : 'r Dem.t * 'r -> enqueue  (** Schedule a daemon run *)
-  | EnqLast : 'r Dem.t * 'r -> enqueue
+  | EnqRun : 'r Dem.t * 'r * Nodes.ThTerm.t option -> enqueue
+      (** Schedule a daemon run *)
+  | EnqLast : 'r Dem.t * 'r * Nodes.ThTerm.t option -> enqueue
       (** Same as EnqRun but remove the waiting event *)
   | EnqAlready : enqueue  (** Don't run but keep the waiting event *)
   | EnqStopped : enqueue  (** Stop and don't run *)
 
 module Wait : sig
-  type daemon_key = DaemonKey : 'runable Dem.t * 'runable -> daemon_key
+  type daemon_key =
+    | DaemonKey :
+        'runable Dem.t * 'runable * Nodes.ThTerm.t option
+        -> daemon_key
 
   module type S = sig
     type delayed
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index f650ed2aae2e08ed3946d3bbf9914ba09ea42bc0..3031ec4dd9db7c5af4b85b034ab92b9d4a5cc61e 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -1,4 +1,4 @@
-(*************************************************************************)
+(************************************************************************)
 (*  This file is part of Colibri2.                                       *)
 (*                                                                       *)
 (*  Copyright (C) 2014-2021                                              *)
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index b3f027adcb9bd5f11115122d49455b32ffb27e47..0e513f3f25c5f2c0e754ec6c8454ea822286d38e 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -542,7 +542,7 @@ module WatchArgs = struct
 
     let attach d r i =
       Egraph.attach_any_value d (IArray.get (Ground.sem r.ground).args i)
-        (fun _ _ _ -> Events.EnqRun (key, r))
+        (fun _ _ _ -> Events.EnqRun (key, r, None))
 
     let run d r =
       let o_current = Context.Ref.get r.current in
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 1885e6518d616e408b58c4e2e99d4f53d3a1bfba..07ed927216150b2a36ac409fb7e13fbed9ef6827 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -32,8 +32,8 @@ type ctx = {
   decls : Expr.Term.Const.t Context.Queue.t;
 }
 
-let create_ctx theories =
-  let t = Scheduler.new_solver () in
+let create_ctx learning theories =
+  let t = Scheduler.new_solver ~learning () in
   let ctx = Scheduler.get_context t in
   Scheduler.init_theories t ~theories;
   {
@@ -376,7 +376,8 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
     ?(time_limit = 1_000_000_000.) ?(size_limit = 1_000_000_000.) ?input_lang
     ?input_mode ~input ?(header_check = false) ?(header_licenses = [])
     ?(header_lang_version = None) ?(type_check = true) ?(type_strict = true)
-    ?(debug = false) ?(context = true) ?(max_warn = max_int) theories =
+    ?(debug = false) ?(context = true) ?(max_warn = max_int) ?(learning = false)
+    theories =
   (* Side-effects *)
   let () = Gc.set gc_opt in
   let () =
@@ -407,7 +408,7 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
       type_check;
       type_strict;
       type_state = Dolmen_loop.Typer.new_state ();
-      solve_state = create_ctx theories;
+      solve_state = create_ctx learning theories;
       export_lang = [];
     }
   in
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 2915ed8e6aeeb71b1b86264e36c25300c43e71fc..2f46a03e276c2a8f0751f49aae1c0e29c1fd3f78 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -1,4 +1,4 @@
-(*************************************************************************)
+(************************************************************************)
 (*  This file is part of Colibri2.                                       *)
 (*                                                                       *)
 (*  Copyright (C) 2014-2021                                              *)
@@ -22,83 +22,102 @@ open Colibri2_popop_lib
 open Colibri2_core
 open ForSchedulers
 
-let debug = Debug.register_info_flag
-  ~desc:"for the scheduler in the simple version"
-  "sched_queue"
-
-let debug_pushpop = Debug.register_info_flag
-  ~desc:"for the scheduler push/pop"
-  "sched_pushpop"
+let debug =
+  Debug.register_info_flag ~desc:"for the scheduler in the simple version"
+    "sched_queue"
 
-let debug_dotgui = Debug.register_flag
-  ~desc:"print graph at interesting time (push/pop)"
-  "sched_dotgui"
+let debug_pushpop =
+  Debug.register_info_flag ~desc:"for the scheduler push/pop" "sched_pushpop"
 
+let debug_dotgui =
+  Debug.register_flag ~desc:"print graph at interesting time (push/pop)"
+    "sched_dotgui"
 
 let var_decay = 1. /. 0.95
 
 let stats_propa = Debug.register_stats_int ~name:"Scheduler.daemon" ~init:0
-let stats_lasteffort = Debug.register_stats_int ~name:"Scheduler.lasteffort" ~init:0
+
+let stats_lasteffort =
+  Debug.register_stats_int ~name:"Scheduler.lasteffort" ~init:0
+
 let stats_dec = Debug.register_stats_int ~name:"Scheduler.decision" ~init:0
+
 let stats_con = Debug.register_stats_int ~name:"Scheduler.conflict" ~init:0
+
 let stats_step = Debug.register_stats_int ~name:"Scheduler.step" ~init:0
-let stats_fix_model = Debug.register_stats_int ~name:"Scheduler.fix_model" ~init:0
+
+let stats_fix_model =
+  Debug.register_stats_int ~name:"Scheduler.fix_model" ~init:0
 
 exception Contradiction
 
+exception ReachStepLimit
+
 module Att = struct
-  type t =
-    | Decision of int * Choice.t
+  type t = Decision of int * Choice.t
+
   type prio = float
+
   type db = float Node.H.t
 
-  let le (x:t) (xp:float) (y:t) (yp:float) =
-    match x, y with
-    | Decision (x,_), Decision (y,_) ->
-      if xp = yp then x <= y else xp >= yp (** min *)
-  let reprio _ = function
-    | Decision (_,choice) -> float_of_int choice.prio
+  let le (x : t) (xp : float) (y : t) (yp : float) =
+    match (x, y) with
+    | Decision (x, _), Decision (y, _) -> if xp = yp then x <= y else xp >= yp
+  (* min *)
+
+  let reprio _ = function Decision (_, choice) -> float_of_int choice.prio
 end
 
-module Prio = Leftistheap.Make(Att)
-
-type bp_kind =
-  | Choices of (Egraph.wt -> unit) Base.Sequence.t
-  | External
-
-type bp =
-  { pre_choices    : Prio.t;
-    pre_prev_scheduler_state : bp option;
-    pre_backtrack_point      : Context.bp;
-    kind                     : bp_kind;
-    pre_level                : int;
-  }
-
-type solve_step =
-  | Propagate
-  | FixModel
-
-type t =
-  { mutable choices    : Prio.t;
-    daemons : Events.daemon_key Context.TimeWheel.t;
-    lasteffort : Events.daemon_key Context.TimeWheel.t;
-    fixing_model : Events.daemon_key list Context.Ref.t;
-    mutable prev_scheduler_state : bp option;
-            solver_state      : Backtrackable.t;
-    (* global *)
-    decprio : Att.db;
-    var_inc  : float ref;
-    context : Context.context;
-    mutable level: int;
-    solve_step: solve_step Context.Ref.t;
-    mutable steps: int;
-  }
+module Prio = Leftistheap.Make (Att)
+
+module LearnSet = Set.Make (struct
+  type t = Ground.t
+
+  let compare = compare
+end)
+
+type bp_kind = Choices of (Egraph.wt -> unit) Base.Sequence.t | External
+
+type bp = {
+  pre_choices : Prio.t;
+  pre_prev_scheduler_state : bp option;
+  pre_backtrack_point : Context.bp;
+  kind : bp_kind;
+  pre_level : int;
+  last_todo : (Egraph.wt -> unit) * bp_kind;
+}
+
+type solve_step = Propagate | FixModel
+
+type t = {
+  mutable choices : Prio.t;
+  daemons : Events.daemon_key Context.TimeWheel.t;
+  lasteffort : Events.daemon_key Context.TimeWheel.t;
+  fixing_model : Events.daemon_key list Context.Ref.t;
+  mutable prev_scheduler_state : bp option;
+  solver_state : Backtrackable.t;
+  (* global *)
+  decprio : Att.db;
+  var_inc : float ref;
+  context : Context.context;
+  mutable level : int;
+  solve_step : solve_step Context.Ref.t;
+  mutable steps : int;
+  mutable stepsl : int;
+  mutable last_todo : (Egraph.wt -> unit) * bp_kind;
+  allow_learning : bool;
+  mutable learning : bool;
+  mutable learning_htbl : int ThTerm.H.t;
+  mutable learning_tbl : int array;
+}
 (** To treat in the reverse order *)
 
 let print_level fmt t =
   let nb_dec =
-    Prio.fold (fun acc x _ -> match x with Att.Decision _ -> acc + 1)
-      0 t.choices in
+    Prio.fold
+      (fun acc x _ -> match x with Att.Decision _ -> acc + 1)
+      0 t.choices
+  in
   Format.fprintf fmt "%i (dec waiting:%i)" t.level nb_dec
 
 let get_steps t = t.steps
@@ -114,12 +133,13 @@ let get_steps t = t.steps
  *    var_inc = t.var_inc
  *   } *)
 
-let new_solver () =
+let new_solver ~learning () =
   let context = Context.create () in
   let daemon_count = ref (-1) in
   let dec_count = ref (-1) in
   let t =
-    { choices = Prio.empty;
+    {
+      choices = Prio.empty;
       daemons = Context.TimeWheel.create (Context.creator context);
       lasteffort = Context.TimeWheel.create (Context.creator context);
       fixing_model = Context.Ref.create (Context.creator context) [];
@@ -129,8 +149,14 @@ let new_solver () =
       decprio = Node.H.create 100;
       var_inc = ref 1.;
       level = 0;
-      solve_step = Context.Ref.create (Context.creator context) (Propagate);
+      solve_step = Context.Ref.create (Context.creator context) Propagate;
       steps = 0;
+      stepsl = 0;
+      last_todo = ((fun _ -> ()), External);
+      allow_learning = learning;
+      learning = false;
+      learning_htbl = ThTerm.H.create 32;
+      learning_tbl = Array.make 0 0;
     }
   in
   let sched_daemon att =
@@ -139,46 +165,46 @@ let new_solver () =
     match get_event_priority att with
     | Immediate -> assert false (* absurd *)
     | Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
-    | LastEffort offset ->
-      Context.TimeWheel.add t.lasteffort att offset
+    | LastEffort offset -> Context.TimeWheel.add t.lasteffort att offset
     | FixingModel ->
-      Context.Ref.set t.fixing_model (att :: (Context.Ref.get t.fixing_model))
+        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;
-    t.choices <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
-        t.choices in
+    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
   Backtrackable.set_sched ~sched_daemon ~sched_decision t.solver_state;
   t
 
-
 let push kind t =
   if Colibri2_popop_lib.Debug.test_flag debug_dotgui then
     Backtrackable.draw_graph ~force:true t.solver_state;
   Debug.dprintf2 debug_pushpop "[Scheduler] push from %a" print_level t;
   let prev =
-    { pre_choices    = t.choices;
+    {
+      pre_choices = t.choices;
       pre_prev_scheduler_state = t.prev_scheduler_state;
-      pre_backtrack_point      = Context.bp t.context;
+      pre_backtrack_point = Context.bp t.context;
       kind;
       pre_level = t.level;
-    } in
+      last_todo = t.last_todo;
+    }
+  in
   t.level <- t.level + 1;
   t.prev_scheduler_state <- Some prev;
   ignore (Context.push t.context);
   prev
 
 let pop_to t prev =
-  Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a"
-    print_level t;
+  Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a" print_level t;
   t.choices <- prev.pre_choices;
   t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
   t.level <- prev.pre_level;
   Context.pop prev.pre_backtrack_point;
+  t.last_todo <- prev.last_todo;
   Backtrackable.draw_graph t.solver_state;
-  Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
-    print_level t
+  Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a" print_level t
 
 (*
   let rec apply_learnt llearnt t d =
@@ -198,7 +224,6 @@ let pop_to t prev =
         conflict_analysis t pexp
 *)
 
-
 (*
   and conflict_analysis t pexp =
     Debug.incr stats_con;
@@ -224,7 +249,177 @@ let pop_to t prev =
     pop_to llearnt t prev
 *)
 
+let run_one_step_propagation_l t =
+  match Context.TimeWheel.next t.daemons with
+  | Some att -> (
+      let (Events.DaemonKey (_, _, blob)) = att in
+      Debug.dprintf0 debug "[Learning] New daemons";
+      match blob with
+      | Some blob -> (
+          Debug.dprintf2 debug "[Learning] %a" ThTerm.pp blob;
+          if t.learning then (
+            (match ThTerm.H.find_opt t.learning_htbl blob with
+            | None ->
+                ThTerm.H.add t.learning_htbl blob
+                  (ThTerm.H.length t.learning_htbl)
+            | Some _ -> ());
+            let d = Backtrackable.get_delayed t.solver_state in
+            Backtrackable.run_daemon d att;
+            true)
+          else
+            match ThTerm.H.find_opt t.learning_htbl blob with
+            | Some i when t.learning_tbl.(i) = 1 ->
+                let d = Backtrackable.get_delayed t.solver_state in
+                Backtrackable.run_daemon d att;
+                true
+            | Some _ -> true
+            | None ->
+                Debug.dprintf0 debug "[Learning] Impossible";
+                raise ReachStepLimit)
+      | None ->
+          Debug.dprintf0 debug "[Learning] Daemons without blob";
+          let d = Backtrackable.get_delayed t.solver_state in
+          Backtrackable.run_daemon d att;
+          true)
+  | None ->
+      Debug.dprintf0 debug "[Learning] Impossible";
+      raise ReachStepLimit
+
+let run_one_step_l t =
+  t.stepsl <- t.stepsl + 1;
+  Debug.dprintf1 debug "[Learning] Step %i" t.stepsl;
+  match run_one_step_propagation_l t with true -> true | false -> false
+
+let rec run_inf_step_l limit t =
+  if t.stepsl = limit then raise ReachStepLimit;
+  Backtrackable.flush t.solver_state;
+  match run_one_step_l t with
+  | true -> run_inf_step_l limit t
+  | false -> Backtrackable.delayed_stop t.solver_state
+
+let learn t =
+  let rec bissec limit prev todo todos i j =
+    Debug.dprintf2 debug "[Scheduler] Bissec %i %i" i j;
+    match j - i with
+    | 0 -> ()
+    | _ -> (
+        pop_to t prev;
+        t.choices <- Prio.reprio t.decprio t.choices;
+        t.last_todo <- (todo, Choices todos);
+        ignore (push (Choices todos) t);
+        t.stepsl <- 0;
+        let m = (i + j) / 2 in
+        for k = m + 1 to j do
+          t.learning_tbl.(k) <- 0
+        done;
+        ThTerm.H.iter
+          (fun x i ->
+            if t.learning_tbl.(i) = 1 then
+              Debug.dprintf2 debug "[Learning] %a" ThTerm.pp x)
+          t.learning_htbl;
+        try
+          todo (Backtrackable.get_delayed t.solver_state);
+          Backtrackable.flush t.solver_state;
+          run_inf_step_l limit t
+        with
+        | Egraph.Contradiction ->
+            Debug.dprintf0 debug "[Scheduler] Bissec contradiction";
+            if i = m then (
+              Debug.dprintf0 debug "[Scheduler] Bissec";
+              pop_to t prev;
+              t.choices <- Prio.reprio t.decprio t.choices;
+              t.last_todo <- (todo, Choices todos);
+              ignore (push (Choices todos) t);
+              t.stepsl <- 0;
+              t.learning_tbl.(i) <- 0;
+              ThTerm.H.iter
+                (fun x i ->
+                  if t.learning_tbl.(i) = 1 then
+                    Debug.dprintf2 debug "[Learning] %a" ThTerm.pp x)
+                t.learning_htbl;
+              try
+                todo (Backtrackable.get_delayed t.solver_state);
+                Backtrackable.flush t.solver_state;
+                run_inf_step_l limit t
+              with
+              | Egraph.Contradiction ->
+                  Debug.dprintf0 debug "[Scheduler] Bissec contradiction"
+              | ReachStepLimit ->
+                  Debug.dprintf0 debug "[Scheduler] Bissec reach step limit";
+                  t.learning_tbl.(i) <- 1)
+            else bissec limit prev todo todos i m
+        | ReachStepLimit ->
+            Debug.dprintf0 debug "[Scheduler] Bissec reach step limit";
+            for k = m to j do
+              t.learning_tbl.(k) <- 1
+            done;
+            if i = m then (
+              Debug.dprintf0 debug "[Scheduler] Bissec";
+              pop_to t prev;
+              t.choices <- Prio.reprio t.decprio t.choices;
+              t.last_todo <- (todo, Choices todos);
+              ignore (push (Choices todos) t);
+              t.stepsl <- 0;
+              t.learning_tbl.(i) <- 0;
+              ThTerm.H.iter
+                (fun x i ->
+                  if t.learning_tbl.(i) = 1 then
+                    Debug.dprintf2 debug "[Learning] %a" ThTerm.pp x)
+                t.learning_htbl;
+              try
+                todo (Backtrackable.get_delayed t.solver_state);
+                Backtrackable.flush t.solver_state;
+                run_inf_step_l limit t
+              with
+              | Egraph.Contradiction ->
+                  Debug.dprintf0 debug "[Scheduler] Bissec contradiction"
+              | ReachStepLimit ->
+                  Debug.dprintf0 debug "[Scheduler] Bissec reach step limit";
+                  t.learning_tbl.(i) <- 1)
+            else (
+              bissec limit prev todo todos (m + 1) j;
+              bissec limit prev todo todos i m))
+  in
+
+  Debug.dprintf0 debug "[Scheduler] Learning";
+  match t.prev_scheduler_state with
+  | None -> ()
+  | Some prev -> (
+      match t.last_todo with
+      | _, External -> ()
+      | todo, Choices todos -> (
+          pop_to t prev;
+          t.choices <- Prio.reprio t.decprio t.choices;
+          t.last_todo <- (todo, Choices todos);
+          ignore (push (Choices todos) t);
+          t.stepsl <- 0;
+          try
+            t.learning <- true;
+            todo (Backtrackable.get_delayed t.solver_state);
+            Backtrackable.flush t.solver_state;
+            run_inf_step_l (-1) t
+          with Egraph.Contradiction ->
+            let j = ThTerm.H.length t.learning_htbl in
+            t.learning_tbl <- Array.make j 1;
+            ThTerm.H.iter
+              (fun x i ->
+                if t.learning_tbl.(i) = 1 then
+                  Debug.dprintf2 debug "[Learning] %a" ThTerm.pp x)
+              t.learning_htbl;
+            t.learning <- false;
+            if ThTerm.H.length t.learning_htbl = 0 then ()
+            else bissec (t.stepsl + 1) prev todo todos 0 (j - 1);
+            ThTerm.H.iter
+              (fun x i ->
+                if t.learning_tbl.(i) = 1 then
+                  Debug.dprintf2 debug "[Learning] %a" ThTerm.pp x)
+              t.learning_htbl;
+            ThTerm.H.reset t.learning_htbl;
+            t.learning_tbl <- Array.make 0 0))
+
 let rec conflict_analysis t =
+  if t.allow_learning then learn t;
+  Debug.dprintf0 debug "[Scheduler] End of learning";
   if Colibri2_popop_lib.Debug.test_flag debug_dotgui then
     Backtrackable.draw_graph ~force:true t.solver_state;
   Debug.incr stats_con;
@@ -232,46 +427,50 @@ let rec conflict_analysis t =
   let rec rewind () =
     match t.prev_scheduler_state with
     | None ->
-      Debug.dprintf0 debug "[Scheduler] learnt clause false at level 0";
-      raise Contradiction
-    | Some prev ->
-      pop_to t prev;
-      t.choices <- Prio.reprio t.decprio t.choices;
-      match prev.kind with
-      | Choices seq -> begin
-        match Base.Sequence.next seq with
-        | None -> rewind ()
-        | Some (choice,choices) ->
-          make_choice t choice choices
-      end
-      | External -> raise Contradiction
+        Debug.dprintf0 debug "[Scheduler] learnt clause false at level 0";
+        raise Contradiction
+    | Some prev -> (
+        pop_to t prev;
+        t.choices <- Prio.reprio t.decprio t.choices;
+        match prev.kind with
+        | Choices seq -> (
+            match Base.Sequence.next seq with
+            | None -> rewind ()
+            | Some (choice, choices) -> make_choice t choice choices)
+        | External -> raise Contradiction)
   in
   rewind ()
 
-and try_run_dec:
-  t -> Prio.t -> Choice.t -> unit = fun t prio choice ->
-  (** First we verify its the decision is at this point needed *)
+and try_run_dec : t -> Prio.t -> Choice.t -> unit =
+ fun t prio choice ->
+  (* First we verify its the decision is at this point needed *)
   let d = Backtrackable.get_delayed t.solver_state in
   match choice.choice d with
-  | Choice.DecNo | Choice.DecTodo [] ->
-    t.choices <- prio
-  | Choice.DecTodo (todo::todos) ->
-    (** We remove the decision it is replaced by the todos,
-        we can change the interface of choice and in that case
-        we want to keep the decision in the current branch *)
-    t.choices <- prio;
-    Debug.incr stats_dec;
-    Backtrackable.delayed_stop t.solver_state;
-    make_choice t todo (Base.Sequence.of_list todos)
+  | Choice.DecNo ->
+      Debug.dprintf1 debug "%s : no choice" choice.print_cho;
+      t.choices <- prio
+  | Choice.DecTodo [] ->
+      Debug.dprintf1 debug "%s : no more choices" choice.print_cho;
+      t.choices <- prio
+  | Choice.DecTodo (todo :: todos) ->
+      (* We remove the decision it is replaced by the todos,
+          we can change the interface of choice and in that case
+          we want to keep the decision in the current branch *)
+      t.choices <- prio;
+      Debug.dprintf1 debug "%s : done" choice.print_cho;
+      Debug.incr stats_dec;
+      Backtrackable.delayed_stop t.solver_state;
+      make_choice t todo (Base.Sequence.of_list todos)
 
 and make_choice t todo todos =
+  t.last_todo <- (todo, Choices todos);
   ignore (push (Choices todos) t);
-  try
-    todo (Backtrackable.get_delayed t.solver_state)
+  try todo (Backtrackable.get_delayed t.solver_state)
   with Egraph.Contradiction ->
+    Debug.dprintf2 debug_pushpop
+      "[Scheduler] Contradiction when chosing at level %a" print_level t;
     conflict_analysis t
 
-
 (* let rec run_until_dec t d =
  *   let act = Prio.min t.choices in
  *   match act with
@@ -285,138 +484,134 @@ and make_choice t todo todos =
  *     end
  *   | Some (Att.Decision (_,_)) | None -> () *)
 
-let [@inline always] prtect_against_contradiction t f g =
+let[@inline always] prtect_against_contradiction t f g =
   match f () with
   | exception Egraph.Contradiction ->
-    Debug.dprintf0 debug "[Scheduler] Contradiction";
-    conflict_analysis t;
-    true
+      Debug.dprintf2 debug_pushpop
+        "[Scheduler] Contradiction when propagating at level %a" print_level t;
+      conflict_analysis t;
+      true
   | r -> g r
 
 let run_one_step_propagation ~nodec t =
   Debug.incr stats_step;
   match Context.TimeWheel.next t.daemons with
-  | Some att -> begin
+  | Some att ->
       Debug.incr stats_propa;
-      prtect_against_contradiction t (fun () ->
+      prtect_against_contradiction t
+        (fun () ->
           let d = Backtrackable.get_delayed t.solver_state in
-          Backtrackable.run_daemon d att
-        ) (fun () -> true)
-    end
+          Backtrackable.run_daemon d att)
+        (fun () -> true)
   | None when nodec -> false
-  | None ->
-    match Context.TimeWheel.next_at_same_time t.lasteffort with
-    | Some att -> begin
-        Debug.dprintf1 debug "[Scheduler] LastEffort mode remaining: %t"
-          (fun fmt -> Fmt.int fmt (Context.TimeWheel.size_at_current_time t.lasteffort));
-        Debug.incr stats_lasteffort;
-        prtect_against_contradiction t (fun () ->
-            let d = Backtrackable.get_delayed t.solver_state in
-            Backtrackable.run_daemon d att
-          ) (fun () -> true)
-      end
-    | None ->
-      match Prio.extract_min t.choices with
-      | Att.Decision (_,chogen), prio ->
-        Debug.dprintf0 debug "[Scheduler] decision";
-        try_run_dec t prio chogen;
-        true
-      | exception Leftistheap.Empty ->
-        Debug.dprintf1 debug "[Scheduler] LastEffort: %i" (Context.TimeWheel.size t.lasteffort);
-        match Context.TimeWheel.next t.lasteffort with
-        | Some att -> begin
-            Debug.incr stats_lasteffort;
-            prtect_against_contradiction t (fun () ->
-                let d = Backtrackable.get_delayed t.solver_state in
-                Backtrackable.run_daemon d att
-          ) (fun () -> true)
-          end
-        | None ->
-          false
+  | None -> (
+      match Context.TimeWheel.next_at_same_time t.lasteffort with
+      | Some att ->
+          Debug.dprintf1 debug "[Scheduler] LastEffort mode remaining: %t"
+            (fun fmt ->
+              Fmt.int fmt (Context.TimeWheel.size_at_current_time t.lasteffort));
+          Debug.incr stats_lasteffort;
+          prtect_against_contradiction t
+            (fun () ->
+              let d = Backtrackable.get_delayed t.solver_state in
+              Backtrackable.run_daemon d att)
+            (fun () -> true)
+      | None -> (
+          match Prio.extract_min t.choices with
+          | Att.Decision (_, chogen), prio ->
+              Debug.dprintf0 debug "[Scheduler] Decision mode";
+              try_run_dec t prio chogen;
+              true
+          | exception Leftistheap.Empty -> (
+              Debug.dprintf1 debug "[Scheduler] LastEffort: %i"
+                (Context.TimeWheel.size t.lasteffort);
+              match Context.TimeWheel.next t.lasteffort with
+              | Some att ->
+                  Debug.incr stats_lasteffort;
+                  prtect_against_contradiction t
+                    (fun () ->
+                      let d = Backtrackable.get_delayed t.solver_state in
+                      Backtrackable.run_daemon d att)
+                    (fun () -> true)
+              | None -> false)))
 
 let run_one_step_fix_model t =
   Debug.incr stats_fix_model;
   match Context.Ref.get t.fixing_model with
-  | att::l -> begin
+  | att :: l ->
       Context.Ref.set t.fixing_model l;
-      prtect_against_contradiction t (fun () ->
+      prtect_against_contradiction t
+        (fun () ->
           let d = Backtrackable.get_delayed t.solver_state in
-          Backtrackable.run_daemon d att
-        ) (fun () -> true)
-    end
+          Backtrackable.run_daemon d att)
+        (fun () -> true)
   | [] ->
-    prtect_against_contradiction t (fun () ->
-        let d = Backtrackable.get_delayed t.solver_state in
-        Fix_model.next_dec d
-      ) (fun seq ->
-        match Base.Sequence.next seq with
-        | None -> false
-        | Some (todo,todos) ->
-          Backtrackable.delayed_stop t.solver_state;
-          make_choice t todo todos;
-          true
-      )
+      prtect_against_contradiction t
+        (fun () ->
+          let d = Backtrackable.get_delayed t.solver_state in
+          Fix_model.next_dec d)
+        (fun seq ->
+          match Base.Sequence.next seq with
+          | None -> false
+          | Some (todo, todos) ->
+              Backtrackable.delayed_stop t.solver_state;
+              make_choice t todo todos;
+              true)
 
 let run_one_step ~nodec t =
   t.steps <- t.steps + 1;
+  Debug.dprintf1 debug "[Scheduler] Step %i" t.steps;
   match Context.Ref.get t.solve_step with
-  | Propagate -> begin
-    match run_one_step_propagation ~nodec t with
+  | Propagate -> (
+      match run_one_step_propagation ~nodec t with
       | true -> true
       | false when nodec -> false
       | false ->
-        Debug.dprintf0 debug "[Scheduler] FixModel";
-        Context.Ref.set t.solve_step FixModel;
-        true
-  end
+          Debug.dprintf0 debug "[Scheduler] FixModel";
+          Context.Ref.set t.solve_step FixModel;
+          true)
   | FixModel -> run_one_step_fix_model t
 
 let rec flush t =
-  try
-    Backtrackable.flush t.solver_state
+  try Backtrackable.flush t.solver_state
   with Egraph.Contradiction ->
-    Debug.dprintf0 debug "[Scheduler] Contradiction";
+    Debug.dprintf2 debug_pushpop
+      "[Scheduler] Contradiction when flushing at level %a" print_level t;
     conflict_analysis t;
     flush t
 
-exception ReachStepLimit
-
 let rec run_inf_step ~limit ~nodec t =
   if t.steps = limit then raise ReachStepLimit;
   flush t;
   match run_one_step ~nodec t with
-  | true ->
-    run_inf_step ~limit ~nodec t
-  | false ->
-    Backtrackable.delayed_stop t.solver_state
+  | true -> run_inf_step ~limit ~nodec t
+  | false -> Backtrackable.delayed_stop t.solver_state
 
-let run_inf_step ?(limit=(-1)) ?(nodec=false) t =
+let run_inf_step ?(limit = -1) ?(nodec = false) t =
   try
-    run_inf_step ~limit  ~nodec t;
+    run_inf_step ~limit ~nodec t;
     Debug.dprintf1 debug_pushpop "[Scheduler] sat(%i)" t.steps
-  with (Contradiction as e) ->
+  with Contradiction as e ->
     Debug.dprintf1 debug_pushpop "[Scheduler] unsat(%i)" t.steps;
     raise e
 
 let init_theories ~theories t =
   try
     let d = Backtrackable.get_delayed t.solver_state in
-    List.iter (fun f -> f d) (ground_init::interp_init::theories);
+    List.iter (fun f -> f d) (ground_init :: interp_init :: theories);
     Backtrackable.flush t.solver_state
   with Egraph.Contradiction ->
     Debug.dprintf0 debug
       "[Scheduler] Contradiction during theory initialization";
     raise Contradiction
 
-
 let add_assertion t f =
   try
     let d = Backtrackable.get_delayed t.solver_state in
     f d;
     flush t
   with Egraph.Contradiction ->
-    Debug.dprintf0 debug
-      "[Scheduler] Contradiction during assertion";
+    Debug.dprintf0 debug "[Scheduler] Contradiction during assertion";
     raise Contradiction
 
 let check_sat ?limit t =
@@ -424,28 +619,24 @@ let check_sat ?limit t =
     flush t;
     run_inf_step ?limit t;
     let d = Backtrackable.get_delayed t.solver_state in
-    if Backtrackable.get_unknown t.solver_state then
-      `Unknown d
-    else
-      `Sat d
-  with Contradiction ->
-    `Unsat
-
-let run_exn ?nodec ?limit ~theories f =
-  let t = new_solver () in
+    if Backtrackable.get_unknown t.solver_state then `Unknown d else `Sat d
+  with Contradiction -> `Unsat
+
+let run_exn ?nodec ?limit ?(learning = false) ~theories f =
+  let t = new_solver ~learning () in
   init_theories ~theories t;
   add_assertion t f;
   flush t;
-  run_inf_step ~nodec:(nodec=Some ()) ?limit t;
+  run_inf_step ~nodec:(nodec = Some ()) ?limit t;
   let d = Backtrackable.get_delayed t.solver_state in
   d
 
 let run ?nodec ?limit ~theories f =
-  try
-    `Done (run_exn ?nodec ?limit ~theories f)
-  with Contradiction ->
-    `Contradiction
+  try `Done (run_exn ?nodec ?limit ~theories f)
+  with Contradiction -> `Contradiction
 
 let pop_to st bp = ignore (pop_to st bp)
+
 let push st = push External st
+
 let get_context t = Context.creator t.context
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index 7eda0504ebb1b00f57c0cbc39abbe16ba99b9d47..88b61ad2c573da4bee4b47945453b6e1cbf2b518 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -18,36 +18,42 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-
-val run_exn:
+val run_exn :
   ?nodec:unit ->
   ?limit:int ->
+  ?learning:bool ->
   theories:(Egraph.wt -> unit) list ->
   (Egraph.wt -> unit) ->
   Egraph.wt
 
-val run:
+val run :
   ?nodec:unit ->
   ?limit:int ->
   theories:(Egraph.wt -> unit) list ->
   (Egraph.wt -> unit) ->
-  [> `Contradiction
-  | `Done of Egraph.wt
-  ]
+  [> `Contradiction | `Done of Egraph.wt ]
 
 type t
 
-val new_solver: unit -> t
-val init_theories: theories:(Egraph.wt -> unit) list -> t -> unit
-val add_assertion: t -> (Egraph.wt -> unit) -> unit
-val check_sat: ?limit:int -> t -> [> `Unsat | `Sat of Egraph.wt | `Unknown of Egraph.wt ]
-val get_steps: t -> int
+val new_solver : learning:bool -> unit -> t
+
+val init_theories : theories:(Egraph.wt -> unit) list -> t -> unit
+
+val add_assertion : t -> (Egraph.wt -> unit) -> unit
+
+val check_sat :
+  ?limit:int -> t -> [> `Unsat | `Sat of Egraph.wt | `Unknown of Egraph.wt ]
 
-val get_context: t -> Context.creator
+val get_steps : t -> int
+
+val get_context : t -> Context.creator
 
 type bp
 
-val push: t -> bp
-val pop_to: t -> bp -> unit
+val push : t -> bp
+
+val pop_to : t -> bp -> unit
+
+module LearnSet : Set.S with type elt = Ground.t
 
 exception ReachStepLimit
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index b6df5194348bd634780cd8cdaa9f5d25863e471e..f7aa4779b9b28bcbd36c2d3c2ecc5e65492ef68f 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -19,36 +19,49 @@
 (*************************************************************************)
 
 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 print_test cout file =
   match result with
   | Some "model" ->
-    Printf.fprintf cout
-      "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --check-status colibri2 --size=10M \
-       --time=30s --max-steps 3500 %%{dep:%s}))))\n"
-      file file;
-    Printf.fprintf cout
-      "(rule (alias runtest) (action (diff %s.oracle %s.res)))\n"
-      file file
+      Printf.fprintf cout
+        "(rule (action (with-stdout-to %s.res (run %s --check-status colibri2 \
+         %%{dep:%s}))))\n"
+        file cmd file;
+      Printf.fprintf cout
+        "(rule (alias runtest) (action (diff %s.oracle %s.res)))\n" file file
   | Some result ->
-    Printf.fprintf cout
-      "(rule (alias runtest) (action (run %%{bin:colibri2} --check-status %s \
-       --dont-print-result --size=10M --time=30s --max-steps 3500 %%{dep:%s})))\n"
-      result file
+      Printf.fprintf cout
+        "(rule (alias runtest) (action (run %s --check-status %s \n\
+         --dont-print-result %%{dep:%s})))\n"
+        cmd result file;
+      Printf.fprintf cout
+        "(rule (alias runtest-learning) (action (run %s --check-status %s \
+         --learning --dont-print-result %%{dep:%s})))\n"
+        cmd result file
   | None ->
-    Printf.fprintf cout
-      "(rule (alias runtest) (action (run %%{bin:colibri2} --check-status \
-       colibri2 --dont-print-result --size=10M --time=30s --max-steps 3500 \
-       %%{dep:%s})))\n"
-      file
-
+      Printf.fprintf cout
+        "(rule (alias runtest) (action (run %s --check-status colibri2 \
+         --dont-print-result %%{dep:%s})))\n"
+        cmd file;
+      Printf.fprintf cout
+        "(rule (alias runtest-learning) (action (run %s --check-status \
+         colibri2 --dont-print-result --learning %%{dep:%s})))\n"
+        cmd file
 
 let () =
   let files = Sys.readdir dir in
   Array.sort String.compare files;
   let files = Array.to_list files in
-  let files = List.filter (fun f -> List.exists (Filename.check_suffix f) ["cnf";".smt2";".psmt2"]) files in
+  let files =
+    List.filter
+      (fun f ->
+        List.exists (Filename.check_suffix f) [ "cnf"; ".smt2"; ".psmt2" ])
+      files
+  in
   let cout = open_out (Filename.concat dir "dune.inc") in
   List.iter (print_test cout) files;
   close_out cout
diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune.inc b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
index 322eaac2c5261bc649295935616081aa22a98ddd..a63167f0516d0604ff19723247bde91df3d2f69d 100644
--- a/src_colibri2/tests/solve/all/steplimitreached/dune.inc
+++ b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
@@ -1 +1,3 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status steplimitreached --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:bag-BagImpl-addqtvc.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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})))
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index e1c91ae0246375ad521b0f8974eac8ced5564d7d..8a470e8f41631aa1b4faa594a48387da1cf0a2cd 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -1,4 +1,12 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:bag-BagImpl-createqtvc.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index d726267b1a5a48ba5bc249631952cd274f9acdb4..9a3098f1bed7ae73d9df3a42047d9765d4bafd0f 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,11 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:anomaly_agetooold2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:assertion_fail.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:fuzzing1.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:fuzzing2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:par8-1-c.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-3.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-4.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:quinn.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:simple_v3_c2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index 8b0deb98767cbea1bba226729d10607cda94442b..33634441266451e5d7912d9b29154467bb4f83e2 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,6 +1,18 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:modus_ponens.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-1.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-3.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:pigeon-4.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/models/dune.inc b/src_colibri2/tests/solve/models/dune.inc
index 4e75d8ea8c88fd94ab4578c8d9860b533be8e050..ff2aa261caace0ce331feaf9636f1c0dc0c42fcf 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} --check-status colibri2 --size=10M --time=30s --max-steps 3500 %{dep:get_value.smt2}))))
+(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 (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 f7418b5cb3ca004d87d1e5cb13ea7739dab7d6bb..48f0c472b8b8532231719bc3b27ade36cb3ca8b5 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,6 +1,18 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:enum.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:tree1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:tree2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:tree3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index 36d70fb599550a81153295c08c0e0ffd693ca44a..0879b8f097646a2d3482d13052461b9e038108db 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,8 +1,24 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:enum.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:enum2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:list4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:parlist0.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_fp/dune.inc b/src_colibri2/tests/solve/smt_fp/dune.inc
index 425259e448fc469ad5e726407f7ad7ffc742a48a..43a2e25af1e4cfe582d32fa8fe29372adc07f0da 100644
--- a/src_colibri2/tests/solve/smt_fp/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/dune.inc
@@ -1 +1,2 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status colibri2 --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:rm_universal.smt2})))
+(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})))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index a2120c44a4dfc3c8eaa426daa39cb23a6e1eb89b..0a776eab81b6bd13f4f5a1c7a787873ac7be0bda 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -1,16 +1,48 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:exists_eq_not_fp_eq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:inf_pos_neg_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:infm_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:infp_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:recognize_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:recognize_float64.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:recognize_rounding_mode.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:rm_instanciation.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:simple_add_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:simple_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:simple_mul_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:to_fp_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:zero_pos_neg_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:zerom_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:zerop_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--dont-print-result %{dep:recognize_float64.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_float64.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
index 4660fd6b4a3bed2ad8f4eedf84f1ea2e6233ed75..d6d0be9784a0b61dfd60878c8aed847242c0da22 100644
--- a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -1,3 +1,9 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:eq_fp_eq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:inf_pos_neg_neq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:nan_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index bb195dcf8a568f03b3111aff577d7a29ed76d517..2c2e89ded6d45c4ab64d12a0fa8452bac48de0bf 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,33 +1,99 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_CombiRepr_normalize.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_conflict_add_disequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_conpoly.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_decide_must_test_is_dis_equal.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_init_always_merge_itself.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_init_and_propa_must_be_ordered.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_case1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_case_4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_case_4_bis.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_itself_last_case.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_must_use_find.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_mult_explication.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_mult_not_linear_in_conflict.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_normalize_use_find_def.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_own_repr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_propacl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_subst_and_conflict_add.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_zero_dom.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:attach_only_when_dom_present.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:init_not_repr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:le.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:le2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:sem_invariant_in_learnt_dec.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_add_pexp_cl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_arith_homogeneous_dist_sign.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_merge_itself_repr_inside.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_set_pending_merge_expsameexp.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_subst_eventdom_find.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:to_real2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 2207c151279b75ee40053bb4297e693a63ecf6e1..32098dbe065e4c8236e9953029f2e4dee7575d88 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -1,11 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_ExpMult_by_zero.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:arith_merge_case2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:le.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:le2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:repr_and_poly.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:repr_fourier.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_merge_itself_repr_empty.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:solver_set_sem_merge_sign.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:to_real2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
index d9b7db5ae21b4d0bffc595c35facaaa589fcb0ce..b0533db1e786e849483d576da545bf09427eb908 100644
--- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -1,7 +1,21 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:ceil.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:div_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:div_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_commut.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_commut2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
index d0b9a0f9ebaeeb0a120c64b42fead5d3e815c68b..fdc03088e9ccf54610f6b382332c93ed58aa07bb 100644
--- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -1,10 +1,30 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:ceil.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:div_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:div_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:div_pos_lt_to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:floor.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_commut.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_commut2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:mul_pos_zero_le.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_quant/dune.inc b/src_colibri2/tests/solve/smt_quant/dune.inc
index 26eca44291134d875e41db0fc91bf2bf93ce6c5f..94c44726ffa9cfb365197972f70c954968c1bf33 100644
--- a/src_colibri2/tests/solve/smt_quant/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/dune.inc
@@ -1,3 +1,6 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status colibri2 --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status colibri2 --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status colibri2 --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall4.smt2})))
+(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})))
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
index cb48b0fe87e0f8c06abc4d54efdce6ab85e3cdfe..d888d22476695e087a41697346133e75a6296291 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
@@ -1 +1,3 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:exists.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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})))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index a80fc1f37b35a7cfda68cd4fa830ad1b8df73b7f..fcea32050f0ee3ba5b20f8dcfcf30ba4fd2de59e 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,11 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:exists.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:exists2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall5.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall6.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall7.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:forall8.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index 9439153d15493cf622e8ba36f8fb06adc1fe6a39..9872a6d3060efdca446859d6b939b45fa4cf283c 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,21 +1,63 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:bad_conflict.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:bcp_dont_like_duplicate.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:bool_not_propa.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:boolexpup.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:clause_normalization.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:clmerge.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:conflict_complete_needed_cl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:directdom_not.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:dis_dom_before_first_age.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:dom_merge_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:equality_condis.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:equality_get_sem.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:exp_sem_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:explimit_cl_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:implication.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:intmap_set_disjoint.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:is_equal_not_propagated.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:ite_sem_bool.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status sat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:substupfalse_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 1f045621ff395d697cd7da26fcf87916e312567c..7003c0e59b3715b4f75dcb76be45ff7b7648a64b 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,13 +1,39 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:NEQ004_size4__decide_eq_us.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:deltaed0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:diff_to_value_for_bool.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:diff_value_substupfalse.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:distinct.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:eq_diamond2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:equality_norm_set.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:fundef.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:many_distinct.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:polyeq_genequality_deltaed.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --check-status unsat --dont-print-result --size=10M --time=30s --max-steps 3500 %{dep:xor.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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 
+--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})))
diff --git a/src_colibri2/tests/test_learning/einstein-Goals-G1.psmt2 b/src_colibri2/tests/test_learning/einstein-Goals-G1.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..9402bbd0d08bcd4a91cc9f8a9babea1831524733
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein-Goals-G1.psmt2
@@ -0,0 +1,130 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-datatypes ((house 0))
+(((H1) (H2) (H3) (H4) (H5))))
+(declare-datatypes ((color 0))
+(((Blue) (Green) (Red) (White) (Yellow))))
+(declare-datatypes ((person 0))
+(((Dane) (Englishman) (German) (Norwegian) (Swede))))
+(declare-datatypes ((drink 0))
+(((Beer) (Coffee) (Milk) (Tea) (Water))))
+(declare-datatypes ((cigar 0))
+(((Blend) (BlueMaster) (Dunhill) (PallMall) (Prince))))
+(declare-datatypes ((pet 0))
+(((Birds) (Cats) (Dogs) (Fish) (Horse))))
+(declare-fun of (house) color)
+
+(declare-fun to_ (color) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_ (of x)) x)))
+
+;; Of_to
+  (assert (forall ((y color)) (= (of (to_ y)) y)))
+
+(declare-fun of1 (house) person)
+
+(declare-fun to_1 (person) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_1 (of1 x)) x)))
+
+;; Of_to
+  (assert (forall ((y person)) (= (of1 (to_1 y)) y)))
+
+(declare-fun of2 (person) drink)
+
+(declare-fun to_2 (drink) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_2 (of2 x)) x)))
+
+;; Of_to
+  (assert (forall ((y drink)) (= (of2 (to_2 y)) y)))
+
+(declare-fun of3 (person) cigar)
+
+(declare-fun to_3 (cigar) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_3 (of3 x)) x)))
+
+;; Of_to
+  (assert (forall ((y cigar)) (= (of3 (to_3 y)) y)))
+
+(declare-fun of4 (person) pet)
+
+(declare-fun to_4 (pet) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_4 (of4 x)) x)))
+
+;; Of_to
+  (assert (forall ((y pet)) (= (of4 (to_4 y)) y)))
+
+(declare-datatypes ((tuple2 2))
+((par (a a1) ((Tuple2 (Tuple2_proj_1 a)(Tuple2_proj_2 a1))))))
+(define-fun leftof ((h1 house)
+  (h2 house)) Bool (ite ((_ is H2) h2) (ite ((_ is H1) h1) true false) 
+                   (ite ((_ is H3) h2) (ite ((_ is H2) h1) true false) 
+                   (ite ((_ is H4) h2) (ite ((_ is H3) h1) true false) 
+                   (ite ((_ is H5) h2) (ite ((_ is H4) h1) true false) false)))))
+
+(define-fun neighbour ((h1 house)
+  (h2 house)) Bool (or (leftof h1 h2) (leftof h2 h1)))
+
+;; Clue1
+  (assert (= (of (to_1 Englishman)) Red))
+
+;; Clue2
+  (assert (= (of4 Swede) Dogs))
+
+;; Clue3
+  (assert (= (of2 Dane) Tea))
+
+;; Clue4
+  (assert (leftof (to_ Green) (to_ White)))
+
+;; Clue5
+  (assert (= (of2 (of1 (to_ Green))) Coffee))
+
+;; Clue6
+  (assert (= (of4 (to_3 PallMall)) Birds))
+
+;; Clue7
+  (assert (= (of3 (of1 (to_ Yellow))) Dunhill))
+
+;; Clue8
+  (assert (= (of2 (of1 H3)) Milk))
+
+;; Clue9
+  (assert (= (of1 H1) Norwegian))
+
+;; Clue10
+  (assert (neighbour (to_1 (to_3 Blend)) (to_1 (to_4 Cats))))
+
+;; Clue11
+  (assert (neighbour (to_1 (to_4 Horse)) (to_1 (to_3 Dunhill))))
+
+;; Clue12
+  (assert (= (of2 (to_3 BlueMaster)) Beer))
+
+;; Clue13
+  (assert (= (of3 German) Prince))
+
+;; Clue14
+  (assert (neighbour (to_1 Norwegian) (to_ Blue)))
+
+;; Clue15
+  (assert (neighbour (to_1 (to_3 Blend)) (to_1 (to_2 Water))))
+
+(assert
+;; G1
+ ;; File "examples/logic/einstein.why", line 134, characters 7-9
+  (not (= (to_4 Fish) German)))
+(check-sat)
diff --git a/src_colibri2/tests/test_learning/einstein-Goals-G2.psmt2 b/src_colibri2/tests/test_learning/einstein-Goals-G2.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..593f9e87c27a802e8e06d413e5b27cd499589e09
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein-Goals-G2.psmt2
@@ -0,0 +1,130 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-datatypes ((house 0))
+(((H1) (H2) (H3) (H4) (H5))))
+(declare-datatypes ((color 0))
+(((Blue) (Green) (Red) (White) (Yellow))))
+(declare-datatypes ((person 0))
+(((Dane) (Englishman) (German) (Norwegian) (Swede))))
+(declare-datatypes ((drink 0))
+(((Beer) (Coffee) (Milk) (Tea) (Water))))
+(declare-datatypes ((cigar 0))
+(((Blend) (BlueMaster) (Dunhill) (PallMall) (Prince))))
+(declare-datatypes ((pet 0))
+(((Birds) (Cats) (Dogs) (Fish) (Horse))))
+(declare-fun of (house) color)
+
+(declare-fun to_ (color) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_ (of x)) x)))
+
+;; Of_to
+  (assert (forall ((y color)) (= (of (to_ y)) y)))
+
+(declare-fun of1 (house) person)
+
+(declare-fun to_1 (person) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_1 (of1 x)) x)))
+
+;; Of_to
+  (assert (forall ((y person)) (= (of1 (to_1 y)) y)))
+
+(declare-fun of2 (person) drink)
+
+(declare-fun to_2 (drink) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_2 (of2 x)) x)))
+
+;; Of_to
+  (assert (forall ((y drink)) (= (of2 (to_2 y)) y)))
+
+(declare-fun of3 (person) cigar)
+
+(declare-fun to_3 (cigar) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_3 (of3 x)) x)))
+
+;; Of_to
+  (assert (forall ((y cigar)) (= (of3 (to_3 y)) y)))
+
+(declare-fun of4 (person) pet)
+
+(declare-fun to_4 (pet) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_4 (of4 x)) x)))
+
+;; Of_to
+  (assert (forall ((y pet)) (= (of4 (to_4 y)) y)))
+
+(declare-datatypes ((tuple2 2))
+((par (a a1) ((Tuple2 (Tuple2_proj_1 a)(Tuple2_proj_2 a1))))))
+(define-fun leftof ((h1 house)
+  (h2 house)) Bool (ite ((_ is H2) h2) (ite ((_ is H1) h1) true false) 
+                   (ite ((_ is H3) h2) (ite ((_ is H2) h1) true false) 
+                   (ite ((_ is H4) h2) (ite ((_ is H3) h1) true false) 
+                   (ite ((_ is H5) h2) (ite ((_ is H4) h1) true false) false)))))
+
+(define-fun neighbour ((h1 house)
+  (h2 house)) Bool (or (leftof h1 h2) (leftof h2 h1)))
+
+;; Clue1
+  (assert (= (of (to_1 Englishman)) Red))
+
+;; Clue2
+  (assert (= (of4 Swede) Dogs))
+
+;; Clue3
+  (assert (= (of2 Dane) Tea))
+
+;; Clue4
+  (assert (leftof (to_ Green) (to_ White)))
+
+;; Clue5
+  (assert (= (of2 (of1 (to_ Green))) Coffee))
+
+;; Clue6
+  (assert (= (of4 (to_3 PallMall)) Birds))
+
+;; Clue7
+  (assert (= (of3 (of1 (to_ Yellow))) Dunhill))
+
+;; Clue8
+  (assert (= (of2 (of1 H3)) Milk))
+
+;; Clue9
+  (assert (= (of1 H1) Norwegian))
+
+;; Clue10
+  (assert (neighbour (to_1 (to_3 Blend)) (to_1 (to_4 Cats))))
+
+;; Clue11
+  (assert (neighbour (to_1 (to_4 Horse)) (to_1 (to_3 Dunhill))))
+
+;; Clue12
+  (assert (= (of2 (to_3 BlueMaster)) Beer))
+
+;; Clue13
+  (assert (= (of3 German) Prince))
+
+;; Clue14
+  (assert (neighbour (to_1 Norwegian) (to_ Blue)))
+
+;; Clue15
+  (assert (neighbour (to_1 (to_3 Blend)) (to_1 (to_2 Water))))
+
+(assert
+;; G2
+ ;; File "examples/logic/einstein.why", line 136, characters 7-9
+  (not (= (to_4 Cats) Norwegian)))
+(check-sat)
diff --git a/src_colibri2/tests/test_learning/einstein-Goals-Wrong.psmt2 b/src_colibri2/tests/test_learning/einstein-Goals-Wrong.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..0e55177a351cfb2a3cb69714440bad68274418b4
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein-Goals-Wrong.psmt2
@@ -0,0 +1,130 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-datatypes ((house 0))
+(((H1) (H2) (H3) (H4) (H5))))
+(declare-datatypes ((color 0))
+(((Blue) (Green) (Red) (White) (Yellow))))
+(declare-datatypes ((person 0))
+(((Dane) (Englishman) (German) (Norwegian) (Swede))))
+(declare-datatypes ((drink 0))
+(((Beer) (Coffee) (Milk) (Tea) (Water))))
+(declare-datatypes ((cigar 0))
+(((Blend) (BlueMaster) (Dunhill) (PallMall) (Prince))))
+(declare-datatypes ((pet 0))
+(((Birds) (Cats) (Dogs) (Fish) (Horse))))
+(declare-fun of (house) color)
+
+(declare-fun to_ (color) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_ (of x)) x)))
+
+;; Of_to
+  (assert (forall ((y color)) (= (of (to_ y)) y)))
+
+(declare-fun of1 (house) person)
+
+(declare-fun to_1 (person) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_1 (of1 x)) x)))
+
+;; Of_to
+  (assert (forall ((y person)) (= (of1 (to_1 y)) y)))
+
+(declare-fun of2 (person) drink)
+
+(declare-fun to_2 (drink) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_2 (of2 x)) x)))
+
+;; Of_to
+  (assert (forall ((y drink)) (= (of2 (to_2 y)) y)))
+
+(declare-fun of3 (person) cigar)
+
+(declare-fun to_3 (cigar) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_3 (of3 x)) x)))
+
+;; Of_to
+  (assert (forall ((y cigar)) (= (of3 (to_3 y)) y)))
+
+(declare-fun of4 (person) pet)
+
+(declare-fun to_4 (pet) person)
+
+;; To_of
+  (assert (forall ((x person)) (= (to_4 (of4 x)) x)))
+
+;; Of_to
+  (assert (forall ((y pet)) (= (of4 (to_4 y)) y)))
+
+(declare-datatypes ((tuple2 2))
+((par (a a1) ((Tuple2 (Tuple2_proj_1 a)(Tuple2_proj_2 a1))))))
+(define-fun leftof ((h1 house)
+  (h2 house)) Bool (ite ((_ is H2) h2) (ite ((_ is H1) h1) true false) 
+                   (ite ((_ is H3) h2) (ite ((_ is H2) h1) true false) 
+                   (ite ((_ is H4) h2) (ite ((_ is H3) h1) true false) 
+                   (ite ((_ is H5) h2) (ite ((_ is H4) h1) true false) false)))))
+
+(define-fun neighbour ((h1 house)
+  (h2 house)) Bool (or (leftof h1 h2) (leftof h2 h1)))
+
+;; Clue1
+  (assert (= (of (to_1 Englishman)) Red))
+
+;; Clue2
+  (assert (= (of4 Swede) Dogs))
+
+;; Clue3
+  (assert (= (of2 Dane) Tea))
+
+;; Clue4
+  (assert (leftof (to_ Green) (to_ White)))
+
+;; Clue5
+  (assert (= (of2 (of1 (to_ Green))) Coffee))
+
+;; Clue6
+  (assert (= (of4 (to_3 PallMall)) Birds))
+
+;; Clue7
+  (assert (= (of3 (of1 (to_ Yellow))) Dunhill))
+
+;; Clue8
+  (assert (= (of2 (of1 H3)) Milk))
+
+;; Clue9
+  (assert (= (of1 H1) Norwegian))
+
+;; Clue10
+  (assert (neighbour (to_1 (to_3 Blend)) (to_1 (to_4 Cats))))
+
+;; Clue11
+  (assert (neighbour (to_1 (to_4 Horse)) (to_1 (to_3 Dunhill))))
+
+;; Clue12
+  (assert (= (of2 (to_3 BlueMaster)) Beer))
+
+;; Clue13
+  (assert (= (of3 German) Prince))
+
+;; Clue14
+  (assert (neighbour (to_1 Norwegian) (to_ Blue)))
+
+;; Clue15
+  (assert (neighbour (to_1 (to_3 Blend)) (to_1 (to_2 Water))))
+
+(assert
+;; Wrong
+ ;; File "examples/logic/einstein.why", line 135, characters 7-12
+  (not (= (to_4 Cats) Swede)))
+(check-sat)
diff --git a/src_colibri2/tests/test_learning/einstein.why b/src_colibri2/tests/test_learning/einstein.why
new file mode 100644
index 0000000000000000000000000000000000000000..45ef944dbec89086fbe011381f3a80610f1980d2
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein.why
@@ -0,0 +1,144 @@
+
+(** {1 Einstein's Logic Problem} *)
+
+(**
+   This problem is usually referred to as Einstein's Logic Problem.
+   see {h <a href="http://en.wikipedia.org/wiki/Zebra_Puzzle">this page</a>}
+   (contribution by Stephane Lescuyer)
+*)
+
+theory Bijection
+  type t
+  type u
+
+  function of t : u
+  function to_ u : t
+
+  axiom To_of : forall x : t. to_ (of x) = x
+  axiom Of_to : forall y : u. of (to_ y) = y
+end
+
+(** {2 Einstein's problem} *)
+
+theory Einstein
+
+  (** Types *)
+
+  type house  = H1 | H2 | H3 | H4 | H5
+  type color  = Blue | Green | Red | White | Yellow
+  type person = Dane | Englishman | German | Norwegian | Swede
+  type drink  = Beer | Coffee | Milk | Tea | Water
+  type cigar  = Blend | BlueMaster | Dunhill | PallMall | Prince
+  type pet    = Birds | Cats | Dogs | Fish | Horse
+
+  (** Each house is associated bijectively to a color and a person *)
+
+  clone Bijection as Color with type t = house, type u = color, axiom .
+  clone Bijection as Owner with type t = house, type u = person, axiom .
+
+  (** Each drink, cigar brand and pet are associated bijectively to a person *)
+
+  clone Bijection as Drink with type t = person, type u = drink, axiom .
+  clone Bijection as Cigar with type t = person, type u = cigar, axiom .
+  clone Bijection as Pet   with type t = person, type u = pet, axiom .
+
+  (** Relative positions of the houses *)
+
+  predicate leftof (h1 h2 : house) =
+    match h1, h2 with
+    | H1, H2
+    | H2, H3
+    | H3, H4
+    | H4, H5 -> true
+    | _      -> false
+    end
+  predicate rightof (h1 h2 : house) =
+    leftof h2 h1
+  predicate neighbour (h1 h2 : house) =
+    leftof h1 h2 \/ rightof h1 h2
+
+  (** {2 Clues} *)
+
+  (** The Englishman lives in a red house *)
+  axiom Clue1: Color.of (Owner.to_ Englishman) = Red
+
+  (** The Swede has dogs *)
+  axiom Clue2: Pet.of Swede = Dogs
+
+  (** The Dane drinks tea *)
+  axiom Clue3: Drink.of Dane = Tea
+
+  (** The green house is on the left of the white one *)
+  axiom Clue4: leftof (Color.to_ Green) (Color.to_ White)
+
+  (** The green house's owner drinks coffee *)
+  axiom Clue5: Drink.of (Owner.of (Color.to_ Green)) = Coffee
+
+  (** The person who smokes Pall Mall has birds *)
+  axiom Clue6: Pet.of (Cigar.to_ PallMall) = Birds
+
+  (** The yellow house's owner smokes Dunhill *)
+  axiom Clue7: Cigar.of (Owner.of (Color.to_ Yellow)) = Dunhill
+
+  (** In the house in the center lives someone who drinks milk *)
+  axiom Clue8: Drink.of (Owner.of H3) = Milk
+
+  (** The Norwegian lives in the first house *)
+  axiom Clue9: Owner.of H1 = Norwegian
+
+  (** The man who smokes Blends lives next to the one who has cats *)
+  axiom Clue10: neighbour
+    (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Pet.to_ Cats))
+
+  (** The man who owns a horse lives next to the one who smokes Dunhills *)
+  axiom Clue11: neighbour
+    (Owner.to_ (Pet.to_ Horse)) (Owner.to_ (Cigar.to_ Dunhill))
+
+  (** The man who smokes Blue Masters drinks beer *)
+  axiom Clue12:
+    Drink.of (Cigar.to_ BlueMaster) = Beer
+
+  (** The German smokes Prince *)
+  axiom Clue13:
+    Cigar.of German = Prince
+
+  (** The Norwegian lives next to the blue house *)
+  axiom Clue14:
+    neighbour (Owner.to_ Norwegian) (Color.to_ Blue)
+
+  (** The man who smokes Blends has a neighbour who drinks water *)
+  axiom Clue15:
+    neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water))
+
+end
+
+(** {2 Goals about Einstein's problem} *)
+
+theory Goals
+  use Einstein
+
+(*
+  lemma First_House_Not_White: Color.of H1 <> White
+  lemma Last_House_Not_Green: Color.of H5 <> Green
+
+  lemma Blue_not_Red: Blue <> Red
+  lemma Englishman_not_H2: Owner.to_ Englishman <> H2
+  lemma Englishman_not_H1: Owner.to_ Englishman <> H1
+
+  lemma Second_House_Blue: Color.of H2 = Blue
+  lemma Green_H4 : Color.of H4 = Green
+  lemma White_H5 : Color.of H5 = White
+  lemma Red_H3 : Color.of H3 = Red
+  lemma Yellow_H1 : Color.of H1 = Yellow
+*)
+  goal G1: Pet.to_ Fish = German
+  goal Wrong: Pet.to_ Cats = Swede
+  goal G2: Pet.to_ Cats = Norwegian
+
+end
+
+(*
+Local Variables:
+compile-command: "why3 ide einstein.why"
+End:
+*)
diff --git a/src_colibri2/tests/test_learning/einstein_simp-Goals-G1.psmt2 b/src_colibri2/tests/test_learning/einstein_simp-Goals-G1.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..bd1737d4b8be9864ae07f4b2ab91a4785800c534
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein_simp-Goals-G1.psmt2
@@ -0,0 +1,59 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-datatypes ((house 0))
+(((H1) (H2) (H3))))
+(declare-datatypes ((color 0))
+(((Blue) (Green) (Red))))
+(declare-datatypes ((person 0))
+(((Dane) (Englishman) (German))))
+(declare-fun of (house) color)
+
+(declare-fun to_ (color) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_ (of x)) x)))
+
+;; Of_to
+  (assert (forall ((y color)) (= (of (to_ y)) y)))
+
+(declare-fun of1 (house) person)
+
+(declare-fun to_1 (person) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_1 (of1 x)) x)))
+
+;; Of_to
+  (assert (forall ((y person)) (= (of1 (to_1 y)) y)))
+
+(declare-datatypes ((tuple2 2))
+((par (a a1) ((Tuple2 (Tuple2_proj_1 a)(Tuple2_proj_2 a1))))))
+(define-fun leftof ((h1 house)
+  (h2 house)) Bool (ite ((_ is H2) h2) (ite ((_ is H1) h1) true false) 
+                   (ite ((_ is H3) h2) (ite ((_ is H2) h1) true false) false)))
+
+(define-fun neighbour ((h1 house)
+  (h2 house)) Bool (or (leftof h1 h2) (leftof h2 h1)))
+
+;; Clue1
+  (assert (= (of (to_1 Englishman)) Green))
+
+;; Clue4
+  (assert (leftof (to_ Red) (to_ Green)))
+
+;; Clue9
+  (assert (= (of1 H1) German))
+
+;; Clue14
+  (assert (neighbour (to_1 Dane) (to_ Blue)))
+
+(assert
+;; G1
+ ;; File "einstein_simp.why", line 79, characters 7-9
+  (not (= (to_1 Englishman) H3)))
+(check-sat)
diff --git a/src_colibri2/tests/test_learning/einstein_simp-Goals-G2.psmt2 b/src_colibri2/tests/test_learning/einstein_simp-Goals-G2.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..681babc345bc101d5daafc231b926f6f0ea13654
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein_simp-Goals-G2.psmt2
@@ -0,0 +1,59 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-datatypes ((house 0))
+(((H1) (H2) (H3))))
+(declare-datatypes ((color 0))
+(((Blue) (Green) (Red))))
+(declare-datatypes ((person 0))
+(((Dane) (Englishman) (German))))
+(declare-fun of (house) color)
+
+(declare-fun to_ (color) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_ (of x)) x)))
+
+;; Of_to
+  (assert (forall ((y color)) (= (of (to_ y)) y)))
+
+(declare-fun of1 (house) person)
+
+(declare-fun to_1 (person) house)
+
+;; To_of
+  (assert (forall ((x house)) (= (to_1 (of1 x)) x)))
+
+;; Of_to
+  (assert (forall ((y person)) (= (of1 (to_1 y)) y)))
+
+(declare-datatypes ((tuple2 2))
+((par (a a1) ((Tuple2 (Tuple2_proj_1 a)(Tuple2_proj_2 a1))))))
+(define-fun leftof ((h1 house)
+  (h2 house)) Bool (ite ((_ is H2) h2) (ite ((_ is H1) h1) true false) 
+                   (ite ((_ is H3) h2) (ite ((_ is H2) h1) true false) false)))
+
+(define-fun neighbour ((h1 house)
+  (h2 house)) Bool (or (leftof h1 h2) (leftof h2 h1)))
+
+;; Clue1
+  (assert (= (of (to_1 Englishman)) Green))
+
+;; Clue4
+  (assert (leftof (to_ Red) (to_ Green)))
+
+;; Clue9
+  (assert (= (of1 H1) German))
+
+;; Clue14
+  (assert (neighbour (to_1 Dane) (to_ Blue)))
+
+(assert
+;; G2
+ ;; File "einstein_simp.why", line 80, characters 7-9
+  (not (= (of (to_1 Dane)) Red)))
+(check-sat)
diff --git a/src_colibri2/tests/test_learning/einstein_simp.why b/src_colibri2/tests/test_learning/einstein_simp.why
new file mode 100644
index 0000000000000000000000000000000000000000..65daa94b94f830d352fd3dea64f67774d8ffb511
--- /dev/null
+++ b/src_colibri2/tests/test_learning/einstein_simp.why
@@ -0,0 +1,88 @@
+
+(** {1 Einstein's Logic Problem} *)
+
+(**
+   This problem is usually referred to as Einstein's Logic Problem.
+   see {h <a href="http://en.wikipedia.org/wiki/Zebra_Puzzle">this page</a>}
+   (contribution by Stephane Lescuyer)
+*)
+
+theory Bijection
+  type t
+  type u
+
+  function of t : u
+  function to_ u : t
+
+  axiom To_of : forall x : t. to_ (of x) = x
+  axiom Of_to : forall y : u. of (to_ y) = y
+end
+
+(** {2 Einstein's problem} *)
+
+theory Einstein
+
+  (** Types *)
+
+  type house  = H1 | H2 | H3
+  type color  = Blue | Green | Red
+  type person = Dane | Englishman | German
+
+  (** Each house is associated bijectively to a color and a person *)
+
+  clone Bijection as Color with type t = house, type u = color, axiom .
+  clone Bijection as Owner with type t = house, type u = person, axiom .
+
+
+  (** Relative positions of the houses *)
+
+  predicate leftof (h1 h2 : house) =
+    match h1, h2 with
+    | H1, H2
+    | H2, H3 -> true
+    | _      -> false
+    end
+  predicate rightof (h1 h2 : house) =
+    leftof h2 h1
+  predicate neighbour (h1 h2 : house) =
+    leftof h1 h2 \/ rightof h1 h2
+
+  (** {2 Clues} *)
+
+  (** The Englishman lives in a green house *)
+  axiom Clue1: Color.of (Owner.to_ Englishman) = Green
+
+  (** The red house is on the left of the green one *)
+  axiom Clue4: leftof (Color.to_ Red) (Color.to_ Green)
+
+  (** The Germann lives in the first house *)
+  axiom Clue9: Owner.of H1 = German
+
+  (** The Dane lives next to the blue house *)
+  axiom Clue14:
+    neighbour (Owner.to_ Dane) (Color.to_ Blue)
+
+end
+
+(** {2 Goals about Einstein's problem} *)
+
+theory Goals
+  use Einstein
+
+(*
+  lemma Dane_H2: Owner.to_ Dane = H2
+  lemma Blue_H1 : Color.of H1 = Blue
+  lemma Red_H2 : Color.of H2 = Red
+  lemma Green_H3 : Color.of H3 = Green
+  lemma Englishman_H3: Owner.to_ Englishman = H3
+*)
+  goal G1: Owner.to_ Englishman = H3
+  goal G2: Color.of (Owner.to_ Dane) = Red
+
+end
+
+(*
+Local Variables:
+compile-command: "why3 ide einstein.why"
+End:
+*)
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index e6d457a57fce677b95e33b2717fa93f700fb2332..884ad987b28a237f8ea9b0f6d7f0c5f480864dfa 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -123,6 +123,7 @@ module Decide = struct
 
   let new_decision n adt c =
     {
+      Choice.print_cho = "Decision made by adt.ml";
       Choice.prio = 1;
       choice =
         (fun d ->
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index 907ed8e5150432fdbaa75281473a81a3ae4767e2..c95cbb4d8ba547900962adbc80c4d82ed78cdcb0 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -121,6 +121,7 @@ module ChoLRA = struct
   let choice n = {
     Choice.prio = 1;
     choice = choose_decision n;
+    print_cho = "FP.Dom_interval.ChoLRA";
   }
 
 end
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 0ffb6fd6f5e556e6eb92a341feccd046a55c9323..e9613f9ba0bfa29b6c97cbab8d0b70af5379cfcd 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -89,7 +89,8 @@ module ChoLRA = struct
   let choice n = {
     Choice.prio = 1;
     choice = choose_decision n;
-  }
+    print_cho = "Decision made by dom_interval.ml";
+    }
 
 end
 
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 26325d9fcd69ffd355807f0f3c2e70c0299052aa..989a8d47540dabbb47b31e840c1559d28e1315c3 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -314,7 +314,7 @@ module ChangePos = struct
     Events.attach_any_dom d Dom_interval.dom
       (fun d n ->
          match Node.HC.find_opt used_in_poly d n with
-         | Some ns -> Events.EnqRun (key,ns)
+         | Some ns -> Events.EnqRun (key,ns,None)
          | None -> Events.EnqAlready)
 
 end
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 00b87b0305888e55228126f72a0b3ebbaea9da69..672d8571a9ef125ad5420dba02ac143900cca103 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -232,7 +232,7 @@ module Daemon = struct
     then Events.EnqAlready
     else begin
       Datastructure.Ref.set scheduled d true;
-      Events.EnqRun (key,())
+      Events.EnqRun (key,(),None)
     end
 
   let delay = Events.Delayed_by 64
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index c9773b4dd422613b99576424fb48401f8b647869..a5c00485b7a8166b07ff98666e91e6e03af346a1 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -117,6 +117,7 @@ end
 let chobool n = {
   Choice.prio = 1;
   choice = ChoBool.choose_decision n;
+  print_cho = "Decision made by boolean.ml";
 }
 
 module TwoWatchLiteral = struct
@@ -145,6 +146,8 @@ module TwoWatchLiteral = struct
 
     let delay = Events.Delayed_by 1
 
+    let blob _ r = snd r
+
     type res_scan =
       | LimitReached
       | Absorbent
@@ -183,19 +186,20 @@ module TwoWatchLiteral = struct
       let args = (Ground.sem r.ground).args in
       if o_from_start = o_from_end then Events.EnqStopped
       else
+        let g = Some (Ground.thterm r.ground) in
         match Egraph.get_value d (Ground.node r.ground) with
         | Some v when not (Value.equal v r.absorbent) ->
           Context.Ref.set r.from_end o_from_start;
-          Events.EnqLast(key,fun d -> IArray.iter ~f:(fun a -> Egraph.set_value d a v) args)
+          Events.EnqLast(key,(fun d -> IArray.iter ~f:(fun a -> Egraph.set_value d a v) args),g)
         | _ ->
           let n_end = IArray.get args o_from_end in
           match check_if_equal_or_set d args r.absorbent (+1) o_from_end o_from_start
                   n_end with
           | LimitReached ->
             Context.Ref.set r.from_start o_from_end;
-            Events.EnqLast(key,fun d -> Egraph.merge d n_end (Ground.node r.ground))
+            Events.EnqLast(key,(fun d -> Egraph.merge d n_end (Ground.node r.ground)),g)
           | Absorbent ->
-            Events.EnqLast(key,fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+            Events.EnqLast(key,(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent),g)
           | ToWatch from_start ->
             if from_start <> o_from_start then (
               Context.Ref.set r.from_start from_start;
@@ -205,9 +209,9 @@ module TwoWatchLiteral = struct
             match check_if_equal_or_set d args r.absorbent (-1) from_start o_from_end n_start with
             | LimitReached ->
               Context.Ref.set r.from_end from_start;
-              Events.EnqLast (key,fun d -> Egraph.merge d n_start (Ground.node r.ground))
+              Events.EnqLast (key,(fun d -> Egraph.merge d n_start (Ground.node r.ground)),g)
             | Absorbent ->
-              Events.EnqLast (key,fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+              Events.EnqLast (key,(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent),g)
             | ToWatch from_end when from_end = o_from_end ->
               Events.EnqAlready
             | ToWatch from_end ->
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 3809ac5f4901b48dfd8c007c63207828e379679f..e6da258e09b69af3e00d6d99a848f57fae5abc66 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -325,7 +325,12 @@ module ChoEquals = struct
       | `Found (cl1, cl2) ->
           DecTodo [ make_equal the (cl1, cl2); make_disequal the (cl1, cl2) ]
 
-  let mk_choice the = { Choice.choice = choose_decision the; prio = 1 }
+  let mk_choice the =
+    {
+      Choice.choice = choose_decision the;
+      prio = 1;
+      print_cho = "Decision made by equality.ml";
+    }
 end
 
 let norm_dom d the =