Checking that equalities belong to the arithmetic theory in the solve() routine.

2 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index f8de2f239..14607f4e4 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -14,11 +14,11 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/normal_form.h"
 
 #include <list>
 
 #include "base/output.h"
-#include "theory/arith/normal_form.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/theory.h"
 
@@ -805,6 +805,7 @@ DeltaRational Comparison::normalizedDeltaRational() const {
 }
 
 Comparison Comparison::parseNormalForm(TNode n) {
+  Debug("polynomial") << "Comparison::parseNormalForm(" << n << ")";
   Comparison result(n);
   Assert(result.isNormalForm());
   return result;
@@ -1080,8 +1081,8 @@ bool Comparison::isNormalEqualityOrDisequality() const {
 /** This must be (= qvarlist qpolynomial) or (= zmonomial zpolynomial)*/
 bool Comparison::isNormalEquality() const {
   Assert(getNode().getKind() == kind::EQUAL);
-
-  return isNormalEqualityOrDisequality();
+  return Theory::theoryOf(getNode()[0].getType()) == THEORY_ARITH &&
+         isNormalEqualityOrDisequality();
 }
 
 /**
@@ -1092,7 +1093,8 @@ bool Comparison::isNormalDistinct() const {
   Assert(getNode().getKind() == kind::NOT);
   Assert(getNode()[0].getKind() == kind::EQUAL);
 
-  return isNormalEqualityOrDisequality();
+  return Theory::theoryOf(getNode()[0][0].getType()) == THEORY_ARITH &&
+         isNormalEqualityOrDisequality();
 }
 
 Node Comparison::mkRatEquality(const Polynomial& p){
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index dfe092aa5..1b97dceb2 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1387,7 +1387,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
   Rational minConstant = 0;
   Node minMonomial;
   Node minVar;
-  if (in.getKind() == kind::EQUAL) {
+  if (in.getKind() == kind::EQUAL &&
+      Theory::theoryOf(in[0].getType()) == THEORY_ARITH) {
     Comparison cmp = Comparison::parseNormalForm(in);
 
     Polynomial left = cmp.getLeft();