Fix the smart constructor of mk_distinct

The smart construct `mk_distinct` produces an SMT-LIB compliant
expression.

src/lib/frontend/cnf.ml

@@ -244,23 +244,7 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
           E.mk_distinct ~iff:true lt
 
         | TAdistinct lt ->
-          (* The current implementation of the distinct expression in
-             Expr clashes with the SMT-LIB specification when used with
-             at least 3 arguments. To prevent a soundness bug, we
-             translate the expected expression into a conjonction
-             of disequations of size 2. *)
-          let args = Array.of_list lt in
-          let acc = ref E.vrai in
-          for i = 0 to Array.length args - 1 do
-            for j = i + 1 to Array.length args - 1 do
-              acc :=
-                E.(mk_and
-                     (mk_distinct ~iff:true
-                        [make_term up_qv name_base args.(i);
-                         make_term up_qv name_base args.(j)]) !acc false)
-            done;
-          done;
-          !acc
+          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

src/lib/frontend/d_cnf.ml

@@ -1337,23 +1337,7 @@ let rec mk_expr
             end
 
           | B.Distinct, _ ->
-            (* The current implementation of the distinct expression in
-               Expr clashes with the SMT-LIB specification when used with
-               at least 3 arguments. To prevent a soundness bug, we
-               translate the expected expression into a conjonction
-               of disequations of size 2. *)
-            let args = Array.of_list args in
-            let acc = ref E.vrai in
-            for i = 0 to Array.length args - 1 do
-              for j = i + 1 to Array.length args - 1 do
-                acc :=
-                  E.(mk_and
-                       (mk_distinct ~iff:true
-                          [aux_mk_expr args.(i); aux_mk_expr args.(j)])
-                       !acc false)
-              done;
-            done;
-            !acc
+            E.mk_distinct ~iff:true (List.map aux_mk_expr args)
 
           | B.Constructor _, _ ->
             let name = get_basename path in

src/lib/structures/expr.ml

@@ -1210,10 +1210,20 @@ 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 fix makes sure that the smart constructor agrees with
+     the SMT-LIB specification when used with at least 3 arguments.
+     To prevent a soundness bug, we translate the expected expression into a
+     conjonction of binary disequations. *)
+  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 =

src/lib/structures/expr.mli

@@ -204,11 +204,6 @@ val pred : t -> t
 
 val mk_eq : iff:bool -> t -> t -> t
 val mk_distinct : iff:bool -> t list -> t
-(** [mk_distinct [t_1; ...; t_n]] produces the expression:
-      t_1 <> t_2 /\ t_2 <> t_3 /\ ... /\ t_(n-1) <> t_n.
-    WARNING: this smart constructor doesn't build the SMT-LIB expression
-     distinct! *)
-
 val mk_builtin : is_pos:bool -> Symbols.builtin -> t list -> t
 
 (** simple smart constructors for formulas *)

tests/models/uf/uf2.models.expected

@@ -2,6 +2,6 @@
 unknown
 (
   (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 2 0))
-  (define-fun a () Int (- 2))
-  (define-fun b () Int 0)
+  (define-fun a () Int 0)
+  (define-fun b () Int (- 2))
 )