fix distinct operator

regression/smt2_solver/distinct/distinct.smt2

@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8) (_ bv1 8)))
+(check-sat)

regression/smt2_solver/distinct/test.desc

@@ -0,0 +1,6 @@
+CORE
+distinct.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$

regression/smt2_solver/distinct2/distinct2.smt2

@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8) (_ bv1 8)(_ bv2 8) (_ bv1 8)))
+(check-sat)

regression/smt2_solver/distinct2/test.desc

@@ -0,0 +1,6 @@
+CORE
+distinct2.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$

regression/smt2_solver/distinct3/distinct3.smt2

@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8)(_ bv0 8)(_ bv2 8) (_ bv2 8)))
+(check-sat)

regression/smt2_solver/distinct3/test.desc

@@ -0,0 +1,6 @@
+CORE
+distinct3.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$

src/solvers/smt2/smt2_parser.cpp

@@ -950,7 +950,23 @@ void smt2_parsert::setup_expressions()
 
   expressions["distinct"] = [this] {
     // pair-wise different constraint, multi-ary
-    return multi_ary("distinct", operands());
+    auto op = operands();
+    if(op.size() == 2)
+      return binary_predicate(ID_notequal, op);
+    else
+    {
+      std::vector<exprt> pairwise_constraints;
+      for(std::size_t i = 0; i < op.size(); i++)
+      {
+        for(std::size_t j = i; j < op.size(); j++)
+        {
+          if(i != j)
+            pairwise_constraints.push_back(
+              binary_exprt(op[i], ID_notequal, op[j], bool_typet()));
+        }
+      }
+      return multi_ary(ID_and, pairwise_constraints);
+    }
   };
 
   expressions["ite"] = [this] {