diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index b16f6a854..de33e7817 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -683,8 +683,8 @@ module Env = struct
   let up_uf_rs dep env tch =
     if RS.is_empty env.ac_rs then env, tch
     else
-      let env, tch, neqs_to_up = MapX.fold
-          (fun r (rr,ex) ((env, tch, neqs_to_up) as acc) ->
+      let env, tch, neqs_to_up, to_up = MapX.fold
+          (fun r (rr,ex) ((env, tch, neqs_to_up, to_up) as acc) ->
              Options.exec_thread_yield ();
              let nrr, ex_nrr = normal_form env rr in
              if X.equal nrr rr then acc
@@ -699,8 +699,27 @@ module Env = struct
                  if X.is_a_leaf r then (r,[r, nrr, ex],nrr) :: tch
                  else tch
                in
-               env, tch, SetXX.add (rr, nrr) neqs_to_up
-          ) env.repr (env, tch, SetXX.empty)
+               (* With AC symbols, we can have r --> rr with rr not appearing in
+                  repr (e.g. [rr = f(0, 0)] when the initial term was
+                  [f(zero, zero)] with [zero --> 0]).
+
+                  This means that the mapping [rr --> nrr] will not appear in
+                  [tch], which will confuse the relations.
+
+                  Hence, when a new mapping r --> nrr is introduced, we manually
+                  add rr --> nrr as a PIVOT in this case. *)
+               let to_up =
+                 match X.ac_extract rr with
+                 | Some _ when not (MapX.mem rr env.repr) ->
+                   MapX.add rr (nrr, ex_nrr) to_up
+                 | _ -> to_up
+               in
+               env, tch, SetXX.add (rr, nrr) neqs_to_up, to_up
+          ) env.repr (env, tch, SetXX.empty, MapX.empty)
+      in
+      let tch =
+        MapX.fold (fun rr (nrr, ex) tch ->
+            (rr, [rr, nrr, ex], nrr) :: tch) to_up tch
       in
       (* Correction : Do not update neqs twice for the same r *)
       update_aux dep neqs_to_up env, tch
diff --git a/tests/dune.inc b/tests/dune.inc
index b94a3f7f2..0799b087b 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -179829,6 +179829,270 @@
     (package alt-ergo)
      (action
       (diff 479.expected 479_fpa.output)))
+  (rule
+   (target 474_ci_cdcl_no_minimal_bj.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 474_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        474.expected
+        474_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        474.expected
+        474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 474_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        474.expected
+        474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target 474_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 474_cdcl.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_cdcl.output)))
+  (rule
+   (target 474_tableaux_cdcl.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_tableaux_cdcl.output)))
+  (rule
+   (target 474_tableaux.output)
+   (deps (:input 474.ae))
+   (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
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_tableaux.output)))
+  (rule
+   (target 474_legacy.output)
+   (deps (:input 474.ae))
+   (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 legacy
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_legacy.output)))
+  (rule
+   (target 474_dolmen.output)
+   (deps (:input 474.ae))
+   (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
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_dolmen.output)))
+  (rule
+   (target 474_fpa.output)
+   (deps (:input 474.ae))
+   (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
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 474.expected 474_fpa.output)))
   (rule
    (target 460_ci_cdcl_no_minimal_bj.output)
    (deps (:input 460.ae))
diff --git a/tests/issues/474.ae b/tests/issues/474.ae
new file mode 100644
index 000000000..4796f479e
--- /dev/null
+++ b/tests/issues/474.ae
@@ -0,0 +1,12 @@
+logic ac f : real, real -> real
+
+function id_2() : real = 2.
+
+axiom ax_1:
+  f(f(id_2, 1.), 0.) <= 0.0
+
+function f_2_1() : real = f(2., 1.)
+
+axiom ax_2: f_2_1 <= 0.0
+
+goal goal_1: false
diff --git a/tests/issues/474.expected b/tests/issues/474.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/issues/474.expected
@@ -0,0 +1,2 @@
+
+unknown