fix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---but this...

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 549878e468d9b5514127f543e68643aa9ca43990..6fe55e50e6b45a3a6f2c2eaab0373cb108625aeb 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -52,6 +52,7 @@ void Smt2::addTheory(Theory theory) {
     defineVar("true", getExprManager()->mkConst(true));
     defineVar("false", getExprManager()->mkConst(false));
     addOperator(kind::AND);
+    addOperator(kind::DISTINCT);
     addOperator(kind::EQUAL);
     addOperator(kind::IFF);
     addOperator(kind::IMPLIES);