diff --git a/regression/smt2_solver/distinct/distinct.smt2 b/regression/smt2_solver/distinct/distinct.smt2
new file mode 100644
index 00000000000..b8b146b1b78
--- /dev/null
+++ b/regression/smt2_solver/distinct/distinct.smt2
@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8) (_ bv1 8)))
+(check-sat)
diff --git a/regression/smt2_solver/distinct/test.desc b/regression/smt2_solver/distinct/test.desc
new file mode 100644
index 00000000000..0cd29473710
--- /dev/null
+++ b/regression/smt2_solver/distinct/test.desc
@@ -0,0 +1,6 @@
+CORE
+distinct.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
diff --git a/regression/smt2_solver/distinct2/distinct2.smt2 b/regression/smt2_solver/distinct2/distinct2.smt2
new file mode 100644
index 00000000000..f6dd5f52f23
--- /dev/null
+++ b/regression/smt2_solver/distinct2/distinct2.smt2
@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8) (_ bv1 8)(_ bv2 8) (_ bv1 8)))
+(check-sat)
diff --git a/regression/smt2_solver/distinct2/test.desc b/regression/smt2_solver/distinct2/test.desc
new file mode 100644
index 00000000000..6d5134967f8
--- /dev/null
+++ b/regression/smt2_solver/distinct2/test.desc
@@ -0,0 +1,6 @@
+CORE
+distinct2.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
diff --git a/regression/smt2_solver/distinct3/distinct3.smt2 b/regression/smt2_solver/distinct3/distinct3.smt2
new file mode 100644
index 00000000000..80753412f04
--- /dev/null
+++ b/regression/smt2_solver/distinct3/distinct3.smt2
@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8)(_ bv0 8)(_ bv2 8) (_ bv2 8)))
+(check-sat)
diff --git a/regression/smt2_solver/distinct3/test.desc b/regression/smt2_solver/distinct3/test.desc
new file mode 100644
index 00000000000..b529a36eafd
--- /dev/null
+++ b/regression/smt2_solver/distinct3/test.desc
@@ -0,0 +1,6 @@
+CORE
+distinct3.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index 0401e884778..a85f0c95b40 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/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] {