diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 8c284f9211f2094bf248037b0994c95271a524c8..a16452301b6f26c1db224c28c602fc489227ceda 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -35,6 +35,8 @@ let stats_set_dom =
   Debug.register_stats_int ~name:"Egraph.set_dom/merge" ~init:0
 let stats_set_value =
   Debug.register_stats_int ~name:"Egraph.set_value/merge" ~init:0
+let stats_register =
+  Debug.register_stats_int ~name:"Egraph.register" ~init:0
 
 module DecTag = DInt
 
@@ -317,6 +319,22 @@ let escape_for_dot pp v =
 
 let output_graph filename t =
   let open Graph in
+  let show_node =
+    match Sys.getenv "COLIBRI2_DOTGUI_ONLY" with
+    | exception Not_found -> (fun _ -> `Show)
+    | l ->
+      let only = DStr.S.of_list (String.split ~by:"," l) in
+      let h = Node.H.create 10 in
+      Node.M.iter (fun node1 node2 ->
+          if DStr.S.mem (Fmt.str "%a" Node.pp node1) only then begin
+            Node.H.replace h node1 `Show;
+            Node.H.change (function
+                | Some `Show -> Some `Show
+                | _ -> Some `Repr) h node2;
+          end
+        ) t.repr;
+      Node.H.find_def h `Hide
+  in
   let module G = struct
     include Imperative.Digraph.Concrete(Node)
     let graph_attributes _ = []
@@ -341,14 +359,18 @@ let output_graph filename t =
         with Not_found -> ()
       in
       let print_sem fmt node =
-        match Only_for_solver.thterm node with
-        | None -> ()
-        | Some thterm ->
-          match Only_for_solver.sem_of_node thterm with
-          | Only_for_solver.ThTerm(sem,v) ->
-            let (module S) = get_thterm sem in
-            Format.fprintf fmt "| {%a | %s}"
-              ThTermKind.pp sem (escape_for_dot S.pp v)
+        match show_node node with
+        | `Show ->
+          begin match Only_for_solver.thterm node with
+          | None -> ()
+          | Some thterm ->
+            match Only_for_solver.sem_of_node thterm with
+            | Only_for_solver.ThTerm(sem,v) ->
+              let (module S) = get_thterm sem in
+              Format.fprintf fmt "| {%a | %s}"
+                ThTermKind.pp sem (escape_for_dot S.pp v)
+          end
+        | _ -> ()
       in
       Format.fprintf fmt "{%a %a %a %a}" (* "{%a | %a | %a}" *)
         Node.pp node
@@ -373,9 +395,12 @@ let output_graph filename t =
   end in
   let g = G.create () in
   Node.M.iter (fun node1 node2 ->
-      if Node.equal node1 node2
-      then G.add_vertex g node1
-      else G.add_edge g node1 (find_def t node2)) t.repr;
+      match show_node node1 with
+      | `Repr | `Show ->
+        if Node.equal node1 node2
+        then G.add_vertex g node1
+        else G.add_edge g node1 (find_def t node2)
+      | `Hide -> ()) t.repr;
   let cout = open_out filename in
   let module Dot = Graphviz.Dot(G) in
   Dot.output_graph cout g;
@@ -463,10 +488,12 @@ module Delayed = struct
          let* events = ValueKind.M.find_opt valuekind valuetable.events in
          Node.M.find_opt node events
        in
-       Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)
+       (* deletion of events are not taken into account for that kind *)
+       ignore (Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v))
     );
     let events = Node.M.find_opt node t.env.event_value in
-    Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)
+    (* deletion of events are not taken into account for that kind *)
+    ignore (Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v))
 
   let add_pending_merge (t : t) node node' =
     Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]"
@@ -487,6 +514,7 @@ module Delayed = struct
   let register t node =
     assert (is_current_env t);
     if not (is_registered t node) then begin
+      Debug.incr stats_register;
       if Debug.test_flag debug_few then begin
         match Only_for_solver.thterm node with
         | None ->
@@ -500,26 +528,30 @@ module Delayed = struct
       (** reg_node *)
       let new_events, node_events = Node.M.find_remove node t.env.event_reg in
       t.env.event_reg <- new_events;
-      Wait.wakeup_events_list Events.Wait.translate_regnode t node_events node;
+      (* deletion of events are not taken into account for that kind *)
+      ignore (Wait.wakeup_events_list Events.Wait.translate_regnode t node_events node);
       (** reg *)
-      Wait.wakeup_events_list Events.Wait.translate_reg
-        t (Some t.env.event_any_reg) node;
+      (* deletion of events are not taken into account for that kind *)
+      ignore (Wait.wakeup_events_list Events.Wait.translate_reg
+                t (Some t.env.event_any_reg) node);
       (** reg_sem *)
       match Only_for_solver.open_node node with
       | Only_for_solver.ThTerm thterm ->
         begin match Only_for_solver.sem_of_node thterm with
           | Only_for_solver.ThTerm(sem,_) ->
             let reg_events = get_table_sem t.env sem in
-            Wait.wakeup_events_list Events.Wait.translate_regsem
-              t (Some reg_events) (thterm)
+            (* deletion of events are not taken into account for that kind *)
+            ignore (Wait.wakeup_events_list Events.Wait.translate_regsem
+                      t (Some reg_events) (thterm))
         end
       | Only_for_solver.Value nodevalue ->
         begin match Value.kind nodevalue with
           | Value(value,_) ->
             let valuetable = t.env.value in
             let reg_events = ValueKind.M.find_opt value valuetable.reg_events in
-            Wait.wakeup_events_list Events.Wait.translate_regvalue
-              t reg_events (nodevalue);
+            (* deletion of events are not taken into account for that kind *)
+            ignore (Wait.wakeup_events_list Events.Wait.translate_regvalue
+                      t reg_events (nodevalue));
             set_value_direct t node nodevalue
         end
     end
@@ -537,9 +569,11 @@ module Delayed = struct
         t.env.repr <- Node.M.add node0' node t.env.repr;
         (** wakeup the daemons register_node *)
         let event, other_event = Node.M.find_remove node0' t.env.event_repr in
-        Wait.wakeup_events_bag Events.Wait.translate_change t other_event node0';
+        (* can be always removed *)
+        ignore (Wait.wakeup_events_bag Events.Wait.translate_change t other_event node0');
         t.env.event_repr <- event;
-        Wait.wakeup_events_list Events.Wait.translate_change t (Some t.env.event_any_repr) node0';
+        (* deletion of events are not taken into account for that kind *)
+        ignore (Wait.wakeup_events_list Events.Wait.translate_change t (Some t.env.event_any_repr) node0');
         (** set the value if node0' is one *)
         match Nodes.Only_for_solver.nodevalue node0' with
         | None -> ()
@@ -568,22 +602,23 @@ module Delayed = struct
     let node = find_def t node0 in
     let domtable = (get_table_dom t.env dom) in
     let new_table = Node.M.add_opt node new_v domtable.table in
-    let domtable = { domtable with table = new_table } in
-    VDomTable.set t.env.dom dom domtable;
-    let events = Node.M.find_opt node domtable.events in
-    Wait.wakeup_events_bag Events.Wait.translate_dom t events (node,dom);
-    Wait.wakeup_events_list Events.Wait.translate_dom t (Some domtable.reg_events) (node,dom)
-
-
-  let set_dom_premerge_pending (type a) t (dom : a DomKind.t) ~from:_ node0 (new_v:a) =
-    Debug.incr stats_set_dom;
-    let node  = find t node0 in
-    let domtable = (get_table_dom t.env dom) in
-    let new_table = Node.M.add node new_v domtable.table in
-    let domtable = { domtable with table = new_table } in
+    let other_events, woken_events = Node.M.find_remove node domtable.events in
+    let domtable = { domtable with table = new_table; events = other_events } in
     VDomTable.set t.env.dom dom domtable;
-    let events = Node.M.find_opt node domtable.events in
-    Wait.wakeup_events_bag Events.Wait.translate_dom t events (node0,dom)
+    let woken_events = Wait.wakeup_events_bag Events.Wait.translate_dom t woken_events (node,dom) in
+    begin match woken_events with
+      | None -> ()
+      | Some woken_events ->
+        let domtable = (get_table_dom t.env dom) in
+        let events =
+          Node.M.add_change (fun events -> events) (fun events b -> Bag.concat events b)
+            node woken_events
+            domtable.events in
+        let domtable = { domtable with events } in
+        VDomTable.set t.env.dom dom domtable;
+    end;
+    (* deletion of events are not taken into account *)
+    ignore (Wait.wakeup_events_list Events.Wait.translate_dom t (Some domtable.reg_events) (node,dom))
 
   let flag_choose_repr_no_value =
     Debug.register_flag
@@ -712,6 +747,10 @@ module Delayed = struct
       Node.pp repr_node Node.pp repr_node0;
     let event, other_event = Node.M.find_remove other_node t.env.event_repr in
 
+    let other_event = Wait.wakeup_events_bag
+        Events.Wait.translate_change t other_event other_node
+    in
+
     (** move node events *)
     begin match other_event with
       | None -> ()
@@ -760,10 +799,10 @@ module Delayed = struct
 
 
     (** wakeup the daemons *)
-    Wait.wakeup_events_bag
-      Events.Wait.translate_change t other_event other_node;
-    Wait.wakeup_events_list
-      Events.Wait.translate_change t (Some t.env.event_any_repr) other_node
+    t.env.event_any_repr <-
+      Option.value ~default:[] @@
+      Wait.wakeup_events_list
+        Events.Wait.translate_change t (Some t.env.event_any_repr) other_node
 
   let continue_merge t node1_0 node2_0 inv  =
     let dom_not_done = merge_dom t node1_0 node2_0 inv in
@@ -908,19 +947,6 @@ module Delayed = struct
     check d node;
     set_dom_pending d dom node (Some v)
 
-  let set_dom_premerge d dom node v =
-    Debug.dprintf4 debug
-      "[Egraph] @[set_dom_premerge for %a with %a@]"
-      Node.pp node (print_dom dom) v;
-    check d node;
-    let node' = match d.todo_delayed_merge with
-      | Some(node1,node2,_) when Node.equal node1 node -> node2
-      | Some(node1,node2,_) when Node.equal node2 node -> node1
-      | _ -> raise (BrokenInvariant(
-          "set_dom_premerge should be used only on the \
-           nodeasses currently merged")) in
-    set_dom_premerge_pending d dom ~from:node' node v
-
   let unset_dom d dom node =
     Debug.dprintf2 debug
       "[Egraph] @[unset_dom for %a@]"
@@ -983,10 +1009,11 @@ module Delayed = struct
     let event = Events.Wait.Event (dem,event) in
     match find t node with
     | node -> (** already registered *)
-      Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node
+      ignore (Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node)
     | exception NotRegistered ->
-      t.env.event_reg <-
-        Node.M.add_change Lists.singleton Lists.add node event t.env.event_reg
+      (* deletion of events are not taken into account *)
+      ignore (t.env.event_reg <-
+                Node.M.add_change Lists.singleton Lists.add node event t.env.event_reg)
 
   let attach_reg_any t dem event =
     let event = Events.Wait.Event (dem,event) in
@@ -1219,6 +1246,30 @@ module type Ro = sig
 
   val is_current_env: t -> bool
 
+  (** {3 Attach Event} *)
+  (** todo rename events and attachment *)
+
+  val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when the dom of the node change *)
+  val attach_any_dom: t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when the dom of any node change *)
+  val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a value is attached to this equivalence class *)
+  val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when any kind of value is attached to this equivalence class *)
+  val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when any node is registered *)
+  val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when this node is registered *)
+  val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a new semantical class is registered *)
+  val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a new value is registered *)
+  val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when it is not anymore the representative class *)
+  val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a node is not its representative class anymore *)
+
 end
 
 module Ro : Ro with type t = Delayed.t = Delayed
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index a964f1b73fd840ec6f8c22da0bcbba4bebaa5b83..6cf8108ced2036e4b99209986d3098215c533c09 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -68,6 +68,30 @@ module type Ro = sig
 
   val is_current_env: t -> bool
 
+  (** {3 Attach Event} *)
+  (** todo rename events and attachment *)
+
+  val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when the dom of the node change *)
+  val attach_any_dom: t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when the dom of any node change *)
+  val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a value is attached to this equivalence class *)
+  val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when any kind of value is attached to this equivalence class *)
+  val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when any node is registered *)
+  val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when this node is registered *)
+  val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a new semantical class is registered *)
+  val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a new value is registered *)
+  val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when it is not anymore the representative class *)
+  val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit
+  (** wakeup when a node is not its representative class anymore *)
+
 end
 
 module Ro : Ro
@@ -92,31 +116,6 @@ val set_value: t -> Node.t -> Value.t -> unit
 
 val merge    : t -> Node.t -> Node.t -> unit
 
-
-(** {3 Attach Event} *)
-(** todo rename events and attachment *)
-
-val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when the dom of the node change *)
-val attach_any_dom: t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when the dom of any node change *)
-val attach_value: t -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a value is attached to this equivalence class *)
-val attach_any_value: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when any kind of value is attached to this equivalence class *)
-val attach_reg_any: t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when any node is registered *)
-val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when this node is registered *)
-val attach_reg_sem: t -> 'a ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a new semantical class is registered *)
-val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a new value is registered *)
-val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when it is not anymore the representative class *)
-val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit
-(** wakeup when a node is not its representative class anymore *)
-
 type choice_state =
   | DecNo
   | DecTodo of (t -> unit) list
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index d6182f65a0d1943cf8184fa60c6ba82d7309789b..0398fdf738bcd71ffc3eb477a55bad620f251eae 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -128,6 +128,7 @@ module Wait = struct
 
   type _ enqueue =
     | EnqRun: 'r -> 'r enqueue
+    | EnqLast: 'r -> 'r enqueue
     | EnqAlready: _ enqueue
     | EnqRedirected: ('e,'r) Dem.t * 'e -> _ enqueue
     | EnqStopped: _ enqueue
@@ -184,13 +185,13 @@ module Wait = struct
 
     val new_pending_daemon : delayed -> ('a, 'b) Dem.t -> 'b -> unit
 
-    val wakeup_event : 'a translate -> delayed -> 'a -> t -> unit
+    val wakeup_event : 'a translate -> delayed -> 'a -> t -> t option
 
     val wakeup_events_list :
-      'a translate -> delayed -> t list option -> 'a -> unit
+      'a translate -> delayed -> t list option -> 'a -> t list option
 
     val wakeup_events_bag :
-      'a translate -> delayed -> t Bag.t option -> 'a -> unit
+      'a translate -> delayed -> t Bag.t option -> 'a -> t Bag.t option
 
     val is_well_initialized : unit -> bool
   end
@@ -261,31 +262,33 @@ module Wait = struct
     let wakeup_event translate t info wevent =
       match wevent with
       | Event (dem,event) ->
-        let rec f : type event r. S.delayed -> (event,r) Dem.t -> event -> unit =
-          fun t dem event ->
+        let rec f : type event r. S.delayed -> (event,r) Dem.t -> event -> _ -> _ =
+          fun t dem event wevent ->
             let module Dem = (val get_dem dem) in
             let event = translate.translate info event in
             match Dem.enqueue (S.readonly t) event with
-            | EnqStopped -> () (** todo remove from the list of event *)
-            | EnqAlready -> ()
-            | EnqRedirected(dem,event) -> f t dem event
-            | EnqRun runable -> new_pending_daemon t dem runable
+            | EnqStopped -> None
+            | EnqAlready -> Some wevent
+            | EnqRedirected(dem,event) -> f t dem event (Event(dem,event))
+            | EnqRun runable -> new_pending_daemon t dem runable; Some wevent
+            | EnqLast runable -> new_pending_daemon t dem runable; None
         in
-        f t dem event
+        f t dem event wevent
 
     let wakeup_events_list translate t events info =
       match events with
       | None | Some [] ->
-        Debug.dprintf0 debug "[Egraph] @[No scheduling@]"
+        Debug.dprintf0 debug "[Egraph] @[No scheduling@]";
+        None
       | Some events ->
-        List.iter (wakeup_event translate t info) events
+        Some (Lists.filter_map_homo (wakeup_event translate t info) events)
 
     let wakeup_events_bag translate t events info =
       let is_empty = match events with
         | None -> true
         | Some events -> Bag.is_empty events in
-      if is_empty then Debug.dprintf0 debug "[Egraph] @[No scheduling@]"
-      else Bag.iter (wakeup_event translate t info) (Opt.get events)
+      if is_empty then (Debug.dprintf0 debug "[Egraph] @[No scheduling@]"; None)
+      else Some (Bag.filter_map_homo (wakeup_event translate t info) (Opt.get events))
 
 
   end
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index df4af5f05529b9d70502abb90b9c665a1cad9c6e..a0f82a433dd06cf267e738a6d42aff8013657643 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -64,9 +64,15 @@ module Wait : sig
 
   type _ enqueue =
     | EnqRun: 'r -> 'r enqueue
+    (** Schedule a daemon run *)
+    | EnqLast: 'r -> 'r enqueue
+    (** Same as EnqRun but remove the waiting event *)
     | EnqAlready: _ enqueue
+    (** Don't run but keep the waiting event *)
     | EnqRedirected: ('e,'r) Dem.t * 'e -> _ enqueue
+    (** Run another daemon *)
     | EnqStopped: _ enqueue
+    (** Stop and don't run *)
 
   type daemon_key =
     | DaemonKey: ('k,'runable) Dem.t * 'runable -> daemon_key
@@ -114,13 +120,13 @@ module Wait : sig
 
     val new_pending_daemon : delayed -> ('a, 'b) Dem.t -> 'b -> unit
 
-    val wakeup_event : 'a translate -> delayed -> 'a -> t -> unit
+    val wakeup_event : 'a translate -> delayed -> 'a -> t -> t option
 
     val wakeup_events_list :
-      'a translate -> delayed -> t list option -> 'a -> unit
+      'a translate -> delayed -> t list option -> 'a -> t list option
 
     val wakeup_events_bag :
-      'a translate -> delayed -> t Bag.t option -> 'a -> unit
+      'a translate -> delayed -> t Bag.t option -> 'a -> t Bag.t option
 
     val is_well_initialized : unit -> bool
   end
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 8183c53b1322c5eff080707616781ce534674f3f..62762e173b643e93f871b418d9663d621d37ee0d 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -1,3 +1,4 @@
+open Colibri2_popop_lib
 open Nodes
 
 module All = struct
@@ -10,14 +11,14 @@ module All = struct
 
   let rec pp_ty fmt ty =
     match ty.args with
-    | [] -> Fmt.pf fmt "%a" Expr.Ty.Const.pp ty.app 
+    | [] -> Fmt.pf fmt "%a" Expr.Ty.Const.pp ty.app
     | _ ->
       Fmt.pf fmt "%a(%a)" Expr.Ty.Const.pp ty.app Fmt.(list ~sep:comma pp_ty) ty.args
 
   type term = {
     app: Expr.Term.Const.t;
     tyargs : ty list;
-    args : Node.t list;
+    args : Node.t IArray.t;
     ty:ty
   }
 end
@@ -89,7 +90,7 @@ module Term = struct
     type t = All.term = {
       app: Expr.Term.Const.t;
       tyargs : Ty.t list;
-      args : Node.t list;
+      args : Node.t IArray.t;
       ty:Ty.t
     }[@@deriving hash, ord, eq ]
 
@@ -97,11 +98,32 @@ module Term = struct
       | [] -> ()
       | l -> Fmt.pf fmt "%a" Fmt.(paren (list ?sep pp)) l
 
+    let array_paren ?(sep=Fmt.nop) ~(paren:_ Fmt.t -> _ Fmt.t) pp fmt t =
+      if IArray.is_empty t then ()
+      else
+        Fmt.pf fmt "%a" (paren (IArray.pp ~sep pp)) t
+
     let pp fmt t =
-      Fmt.pf fmt "%a%a%a"
-        Expr.Term.Const.pp t.app
-        Fmt.(list_paren ~sep:comma ~paren:brackets Ty.pp) t.tyargs
-        Fmt.(list_paren ~sep:comma ~paren:parens Node.pp) t.args
+      let infix sep =
+        Fmt.(array_paren ~sep:(fun fmt () -> Fmt.pf fmt "@ %s " sep) ~paren:parens Node.pp) fmt t.args
+      in
+      match t.app.builtin with
+      | Expr.Equal
+      | Expr.Equiv -> infix "="
+      | Expr.Lt -> infix "<"
+      | Expr.Leq -> infix "≤"
+      | Expr.Gt -> infix ">"
+      | Expr.Geq -> infix "≥"
+      | Expr.Imply -> infix "⇒"
+      | Expr.And -> infix "∧"
+      | Expr.Or -> infix "∨"
+      | Expr.Sub -> infix "-"
+      | Expr.Mul -> infix "*"
+      | _ ->
+        Fmt.pf fmt "%a%a%a"
+          Expr.Term.Const.pp t.app
+          Fmt.(list_paren ~sep:comma ~paren:brackets Ty.pp) t.tyargs
+          Fmt.(array_paren ~sep:comma ~paren:parens Node.pp) t.args
   end
   include T
   include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
@@ -158,7 +180,7 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
     ThTerm.node @@ ThTerm.index @@
       { Term.app = f;
         tyargs = List.map (Ty.convert subst.ty) tyargs;
-        args = List.map (convert ~subst) args;
+        args = IArray.of_list_map ~f:(convert ~subst) args;
         ty = Ty.convert subst.ty t.ty;
       }
   | Expr.Binder (Exists(ty_vars,term_vars) as b, body)
@@ -215,7 +237,7 @@ module Defs = struct
         | exception Not_found -> ()
         | fundef ->
           let subst = {
-            Subst.term = Expr.Term.Var.M.of_list (List.combine fundef.tvl tvl);
+            Subst.term = Expr.Term.Var.M.of_list (Base.List.mapi ~f:(fun i v -> (v,IArray.get tvl i)) fundef.tvl);
             Subst.ty = Expr.Ty.Var.M.of_list (List.combine fundef.tyl tyl);
           } in
           let n = convert ~subst fundef.body in
@@ -254,21 +276,32 @@ let () = Egraph.register_dom (module struct
 
 let tys d n = (Base.Option.value ~default:Ty.S.empty (Egraph.get_dom d dom_tys n))
 
+
+let add_ty d n ty =
+  (match Egraph.get_dom d dom_tys n with
+   | None -> Egraph.set_dom d dom_tys n (Ty.S.singleton ty)
+   | Some tys ->
+     match Ty.S.add_new Exit ty tys with
+     | exception Exit -> ()
+     | tys -> Egraph.set_dom d dom_tys n tys
+  )
+
 let init d =
   Demon.Fast.register_init_daemon ~name:"Ground.convert"
     (module ThTerm)
     (fun d g ->
        let n = ThTerm.node g in
        let s = ThTerm.sem g in
-       (match Egraph.get_dom d dom_tys n with
-        | None -> Egraph.set_dom d dom_tys n (Ty.S.singleton s.ty)
-        | Some tys ->
-          match Ty.S.add_new Exit s.ty tys with
-          | exception Exit -> ()
-          | tys -> Egraph.set_dom d dom_tys n tys
-       );
+       add_ty d n s.ty;
        Defs.converter d g;
        Datastructure.Queue.iter registered_converter d ~f:(fun f -> f d g))
+    d;
+  Demon.Fast.register_init_daemon ~name:"Ground.convert"
+    (module ThClosedQuantifier)
+    (fun d g ->
+       let n = ThClosedQuantifier.node g in
+       add_ty d n Ty.bool
+    )
     d
 
 include ThTerm
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index 8321dac26b9c3a9418b23fefebb3fd229544e480..aa66b0730f6780af04b6c2982f4ad8632a082adf 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -1,3 +1,4 @@
+open Colibri2_popop_lib
 open Nodes
 
 module All: sig
@@ -9,7 +10,7 @@ module All: sig
   type term = {
     app: Expr.Term.Const.t;
     tyargs : ty list;
-    args : Node.t list;
+    args : Node.t IArray.t;
     ty:ty
   }
 
@@ -74,7 +75,7 @@ module Term: sig
   type t = All.term = {
     app: Expr.Term.Const.t;
     tyargs : Ty.t list;
-    args : Node.t list;
+    args : Node.t IArray.t;
     ty:Ty.t
   } [@@deriving hash, ord, eq ]
 
@@ -87,7 +88,7 @@ include RegisteredThTerm with type s := Term.t
 
 val convert : ?subst:Subst.t -> Expr.Term.t -> Node.t
 
-val apply : Expr.Term.Const.t -> Ty.t list -> Node.t list -> Term.t
+val apply : Expr.Term.Const.t -> Ty.t list -> Node.t IArray.t -> Term.t
 
 val init: Egraph.t -> unit
 
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index c93668b6e3cb79ff335d191fa7c525a0f07f38d1..eca08223ad2e17d053c739dcf4dc99e0820c4cf1 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -166,12 +166,19 @@ let node d n =
     else (
       Node.H.replace parent n' ();
       let r =
-        get_registered
-          (fun n' -> raise (CantInterpretNode n'))
-          Data.node
-          (fun f d x -> f aux d x)
-          d n'
+        try
+          get_registered
+            (fun n' -> raise (CantInterpretNode n'))
+            Data.node
+            (fun f d x -> f aux d x)
+            d n'
+        with CantInterpretNode _ as exn ->
+          if Ground.Ty.S.is_empty (Ground.tys d n') then (
+            Fmt.epr "@.%a does not have type@." Node.pp n';
+            raise exn)
+          else ty d (Ground.Ty.S.choose (Ground.tys d n'))
       in
+
       Node.H.remove parent n';
       SeqLim.incr_depth d r)
   in
@@ -194,7 +201,7 @@ let check_ground_terms d =
   Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
       if Option.is_none (Egraph.get_value d (Ground.node g)) then
         raise (GroundTermWithoutValueAfterModelFixing g);
-      List.iter (Ground.sem g).args ~f:(fun n ->
+      IArray.iter (Ground.sem g).args ~f:(fun n ->
           if Option.is_none (Egraph.get_value d n) then
             raise (ArgOfGroundTermWithoutValueAfterModelFixing (g, n)));
       if not (check d g) then (
@@ -230,14 +237,15 @@ let sequence_of_ground d =
   Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
       let n = Egraph.find d (Ground.node g) in
       push n;
-      List.iter ~f:push (Ground.sem g).args;
+      IArray.iter ~f:push (Ground.sem g).args;
       Hashtbl.add_multi n2g ~key:n ~data:g);
   let partition =
     WTO.partition ?pref:None ~inits:(Queue.to_list inits) ~succs:(fun n ->
-        if Option.is_some (Egraph.get_value d n) then []
+        if Option.is_some (Egraph.get_value d n) then Sequence.empty
         else
           let gs = Hashtbl.find_multi n2g n in
-          List.concat_map gs ~f:(fun g -> (Ground.sem g).args))
+          Sequence.concat_map (Sequence.of_list gs) ~f:(fun g ->
+              IArray.to_seq (Ground.sem g).args))
   in
   Debug.dprintf2 debug "FixModel wto:%a" (Wto.pp_partition Node.pp) partition;
   Sequence.Generator.run (partition_to_seq partition)
@@ -287,13 +295,7 @@ module Fix_model = struct
               | None ->
                   Debug.dprintf2 debug "FixModel %a has no value" Node.pp n;
                   assert (Egraph.is_current_env d);
-                  let seq =
-                    let tys = Ground.tys d n in
-                    try node d n
-                    with
-                    | CantInterpretNode _ when not (Ground.Ty.S.is_empty tys) ->
-                      ty d (Ground.Ty.S.choose tys)
-                  in
+                  let seq = node d n in
                   let seq =
                     seq |> spy_sequence "got"
                     |> (fun s -> s 0)
@@ -332,17 +334,15 @@ let () =
       | exn -> raise exn)
 
 (** Helpers *)
-module TwoWatchLiteral = struct
+module WatchArgs = struct
   (** todo move the check to enqueue; but it requires to be able to attach event
       in delayed_ro *)
 
   module Daemon = struct
     type t = {
       callback : Egraph.t -> Ground.t -> unit;
-      ground : Ground.t;  (** perhaps ground should have an array for args *)
-      args : Node.t array;
-      from_start : int Context.Ref.t;  (** already set before *)
-      from_end : int Context.Ref.t;  (** already set after *)
+      ground : Ground.t;
+      current : int Context.Ref.t;  (** already set before *)
     }
 
     type runable = t
@@ -365,68 +365,45 @@ module TwoWatchLiteral = struct
 
           type t = event
 
-          let name = "Interp.TwoWatchLiteral"
+          let name = "Interp.WatchArgs"
         end)
 
     let delay = Events.FixingModel
 
-    let rec check_if_set d args incr stop i =
-      if Option.is_none (Egraph.get_value d args.(i)) then i
+    let rec check_if_set d args i =
+      if Option.is_none (Egraph.get_value d (IArray.get args i)) then Some i
       else
-        let i = incr + i in
-        if i = stop then stop else check_if_set d args incr stop i
+        let i = 1 + i in
+        if IArray.length args <= i then None else check_if_set d args i
 
-    let attach d r i = Egraph.attach_any_value d r.args.(i) key r
+    let attach d r i =
+      Egraph.attach_any_value d (IArray.get (Ground.sem r.ground).args i) key r
 
     let run d r =
-      let o_from_start = Context.Ref.get r.from_start in
-      let o_from_end = Context.Ref.get r.from_end in
-      (if o_from_end < o_from_start then ()
-      else
-        let from_start =
-          check_if_set d r.args 1 (o_from_end + 1) o_from_start
-        in
-        if o_from_end < from_start then (
-          Context.Ref.set r.from_start from_start;
-          r.callback d r.ground)
-        else (
-          if from_start <> o_from_start then (
-            Context.Ref.set r.from_start from_start;
-            attach d r from_start);
-          if o_from_end = from_start then ()
-          else
-            let from_end = check_if_set d r.args (-1) from_start o_from_end in
-            Context.Ref.set r.from_end from_end));
+      let o_current = Context.Ref.get r.current in
+      assert (o_current < IArray.length (Ground.sem r.ground).args);
+      (match check_if_set d (Ground.sem r.ground).args o_current with
+      | None -> r.callback d r.ground
+      | Some current ->
+          assert (current <> o_current);
+          attach d r current);
       None
 
     let create d callback ground =
-      match (Ground.sem ground).args with
-      | [] -> callback d ground
-      | _ ->
-          let args = Array.of_list (Ground.sem ground).args in
-          let r from_start from_end =
-            assert (from_start <= from_end);
-            Debug.dprintf4 debug "Interp create %a (%i-%i)" Ground.pp ground
-              from_start from_end;
-            {
-              callback;
-              ground;
-              args;
-              from_start = Context.Ref.create (Egraph.context d) from_start;
-              from_end = Context.Ref.create (Egraph.context d) from_end;
-            }
-          in
-          let from_start = check_if_set d args 1 (Array.length args) 0 in
-          if from_start = Array.length args then callback d ground
-          else if from_start = Array.length args - 1 then
-            attach d (r from_start from_start) from_start
-          else
-            let from_end =
-              check_if_set d args (-1) from_start (Array.length args - 1)
-            in
-            let r = r from_start from_end in
-            attach d r from_start;
-            attach d r from_end
+      if IArray.is_empty (Ground.sem ground).args then callback d ground
+      else
+        let r current =
+          (* Debug.dprintf3 debug "Interp create %a (%i)" Ground.pp ground
+           *   current; *)
+          {
+            callback;
+            ground;
+            current = Context.Ref.create (Egraph.context d) current;
+          }
+        in
+        match check_if_set d (Ground.sem ground).args 0 with
+        | None -> callback d ground
+        | Some current -> attach d (r current) current
   end
 
   let () = Egraph.Wait.register_dem (module Daemon)
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index 7bf4fe34c8d8810fe93844e17081208b7ee3ef59..ec5491375600e21b9d2c058dde5c1aa5ef4e70a3 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -82,7 +82,7 @@ module Fix_model : sig
       needed. Could raise unsatisfiable if all the model have been tried *)
 end
 
-module TwoWatchLiteral : sig
+module WatchArgs : sig
   val create : Egraph.t -> (Egraph.t -> Ground.t -> unit) -> Ground.t -> unit
   (** call the given function when all the arguments of the ground term have a value *)
 end
diff --git a/src_colibri2/popop_lib/IArray.ml b/src_colibri2/popop_lib/IArray.ml
index 8818468faff705f580c6ef03065216baa0edc04a..cf071ce33ef7b2ba0c1c05c7bcd9ef32d4e81229 100644
--- a/src_colibri2/popop_lib/IArray.ml
+++ b/src_colibri2/popop_lib/IArray.ml
@@ -20,16 +20,36 @@
 
 type 'a t = 'a array
 
+let is_empty = function [||] -> true | _ -> false
+let not_empty = function [||] -> false | _ -> true
+let empty = [||]
+
 let of_list = Array.of_list
+let of_list_map ~f = function
+  | [] -> empty
+  | h::l ->
+    let len = List.length l in
+    let a = Array.make (len + 1) (f h) in
+    let rec fill i = function
+      | [] -> ()
+      | hd::tl ->
+        Array.unsafe_set a i (f hd);
+        fill (i+1) tl
+    in
+    fill 1 l;
+    a
+
 let of_array = Array.copy
 let of_iter l (iter : ('a -> unit) -> unit) =
-  if l = 0 then [||] else
+  if l = 0 then empty else
     let res = Array.make l (Obj.magic 0 : 'a) in
     let r = ref 0 in
     iter (fun v -> res.(!r) <- v; incr r);
     assert (!r == l);
     res
 
+let to_list = Array.to_list
+let to_seq = Base.Array.to_sequence
 
 
 let length = Array.length
@@ -96,15 +116,79 @@ let hash_fold_t h s t =
 
 let get = Array.get
 
-let iter = Array.iter
-let iteri = Array.iteri
-let fold = Array.fold_left
+let iter ~f a = Array.iter f a
+let iteri ~f a = Array.iteri f a
+let fold ~f ~init a = Array.fold_left f init a
 
-let foldi f x a =
+let foldi a ~init:x ~f =
   let r = ref x in
   for i = 0 to Array.length a - 1 do
     r := f i !r (Array.unsafe_get a i)
   done;
   !r
 
-let pp sep p fmt a = Pp.iter1 iter sep p fmt a
+let foldi_non_empty_exn ~init ~f a =
+  if Array.length a = 0 then invalid_arg "IArray.fold_non_empty_exn: empty array";
+  let r = ref (init (Array.unsafe_get a 0)) in
+  for i = 1 to Array.length a - 1 do
+    r := f i !r (Array.unsafe_get a i)
+  done;
+  !r
+
+let fold2_exn ~init ~f a1 a2 =
+  if Array.length a1 <> Array.length a2 then invalid_arg "IArray.fold2_exn: different length";
+  let r = ref init in
+  for i = 0 to Array.length a1 - 1 do
+    r := f !r a1.(i) a2.(i)
+  done;
+  !r
+
+let for_alli ~f a1 =
+  let exception False in
+  try
+    for i = 0 to Array.length a1 - 1 do
+      if not (f i a1.(i)) then raise False
+    done;
+    true
+  with False -> false
+
+let for_alli_non_empty_exn ~init ~f a =
+  if Array.length a = 0 then invalid_arg "IArray.for_alli_non_empty_exn: empty array";
+  let first = init a.(0) in
+  let exception False in
+  try
+    for i = 1 to Array.length a - 1 do
+      if not (f i first a.(i)) then raise False
+    done;
+    true
+  with False -> false
+
+let for_all2_exn ~f a1 a2 =
+  if Array.length a1 <> Array.length a2 then invalid_arg "IArray.fold2_exn: different length";
+  let exception False in
+  try
+    for i = 0 to Array.length a1 - 1 do
+      if not (f a1.(i) a2.(i)) then raise False
+    done;
+    true
+  with False -> false
+
+let map ~f a = Array.map f a
+
+let pp ?(sep=Fmt.comma) p fmt a = Pp.iter1 (fun f e -> iter ~f e) sep p fmt a
+
+let extract1_exn = function
+  | [| a |] -> a
+  | _ -> invalid_arg "IArray not of size 1"
+
+let extract2_exn = function
+  | [| a; b |] -> (a,b)
+  | _ -> invalid_arg "IArray not of size 2"
+
+let extract3_exn = function
+  | [| a; b; c |] -> (a,b,c)
+  | _ -> invalid_arg "IArray not of size 3"
+
+let extract4_exn = function
+  | [| a; b; c; d |] -> (a,b,c,d)
+  | _ -> invalid_arg "IArray not of size 4"
diff --git a/src_colibri2/popop_lib/IArray.mli b/src_colibri2/popop_lib/IArray.mli
index 319b6a31c68d222a3f9c0fadea9b99af73d18323..bb21e7d189444a498a9cf53218143a7fa9623873 100644
--- a/src_colibri2/popop_lib/IArray.mli
+++ b/src_colibri2/popop_lib/IArray.mli
@@ -25,11 +25,15 @@
 type 'a t
 
 val of_list: 'a list -> 'a t
+val of_list_map: f:('a -> 'b) -> 'a list -> 'b t
 val of_array: 'a array -> 'a t
 val of_iter: int -> (('a -> unit) -> unit) -> 'a t
 (** create the array using an iterator. The integer indicate the
     number of iteration that will occur *)
 
+val empty: 'a t
+val is_empty: 'a t -> bool
+val not_empty: 'a t -> bool
 val length: 'a t -> int
 
 val compare: ('a -> 'a ->  int)  -> 'a t -> 'a t -> int
@@ -41,9 +45,25 @@ val hash   : ('a -> int) -> 'a t -> int
 val hash_fold_t   : 'a Base.Hash.folder -> 'a t Base.Hash.folder
 
 
-val iter : ('a -> unit)  -> 'a t -> unit
-val iteri : (int -> 'a -> unit)  -> 'a t -> unit
-val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
-val foldi : (int -> 'b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+val iter : f:('a -> unit)  -> 'a t -> unit
+val iteri : f:(int -> 'a -> unit)  -> 'a t -> unit
+val fold : f:('b -> 'a -> 'b) -> init:'b -> 'a t -> 'b
+val foldi : 'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b) -> 'b
+val foldi_non_empty_exn : init:('a -> 'b) -> f:(int -> 'b -> 'a -> 'b) -> 'a t -> 'b
+(** The accumulator is obtained with the first elements *)
 
-val pp: unit Pp.pp -> 'a Pp.pp -> 'a t Pp.pp
+val fold2_exn : init:'acc -> f:('acc -> 'a -> 'b -> 'acc) -> 'a t -> 'b t -> 'acc
+val for_alli : f:(int -> 'a -> bool) -> 'a t -> bool
+val for_all2_exn : f:('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+val for_alli_non_empty_exn : init:('a -> 'acc) -> f:(int -> 'acc -> 'a -> bool) -> 'a t -> bool
+val map: f:('a -> 'b) -> 'a t -> 'b t
+
+val pp: ?sep:unit Pp.pp -> 'a Pp.pp -> 'a t Pp.pp
+
+val extract1_exn: 'a t -> 'a
+val extract2_exn: 'a t -> 'a * 'a
+val extract3_exn: 'a t -> 'a * 'a * 'a
+val extract4_exn: 'a t -> 'a * 'a * 'a * 'a
+
+val to_list: 'a t -> 'a list
+val to_seq: 'a t -> 'a Base.Sequence.t
diff --git a/src_colibri2/popop_lib/bag.ml b/src_colibri2/popop_lib/bag.ml
index 6b0c87eaf76f990c44206f9ea4e92e893ee79f93..4f3ff8024fb7dbe3b3c88893d3bc481ed99c7b97 100644
--- a/src_colibri2/popop_lib/bag.ml
+++ b/src_colibri2/popop_lib/bag.ml
@@ -137,6 +137,37 @@ let rec filter f = function
   | List xs -> list (List.filter f xs)
   | Concat(a,b) -> concat (filter f a) (filter f b)
 
+let rec filter_map_homo f = function
+  | Empty -> Empty
+  | Elt x as e -> (match f x with | Some x' -> if x == x' then e else Elt x'
+                                  | None -> Empty)
+  | Add(x,ts) as e -> (match f x with
+      | Some x' when x == x' ->
+        let ts' = filter_map_homo f ts in
+        if ts == ts' then e else add x' ts'
+      | Some x' -> add  x' (filter_map_homo f ts)
+      | None -> filter_map_homo f ts)
+  | App(ts,x) as e -> (match f x with
+      | Some x' when x == x' ->
+        let ts' = filter_map_homo f ts in
+        if ts == ts' then e else append ts' x'
+      | Some x' -> append  (filter_map_homo f ts) x'
+      | None -> filter_map_homo f ts)
+  | List xs as e ->
+    let rec aux f same old accu = function
+      | [] -> if same then old else list (List.rev accu)
+      | x :: l ->
+        match f x with
+        | None -> aux f false old accu l
+        | Some v when v == x -> aux f same old (v :: accu) l
+        | Some v -> aux f false old (v :: accu) l
+    in
+    aux f true e [] xs
+  | Concat(a,b) as e ->
+    let a' = (filter_map_homo f a) in
+    let b' = (filter_map_homo f b) in
+    if a == a' && b == b' then e else concat a' b'
+
 let rec partition f = function
   | Empty -> Empty , Empty
   | Elt x as e -> if f x then e,Empty else Empty,e
diff --git a/src_colibri2/popop_lib/bag.mli b/src_colibri2/popop_lib/bag.mli
index 36ed27e0302722ae278df291c898159b65e2f490..20a788d2bd59af8cc4b0ef9fc335cd47ad59ddd2 100644
--- a/src_colibri2/popop_lib/bag.mli
+++ b/src_colibri2/popop_lib/bag.mli
@@ -44,6 +44,9 @@ val for_all : ('a -> bool) -> 'a t -> bool
 val exists  : ('a -> bool) -> 'a t -> bool
 
 val filter : ('a -> bool) -> 'a t -> 'a t
+val filter_map_homo : ('a -> 'a option) -> 'a t -> 'a t
+(** homogeneous, physical identity kept for identity *)
+
 val partition : ('a -> bool) -> 'a t -> 'a t * 'a t
 
 val length : 'a t -> int
diff --git a/src_colibri2/popop_lib/lists.ml b/src_colibri2/popop_lib/lists.ml
index b716051273cdf24858349e59b7fa274c2049bf33..f16a4477f100b7146aee6af0cba3c6276b76903c 100644
--- a/src_colibri2/popop_lib/lists.ml
+++ b/src_colibri2/popop_lib/lists.ml
@@ -141,3 +141,14 @@ let rec last_rev n = function
     else rev,a::rem, n
 
 let hash f = List.fold_left (fun acc x -> (f x) * 65599 + acc)
+
+let filter_map_homo f l =
+  let rec aux f same old accu = function
+    | [] -> if same then old else List.rev accu
+    | x :: l ->
+      match f x with
+      | None -> aux f false old accu l
+      | Some v when v == x -> aux f same old (v :: accu) l
+      | Some v -> aux f false old (v :: accu) l
+  in
+  aux f true l [] l
diff --git a/src_colibri2/popop_lib/lists.mli b/src_colibri2/popop_lib/lists.mli
index 8d593933f35de943c064c586212307733e22e5c7..d0c772b6c12c8e5abb79910324b2d33dc84baff6 100644
--- a/src_colibri2/popop_lib/lists.mli
+++ b/src_colibri2/popop_lib/lists.mli
@@ -88,3 +88,5 @@ val last_rev : int -> 'a list -> 'a list * 'a list * int
 *)
 
 val hash: ('a -> int) -> int -> 'a list -> int
+
+val filter_map_homo: ('a -> 'a option) -> 'a list -> 'a list
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
index a53a7bd6cecd10bf4aacb4d88ad2a19d549de02d..f7a4d3d58a8896bac14b34227d46b43c254393e4 100644
--- a/src_colibri2/stdlib/wto.ml
+++ b/src_colibri2/stdlib/wto.ml
@@ -139,7 +139,7 @@ module Make(N:sig
                             numbering.  Note that we replaced the DFN=0
                             test by presence in the Hashtable. *)
       mutable num: level;          (* Number of visited nodes. *)
-      succs: N.t -> (N.t list);    (* Successors transition. *)
+      succs: N.t -> (N.t Base.Sequence.t);    (* Successors transition. *)
       stack: N.t Stack.t
     }
 
@@ -169,11 +169,11 @@ module Make(N:sig
       DFN.replace state.dfn vertex (Parent n);
       (* Visit all its successors *)
       let succs = state.succs vertex in
-      let (loop,partition) = List.fold_left (fun (loop,partition) succ ->
+      let (loop,partition) = Base.Sequence.fold ~f:(fun (loop,partition) succ ->
           let (loop',partition) = visit ~pref state succ partition in
           let loop = min_loop loop loop' in
           (loop,partition)
-        ) (NoLoop,partition) succs
+        ) ~init:(NoLoop,partition) succs
       in
       match loop with
       (* We are not in a loop. Add the vertex to the partition *)
@@ -209,13 +209,13 @@ module Make(N:sig
         (* Makes [vertex] invisible in the subsequents visits. *)
         DFN.replace state.dfn vertex Invisible;
         (* Restart the component analysis *)
-        let component = List.fold_left
-            (fun component succ ->
+        let component = Base.Sequence.fold
+            ~f:(fun component succ ->
                let (loop,component) = visit ~pref state succ component in
                (* Since we reset the component we should have no loop *)
                assert (is_no_loop loop);
                component
-            ) [] succs
+            ) ~init:[] succs
         in
         (NoLoop,Component(vertex,component)::partition)
       | _ ->
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
index d09bd5a537687ced45cdfda8d37a5e7463eb0f05..a4226b3b926b18f9f1510658c4a0b42bb713adfb 100644
--- a/src_colibri2/stdlib/wto.mli
+++ b/src_colibri2/stdlib/wto.mli
@@ -60,7 +60,9 @@ module Make(Node:sig
 
   (** Implements Bourdoncle "Efficient chaotic iteration strategies with
   widenings" algorithm to compute a WTO. *)
-  val partition: ?pref:pref -> inits:Node.t list -> succs:(Node.t -> Node.t list) -> Node.t partition
+  val partition: ?pref:pref -> inits:Node.t list ->
+    succs:(Node.t -> Node.t Base.Sequence.t) ->
+    Node.t partition
 
   val equal_component: Node.t component -> Node.t component -> bool
   val equal_partition: Node.t partition -> Node.t partition -> bool
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index c4b59b529548dfedfa3f3837e1d055ce3864e223..7155d1b705b7442f4ba553530501407ac8e74d09 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -3,7 +3,7 @@ let result = Sys.argv.(2)
 
 let print_test cout file =
   Printf.fprintf cout
-    "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 1300 %%{dep:%s}))))\n"
+    "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 3000 %%{dep:%s}))))\n"
     file file;
   Printf.fprintf cout
     "(rule (alias runtest) (action (diff oracle %s.res)))\n"
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index 321eff40853839f9c1ed2a6d243e5d858dffb971..a3f62fc4b1da922cfe7cc9e744d33462d929f778 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,23 +1,23 @@
 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:anomaly_agetooold.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
 (rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:anomaly_agetooold2.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold2.cnf}))))
 (rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
-(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:assertion_fail.cnf}))))
+(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:assertion_fail.cnf}))))
 (rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
-(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:fuzzing1.cnf}))))
+(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing1.cnf}))))
 (rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
-(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:fuzzing2.cnf}))))
+(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing2.cnf}))))
 (rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
-(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:par8-1-c.cnf}))))
+(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:par8-1-c.cnf}))))
 (rule (alias runtest) (action (diff oracle par8-1-c.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-2.cnf}))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-3.cnf}))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-4.cnf}))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
-(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:quinn.cnf}))))
+(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:quinn.cnf}))))
 (rule (alias runtest) (action (diff oracle quinn.cnf.res)))
-(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:simple_v3_c2.cnf}))))
+(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:simple_v3_c2.cnf}))))
 (rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index 6d83227b406cae6bb12ecd5937688a5b6d109474..5766ddefedd107515845f373eae117792d2a25f5 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,13 +1,13 @@
 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:anomaly_agetooold.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
 (rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:modus_ponens.cnf}))))
+(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:modus_ponens.cnf}))))
 (rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
-(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-1.cnf}))))
+(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-1.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-2.cnf}))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-3.cnf}))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1300 %{dep:pigeon-4.cnf}))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
index 5c9df097ee6d07ceb7f346a751875c47e26d4ab2..38973a52198121e5a3d7b80a62a4d077e18d83dd 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,13 +1,13 @@
 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
 (rule (alias runtest) (action (diff oracle enum.smt2.res)))
-(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
+(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
 (rule (alias runtest) (action (diff oracle list0.smt2.res)))
-(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))
+(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
 (rule (alias runtest) (action (diff oracle list1.smt2.res)))
-(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:tree1.smt2}))))
+(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree1.smt2}))))
 (rule (alias runtest) (action (diff oracle tree1.smt2.res)))
-(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:tree2.smt2}))))
+(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree2.smt2}))))
 (rule (alias runtest) (action (diff oracle tree2.smt2.res)))
-(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:tree3.smt2}))))
+(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree3.smt2}))))
 (rule (alias runtest) (action (diff oracle tree3.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index b72105b22d56120c492760028381cb5e31dae98c..9c4a2ebd51587acbfe31ccf0a461a9757b1d4c06 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,15 +1,15 @@
 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum.smt2}))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
 (rule (alias runtest) (action (diff oracle enum.smt2.res)))
-(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:enum2.smt2}))))
+(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum2.smt2}))))
 (rule (alias runtest) (action (diff oracle enum2.smt2.res)))
-(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list0.smt2}))))
+(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
 (rule (alias runtest) (action (diff oracle list0.smt2.res)))
-(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list1.smt2}))))
+(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
 (rule (alias runtest) (action (diff oracle list1.smt2.res)))
-(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list2.smt2}))))
+(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list2.smt2}))))
 (rule (alias runtest) (action (diff oracle list2.smt2.res)))
-(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list3.smt2}))))
+(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list3.smt2}))))
 (rule (alias runtest) (action (diff oracle list3.smt2.res)))
-(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:list4.smt2}))))
+(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list4.smt2}))))
 (rule (alias runtest) (action (diff oracle list4.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index d5fd2eeb1a8647d1e98a6e335ce66f38584f8f4e..b5a74a06e759efdb4a3a75581b2d513a7ad265e3 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,67 +1,67 @@
 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_CombiRepr_normalize.smt2}))))
+(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_CombiRepr_normalize.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_CombiRepr_normalize.smt2.res)))
-(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_conflict_add_disequality.smt2}))))
+(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conflict_add_disequality.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_conflict_add_disequality.smt2.res)))
-(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_conpoly.smt2}))))
+(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conpoly.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_conpoly.smt2.res)))
-(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
+(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_decide_must_test_is_dis_equal.smt2.res)))
-(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_init_always_merge_itself.smt2}))))
+(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_always_merge_itself.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_init_always_merge_itself.smt2.res)))
-(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
+(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_init_and_propa_must_be_ordered.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case1.smt2}))))
+(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case1.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_case1.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case_4.smt2}))))
+(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case_4_bis.smt2}))))
+(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4_bis.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_case_4_bis.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_itself_coef_of_repr_is_one.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_itself_last_case.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_last_case.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_itself_last_case.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_itself_pivot_not_in_p12.smt2.res)))
-(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_must_use_find.smt2}))))
+(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_must_use_find.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_must_use_find.smt2.res)))
-(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_mult_explication.smt2}))))
+(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_explication.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_mult_explication.smt2.res)))
-(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
+(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_mult_not_linear_in_conflict.smt2.res)))
-(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_normalize_use_find_def.smt2}))))
+(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_normalize_use_find_def.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_normalize_use_find_def.smt2.res)))
-(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_own_repr.smt2}))))
+(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_own_repr.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_own_repr.smt2.res)))
-(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_propacl.smt2}))))
+(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_propacl.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_propacl.smt2.res)))
-(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_subst_and_conflict_add.smt2}))))
+(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_subst_and_conflict_add.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_subst_and_conflict_add.smt2.res)))
-(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_zero_dom.smt2}))))
+(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_zero_dom.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res)))
-(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:attach_only_when_dom_present.smt2}))))
+(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:attach_only_when_dom_present.smt2}))))
 (rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res)))
-(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:init_not_repr.smt2}))))
+(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:init_not_repr.smt2}))))
 (rule (alias runtest) (action (diff oracle init_not_repr.smt2.res)))
-(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le.smt2}))))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
 (rule (alias runtest) (action (diff oracle le.smt2.res)))
-(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le2.smt2}))))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
 (rule (alias runtest) (action (diff oracle le2.smt2.res)))
-(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul.smt2}))))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
 (rule (alias runtest) (action (diff oracle mul.smt2.res)))
-(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:sem_invariant_in_learnt_dec.smt2}))))
+(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
 (rule (alias runtest) (action (diff oracle sem_invariant_in_learnt_dec.smt2.res)))
-(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_add_pexp_cl.smt2}))))
+(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_add_pexp_cl.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_add_pexp_cl.smt2.res)))
-(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
+(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_arith_homogeneous_dist_sign.smt2.res)))
-(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_merge_itself_repr_inside.smt2}))))
+(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_inside.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_merge_itself_repr_inside.smt2.res)))
-(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
+(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_set_pending_merge_expsameexp.smt2.res)))
-(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_subst_eventdom_find.smt2}))))
+(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_subst_eventdom_find.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_subst_eventdom_find.smt2.res)))
-(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real.smt2}))))
+(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
 (rule (alias runtest) (action (diff oracle to_real.smt2.res)))
-(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real2.smt2}))))
+(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
 (rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 533c77d3f1805b486c2518c6c3c4d3288c47c360..7247c5c7a1db0e5484792b17b71e654536ceeaa9 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -1,23 +1,23 @@
 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_ExpMult_by_zero.smt2}))))
+(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_ExpMult_by_zero.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:arith_merge_case2.smt2}))))
+(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case2.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res)))
-(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le.smt2}))))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
 (rule (alias runtest) (action (diff oracle le.smt2.res)))
-(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:le2.smt2}))))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
 (rule (alias runtest) (action (diff oracle le2.smt2.res)))
-(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul.smt2}))))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
 (rule (alias runtest) (action (diff oracle mul.smt2.res)))
-(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:repr_and_poly.smt2}))))
+(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_and_poly.smt2}))))
 (rule (alias runtest) (action (diff oracle repr_and_poly.smt2.res)))
-(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:repr_fourier.smt2}))))
+(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_fourier.smt2}))))
 (rule (alias runtest) (action (diff oracle repr_fourier.smt2.res)))
-(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_merge_itself_repr_empty.smt2}))))
+(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_empty.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
-(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:solver_set_sem_merge_sign.smt2}))))
+(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_sem_merge_sign.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_set_sem_merge_sign.smt2.res)))
-(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real.smt2}))))
+(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
 (rule (alias runtest) (action (diff oracle to_real.smt2.res)))
-(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:to_real2.smt2}))))
+(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
 (rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
index 7fd6061c92ad9f7a1383f0e1503c90cf59e94078..4933b571de77711d0319d023095300c5e79aeac8 100644
--- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -1,15 +1,15 @@
 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:ceil.smt2}))))
+(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
 (rule (alias runtest) (action (diff oracle ceil.smt2.res)))
-(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos.smt2}))))
+(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
 (rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos_lt.smt2}))))
+(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
 (rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
-(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut.smt2}))))
+(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
-(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut2.smt2}))))
+(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
-(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos.smt2}))))
+(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
-(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos_lt.smt2}))))
+(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
index 3ea098f59acbdea23f34efa70b24bb3dab0f0152..3910cff2d287652fcf7e49bd14816f68ccd420ab 100644
--- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -1,21 +1,21 @@
 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:ceil.smt2}))))
+(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
 (rule (alias runtest) (action (diff oracle ceil.smt2.res)))
-(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos.smt2}))))
+(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
 (rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos_lt.smt2}))))
+(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
 (rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:div_pos_lt_to_real.smt2}))))
+(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt_to_real.smt2}))))
 (rule (alias runtest) (action (diff oracle div_pos_lt_to_real.smt2.res)))
-(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:floor.smt2}))))
+(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:floor.smt2}))))
 (rule (alias runtest) (action (diff oracle floor.smt2.res)))
-(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut.smt2}))))
+(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
-(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_commut2.smt2}))))
+(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
-(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos.smt2}))))
+(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
-(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos_lt.smt2}))))
+(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
-(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:mul_pos_zero_le.smt2}))))
+(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_zero_le.smt2}))))
 (rule (alias runtest) (action (diff oracle mul_pos_zero_le.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
index d88d5660a9e0d6585c47750a1db1586cb87c1cc5..cc94dac9716739bdac8e54c45fde7da6e6e14977 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
@@ -1,9 +1,9 @@
 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists.smt2}))))
+(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
 (rule (alias runtest) (action (diff oracle exists.smt2.res)))
-(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall0.smt2}))))
+(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
 (rule (alias runtest) (action (diff oracle forall0.smt2.res)))
-(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall3.smt2}))))
+(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
 (rule (alias runtest) (action (diff oracle forall3.smt2.res)))
-(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall4.smt2}))))
+(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
 (rule (alias runtest) (action (diff oracle forall4.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index 63371f6c63046bb77566e762b2743cb05a9fc79b..b5b0d93926e5859fb77b5bd91b7ed7c60018470c 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,23 +1,23 @@
 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists.smt2}))))
+(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
 (rule (alias runtest) (action (diff oracle exists.smt2.res)))
-(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists2.smt2}))))
+(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists2.smt2}))))
 (rule (alias runtest) (action (diff oracle exists2.smt2.res)))
-(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall0.smt2}))))
+(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
 (rule (alias runtest) (action (diff oracle forall0.smt2.res)))
-(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall1.smt2}))))
+(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall1.smt2}))))
 (rule (alias runtest) (action (diff oracle forall1.smt2.res)))
-(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall2.smt2}))))
+(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall2.smt2}))))
 (rule (alias runtest) (action (diff oracle forall2.smt2.res)))
-(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall3.smt2}))))
+(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
 (rule (alias runtest) (action (diff oracle forall3.smt2.res)))
-(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall4.smt2}))))
+(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
 (rule (alias runtest) (action (diff oracle forall4.smt2.res)))
-(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall5.smt2}))))
+(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall5.smt2}))))
 (rule (alias runtest) (action (diff oracle forall5.smt2.res)))
-(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall6.smt2}))))
+(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall6.smt2}))))
 (rule (alias runtest) (action (diff oracle forall6.smt2.res)))
-(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall7.smt2}))))
+(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall7.smt2}))))
 (rule (alias runtest) (action (diff oracle forall7.smt2.res)))
-(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall8.smt2}))))
+(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall8.smt2}))))
 (rule (alias runtest) (action (diff oracle forall8.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index 6b3b1650084289b33e2b7ca16d55c1c2740feec1..d9082d43c00e19390f1f71af55917ec143b021a8 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,43 +1,43 @@
 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:bad_conflict.smt2}))))
+(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bad_conflict.smt2}))))
 (rule (alias runtest) (action (diff oracle bad_conflict.smt2.res)))
-(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:bcp_dont_like_duplicate.smt2}))))
+(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bcp_dont_like_duplicate.smt2}))))
 (rule (alias runtest) (action (diff oracle bcp_dont_like_duplicate.smt2.res)))
-(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:bool_not_propa.smt2}))))
+(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bool_not_propa.smt2}))))
 (rule (alias runtest) (action (diff oracle bool_not_propa.smt2.res)))
-(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:boolexpup.smt2}))))
+(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:boolexpup.smt2}))))
 (rule (alias runtest) (action (diff oracle boolexpup.smt2.res)))
-(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:clause_normalization.smt2}))))
+(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clause_normalization.smt2}))))
 (rule (alias runtest) (action (diff oracle clause_normalization.smt2.res)))
-(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:clmerge.smt2}))))
+(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clmerge.smt2}))))
 (rule (alias runtest) (action (diff oracle clmerge.smt2.res)))
-(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:conflict_complete_needed_cl.smt2}))))
+(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:conflict_complete_needed_cl.smt2}))))
 (rule (alias runtest) (action (diff oracle conflict_complete_needed_cl.smt2.res)))
-(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:directdom_not.smt2}))))
+(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:directdom_not.smt2}))))
 (rule (alias runtest) (action (diff oracle directdom_not.smt2.res)))
-(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:dis_dom_before_first_age.smt2}))))
+(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dis_dom_before_first_age.smt2}))))
 (rule (alias runtest) (action (diff oracle dis_dom_before_first_age.smt2.res)))
-(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:dom_merge_equality.smt2}))))
+(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dom_merge_equality.smt2}))))
 (rule (alias runtest) (action (diff oracle dom_merge_equality.smt2.res)))
-(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality.smt2}))))
+(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality.smt2}))))
 (rule (alias runtest) (action (diff oracle equality.smt2.res)))
-(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality_condis.smt2}))))
+(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_condis.smt2}))))
 (rule (alias runtest) (action (diff oracle equality_condis.smt2.res)))
-(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality_get_sem.smt2}))))
+(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_get_sem.smt2}))))
 (rule (alias runtest) (action (diff oracle equality_get_sem.smt2.res)))
-(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exp_sem_equality.smt2}))))
+(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exp_sem_equality.smt2}))))
 (rule (alias runtest) (action (diff oracle exp_sem_equality.smt2.res)))
-(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:explimit_cl_equality.smt2}))))
+(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:explimit_cl_equality.smt2}))))
 (rule (alias runtest) (action (diff oracle explimit_cl_equality.smt2.res)))
-(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:implication.smt2}))))
+(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:implication.smt2}))))
 (rule (alias runtest) (action (diff oracle implication.smt2.res)))
-(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:intmap_set_disjoint.smt2}))))
+(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:intmap_set_disjoint.smt2}))))
 (rule (alias runtest) (action (diff oracle intmap_set_disjoint.smt2.res)))
-(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:is_equal_not_propagated.smt2}))))
+(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:is_equal_not_propagated.smt2}))))
 (rule (alias runtest) (action (diff oracle is_equal_not_propagated.smt2.res)))
-(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:ite_sem_bool.smt2}))))
+(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ite_sem_bool.smt2}))))
 (rule (alias runtest) (action (diff oracle ite_sem_bool.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:polyeq_genequality.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
 (rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
-(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:substupfalse_equality.smt2}))))
+(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:substupfalse_equality.smt2}))))
 (rule (alias runtest) (action (diff oracle substupfalse_equality.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 0195ec1bf0f248e0635d9927f0496366e986bc81..137b8afa13e57da969cdb2449c825f4f2cb3b0e2 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,27 +1,27 @@
 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
+(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
 (rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res)))
-(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:deltaed0.smt2}))))
+(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:deltaed0.smt2}))))
 (rule (alias runtest) (action (diff oracle deltaed0.smt2.res)))
-(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:diff_to_value_for_bool.smt2}))))
+(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_to_value_for_bool.smt2}))))
 (rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res)))
-(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:diff_value_substupfalse.smt2}))))
+(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_value_substupfalse.smt2}))))
 (rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res)))
-(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:distinct.smt2}))))
+(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:distinct.smt2}))))
 (rule (alias runtest) (action (diff oracle distinct.smt2.res)))
-(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:eq_diamond2.smt2}))))
+(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:eq_diamond2.smt2}))))
 (rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
-(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:equality_norm_set.smt2}))))
+(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_norm_set.smt2}))))
 (rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
-(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:fundef.smt2}))))
+(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fundef.smt2}))))
 (rule (alias runtest) (action (diff oracle fundef.smt2.res)))
-(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
+(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
 (rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res)))
-(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:many_distinct.smt2}))))
+(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:many_distinct.smt2}))))
 (rule (alias runtest) (action (diff oracle many_distinct.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:polyeq_genequality.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
 (rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:polyeq_genequality_deltaed.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality_deltaed.smt2}))))
 (rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res)))
-(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:xor.smt2}))))
+(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:xor.smt2}))))
 (rule (alias runtest) (action (diff oracle xor.smt2.res)))
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index c00d1838eb33e5b5fb9bb7ec2eab2ff9b4cc06ee..e8b62ee4055d68c711bb292358b4656e1d83a736 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -160,7 +160,8 @@ let converter d (f : Ground.t) =
   let reg n = Egraph.register d n in
   let open Monad in
   match Ground.sem f with
-  | { app = { builtin = Expr.Tester { adt; case; _ }; _ }; args = [ e ]; _ } ->
+  | { app = { builtin = Expr.Tester { adt; case; _ }; _ }; args; _ } ->
+      let e = IArray.extract1_exn args in
       reg e;
       wait.for_value d Boolean.BoolValue.key r
         (set e
@@ -177,18 +178,16 @@ let converter d (f : Ground.t) =
             | One { case = case'; _ } -> Some (Case.equal case case')));
       Adt_value.propagate_value d f
   | { app = { builtin = Expr.Constructor { case; _ }; _ }; args; _ } ->
-      List.iter reg args;
+      IArray.iter ~f:reg args;
       let fields =
-        Base.List.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
+        IArray.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
             Field.M.add field a acc)
       in
       upd_dom d r (One { case; fields });
       Adt_value.propagate_value d f
-  | {
-   app = { builtin = Expr.Destructor { case; field; adt; _ }; _ };
-   args = [ e ];
-   _;
-  } ->
+  | { app = { builtin = Expr.Destructor { case; field; adt; _ }; _ }; args; _ }
+    ->
+      let e = IArray.extract1_exn args in
       reg e;
       Egraph.register_decision d (Decide.new_decision e adt case);
       let upd d =
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index 9882da027f603b11c35e1806ada56fa9525c5d4c..eb1c0974e58a6de1363353ce95801588004260d6 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -22,7 +22,7 @@ module T' = struct
     }
     [@@deriving eq, ord, hash]
 
-    let pp fmt c = Fmt.pf fmt "%i(%a)" c.case (Field.M.pp Value.pp) c.fields
+    let pp fmt c = Fmt.pf fmt "ADT.%i(%a)" c.case (Field.M.pp Value.pp) c.fields
   end
 
   include T
@@ -43,7 +43,8 @@ let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
 let compute d g =
   match Ground.sem g with
-  | { app = { builtin = Expr.Tester { case; _ }; _ }; args = [ e ]; _ } ->
+  | { app = { builtin = Expr.Tester { case; _ }; _ }; args; _ } ->
+      let e = IArray.extract1_exn args in
       let v = coerce_nodevalue (interp d e) in
       let v = value v in
       `Some
@@ -55,16 +56,13 @@ let compute d g =
    _;
   } ->
       let fields =
-        Base.List.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
+        IArray.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
             Field.M.add field (interp d a) acc)
       in
       let v = { tyargs; adt; case; fields } in
       `Some (nodevalue (index v))
-  | {
-   app = { builtin = Expr.Destructor { case; field; _ }; _ };
-   args = [ e ];
-   _;
-  } ->
+  | { app = { builtin = Expr.Destructor { case; field; _ }; _ }; args; _ } ->
+      let e = IArray.extract1_exn args in
       let v = coerce_nodevalue (interp d e) in
       let v = value v in
       if Case.equal case v.case then
@@ -92,7 +90,7 @@ let propagate_value d g =
         Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate
           d g
   in
-  Interp.TwoWatchLiteral.create d f g
+  Interp.WatchArgs.create d f g
 
 let sequence_of_cases d ty tyargs all_cases cases =
   let open Interp.SeqLim in
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index cbb5f1848077d1475a103e73f67f836eb78d7b19..b362031ac2d2427a188ec0aee5440b3f3359178a 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -228,7 +228,8 @@ let converter d (f:Ground.t) =
   | { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty }
     when Ground.Ty.equal ty Ground.Ty.int ->
     upd_dom d r D.integers
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let (a,b) = IArray.extract2_exn args in
     reg a; reg b;
     let wakeup =
       set r (let+ va = get a and+ vb = get b in D.add va vb) &&
@@ -236,7 +237,8 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in D.minus vr va)
     in
     List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b;r]
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let (a,b) = IArray.extract2_exn args in
     reg a; reg b;
     let wakeup =
       set r (let+ va = get a and+ vb = get b in D.minus va vb) &&
@@ -244,20 +246,25 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in D.minus va vr)
     in
     List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b;r]
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a;
     let wakeup =
       set r (let+ va = get a in D.mult_cst Q.minus_one va) &&
       set a (let+ vr = get r in D.mult_cst Q.minus_one vr)
     in
     List.iter (fun n -> wait.for_dom d dom n wakeup) [a;r]
-  | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false) `Lt a b
-  | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some true | Gt -> Some false) `Le a b
-  | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Le -> None | Lt -> Some false  | Ge | Gt -> Some true) `Ge a b
-  | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some false  | Gt -> Some true) `Gt a b
   | _ -> ()
 
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index ca059d1598ea2e451b02f4f9bee1e51957b01042..55052ceef36ff1b5566fcf560817dbe1a1acfd72 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -192,13 +192,16 @@ let converter d (f:Ground.t) =
     let res = Ground.node f in
   let reg n = Egraph.register d n in
   match Ground.sem f with
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.one;b,Q.one])
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.one;b,Q.minus_one])
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a;
     assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.minus_one])
   | _ -> ()
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index e162fde0304ae5eb0b86d5e3b549cd584d4e94d2..5907e5f0eb6c24d8ae6eccb5be051c2381cead1b 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -359,20 +359,24 @@ let converter d (f:Ground.t) =
   let res = Ground.node f in
   let reg n = Egraph.register d n in
   match Ground.sem f with
-  | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     assume_poly_equality d res (Product.of_list [a,Q.one;b,Q.one])
-  | { app = {builtin = Expr.Div}; tyargs = []; args = [num;den]; _ } ->
+  | { app = {builtin = Expr.Div}; tyargs = []; args; _ } ->
+    let num,den = IArray.extract2_exn args in
     reg num; reg den;
     wait.for_dom d Dom_interval.dom den
       (fun d _ ->
          if Dom_interval.is_not_zero d den then
            assume_poly_equality d num (Product.of_list [res,Q.one;den,Q.one])
       )
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     List.iter (fun x -> wait.for_dom d dom x (factorize res a Q.one b)) [a;b]
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     List.iter (fun x -> wait.for_dom d dom x (factorize res a Q.minus_one b)) [a;b]
   | _ -> ()
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 9549bce8f25d7c3645c94572ee91e888be47cbea..23aad9c4b967f78ffbfd4ed8dc850f8297f65edd 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -102,13 +102,17 @@ let make_equations d (eqs,vars) g =
   | Some truth ->
     let p,bound,p_non_norm =
       match Ground.sem g with
-      | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Strict truth a b
-      | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Large truth a b
-      | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Large truth b a
-      | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Strict truth b a
       | _ -> assert false
     in
@@ -205,7 +209,7 @@ let converter d (f:Ground.t) =
       Egraph.attach_dom d n Dom_polynome.dom Daemon.key ();
       Egraph.attach_node d n Daemon.key ();
     in
-    List.iter attach args;
+    IArray.iter ~f:attach args;
     Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key ();
     Datastructure.Queue.push comparisons d f;
     Egraph.register_delayed_event d Daemon.key ()
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index 2daa4f5bcce43ffb06e1fdc88f491f96a43d0cfd..50d80ce3532ac65d55263a8106cbe8a8b91003ad 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -9,7 +9,8 @@ let init,attach =
 let converter d (f:Ground.t) =
   let res = Ground.node f in
   match Ground.sem f with
-  | { app = {builtin = Expr.Mul}; tyargs = []; args = [arg1;arg2]; _ } -> begin
+  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } -> begin
+      let arg1,arg2 = Colibri2_popop_lib.IArray.extract2_exn args in
       Egraph.register d arg1; Egraph.register d arg2;
       attach d arg1 (res,arg2);
       attach d arg2 (res,arg1)
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 70d14e86d5d655ef0c0073398f2a579b46a553bd..4410b095a39f37a255ba00dcec974c93aa892804 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -133,34 +133,48 @@ module Check = struct
             ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
             | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
             );
-          args = [a] } ->
+          args } ->
+        let a = IArray.extract1_exn args in
         !< (!> a)
-      | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Integer s}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         !< (Q.of_string s)
-      | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Decimal s}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         !< (Q.of_string_decimal s)
-      | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Rational s}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         !< (Q.of_string_decimal s)
-      | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Add}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Q.add !>a !>b)
-      | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Sub}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Q.sub !>a !>b)
-      | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; ty = _ } ->
+      | { app = {builtin = Expr.Minus}; tyargs = []; args; ty = _ } ->
+        let a = IArray.extract1_exn args in
         !< (Q.neg !>a)
-      | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Mul}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Q.mul !>a !>b)
-      | { app = {builtin = Expr.Div}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Div}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         if Q.is_zero !>b then `Uninterp
         else !< (Q.div !>a !>b)
-      | { app = {builtin = Expr.Lt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.lt !>arg1 !>arg2)
-      | { app = {builtin = Expr.Leq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.leq !>arg1 !>arg2)
-      | { app = {builtin = Expr.Gt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.gt !>arg1 !>arg2)
-      | { app = {builtin = Expr.Geq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.geq !>arg1 !>arg2)
-      | { app = {builtin = Expr.Floor}; tyargs = []; args = [a]; _ } ->
+      | { app = {builtin = Expr.Lt}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.lt !>a !>b)
+      | { app = {builtin = Expr.Leq}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.leq !>a !>b)
+      | { app = {builtin = Expr.Gt}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.gt !>a !>b)
+      | { app = {builtin = Expr.Geq}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.geq !>a !>b)
+      | { app = {builtin = Expr.Floor}; tyargs = []; args; _ } ->
+        let a = IArray.extract1_exn args in
         !< (Q.floor (!> a))
       | _ -> `None
 
@@ -182,7 +196,7 @@ module Check = struct
       | `Some v -> Egraph.set_value d (Ground.node g) v
       | `Uninterp -> Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate d g
     in
-    Interp.TwoWatchLiteral.create d f g
+    Interp.WatchArgs.create d f g
 end
 
       (** {2 Initialization} *)
@@ -204,15 +218,20 @@ let converter d (f:Ground.t) =
         ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
         | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
         );
-      args = [a] } ->
+      args } ->
+    let a = IArray.extract1_exn args in
     merge a; Check.attach d f
-  | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.Integer s}; tyargs = []; args; _ } ->
+    assert ( IArray.is_empty args);
     merge (cst (Q.of_string s))
-  | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.Decimal s}; tyargs = []; args; _ } ->
+assert ( IArray.is_empty args);
     merge (cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.Rational s}; tyargs = []; args; _ } ->
+assert ( IArray.is_empty args);
     merge (cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b; Check.attach d f;
     let wait =
       set r (let+ va = get a and+ vb = get b in Q.add va vb) &&
@@ -220,7 +239,8 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in Q.sub vr va)
     in
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b; Check.attach d f;
     let wait =
       set r (let+ va = get a and+ vb = get b in Q.sub va vb) &&
@@ -228,30 +248,37 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in Q.sub va vr)
     in
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
-  | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; _ } ->
-    reg a; reg b; Check.attach d f;
-    let wait =
-      set r (let+ va = get a and+ vb = get b in Q.mul va vb) &&
-      set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.div vr vb)) &&
-      set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
-    in
-    List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } ->
+  let a,b = IArray.extract2_exn args in
+  reg a; reg b; Check.attach d f;
+  let wait =
+    set r (let+ va = get a and+ vb = get b in Q.mul va vb) &&
+    set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.div vr vb)) &&
+    set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
+  in
+  List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
+  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a; Check.attach d f;
     let wait =
       set r (let+ va = get a in Q.neg va) &&
       set a (let+ vr = get r in Q.neg vr)
     in
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;r]
-  | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.lt a b; Check.attach d f;
-  | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.le a b; Check.attach d f;
-  | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.gt a b; Check.attach d f;
-  | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.ge a b; Check.attach d f;
-  | { app = {builtin = Expr.Floor}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Floor}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a; Check.attach d f;
   | _ -> ()
 
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 89fd485417fd2fb4bea3c7b2276af896d7c40ba8..b3ee59315080ca2e4b318110d7a5a3bf3a55b9b2 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -70,360 +70,211 @@ let set_bool env node b =
 
 let mulbool b1 b2 = not(Equal.bool b1 b2)
 
-module T = struct
-  open Base
-  type t =
-    { topnot: bool;
-      lits: (Node.t * bool) IArray.t;
-    }
-  [@@deriving eq,ord,hash]
-
-
-  let print_cl fmt node b =
-    if b
-    then Fmt.pf fmt "¬ %a" Node.pp node
-    else Node.pp fmt node
-
-  let isnot v =
-    if IArray.length v.lits = 1 then
-      let node,sign = IArray.get v.lits 0 in
-      assert (v.topnot && not sign);
-      Some node
-    else
-      None
-
-  let pp fmt x =
-    match isnot x with
-    | Some node ->
-      print_cl fmt node true
-    | None ->
-      let print_cl topnot fmt (node,b) = print_cl fmt node (mulbool topnot b) in
-      let aux b fmt' m = IArray.fold (fun sofar e -> e::sofar) [] m
-                        |> List.rev
-                        |> Fmt.(list ~sep:(const char ',') (print_cl b) fmt')
-      in
-      if x.topnot
-      then Fmt.pf fmt "â‹€(%a)" (aux true) x.lits
-      else Fmt.pf fmt "⋁(%a)" (aux false) x.lits
-
-end
-
-let sem = ThTermKind.create_key (module struct type t = T.t let name = "Prop" end)
-
-(* let iter f x = IArray.iter f x.lits *)
-
-let fold f acc x = IArray.fold f acc x.T.lits
-
-let find x n =
-  fold (fun acc (n1,b) -> if Node.equal n1 n then Some b else acc) None x
-
-let node_of_bool b =
-  if b then node_true else node_false
-
-module Th = struct
-  include T
-  include MkDatatype(T)
-
-  let key = sem
+let _true = node_true
+let _false = node_false
 
-  exception TopKnown of bool
+let set_true env node = set_bool env node true
+let set_false env node = set_bool env node false
 
-  exception Found of Node.t * bool
-  let find_not_known d l =
-    IArray.iter (fun (node,b) ->
-      match Egraph.get_value d node with
-      | Some _ -> ()
-      | None -> raise (Found (node,b))
-    ) l
+let a = Expr.Term.Var.mk "a" Expr.Ty.bool
+let ta = Expr.Term.of_var a
 
-  let _bcp d l absorbent =
-    try
-      let res = IArray.fold (fun acc node ->
-        match is d node, acc with
-        | Some b, _ when Bool.equal b absorbent -> raise (TopKnown absorbent)
-        | Some _, _ -> acc
-        | None, Some _ -> raise Exit
-        | None, None -> Some node)
-        None l in
-      match res with
-      | None -> raise (TopKnown (not absorbent))
-      | _ -> res
-    with Exit -> None
+let _not =
+  let e = Expr.Term.neg ta in
+  fun na ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na] } in
+    Ground.convert ~subst e
 
-end
+let _gen mk l =
+  let v = List.map (fun _ -> Expr.Term.Var.mk "b" Expr.Ty.bool) l in
+  let t = List.map Expr.Term.of_var v in
+  let subst = { Ground.Subst.empty with
+                term = Expr.Term.Var.M.of_list (List.combine v l) } in
+  Ground.convert ~subst (mk t)
 
-module ThE = ThTermKind.Register(Th)
+let _and = _gen Expr.Term._and
+let _or = _gen Expr.Term._or
 
-module DaemonPropaNot = struct
+(** {2 Choice on bool} *)
 
-  module Data = struct
-    type t = Th.t * Node.t * Node.t
-    let pp fmt (v,cl1,cl2) =
-      Format.fprintf fmt "%a,%a -> %a" Th.pp v Node.pp cl1 Node.pp cl2
-  end
+module ChoBool = struct
+  let make_decision env node b =
+    Debug.dprintf3 Egraph.print_decision "[Bool] decide %b on %a" b Node.pp node;
+    set_bool env node b
 
-  let delay = Events.Delayed_by 1
-  let key = Demon.Fast.create "Bool.DaemonPropaNot"
-  let throttle = 100
-  let wakeup d =
-    function
-    | Events.Fired.EventValue(_,_,((_,node,ncl))) ->
-      begin match is d node with
-        | None -> raise Impossible
-        | Some b ->
-          set_bool d ncl (not b)
-      end;
-    | _ -> raise UnwaitedEvent
-
-  let init d thterm node =
-    let v = ThE.sem thterm in
-    let own = ThE.node thterm in
-    match is d own with
-    | Some b ->
-      set_bool d node (not b)
-    | None ->
-      match is d node with
-      | Some b ->
-        set_bool d own (not b)
-      | None ->
-        let events = [Demon.Create.EventValue(own,dom,(v,own,node));
-                      Demon.Create.EventValue(node,dom,(v,node,own))] in
-        Demon.Fast.attach d key events
+  let choose_decision node env =
+    match is env node with
+    | Some _ ->
+      Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
+      Egraph.DecNo
+    | None -> DecTodo
+                (List.map (fun v env -> make_decision env node v)
+                   (Shuffle.shufflel [true;false]))
 
 end
 
-module RDaemonPropaNot = Demon.Fast.Register(DaemonPropaNot)
+let chobool n = {
+  Egraph.prio = 1;
+  choice = ChoBool.choose_decision n;
+}
 
-module DaemonPropa = struct
-  type watcher = (int,int) Context.Ref2.t
+module TwoWatchLiteral = struct
+  (** todo move the check to enqueue; but it requires to be able to attach event
+      in delayed_ro *)
 
-  type d =
-    | Lit of ThE.t (* prop *) * int (* watched *) * watcher
-  | All of ThE.t
+  module Daemon = struct
+    type t = {
+      absorbent: Value.t;
+      ground : Ground.t;  (** perhaps ground should have an array for args *)
+      from_start : int Context.Ref.t;  (** already set before *)
+      from_end : int Context.Ref.t;  (** already set after *)
+    }
 
-  let key = Demon.Fast.create "Bool.DaemonPropa"
+    type runable = (Egraph.t -> unit)
 
-  module Data = struct
-    type t = d
-    let pp fmt = function
-      | Lit (thterm,i,w) ->
-        let w,n = Context.Ref2.get w in
-        Format.fprintf fmt "Lit(%a,%i(%i,%i),%a)" ThE.pp thterm i w n
-          Node.pp (ThE.node thterm)
-      | All thterm -> Format.fprintf fmt "All(%a)" ThE.pp thterm
-  end
+    let print_runable = Fmt.nop
 
-  let delay = Events.Delayed_by 1
-  let throttle = 100
-
-  let wakeup_lit d thterm watched watcher =
-    let v = ThE.sem thterm in
-    let own = ThE.node thterm in
-    let set_dom_up_true d own _ _ =
-      let b = (not v.topnot) in
-      match is d own with
-      | Some b' when Equal.bool b' b -> ()
-      | _ -> set_bool d own b in
-    let merge_bcp node sign =
-      Debug.dprintf2 debug "[Bool] @[merge_bcp %a@]" Node.pp node;
-      match is d own with
-      | Some b' ->
-        let b = mulbool sign (mulbool b' v.topnot) in
-        set_bool d node b
-      | None -> (** merge *)
-        match is d node with
-        | Some b' ->
-          let b = mulbool sign (mulbool b' v.topnot) in
-          set_bool d own b
-        | None -> (** merge *)
-          if mulbool v.topnot sign
-          then DaemonPropaNot.init d thterm node
-          else Egraph.merge d own node in
-    let rec find_watch dir pos bound =
-      assert (dir = 1 || dir = -1);
-      if pos = bound
-      then
-        let node,sign = IArray.get v.lits pos in
-        (merge_bcp node sign; raise Exit)
-      else
-        let node,sign = IArray.get v.lits pos in
-        match is d node with
-        | None -> node,pos
-        | Some b when mulbool b sign (** true absorbent of or *) ->
-          set_dom_up_true d own node b; raise Exit
-        | Some _ (** false *) -> find_watch dir (dir+pos) bound
-    in
-    try
-      let w1, w2 = Context.Ref2.get watcher in
-      if w1 = -1 (** already done *)
-      then false
-      else begin
-        assert (watched = w1 || watched = w2);
-        assert (w1 < w2);
-        let dir,bound = if watched = w1 then 1,w2 else -1,w1 in
-        let clwatched, watched = find_watch dir watched bound in
-        if dir = 1
-        then Context.Ref2.set1 watcher watched
-        else Context.Ref2.set2 watcher watched;
-        Demon.Fast.attach d key
-          [Demon.Create.EventValue(clwatched,dom,
-                                   Lit(thterm,watched,watcher))] ;
-        true
-      end
-    with Exit ->
-      Context.Ref2.set watcher (-1) (-1);
-      false
-
-  let wakeup_own d thterm =
-    let v = ThE.sem thterm in
-    let own = ThE.node thterm in
-    begin match is d own with
-    | None -> (* only during init *)
-      Demon.Fast.attach d key
-        [Demon.Create.EventValue(own, dom, All thterm)];
-      true
-    (** \/ c1 c2 = false ==> c1 = false /\ c2 = false *)
-    | Some b when not (mulbool v.topnot b) ->
-      let set_dom_down_false (node,sign) = set_bool d node sign in
-      IArray.iter set_dom_down_false v.lits;
-      false
-    | Some _ -> true
-    end
-
-  (** return true if things should be propagated *)
-  let init d thterm =
-    let v = ThE.sem thterm in
-    wakeup_own d thterm &&
-    let last = IArray.length v.lits - 1 in
-    assert (last <> 0);
-    let watcher = Context.Ref2.create (Egraph.context d) 0 last in
-    wakeup_lit d thterm 0 watcher &&
-    wakeup_lit d thterm last watcher
-
-  let wakeup d = function
-    | Events.Fired.EventValue(_,_,Lit(thterm,watched,next)) ->
-      ignore (wakeup_lit d thterm watched next)
-    | Events.Fired.EventValue(_ownr,_,All thterm) ->
-      (** use this own because the other is the representant *)
-      ignore (wakeup_own d thterm)
-    | _ -> raise UnwaitedEvent
+    type event = t
 
+    let print_event fmt r = Ground.pp fmt r.ground
 
-end
+    let key =
+      Events.Dem.create_key
+        (module struct
+          type d = runable
 
-module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
-
-module DaemonInit = struct
-  let key = Demon.Fast.create "Bool.DaemonInit"
-
-  module Data = DUnit
-
-  let delay = Events.Delayed_by 1
-  let throttle = 100
-  let wakeup d = function
-    | Events.Fired.EventRegSem(thterm,()) ->
-      begin try
-          let thterm = ThE.coerce_thterm thterm in
-          let v = ThE.sem thterm in
-          match T.isnot v with
-          | Some node ->
-            Egraph.register d node;
-            DaemonPropaNot.init d thterm node
-          | None ->
-            assert (not lazy_propagation);
-            IArray.iter (fun (node,_) -> Egraph.register d node) v.lits;
-            if DaemonPropa.init d thterm then ()
-        (** we could register a decision here, if we want to do
-            decision on any boolean operations not only variable *)
-        with Exit -> ()
-      end
-    | _ -> raise UnwaitedEvent
+          type t = event
 
-end
+          let name = "Interp.TwoWatchLiteral"
+        end)
 
-module RDaemonInit = Demon.Fast.Register(DaemonInit)
+    let delay = Events.Delayed_by 1
 
+    type res_scan =
+      | LimitReached
+      | Absorbent
+      | ToWatch of int
 
-let _true = node_true
-let _not node =
-  index sem {topnot = true; lits = IArray.of_list [node,false]}
-
-
-let filter fold_left =
-  let m = fold_left (fun acc (e,b) ->
-      Node.M.add_change (fun b -> b)
-        (fun b1 b2 -> if Equal.bool b1 b2 then b1 else raise Exit) e b acc)
-      Node.M.empty  in
-  Node.M.bindings m
-
-let gen topnot l =
-  try
-    let l = filter (fun f acc -> List.fold_left f acc l) in
-    match l with
-    | [] -> if topnot then node_true else node_false
-    | [node,b] when mulbool topnot b -> _not node
-    | [node,_] -> node
-    | l ->
-      index sem {topnot; lits = IArray.of_list l}
-  with Exit -> if topnot then node_false else node_true
-
-let _or_and b l =
-  try
-    let l = filter (fun f acc ->
-        List.fold_left (fun acc e -> f acc (e,b)) acc l) in
-    match l with
-    | [] -> if b then node_true else node_false
-    | [a,b'] -> assert (Equal.bool b b'); a
-    | l ->
-      index sem {topnot = b; lits = IArray.of_list l}
-  with Exit -> if b then node_false else node_true
-
-let _or  = _or_and false
-let _and = _or_and true
-
-let mk_clause m =
-  if Node.M.is_empty m then node_false
-  else let len = Node.M.cardinal m in
-    if len = 1 then
-      let node,b = Node.M.choose m in
-      if b then _not node else node
-    else
-      index sem {topnot=false;
-                     lits = IArray.of_iter len
-                         (fun iter -> Node.M.iter (fun node b -> iter (node,b)) m)}
+    let rec check_if_set d args absorbent incr stop i =
+      match Egraph.Ro.get_value d (IArray.get args i) with
+      | None -> ToWatch i
+      | Some b when Value.equal b absorbent ->
+        Absorbent
+      | Some _ -> (* neutral *)
+        let i = incr + i in
+        if i = stop then LimitReached else
+          check_if_set d args absorbent incr stop i
 
-let _false = node_false
+    let rec check_if_equal_or_set d args absorbent incr stop i n =
+      match check_if_set d args absorbent incr stop i with
+      | LimitReached | Absorbent as r -> r
+      | ToWatch i as r ->
+        if not (Egraph.Ro.is_equal d n (IArray.get args i)) then r
+        else
+        let i = incr + i in
+        if i = stop then LimitReached else
+          check_if_equal_or_set d args absorbent incr stop i n
 
-let set_true env node = set_bool env node true
-let set_false env node = set_bool env node false
+    let attach d r i =
+      Egraph.Ro.attach_value d
+        (IArray.get (Ground.sem r.ground).args i) BoolValue.key key r;
+      Egraph.Ro.attach_node d (IArray.get (Ground.sem r.ground).args i) key r
 
-(** {2 Choice on bool} *)
+    let run d r = r d; None
 
-module ChoBool = struct
-  let make_decision env node b =
-    Debug.dprintf3 Egraph.print_decision "[Bool] decide %b on %a" b Node.pp node;
-    set_bool env node b
+    let enqueue d r =
+      let o_from_start = Context.Ref.get r.from_start in
+      let o_from_end = Context.Ref.get r.from_end in
+      let args = (Ground.sem r.ground).args in
+      if o_from_start = o_from_end then Events.Wait.EnqStopped
+      else
+        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.Wait.EnqLast(fun d -> Egraph.merge d n_end (Ground.node r.ground))
+        | Absorbent ->
+          Events.Wait.EnqLast(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+        | ToWatch from_start ->
+          if from_start <> o_from_start then (
+            Context.Ref.set r.from_start from_start;
+            attach d r from_start;
+          );
+          let n_start = IArray.get args from_start in
+          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.Wait.EnqLast (fun d -> Egraph.merge d n_start (Ground.node r.ground))
+          | Absorbent ->
+            Events.Wait.EnqLast (fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+          | ToWatch from_end when from_end = o_from_end ->
+            Events.Wait.EnqAlready
+          | ToWatch from_end ->
+            Context.Ref.set r.from_end from_end;
+            attach d r from_end;
+            Events.Wait.EnqAlready
+
+    let enqueue d event =
+      match event with
+      | Events.Fired.EventValue (_, _, r)
+      | Events.Fired.EventChange  (_, r) ->
+        enqueue d r
+      | _ -> raise Impossible
+
+    let create d absorbent ground =
+      let args = (Ground.sem ground).args in
+      assert (IArray.not_empty args);
+      if IArray.length args = 1 then
+        Egraph.merge d (IArray.get args 0) (Ground.node ground)
+      else
+      let r from_start from_end =
+        assert (from_start < from_end);
+        Debug.dprintf4 debug "Bool create %a (%i-%i)" Ground.pp ground
+          from_start from_end;
+        {
+          ground; absorbent;
+          from_start = Context.Ref.create (Egraph.context d) from_start;
+          from_end = Context.Ref.create (Egraph.context d) from_end;
+        }
+      in
+      match check_if_set (d :> Egraph.Ro.t) args absorbent 1 (IArray.length args - 1) 0 with
+      | LimitReached ->
+        Egraph.merge d (IArray.get args (IArray.length args - 1)) (Ground.node ground)
+      | Absorbent ->
+        Egraph.set_value d (Ground.node ground) absorbent
+      | ToWatch from_start ->
+        let n_start = IArray.get args from_start in
+        match
+          check_if_equal_or_set (d :> Egraph.Ro.t) args absorbent (-1) from_start (IArray.length args - 1) n_start
+        with
+        | LimitReached ->
+          Egraph.merge d n_start (Ground.node ground)
+        | Absorbent ->
+          Egraph.set_value d (Ground.node ground) absorbent
+        | ToWatch from_end ->
+          let r = r from_start from_end in
+          attach (d :> Egraph.Ro.t) r from_start;
+          attach (d :> Egraph.Ro.t) r from_end
+  end
 
-  let choose_decision node env =
-    match is env node with
-    | Some _ ->
-      Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
-      Egraph.DecNo
-    | None -> DecTodo
-                (List.map (fun v env -> make_decision env node v)
-                   (Shuffle.shufflel [true;false]))
+  let () = Egraph.Wait.register_dem (module Daemon)
 
+  let create = Daemon.create
 end
 
-let chobool n = {
-  Egraph.prio = 1;
-  choice = ChoBool.choose_decision n;
-}
+let init_got_value_bool,wait_for_this_node_get_a_value =
+  Demon.Fast.register_get_value_daemon
+    ~name:"GotBoolValue.bool"
+    ~pp:Fmt.nop
+    (module BoolValue)
+    (fun d n v f -> f d n v)
 
 
 let converter d (f:Ground.t) =
   let res = Ground.node f in
-  let reg_args args = List.iter (Egraph.register d) args in
+  let reg_args args = IArray.iter ~f:(Egraph.register d) args in
   let reg n =
     Egraph.register d n;
     Egraph.merge d res n
@@ -433,16 +284,35 @@ let converter d (f:Ground.t) =
     when Ground.Ty.equal ty Ground.Ty.bool  ->
     Egraph.register_decision d (chobool res)
   | { app = {builtin = Expr.Or}; tyargs = []; args; _ } ->
-    reg_args args; reg (_or args)
+    reg_args args;
+    TwoWatchLiteral.create d values_true f
   | { app = {builtin = Expr.And}; tyargs = []; args; _ } ->
-    reg_args args; reg (_and args)
-  | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2] as args; _ } ->
-    reg_args args; reg (gen false [arg1,true;arg2,false])
-  | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg] as args; _ } ->
-    reg_args args; reg (_not arg)
-  | { app = {builtin = Expr.True}; tyargs = []; args = []; _ } ->
+    reg_args args;
+    TwoWatchLiteral.create d values_false f
+  | { app = {builtin = Expr.Imply}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
+    reg_args args;
+    let wait d n v =
+      if Node.equal n res then
+        if not v then (set_bool d a true; set_bool d b false);
+      if Node.equal n a then
+        (if v then (if is_true d res then set_bool d b true)
+         else set_bool d res true);
+      if Node.equal n b then
+        if v then set_bool d res true
+        else if is_true d res then set_bool d a false
+    in
+    List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;res]
+  | { app = {builtin = Expr.Neg}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
+    reg_args args;
+    wait_for_this_node_get_a_value d a (fun d _ v -> set_bool d res (not v));
+    wait_for_this_node_get_a_value d res (fun d _ v -> set_bool d a (not v))
+  | { app = {builtin = Expr.True}; tyargs = []; args; _ } ->
+    assert ( IArray.is_empty args);
     reg _true
-  | { app = {builtin = Expr.False}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.False}; tyargs = []; args; _ } ->
+    assert ( IArray.is_empty args);
     reg _false
   | _ -> ()
 
@@ -459,33 +329,34 @@ let init_check d =
         check r
       in
       match Ground.sem t with
-      | { app = {builtin = Expr.Or}; tyargs = []; args = args; ty = _ } ->
-        !< (List.fold_left (||) false (List.map (!>) args))
-      | { app = {builtin = Expr.And}; tyargs = []; args = args; ty = _ } ->
-        !< (List.fold_left (&&) true (List.map (!>) args))
-      | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !< ( not (!> arg1) || !> arg2 )
-      | { app = {builtin = Expr.Xor}; tyargs = []; args = [arg1;arg2]; _ } ->
-        !< ( not (Bool.equal (!> arg1) (!> arg2) ))
-      | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg]; ty = _ } ->
-        !< (not (!> arg))
-      | { app = {builtin = Expr.True}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Or}; tyargs = []; args; ty = _ } ->
+        !< (IArray.fold ~f:(||) ~init:false (IArray.map ~f:(!>) args))
+      | { app = {builtin = Expr.And}; tyargs = []; args; ty = _ } ->
+        !< (IArray.fold ~f:(&&) ~init:true (IArray.map ~f:(!>) args))
+      | { app = {builtin = Expr.Imply}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !< ( not (!> a) || !> b )
+      | { app = {builtin = Expr.Xor}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
+        !< ( not (Bool.equal (!> a) (!> b) ))
+      | { app = {builtin = Expr.Neg}; tyargs = []; args; ty = _ } ->
+        let a = IArray.extract1_exn args in
+        !< (not (!> a))
+      | { app = {builtin = Expr.True}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         check values_true
-      | { app = {builtin = Expr.False}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.False}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         check values_false
       | _ -> None
     )
 
 let th_register env =
-  RDaemonPropaNot.init env;
-  RDaemonPropa.init env;
-  RDaemonInit.init env;
-  Demon.Fast.attach env
-    DaemonInit.key [Demon.Create.EventRegSem(sem,())];
   Egraph.register env node_true;
   Egraph.register env node_false;
   Ground.register_converter env converter;
   init_check env;
+  init_got_value_bool env;
   ()
 
 let () = Egraph.add_default_theory th_register
@@ -516,5 +387,3 @@ let default_value = true
 
 
 
-
-type t = T.t
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index e605b717a5154b9024ad85aecb1785bc8aeabef0..c170d909a91cbf1b4d9e1c134194952667f24cca 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -18,8 +18,6 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-type t
-val sem: t ThTermKind.t
 val dom: bool ValueKind.t
 
 val _true : Node.t
@@ -27,10 +25,6 @@ val _false : Node.t
 val _and  : Node.t list -> Node.t
 val _or   : Node.t list -> Node.t
 val _not  : Node.t -> Node.t
-val gen   : bool -> (Node.t * bool) list -> Node.t
-(** [gen d b0 [cl1,b1;cl2,c2]] is
-    not_b0 (or (not_b1 cl1,not_b2 cl2)) with not_x f = if x then not f else f
-*)
 
 val set_true  : Egraph.t -> Node.t -> unit
 val set_false : Egraph.t -> Node.t -> unit
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 29bef0af8486fe492dc1207670cffa304078b935..b0234ea78d25d869cbfbb0ee016579919fe5ff4e 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -578,21 +578,23 @@ let init_check d =
         check r
       in
       match Ground.sem t with
-      | { app = {builtin = Expr.Equal}; tyargs = [_]; args = a::l; ty = _ } ->
-        let a = interp a in
-        !< (List.for_all (fun t -> Value.equal a (interp t)) l)
-      | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Equal}; tyargs = [_]; args; ty = _ } ->
+        assert (IArray.not_empty args);
+        !< (IArray.for_alli_non_empty_exn ~init:interp ~f:(fun _ a t -> Value.equal a (interp t)) args)
+      | { app = {builtin = Expr.Equiv}; tyargs = [_]; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Value.equal (interp a) (interp b))
-      | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; ty = _ } ->
+      | { app = {builtin = Expr.Distinct}; tyargs = [_]; args; ty = _ } ->
         begin
           try
             let fold acc v = Value.S.add_new Exit (interp v) acc in
-            let _ = List.fold_left fold Value.S.empty args in
+            let _ = IArray.fold ~f:fold ~init:Value.S.empty args in
             check Boolean.values_true
           with Exit ->
             check Boolean.values_false
         end
-      | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Ite}; tyargs = [_]; args; ty = _ } ->
+        let c,a,b = IArray.extract3_exn args in
         check (if (!> c) then interp a else interp b)
       | _ -> None
     )
@@ -610,14 +612,17 @@ let converter d (t:Ground.t) =
   in
   match Ground.sem t with
   | { app = {builtin = Expr.Equal}; tyargs = [_]; args = l; _ } ->
-    reg (equality (List.map of_term l))
-  | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; _ } ->
+    reg (equality (List.map of_term (IArray.to_list l)))
+  | { app = {builtin = Expr.Equiv}; tyargs = [_]; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg (equality [of_term a;of_term b])
-  | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; _ } ->
-    reg (disequality (List.map of_term args))
-  | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; _ } ->
+  | { app = {builtin = Expr.Distinct}; tyargs = [_]; args; _ } ->
+    reg (disequality (List.map of_term (IArray.to_list args)))
+  | { app = {builtin = Expr.Ite}; tyargs = [_]; args; _ } ->
+    let c,a,b = IArray.extract3_exn args in
     reg (ite (of_term c) (of_term a) (of_term b))
-  | { app = {builtin = Expr.Xor}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Xor}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg (disequality ([of_term a;of_term b]))
   | _ -> ()
 
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index daa271b5373d057cc9502f1814e53612d3909c75..61c29b4c0cfbb75fe92fc644734344cb0134c3db 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -13,7 +13,7 @@ type t' = {
   triggers : Trigger.t list;
   ups :
     (Expr.Ty.t list
-    * Pattern.t list
+    * Pattern.t IArray.t
     * int (* from which argument we come *)
     * t)
     list
@@ -56,8 +56,7 @@ let rec exec d acc substs n ip =
           if Ground.Subst.S.is_empty substs then substs
           else
             let i = ref (-1) in
-            Base.List.fold2_exn args pargs ~init:substs
-              ~f:(fun substs args parg ->
+            IArray.fold2_exn args pargs ~init:substs ~f:(fun substs args parg ->
                 incr i;
                 if Int.equal !i pos then substs
                 else Pattern.match_term d substs args parg)
@@ -155,13 +154,13 @@ let insert_pattern d (trigger : Trigger.t) =
         let ips = [ ip ] in
         ips
   and insert_children pp_vars f tytl tl =
-    List.foldi
-      (fun acc pos p ->
+    IArray.foldi
+      ~f:(fun pos acc p ->
         let f_pos = F_Pos.{ f; pos } in
         let ips = aux f_pos pp_vars p in
         let ips = List.map (add_up f_pos tytl tl) ips in
         ips @ acc)
-      [] tl
+      ~init:[] tl
   in
   let pp_vars = Pattern.get_pps trigger.pat in
   match trigger.pat with
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index 2f566d44bbb701123bbea8b52a32efcb55bb912d..df42bb012d5d6047d81ffcea5544d31acc4146d4 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -1,3 +1,4 @@
+open Colibri2_popop_lib
 (** information added on nodes *)
 
 type t = {
@@ -22,7 +23,10 @@ let congruence_closure d ~other parent0 ~repr parent1 =
       let h = Ground.Term.H.create 10 in
       let norm g =
         let g = Ground.sem g in
-        { g with Ground.Term.args = List.map find_as_if g.Ground.Term.args }
+        {
+          g with
+          Ground.Term.args = IArray.map ~f:find_as_if g.Ground.Term.args;
+        }
       in
       let s = ref (Ground.S.union g1 g2) in
       let not_first g = s := Ground.S.remove g !s in
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 79dc1057cc60618e1099562390f700648ccf1ec9..26af230dfaba9d4a79cc8cd93e8a02dc4a1e9bda 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -8,7 +8,7 @@ module T = struct
 
   type t =
     | Var of Expr.Term.Var.t
-    | App of F.t * Expr.Ty.t list * t list
+    | App of F.t * Expr.Ty.t list * t IArray.t
     | Node of Node.t
   [@@deriving eq, ord, hash]
 
@@ -18,7 +18,7 @@ module T = struct
         Fmt.pf fmt "%a[%a](%a)" F.pp f
           Fmt.(list ~sep:comma Expr.Ty.pp)
           tyl
-          Fmt.(list ~sep:comma pp)
+          Fmt.(IArray.pp ~sep:comma pp)
           tl
     | Node n -> Node.pp fmt n
 end
@@ -35,7 +35,7 @@ let rec of_term ~subst (t : Expr.Term.t) =
   | App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term ~subst a
   | App (f, tys, tl) ->
       (* todo type substitution *)
-      App (f, tys, List.map (of_term ~subst) tl)
+      App (f, tys, IArray.of_list_map ~f:(of_term ~subst) tl)
   | _ -> (* absurd *) assert false
 
 let init = Ground.Subst.S.singleton Ground.Subst.empty
@@ -61,13 +61,13 @@ let rec match_ty substs (ty : Ground.Ty.t) (p : Expr.Ty.t) : Ground.Subst.S.t =
 
 let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
     Ground.Subst.S.t =
-  Debug.dprintf4 debug "[Quant] matching %a %a" pp p Node.pp n;
+  Debug.dprintf4 debug_full "[Quant] matching %a %a" pp p Node.pp n;
   if Ground.Subst.S.is_empty substs then substs
   else
     match p with
     | Var v ->
         let match_ty (acc : Ground.Subst.S.t) ty : Ground.Subst.S.t =
-          Debug.dprintf4 debug "[Quant] match_ty %a %a" Expr.Ty.pp v.ty
+          Debug.dprintf4 debug_full "[Quant] match_ty %a %a" Expr.Ty.pp v.ty
             Ground.Ty.pp ty;
           Ground.Subst.S.union (match_ty substs ty v.ty) acc
         in
@@ -101,7 +101,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
             if Ground.Subst.S.is_empty substs then acc
             else
               let substs =
-                Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
+                IArray.fold2_exn args pargs ~init:substs ~f:(match_term d)
               in
               Ground.Subst.S.union substs acc)
           Ground.Subst.S.empty s
@@ -139,7 +139,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
           let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
           assert (Term.Const.equal f pf);
           List.for_all2 (check_ty subst) tyl ptyl
-          && List.for_all2 (check_term d subst) args pargs)
+          && IArray.for_all2_exn ~f:(check_term d subst) args pargs)
         s
   | Node n' -> Egraph.is_equal d n n'
 
@@ -158,14 +158,16 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
               (Ground.tys d n)
           then Node.S.singleton (Egraph.find_def d n)
           else raise Not_found)
-  | App (pf, ptyl, []) ->
+  | App (pf, ptyl, pargs) when IArray.is_empty pargs ->
       let g =
-        Ground.apply pf (List.map (Ground.Ty.convert subst.ty) ptyl) []
+        Ground.apply pf
+          (List.map (Ground.Ty.convert subst.ty) ptyl)
+          IArray.empty
         |> Ground.index |> Ground.node
       in
       if Egraph.is_registered d g then Node.S.singleton (Egraph.find d g)
       else raise Not_found
-  | App (pf, ptyl, parg :: pargs) ->
+  | App (pf, ptyl, pargs) ->
       let find_app pos n =
         Opt.get_def Ground.S.empty
         @@
@@ -189,9 +191,9 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
         nodes
       in
       let nodes =
-        Lists.fold_lefti
-          (fun acc i parg -> Node.S.inter acc (get_parents (i + 1) parg))
-          (get_parents 0 parg) pargs
+        IArray.foldi_non_empty_exn
+          ~f:(fun i acc parg -> Node.S.inter acc (get_parents (i + 1) parg))
+          ~init:(get_parents 0) pargs
       in
       if Node.S.is_empty nodes then raise Not_found else nodes
   | Node n -> Node.S.singleton n
@@ -204,16 +206,18 @@ let get_pps pattern =
     match p with
     | Var v -> Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
     | App (f, _, tl) ->
-        List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
+        IArray.foldi
+          ~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
+          ~init:acc tl
     | Node _ -> acc
   in
   let m =
     match pattern with
     | Var _ | Node _ -> Expr.Term.Var.M.empty
     | App (f, _, tl) ->
-        List.foldi
-          (fun acc pos p -> aux acc F_Pos.{ f; pos } p)
-          Expr.Term.Var.M.empty tl
+        IArray.foldi
+          ~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
+          ~init:Expr.Term.Var.M.empty tl
   in
   Expr.Term.Var.M.map
     (fun s ->
@@ -261,7 +265,7 @@ let match_any_term d (p : t) : Ground.Subst.S.t =
           assert (Term.Const.equal f pf);
           let substs = List.fold_left2 match_ty init tyl ptyl in
           let substs =
-            Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
+            IArray.fold2_exn args pargs ~init:substs ~f:(match_term d)
           in
           Ground.Subst.S.union substs acc)
         Ground.Subst.S.empty
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index c8e528bfb03dc584542b9c4b59f1c95bc6f16049..a545681a16217f9c9076b5f07d626883ae2fce6c 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -1,8 +1,9 @@
+open Colibri2_popop_lib
 (** Pattern *)
 
 type t =
   | Var of Expr.Term.Var.t
-  | App of F.t * Expr.Ty.t list * t list
+  | App of F.t * Expr.Ty.t list * t IArray.t
   | Node of Node.t
 
 include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 15da41554e9a460f278dd02bcbc56a621fc2b22e..aab7a0b9df825935ef1d1926fd23270aefe8a0cc 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -215,7 +215,10 @@ let init, attach =
           List.iter (add_trigger d) triggers
       (* Todo match with current terms *))
 
-let quantifier_registered d th = attach d (Ground.ThClosedQuantifier.node th) th
+let quantifier_registered d th =
+  let n = Ground.ThClosedQuantifier.node th in
+  if Boolean.is_unknown d n then Egraph.register_decision d (Boolean.chobool n);
+  attach d n th
 
 (** Verify that this term is congruent closure to another already existing term
    So it is useless. f(a) is useless if a == b and f(a) == f(b) and f(b) is
@@ -224,27 +227,26 @@ let quantifier_registered d th = attach d (Ground.ThClosedQuantifier.node th) th
 let application_useless d thg =
   let g = Ground.sem thg in
   let n = Ground.node thg in
-  match g.args with
-  | [] -> false (* No argument no congruence closure *)
-  | _ ->
-      let find_app pos n =
-        Opt.get_def Ground.S.empty
-        @@
-        let open Option in
-        let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
-        F_Pos.M.find_opt { f = g.app; pos } info.parents
-      in
-      let check_arg pos arg =
-        Ground.S.exists
-          (fun arg ->
-            Egraph.is_equal d n (Ground.node arg)
-            && List.for_all2 Ground.Ty.equal (Ground.sem arg).tyargs g.tyargs)
-          (find_app pos arg)
-      in
-      Base.List.for_alli ~f:check_arg g.args
+  if IArray.is_empty g.args then false (* No argument no congruence closure *)
+  else
+    let find_app pos n =
+      Opt.get_def Ground.S.empty
+      @@
+      let open Option in
+      let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
+      F_Pos.M.find_opt { f = g.app; pos } info.parents
+    in
+    let check_arg pos arg =
+      Ground.S.exists
+        (fun arg ->
+          Egraph.is_equal d n (Ground.node arg)
+          && List.for_all2 Ground.Ty.equal (Ground.sem arg).tyargs g.tyargs)
+        (find_app pos arg)
+    in
+    IArray.for_alli ~f:check_arg g.args
 
 let add_info_on_ground_terms d thg =
-  Debug.dprintf2 debug "[Quant] add_info_on_ground_terms %a" Ground.pp thg;
+  Debug.dprintf2 debug_full "[Quant] add_info_on_ground_terms %a" Ground.pp thg;
   let res = Ground.node thg in
   let g = Ground.sem thg in
   let merge_info other info =
@@ -265,7 +267,7 @@ let add_info_on_ground_terms d thg =
         parents = F_Pos.M.singleton { f = g.app; pos } (Ground.S.singleton thg);
       }
   in
-  List.iteri add_pc g.args;
+  IArray.iteri ~f:add_pc g.args;
   merge_info res
     { Info.empty with apps = F.M.singleton g.app (Ground.S.singleton thg) };
   Context.Queue.push (F.EnvApps.find Pattern.env_ground_by_apps d g.app) thg;
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index c2b9728ecdcc49691e121d162ac3867ec212a817..4232d43c936ae90e49541f2ac7e3f3a17de3d72b 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -34,7 +34,7 @@ let compute_top_triggers (cq : Ground.ThClosedQuantifier.t) =
         ( {
             builtin =
               ( Expr.And | Expr.Equal | Expr.Equiv | Expr.Or | Expr.Xor
-              | Expr.Imply );
+              | Expr.Imply | Expr.Ite );
             _;
           },
           _,
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index 81c29343f3b6fdc636ec7a3b614c4d91fe3c5979..a20932dd6e3327da0d9cb355d099fcdb57f4c42b 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -278,11 +278,9 @@ module UFModel = struct
   module Values = struct
     (** instantiated function symbol *)
     module T = struct
-      let hash_fold_list = Base.hash_fold_list
-
-      type t = Value.t list [@@deriving eq, ord, hash]
+      type t = Value.t IArray.t [@@deriving eq, ord, hash]
 
-      let pp fmt l = Fmt.(list ~sep:comma Value.pp) fmt l
+      let pp fmt l = Fmt.(IArray.pp ~sep:comma Value.pp) fmt l
     end
 
     include T
@@ -310,7 +308,7 @@ module UFModel = struct
     let check_or_update g d _ =
       let interp n = Option.get_exn (Egraph.get_value d n) in
       let s = Ground.sem g in
-      let lv = List.map interp s.args in
+      let lv = IArray.map ~f:interp s.args in
       let v = interp (Ground.node g) in
       match find d s lv with
       | Some v' -> if not (Value.equal v v') then Egraph.contradiction d
@@ -320,7 +318,7 @@ module UFModel = struct
     f d g
 
   let init_attach_value d g =
-    Interp.TwoWatchLiteral.create d on_uninterpreted_domain g
+    Interp.WatchArgs.create d on_uninterpreted_domain g
 end
 
 module On_uninterpreted_domain = struct
@@ -331,7 +329,7 @@ module On_uninterpreted_domain = struct
   let check d t =
     let interp n = Option.get_exn (Egraph.get_value d n) in
     let s = Ground.sem t in
-    let lv = List.map interp s.args in
+    let lv = IArray.map ~f:interp s.args in
     let v = interp (Ground.node t) in
     match UFModel.find d s lv with Some v' -> Value.equal v v' | None -> false
 end
@@ -346,7 +344,7 @@ let init_check d =
 let converter d (t : Ground.t) =
   match Ground.sem t with
   | { app = { builtin = Dolmen_std.Expr.Base; _ }; args; _ } ->
-      List.iter (Egraph.register d) args;
+      IArray.iter ~f:(Egraph.register d) args;
       UFModel.init_attach_value d t
   | _ -> ()