diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index 265700244..ae23a9a4c 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -447,8 +447,16 @@ module Main : S = struct
   let make_unique sa =
     let mp =
       List.fold_left
-        (fun mp ((ra, aopt ,_ ,_) as e) ->
-           LRE.add (LR.make ra, aopt) e mp
+        (fun mp ((ra, aopt ,_ , _) as e) ->
+           (* Make sure to prefer equalities of [Subst] origin because they are
+              used for partial computations (see {!Rel_utils}). In general, we
+              want to make sure that the relations see all the equalities from
+              representative changes in the union-find. *)
+           LRE.update (LR.make ra, aopt) (function
+               | Some ((_, _, _, Th_util.Subst) as e') -> Some e'
+               | _ -> Some e
+             ) mp
+
         ) LRE.empty sa
     in
     LRE.fold (fun _ e acc -> e::acc) mp []
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index b31d0391c..6687c0c15 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -173,33 +173,12 @@ end = struct
               | None -> eqs) se eqs) sm eqs
 
   let update env uf r1 r2 orig eqs =
-    (* The `Subst` origin is used when `r1 -> r2` is added in the
-        union-find. The `CS _` and `NCS _` origins are used for case splits. In
-        both cases, we want to be propagating the constant.
-
-        Note that equalities of `Subst` origins are oriented: for `Subst`, `r2`
-        is the (new) normal form for `r1.
-
-        Usually, this would be true of case-split equalities as well (of the
-        form `r = v` where `v` is the chosen value), but this is not true for
-        the case splits that come from the arrays theory (in fact, the array
-        theory produces *dis*equality case splits, and the equality ends up in
-        the `NCS` instead), so we don't try to be smart and pay the (small)
-        performance cost.
-
-        `Other` cases should (I believe...) be subsumed by `Subst`. The original
-        code in the arithmetic theory that this is lifted from from was only
-        considering `Subst`, and was allowing possibly incorrect models.
-
-        Note that we need to handle `CS` and `NCS` here to produce correct
-        models, but also this can cause eager enumeration, so by excess of
-        caution we only use it when model generation has been requested. It is
-        unknown whether eager enumeration would be an actual problem in
-        practice. *)
+    (* The `Subst` origin is used when `r1 -> r2` is added in the union-find, so
+       we want to be propagating the constant on the RHS.
+
+       The other origins are subsumed. *)
     match orig with
     | Th_util.Subst when X.is_constant r2 -> update env uf r1 eqs
-    | CS _ | NCS _ when Options.get_interpretation () ->
-      update env uf r2 (update env uf r1 eqs)
     | _ -> eqs
 
 
diff --git a/tests/dune.inc b/tests/dune.inc
index 829ea61e2..df3c921cd 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -175752,6 +175752,27 @@
 
 ; Auto-generated part begin
 (subdir issues
+  (rule
+   (target 883.dolmen_dolmen.output)
+   (deps (:input 883.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps 883.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 883.dolmen.expected 883.dolmen_dolmen.output)))
   (rule
    (target 777.models_tableaux.output)
    (deps (:input 777.models.smt2))
diff --git a/tests/issues/883.dolmen.expected b/tests/issues/883.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/issues/883.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/issues/883.dolmen.smt2 b/tests/issues/883.dolmen.smt2
new file mode 100644
index 000000000..75a70f619
--- /dev/null
+++ b/tests/issues/883.dolmen.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (= ((_ int2bv 2) x) #b11))
+(assert (<= x 0))
+(assert (<= 0 x))
+(check-sat)