diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index fc816cd14..53adde375 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1210,10 +1210,21 @@ let mk_nary_eq l =
   with Exit ->
     vrai
 
-let mk_distinct ~iff tl =
-  match tl with
-  | [a; b] -> neg (mk_eq ~iff a b)
-  | _ -> neg (mk_nary_eq tl)
+let mk_distinct ~iff args =
+  (* This hot fix makes sure that the smart constructor agrees with
+     the usual semantic of distinct when used with at least 3 arguments.
+     To prevent a soundness bug, we translate the expected expression into a
+     conjonction of binary disequations.
+     See issue: https://github.com/OCamlPro/alt-ergo/issues/889 *)
+  let args = Array.of_list args in
+  let acc = ref vrai in
+  for i = 0 to Array.length args - 1 do
+    for j = i + 1 to Array.length args - 1 do
+      acc :=
+        mk_and (neg (mk_eq ~iff args.(i) args.(j))) !acc false
+    done;
+  done;
+  !acc
 
 let mk_builtin ~is_pos n l =
   let pos =
diff --git a/tests/dune.inc b/tests/dune.inc
index 2b26613f9..c794bd6e6 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -170928,6 +170928,258 @@
 
 ; Auto-generated part begin
 (subdir issues
+  (rule
+   (target 889_ci_cdcl_no_minimal_bj.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --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
+        889.expected
+        889_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        889.expected
+        889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 889_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target 889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff
+        889.expected
+        889_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target 889_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (alias runtest-ci)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 889_cdcl.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_cdcl.output)))
+  (rule
+   (target 889_tableaux_cdcl.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_tableaux_cdcl.output)))
+  (rule
+   (target 889_tableaux.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_tableaux.output)))
+  (rule
+   (target 889_legacy.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend legacy
+             --timelimit=2
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_legacy.output)))
+  (rule
+   (target 889_dolmen.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --timelimit=2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_dolmen.output)))
+  (rule
+   (target 889_fpa.output)
+   (deps (:input 889.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --timelimit=2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 889.expected 889_fpa.output)))
   (rule
    (target 777.models_tableaux.output)
    (deps (:input 777.models.smt2))
diff --git a/tests/issues/889.expected b/tests/issues/889.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/issues/889.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/issues/889.smt2 b/tests/issues/889.smt2
new file mode 100644
index 000000000..1b9e8063a
--- /dev/null
+++ b/tests/issues/889.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+(assert (not (distinct a b c)))
+(assert (distinct a b))
+(check-sat)