From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 17 Jul 2012 20:34:34 +0000 (+0000)
Subject: fix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---but this... 
X-Git-Tag: cvc5-1.0.0~7920
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=159a9a457761d47077bf45e82daedf7e6883f3fc;p=cvc5.git

fix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---but this only gave trouble in strict parsing mode
---

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 549878e46..6fe55e50e 100644
--- 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);