Clean up

src/lib/frontend/cnf.ml

@@ -239,13 +239,9 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
           let res = make_term up_qv name_base t in
           if negated then E.neg res else res
 
-        | TAneq lt ->
+        | TAneq lt | TAdistinct lt ->
           let lt = List.map (make_term up_qv name_base) lt in
           E.mk_distinct ~iff:true lt
-
-        | TAdistinct lt ->
-          E.mk_distinct ~iff:true (List.map (make_term up_qv name_base) lt)
-
         | TAle [t1;t2] ->
           E.mk_builtin ~is_pos:true Sy.LE
             [make_term up_qv name_base t1;

src/lib/frontend/d_cnf.ml

@@ -1337,7 +1337,7 @@ let rec mk_expr
             end
 
           | B.Distinct, _ ->
-            E.mk_distinct ~iff:true (List.map aux_mk_expr args)
+            E.mk_distinct ~iff:true (List.map (fun t -> aux_mk_expr t) args)
 
           | B.Constructor _, _ ->
             let name = get_basename path in

src/lib/structures/expr.ml

@@ -1211,10 +1211,11 @@ let mk_nary_eq l =
     vrai
 
 let mk_distinct ~iff args =
-  (* This fix makes sure that the smart constructor agrees with
-     the SMT-LIB specification when used with at least 3 arguments.
+  (* 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. *)
+     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