diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 15e7954362f0fe2c08eceacac40b83757b38cd13..e46dceb1581d841551c683d6c3adff5913c9c71a 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -9,6 +9,8 @@
 (rule (alias runtest) (action (diff oracle le2.smt2.res)))
 (rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1000 %{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 1000 %{dep:repr_and_poly.smt2}))))
+(rule (alias runtest) (action (diff oracle repr_and_poly.smt2.res)))
 (rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 1000 %{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 1000 %{dep:solver_set_sem_merge_sign.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/repr_and_poly.smt2 b/src_colibri2/tests/solve/smt_lra/unsat/repr_and_poly.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..71a2c71bb204790c8947d4ccda5c20065e066d14
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/unsat/repr_and_poly.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun t1 () Real)
+(declare-fun t2 () Real)
+
+(assert (= t1 (+ a b)))
+(assert (= t2 (+ a c)))
+
+(assert (= b c))
+(assert (not (= t1 t2)))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 60755baf760e7a5f1eaf1b280a3ccd7cc276de64..d96637f8c04394eecd8ea06a152bfa5b9a2385bd 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -49,9 +49,13 @@ let add_used d cl' new_cl =
           | Some b -> Some (Bag.append b cl')
           | None ->
             begin match Egraph.get_dom d dom_poly used with
-              | None -> Egraph.set_dom d dom_poly used (Polynome.monome Q.one used)
+              | None ->
+                (** If a used node have no polynome associated, we set it to
+                   itself. This allows to be warned when this node is merged. It
+                   is the reason why this module doesn't specifically wait for
+                   representative change *)
+                Egraph.set_dom d dom_poly used (Polynome.monome Q.one used)
               | Some p ->
-                Format.eprintf "used=%a p=%a@." Node.pp used Polynome.pp p;
                 assert (Polynome.equal (Polynome.monome Q.one used) p)
             end;
             Some (Bag.elt cl')
@@ -165,8 +169,8 @@ end
 
 let () = Egraph.register_dom(module Th)
 
-let assume_poly_equality d n p =
-  Debug.dprintf4 debug "assume1: %a = %a" Node.pp n Polynome.pp p;
+let assume_poly_equality d n (p:Polynome.t) =
+  (* Debug.dprintf4 debug "assume1: %a = %a" Node.pp n Polynome.pp p; *)
   let n = Egraph.find d n in
   let add acc cl c =
     let cl = Egraph.find d cl in
@@ -175,7 +179,7 @@ let assume_poly_equality d n p =
     | Some p -> Polynome.x_p_cy acc c 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;
+  (* Debug.dprintf4 debug "assume2: %a = %a" Node.pp n Polynome.pp p; *)
   Th.solve_one d n p
 
 (** {2 Initialization} *)