diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index c40edf14e44ecc3a0dfb83e8b109cb474c33847d..b8d60a3d62c64244346105e39aaf9be048dcd757 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -573,6 +573,37 @@ module Fast = struct
     RDaemonInit.init init_d;
     attach init_d DaemonInit.key [Create.EventChangeAny(())]
 
+  let register_change_domain_daemon
+    (type a) (type b)
+    ~name
+    ?(immediate=false)
+    ?(throttle=100)
+    ?(pp=Fmt.nop)
+    (dom:a DomKind.t)
+    (f:Egraph.t -> Node.t -> b -> unit)
+    =
+    let module DaemonInit = struct
+      let key = create name
+      module Data = struct
+        type t = b
+        let pp = pp
+      end
+      let immediate = immediate
+      let throttle = throttle
+      let wakeup d = function
+        | Events.Fired.EventDom(node,dom',data) ->
+          assert (DomKind.equal dom dom');
+          f d node data
+        | _ -> raise UnwaitedEvent
+    end in
+    let module RDaemonInit = Register(DaemonInit) in
+    let attach d n data =
+      attach d DaemonInit.key [Create.EventDom(n,dom,data)];
+      match Egraph.get_dom d dom n with
+      | None -> ()
+      | Some _ -> f d n data
+    in
+    RDaemonInit.init, attach
 
   let register_get_value_daemon
     (type a) (type b)
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index 33d853379c1d435749d6c6cbfa5709d020899b0c..f9d763328429925da8fa1c63e2052ebd0f15fde3 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -159,6 +159,17 @@ module Fast: sig
     unit
     (** *)
 
+  (** helper *)
+  val register_change_domain_daemon:
+    name:string ->
+    ?immediate:bool ->
+    ?throttle:int ->
+    ?pp:('b Fmt.t) ->
+    'a DomKind.t ->
+    (Egraph.t -> Node.t -> 'b -> unit) ->
+    (Egraph.t -> unit) * (Egraph.t -> Node.t -> 'b -> unit)
+    (** *)
+
   (** helper *)
   val register_get_value_daemon:
     name:string ->
diff --git a/src_colibri2/popop_lib/popop_stdlib.ml b/src_colibri2/popop_lib/popop_stdlib.ml
index e1c27c3a2f1707d1edb7942a223df63f0f90ee47..78fc690efe31a1a10df85ed6b71be9548431d9be 100644
--- a/src_colibri2/popop_lib/popop_stdlib.ml
+++ b/src_colibri2/popop_lib/popop_stdlib.ml
@@ -44,7 +44,7 @@ module OrderedHashed (X : TaggedType) =
 struct
   type t = X.t
   let hash = X.tag
-  let equal ts1 ts2 = X.tag ts1 == X.tag ts2 (** Todo ts1 == ts2? *)
+  let [@ocaml.always inline] equal ts1 ts2 = X.tag ts1 == X.tag ts2 (** Todo ts1 == ts2? *)
   let compare ts1 ts2 = Stdlib.compare (X.tag ts1) (X.tag ts2)
   let pp = X.pp
   let hash_fold_t s x = Base.Hash.fold_int s (X.tag x)
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 075dc5144a633b42a38326751dd0a4ba34656ec1..2929d544f4c5807502a95d3bf877382514921d48 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -48,7 +48,7 @@ let solve0a _ =
       register env a1; register env _1;
       merge env a1 _1
   in
-  assert_bool "a+1 = 1 => a = 0" (is_equal env a LRA.zero)
+  assert_bool "a+1 = 1 => a = 0" (is_equal env a LRA.RealValue.zero)
 
 (* let solve0b _ =
  *   let a  = fresh Term._Real "ar" in
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 9a070bd559af4b39294da13fe1edc2b8575fc684..b49b885ce1892365eb1ab5328482be5f0a4e9046 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -18,321 +18,11 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-open Colibri2_popop_lib
 open Colibri2_core
 open Colibri2_stdlib.Std
 
-let debug = Debug.register_info_flag
-  ~desc:"for the arithmetic theory"
-  "LRA"
-
-type bound = Colibrics_lib.Interval.Bound.t = Strict | Large
-  [@@deriving eq,ord,show,hash]
-module S = struct
-  module T = struct
-    type t =
-      | Add of Q.t * Node.t * Q.t * Node.t
-      | GZero of Node.t * bound
-      [@@ deriving eq,ord,hash]
-
-    let pp fmt = function
-      | Add (q1,cl1,q2,cl2) ->
-        let pp fmt (q,node) =
-          if Q.equal q Q.one then Node.pp fmt node else
-          if Q.equal q Q.minus_one
-          then Format.fprintf fmt "-%a" Node.pp node
-          else Format.fprintf fmt "%a%a" Q.pp q Node.pp node
-        in
-        if Q.equal q2 Q.minus_one
-        then Format.fprintf fmt "%a - %a" pp (q1,cl1) Node.pp cl2
-        else Format.fprintf fmt "%a + %a" pp (q1,cl1) pp (q2,cl2)
-      | GZero (node,b) ->
-        Format.fprintf fmt "0 %a %a" Interval.Bound.pp b Node.pp node
-
-  end
-  include T
-  include Popop_stdlib.MkDatatype(T)
-  let key = ThTermKind.create_key (module struct type nonrec t = t let name = "SARITH" end)
-end
-
-module SE = ThTermKind.Register(S)
-
-(** Polynome *)
-let propa_dem = Demon.Key.create "Arith.DaemonPropa"
-
-let print_bag_cl = Colibri2_popop_lib.Bag.pp Pp.comma Node.pp
-
-let minus_or_one inv =
-  if inv then Q.minus_one else Q.one
-
-let print_bag_node = Bag.pp Format.(const char ',') Node.pp
-
-module DaemonPropa = struct
-  let key = Demon.Fast.create "LRA.DaemonPropa"
-
-  module Data = SE
-
-  let immediate = false
-  let throttle = 100
-
-  let gt_zero = Dom_interval.D.gt Q.zero
-  let ge_zero = Dom_interval.D.ge Q.zero
-  let lt_zero = Dom_interval.D.lt Q.zero
-  let le_zero = Dom_interval.D.le Q.zero
-
-  let get_dom del node =
-    Opt.get_def Dom_interval.D.reals (Egraph.get_dom del Dom_interval.dom node)
-  let get_value del node =
-      match Egraph.get_value del RealValue.key node with
-        | None -> Dom_interval.D.reals
-        | Some d -> Dom_interval.D.singleton d
-
-  let upd del node d d' =
-    match Dom_interval.D.inter d d' with
-    | None ->
-      Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
-        Node.pp node Dom_interval.D.pp d Dom_interval.D.pp d';
-      Egraph.contradiction del
-    | Some d' ->
-      if not (Dom_interval.D.equal d d')
-      then Dom_interval.set_dom del node d'
-
-  let upd_value del node d d' =
-    match Dom_interval.D.inter d d' with
-    | None ->
-      Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
-        Node.pp node Dom_interval.D.pp d Dom_interval.D.pp d';
-      Egraph.contradiction del
-    | Some d' ->
-      if not (Dom_interval.D.equal d d')
-      then Dom_interval.set_dom del node d'
-
-  let propagate del s =
-    match SE.sem s with
-    | S.Add(q1,cl1,q2,cl2) ->
-      let cl0 = SE.node s in
-      let d0 = get_value del cl0 in
-      if Q.equal q1 Q.one && Q.equal q2 Q.minus_one &&
-         Dom_interval.D.equal d0 Dom_interval.D.zero then
-        Egraph.merge del cl1 cl2
-      else
-        let d1 = get_value del cl1 in
-        let d2 = get_value del cl2 in
-        let upd_value node d d' = upd_value del node d d' in
-        let qd1 = Dom_interval.D.mult_cst q1 d1 in
-        let qd2 = Dom_interval.D.mult_cst q2 d2 in
-        upd_value cl0 d0 (Dom_interval.D.add qd1 qd2);
-        upd_value cl1 d1 (Dom_interval.D.mult_cst (Q.inv q1) (Dom_interval.D.minus d0 qd2));
-        upd_value cl2 d2 (Dom_interval.D.mult_cst (Q.inv q2) (Dom_interval.D.minus d0 qd1))
-    | S.GZero(node,b) -> begin
-        let cl0 = SE.node s in
-        let d = get_value del node in
-        let dzero_true  = if equal_bound b Strict then gt_zero else ge_zero in
-        let dzero_false = if equal_bound b Strict then le_zero else lt_zero in
-        if Dom_interval.D.is_included d dzero_true
-        then begin
-          Boolean.set_true del cl0
-        end
-        else if Dom_interval.D.is_included d dzero_false
-        then
-          Boolean.set_false del cl0
-      end
-
-  let wakeup del = function
-    | Events.Fired.EventValue(_,_,_,s)
-    | Events.Fired.EventDom(_,_,s) ->
-      propagate del s
-    | Events.Fired.EventChange(_,s) ->
-      propagate del s
-    | _ -> raise UnwaitedEvent
-
-  let init d s =
-    begin match SE.sem s with
-      | S.Add (c1,cl1,c2,cl2) ->
-        Egraph.register d cl1; Egraph.register d cl2;
-        Demon.Fast.attach d key
-          [Demon.Create.EventValue(SE.node s, RealValue.key, s);
-           Demon.Create.EventValue(cl1, RealValue.key, s);
-           Demon.Create.EventValue(cl2, RealValue.key, s);
-          ];
-        let cl = (SE.node s) in
-        let add acc c cl =
-          let cl = Egraph.find d cl in
-          match Egraph.get_dom d Dom_polynome.dom_poly cl with
-          | None -> Polynome.add acc (Polynome.monome c cl)
-          | Some p -> Polynome.x_p_cy acc c p
-        in
-        let p1 = add (add Polynome.zero c1 cl1) c2 cl2 in
-        Dom_polynome.solve_one d cl p1
-      | GZero (node,_) ->
-        Egraph.register d node;
-        Demon.Fast.attach d key
-          [Demon.Create.EventValue(SE.node s, Boolean.dom, s);
-           Demon.Create.EventValue(node, RealValue.key, s)]
-    end;
-    propagate d s;
-end
-
-module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
-
-let zero = RealValue.cst Q.zero
-let one = RealValue.cst Q.one
-let index s = SE.index s
-
-let add' q1 cl1 q2 cl2 =
-  let norm q node = if Q.equal q Q.zero then Q.one, zero else q, node in
-  let q1, cl1 = norm q1 cl1 in
-  let q2, cl2 = norm q2 cl2 in
-  if Q.leq q2 q1 then
-    index (S.Add(q1,cl1,q2,cl2))
-  else
-    index (S.Add(q2,cl2,q1,cl1))
-
-let of_poly p =
-  let m, c = Polynome.get_tree p in
-  let rec aux = function
-    | Polynome.Empty -> `None
-    | Node(left,node,q,right,_) ->
-      let left = aux left in
-      let right = aux right in
-      let r =
-        match left, right with
-        | `Some (lq,l), `Some (rq,r) ->
-          `Some(Q.one,SE.node (add' lq l rq r))
-        | `None, r | r, `None -> r
-      in
-      match r with
-      | `None -> `Some(q,node)
-      | `Some(rq,r) -> `Some(Q.one,SE.node (add' q node rq r))
-  in
-  match aux m with
-  | `None -> RealValue.cst c
-  | `Some(rq,r) when Q.equal rq Q.one && Q.equal c Q.zero -> r
-  | `Some(rq,r) -> SE.node (add' rq r c one)
-
-let to_poly = function
-  | S.Add(q1,cl1,q2,cl2) -> Polynome.of_list Q.one [cl1,q1;cl2,q2]
-  | GZero _ -> raise Impossible
-
-(** API *)
-
-let index x = SE.node (SE.index x)
-
-let as_node node = index (S.Add (Q.one,node,Q.one,zero))
-
-let add' q1 cl1 q2 cl2 =
-  SE.node (add' q1 cl1 q2 cl2)
-
-let add cl1 cl2 =
-  add' Q.one cl1 Q.one cl2
-
-let sub cl1 cl2 =
-  index (S.Add(Q.one,cl1,Q.minus_one,cl2))
-
-let neg cl2 =
-  index (S.Add(Q.one,zero,Q.minus_one,cl2))
-
-let mult _node1 _node2 = raise (TODO "mult without constant")
-
-let mult_cst cst node =
-  add' cst node Q.one zero
-
-let gt_zero node =
-  SE.node (SE.index (GZero(node,Strict)))
-
-let ge_zero node =
-  SE.node (SE.index (GZero(node,Large)))
-
-let lt cl1 cl2 = gt_zero (sub cl2 cl1)
-let le cl1 cl2 = ge_zero (sub cl2 cl1)
-let gt cl1 cl2 = lt cl2 cl1
-let ge cl1 cl2 = le cl2 cl1
-
-(** {2 Initialization} *)
-let converter d (f:Ground.t) =
-    let res = Ground.node f in
-  let of_term n = Egraph.register d n; n in
-  let reg n =
-    Egraph.register d n;
-    Egraph.merge d res n
-  in
-  match Ground.sem f with
-  | { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty }
-    when Ground.Ty.equal ty Ground.Ty.real  ->
-    Egraph.register_decision d (Dom_interval.ChoLRA.choice res)
-  | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } ->
-    reg (RealValue.cst (Q.of_string s))
-  | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } ->
-    reg (RealValue.cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } ->
-    reg (RealValue.cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
-    reg (add (of_term a) (of_term b))
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
-    reg (sub (of_term a) (of_term b))
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
-    reg (neg (of_term a))
-  | { app = {builtin = Expr.Lt}; tyargs = []; args = [arg1;arg2]; _ } ->
-    reg (lt (of_term arg1) (of_term arg2))
-  | { app = {builtin = Expr.Leq}; tyargs = []; args = [arg1;arg2]; _ } ->
-    reg (le (of_term arg1) (of_term arg2))
-  | { app = {builtin = Expr.Gt}; tyargs = []; args = [arg1;arg2]; _ } ->
-    reg (gt (of_term arg1) (of_term arg2))
-  | { app = {builtin = Expr.Geq}; tyargs = []; args = [arg1;arg2]; _ } ->
-    reg (ge (of_term arg1) (of_term arg2))
-  | _ -> ()
-
-let th_register env =
-  RDaemonPropa.init env;
-  Demon.Fast.register_init_daemon
-    ~immediate:true
-    ~name:"LRA.DaemonInit"
-    (module SE)
-    DaemonPropa.init
-    env;
-  Ground.register_converter env converter;
-  Demon.Fast.register_init_daemon_value
-    ~name:"RealValueToDom"
-    (module RealValue)
-    (fun d value ->
-       let v = RealValue.value value in
-       let s = Dom_interval.D.singleton v in
-       Egraph.set_dom d Dom_interval.dom (RealValue.node value) s;
-       let cl = RealValue.node value in
-       let p1 = Polynome.of_list v [] in
-       Dom_polynome.solve_one d cl p1
-    ) env;
-  ()
-
-let () = Egraph.add_default_theory th_register
-
-
-(** {2 Interpretations} *)
-let () =
-  let gzero bound n =
-    let v = (match bound with | Strict -> Q.lt | Large -> Q.le) Q.zero n in
-    (if v then Boolean.values_true else Boolean.values_false)
-  in
-  let interp ~interp (t:S.t) =
-    let get_v n = RealValue.value (RealValue.coerce_nodevalue (interp n)) in
-    match t with
-    | Add(q1,n1,q2,n2) ->
-      let v = Q.( q1 * (get_v n1) + q2 * (get_v n2)) in
-      RealValue.nodevalue (RealValue.index v)
-    | GZero(n,bound) ->
-      gzero bound (get_v n)
-  in
-  Interp.Register.thterm S.key interp
-
 let default_value = Q.zero
 
-(* let () =
- *   Interp.Register.model Term._Real (fun d n ->
- *       let v = Egraph.get_value d real n in
- *       let v = Colibri2_popop_lib.Opt.get_def default_value v in
- *       let v = RealValue.nodevalue (RealValue.index v Term._Real) in
- *       v) *)
-
 let () =
   Interp.Register.id (fun interp t ->
       let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp t)) in
@@ -364,5 +54,88 @@ let () =
   | _ -> None
     )
 
-
 module RealValue = RealValue
+
+let th_register env =
+  Dom_interval.init env;
+  Dom_polynome.init env;
+  RealValue.init env
+
+let () = Egraph.add_default_theory th_register
+
+
+(** Helpers to remove *)
+
+let a = Expr.Term.Var.mk "a" Expr.Ty.real
+let b = Expr.Term.Var.mk "b" Expr.Ty.real
+let ta = Expr.Term.of_var a
+let tb = Expr.Term.of_var b
+
+let c = Expr.Term.Var.mk "c" Expr.Ty.real
+let d = Expr.Term.Var.mk "d" Expr.Ty.real
+let tc = Expr.Term.of_var c
+let td = Expr.Term.of_var d
+
+let add =
+  let e = Expr.Term.Real.add ta tb in
+  fun na nb ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,nb] } in
+    Ground.convert ~subst e
+
+let add' =
+  let e = Expr.Term.Real.(add (mul tc ta) (mul td tb)) in
+  fun qa na qb nb ->
+    let qa = RealValue.cst qa in
+    let qb = RealValue.cst qb in
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,nb;c,qa;d,qb] } in
+    Ground.convert ~subst e
+
+let sub =
+  let e = Expr.Term.Real.sub ta tb in
+  fun na nb ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,nb] } in
+    Ground.convert ~subst e
+
+let mult_cst =
+  let e = Expr.Term.Real.(mul tc ta) in
+  fun qa na ->
+    let qa = RealValue.cst qa in
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;c,qa] } in
+    Ground.convert ~subst e
+
+let mult =
+  let e = Expr.Term.Real.(mul ta tb) in
+  fun na nb ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,nb] } in
+    Ground.convert ~subst e
+
+let gt_zero =
+  let e = Expr.Term.Real.(gt ta tb) in
+  fun na ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,RealValue.zero] } in
+    Ground.convert ~subst e
+
+let ge_zero =
+  let e = Expr.Term.Real.(ge ta tb) in
+  fun na ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,RealValue.zero] } in
+    Ground.convert ~subst e
+
+let cmp cmp =
+  let e = cmp ta tb in
+  fun na nb ->
+    let subst = { Ground.Subst.empty with
+                  term = Expr.Term.Var.M.of_list [a,na;b,nb] } in
+    Ground.convert ~subst e
+
+let lt = cmp Expr.Term.Real.lt
+let le = cmp Expr.Term.Real.le
+let gt = cmp Expr.Term.Real.gt
+let ge = cmp Expr.Term.Real.ge
diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli
index 268e693d7941e925b64f4c696478813a60a5204c..47b7125b426920ee532c6690eadc103da3b60555 100644
--- a/src_colibri2/theories/LRA/LRA.mli
+++ b/src_colibri2/theories/LRA/LRA.mli
@@ -18,6 +18,19 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
+module RealValue : sig
+  include ValueKind.Registered with type s = Q.t
+
+  val cst': Q.t -> t
+  val cst:  Q.t -> Node.t
+  val zero: Node.t
+
+end
+
+val th_register: Egraph.t -> unit
+
+(** helpers to remove *)
+
 val add' : Q.t -> Node.t -> Q.t -> Node.t -> Node.t
 val add : Node.t -> Node.t -> Node.t
 val sub : Node.t -> Node.t -> Node.t
@@ -27,20 +40,9 @@ val mult_cst : Q.t -> Node.t -> Node.t
 
 val mult : Node.t -> Node.t -> Node.t
 
-val th_register : Egraph.t -> unit
-val zero: Node.t
-
 val gt_zero: Node.t -> Node.t
 val ge_zero: Node.t -> Node.t
 val lt: Node.t -> Node.t -> Node.t
 val le: Node.t -> Node.t -> Node.t
 val gt: Node.t -> Node.t -> Node.t
 val ge: Node.t -> Node.t -> Node.t
-
-module RealValue : sig
-  include ValueKind.Registered with type s = Q.t
-
-  val cst': Q.t -> t
-  val cst:  Q.t -> Node.t
-
-end
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index dfa402a5030a302407b2b9286c4c8baa15a7c249..3f0cebfc81d78f4161e14c8b09f06f19260aafb4 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -91,3 +91,127 @@ module ChoLRA = struct
 end
 
 let choice = ChoLRA.choice
+
+module Monad : sig
+  type 'a monad = Egraph.t -> Node.t -> 'a
+  val get: Node.t -> D.t option monad
+  val set: Node.t -> D.t option monad -> unit monad
+  val getb: Node.t -> bool option monad
+  val setb: Node.t -> bool option option monad -> unit monad
+  val (let+): 'b option monad -> ('b -> 'c) -> 'c option monad
+  val (and+): 'b option monad -> 'c option monad -> ('b * 'c) option monad
+  val (&&): unit monad -> unit monad -> unit monad
+end = struct
+  type 'a monad = Egraph.t -> Node.t -> 'a
+  let [@ocaml.always inline] get_dom dom n' = fun d _ ->
+    Egraph.get_dom d dom n'
+  let [@ocaml.always inline] set_dom (type b) (dom:b DomKind.t) n' v' d n =
+    if Node.equal n n' then () else
+      Option.iter
+        (fun (v':b) -> Egraph.set_dom d dom n' v')
+        (v' d n)
+  let [@ocaml.always inline] set n' v' d n =
+    if Node.equal n n' then () else
+      Option.iter
+        (fun v' ->
+           match Egraph.get_dom d dom n' with
+           | None -> Egraph.set_dom d dom n' v'
+           | Some old ->
+             match D.inter old v' with
+             | None ->
+               Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
+                 Node.pp n' D.pp old D.pp v';
+               Egraph.contradiction d
+             | Some d' ->
+               if not (D.equal v' d')
+               then Egraph.set_dom d dom n' v')
+        (v' d n)
+  let [@ocaml.always inline] get a = get_dom dom a
+  let [@ocaml.always inline] get_value key n' = fun d _ ->
+    Egraph.get_value d key n'
+  let [@ocaml.always inline] set_value (type b)
+      (value:(module ValueKind.Registered with type s = b))
+      n' (v':b option option monad) : unit monad =
+    fun d n ->
+    if Node.equal n n' then () else
+      let module V = (val value) in
+      Option.iter
+        (Option.iter (fun v' -> Egraph.set_value d n' (V.nodevalue (V.index v'))))
+        (v' d n)
+  let getb a = get_value Boolean.dom a
+  let setb a = set_value (module Boolean.BoolValue) a
+  let [@ocaml.always inline] (let+) a (f:'b -> 'a) = fun d n -> Option.map f (a d n)
+  let [@ocaml.always inline] (and+) a b = fun d n -> match a d n, b d n with
+    | Some a, Some b -> Some (a,b) | _ -> None
+  let [@ocaml.always inline] (&&) a b = fun d n -> a d n; b d n
+
+end
+
+let init_got_value_bool,wait_for_this_node =
+  Demon.Fast.register_change_domain_daemon
+    ~name:"GotDomInterval"
+    ~pp:Fmt.nop
+    dom
+    (fun d n f -> f d n)
+
+(** {2 Initialization} *)
+let converter d (f:Ground.t) =
+  let r = Ground.node f in
+  let reg n = Egraph.register d n in
+  let open Monad in
+  let cmp cmp a b =
+    reg a; reg b;
+    let wait =
+      setb r (let+ va = get a and+ vb = get b in
+              cmp (D.is_comparable va vb))
+    in
+    List.iter (fun n -> wait_for_this_node d n wait) [a;b]
+  in
+  match Ground.sem f with
+  | { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty }
+    when Ground.Ty.equal ty Ground.Ty.real  ->
+    Egraph.register_decision d (ChoLRA.choice r)
+  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+    reg a; reg b;
+    let wait =
+      set r (let+ va = get a and+ vb = get b in D.add va vb) &&
+      set a (let+ vb = get b and+ vr = get r in D.minus vr vb) &&
+      set b (let+ va = get a and+ vr = get r in D.minus vr va)
+    in
+    List.iter (fun n -> wait_for_this_node d n wait) [a;b;r]
+  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+    reg a; reg b;
+    let wait =
+      set r (let+ va = get a and+ vb = get b in D.minus va vb) &&
+      set a (let+ vb = get b and+ vr = get r in D.add vr vb) &&
+      set b (let+ va = get a and+ vr = get r in D.minus va vr)
+    in
+    List.iter (fun n -> wait_for_this_node d n wait) [a;b;r]
+  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+    reg a;
+    let wait =
+      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_this_node d n wait) [a;r]
+  | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+    cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false)  a b
+  | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+    cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some true | Gt -> Some false) a b
+  | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+    cmp (function | Uncomparable | Le -> None | Lt -> Some false  | Ge | Gt -> Some true) a b
+  | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+    cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some false  | Gt -> Some true) a b
+  | _ -> ()
+
+let init env =
+  Demon.Fast.register_init_daemon_value
+    ~name:"RealValueToDomInterval"
+    (module RealValue)
+    (fun d value ->
+       let v = RealValue.value value in
+       let s = D.singleton v in
+       Egraph.set_dom d dom (RealValue.node value) s
+    ) env;
+  Ground.register_converter env converter;
+  init_got_value_bool env
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d8be888cc36ed8675a495c4a6d0be604b343f714
--- /dev/null
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -0,0 +1 @@
+val init: Egraph.t -> unit
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 4083cfc661b3ec14c7799e83cf17c2c24512e3ad..60755baf760e7a5f1eaf1b280a3ccd7cc276de64 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -174,8 +174,34 @@ let assume_poly_equality d n p =
     | None -> Polynome.add acc (Polynome.monome c cl)
     | Some p -> Polynome.x_p_cy acc c p
   in
-  let p = Polynome.fold add Polynome.zero p in
+  let p = Polynome.fold add (Polynome.cst p.cst) p in
   Debug.dprintf4 debug "assume2: %a = %a" Node.pp n Polynome.pp p;
   Th.solve_one d n p
 
-let solve_one = Th.solve_one
+(** {2 Initialization} *)
+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]; _ } ->
+    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]; _ } ->
+    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]; _ } ->
+    reg a;
+    assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.minus_one])
+  | _ -> ()
+
+let init env =
+    Demon.Fast.register_init_daemon_value
+    ~name:"RealValueToDomPoly"
+    (module RealValue)
+    (fun d value ->
+       let v = RealValue.value value in
+       let cl = RealValue.node value in
+       let p1 = Polynome.of_list v [] in
+       assume_poly_equality d cl p1
+    ) env;
+    Ground.register_converter env converter
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index 9e4c64f2cc42a974bb7f99a215f620b1331ceb44..e5bc052a393f01770b872b6cae37a577607ecf72 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -22,4 +22,4 @@ val assume_poly_equality: Egraph.t -> Node.t -> Polynome.t -> unit
 
 val dom_poly: Polynome.t DomKind.t
 
-val solve_one: Egraph.t -> Node.t -> Polynome.t -> unit
+val init: Egraph.t -> unit
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 8d770278d458b1ddee263bd2bc9105bd81c400dc..3bc4f065b028be6fdd6108e5efd75f76f8e06b42 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -21,15 +21,121 @@
 open Colibri2_core
 open Colibri2_stdlib.Std
 
-let real = ValueKind.create_key (module struct type t = Q.t let name = "Q" end)
-
 module RealValue = ValueKind.Register(struct
     include Q
-    let key = real
+    let key = ValueKind.create_key (module struct type t = Q.t let name = "Q" end)
   end)
 
-let cst' c = RealValue.index ~basename:(Format.asprintf "%aR" Q.pp c) c
+include RealValue
 
-let cst c = RealValue.node (cst' c)
+let cst' c = index ~basename:(Format.asprintf "%aR" Q.pp c) c
 
-include RealValue
+let cst c = node (cst' c)
+
+let zero = cst Q.zero
+let one = cst Q.one
+
+let init_got_value,wait_for_this_node_get_a_value =
+  Demon.Fast.register_get_value_daemon
+    ~name:"GotRealValue"
+    ~pp:Fmt.nop
+    (module RealValue)
+    (fun d n v f -> f d n v)
+
+let init_got_value_bool,wait_for_this_node_get_a_value_bool =
+  Demon.Fast.register_get_value_daemon
+    ~name:"GotRealValue.bool"
+    ~pp:Fmt.nop
+    (module Boolean.BoolValue)
+    (fun d n v f -> f d n v)
+
+module Monad : sig
+  type ('a,'b) monad = Egraph.t -> Node.t -> 'a -> 'b
+  val get: Node.t -> (Q.t,Q.t option) monad
+  val set: Node.t -> ('a,Q.t option) monad -> ('a,unit) monad
+  val getb: Node.t -> (bool,bool option) monad
+  val setb: Node.t -> ('a,bool option) monad -> ('a,unit) monad
+  val (let+): ('a,'b option) monad -> ('b -> 'c) -> ('a,'c option) monad
+  val (and+): ('a,'b option) monad -> ('a,'c option) monad -> ('a,('b * 'c) option) monad
+  val (&&): ('a,unit) monad -> ('a,unit) monad -> ('a,unit) monad
+end = struct
+  type ('a,'b) monad = Egraph.t -> Node.t -> 'a -> 'b
+  let [@ocaml.always inline] get' key n' = fun d n v ->
+    if Node.equal n n' then Some v else Egraph.get_value d key n'
+  let [@ocaml.always inline] set' : type b.
+      (module ValueKind.Registered with type s = b) ->
+    Node.t -> ('a,b option) monad -> ('a, unit) monad =
+    fun value n' v' d n v ->
+    let module V = (val value) in
+    if Node.equal n n' then () else
+      Option.iter
+        (fun (v':b) -> Egraph.set_value d n' (V.nodevalue (V.index v')))
+        (v' d n v)
+  let [@ocaml.always inline] get a = get' key a
+  let [@ocaml.always inline] set a = set' (module RealValue) a
+  let getb a = get' Boolean.BoolValue.key a
+  let setb a = set' (module Boolean.BoolValue) a
+  let [@ocaml.always inline] (let+) a (f:'b -> 'a) = fun d n v -> Option.map f (a d n v)
+  let [@ocaml.always inline] (and+) a b = fun d n v -> match a d n v, b d n v with
+    | Some a, Some b -> Some (a,b) | _ -> None
+  let [@ocaml.always inline] (&&) a b = fun d n v -> a d n v; b d n v
+
+end
+
+(** {2 Initialization} *)
+let converter d (f:Ground.t) =
+  let r = Ground.node f in
+  let reg n = Egraph.register d n in
+  let merge n = Egraph.register d n; Egraph.merge d r n in
+  let open Monad in
+  let cmp cmp a b =
+        reg a; reg b;
+    let wait =
+      setb r (let+ va = get a and+ vb = get b in cmp va vb)
+    in
+    List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b]
+  in
+  match Ground.sem f with
+  | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } ->
+    merge (cst (Q.of_string s))
+  | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } ->
+    merge (cst (Q.of_string_decimal s))
+  | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } ->
+    merge (cst (Q.of_string_decimal s))
+  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+    reg a; reg b;
+    let wait =
+      set r (let+ va = get a and+ vb = get b in Q.add va vb) &&
+      set a (let+ vb = get b and+ vr = get r in Q.sub vr vb) &&
+      set b (let+ va = get a and+ vr = get r in Q.sub vr va)
+    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]; _ } ->
+    reg a; reg b;
+    let wait =
+      set r (let+ va = get a and+ vb = get b in Q.sub va vb) &&
+      set a (let+ vb = get b and+ vr = get r in Q.add vr vb) &&
+      set b (let+ va = get a and+ vr = get r in Q.sub va vr)
+    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]; _ } ->
+    reg a;
+    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]; _ } ->
+    cmp Q.lt a b
+  | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+    cmp Q.le a b
+  | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+    cmp Q.gt a b
+  | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+    cmp Q.ge a b
+  | _ -> ()
+
+let init env =
+  Ground.register_converter env converter;
+  init_got_value_bool env;
+  init_got_value env
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 0988142fd014c76dc1e498019f27f3f9ea317398..00551a1e1eb0b18a6c45598bb51cc08900d495f1 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -22,3 +22,7 @@ include ValueKind.Registered with type s = Q.t
 
 val cst': Q.t -> t
 val cst:  Q.t -> Node.t
+
+val zero: Node.t
+
+val init: Egraph.t -> unit