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

4 files changed, 178 insertions, 6 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();
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 09c012ffa..78bb67bcb 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -42,7 +42,8 @@ SMT_TESTS = \
 	fuzz01.smt
 
 # Regression tests for SMT2 inputs
-SMT2_TESTS =
+SMT2_TESTS = \
+	bug800.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = 
diff --git a/test/regress/regress0/uflra/bug800.smt2 b/test/regress/regress0/uflra/bug800.smt2
new file mode 100644
index 000000000..d36f62b16
--- /dev/null
+++ b/test/regress/regress0/uflra/bug800.smt2
@@ -0,0 +1,168 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_UFLRA)
+(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+
+
+(declare-fun |__ADDRESS_OF_main::c1| () Real)
+(declare-fun |__ADDRESS_OF_main::x1| () Real)
+(declare-fun |__ADDRESS_OF_main::x2| () Real)
+(declare-fun |__ADDRESS_OF_main::c2| () Real)
+(declare-fun |main::x3@3| () Real)
+(declare-fun |main::x1@3| () Real)
+(declare-fun |__ADDRESS_OF_main::d3| () Real)
+(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
+(declare-fun |main::x2@3| () Real)
+(declare-fun |main::d3@2| () Real)
+(declare-fun |__VERIFIER_assert::cond@2| () Real)
+(declare-fun |__ADDRESS_OF_main::x3| () Real)
+(declare-fun |main::d1@2| () Real)
+(declare-fun |__ADDRESS_OF_main::d2| () Real)
+(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_0| () Real)
+(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
+(declare-fun |__ADDRESS_OF_main::d1| () Real)
+(declare-fun |main::d2@2| () Real)
+(define-fun _7 () Real 0)
+(define-fun _8 () Real |__ADDRESS_OF_main::x1|)
+(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
+(define-fun _10 () Bool (= _8 _9))
+(define-fun _11 () Real |__ADDRESS_OF_main::x2|)
+(define-fun _12 () Real (__BASE_ADDRESS_OF__ _11))
+(define-fun _13 () Bool (= _11 _12))
+(define-fun _14 () Bool (and _10 _13))
+(define-fun _15 () Real |__ADDRESS_OF_main::x3|)
+(define-fun _16 () Real (__BASE_ADDRESS_OF__ _15))
+(define-fun _17 () Bool (= _15 _16))
+(define-fun _18 () Bool (and _14 _17))
+(define-fun _19 () Real |__ADDRESS_OF_main::d1|)
+(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
+(define-fun _21 () Bool (= _19 _20))
+(define-fun _22 () Real 1)
+(define-fun _23 () Real |main::d1@2|)
+(define-fun _24 () Bool (= _23 _22))
+(define-fun _25 () Bool (and _21 _24))
+(define-fun _26 () Bool (and _18 _25))
+(define-fun _27 () Real |__ADDRESS_OF_main::d2|)
+(define-fun _28 () Real (__BASE_ADDRESS_OF__ _27))
+(define-fun _29 () Bool (= _27 _28))
+(define-fun _30 () Real |main::d2@2|)
+(define-fun _31 () Bool (= _30 _22))
+(define-fun _32 () Bool (and _29 _31))
+(define-fun _33 () Bool (and _26 _32))
+(define-fun _34 () Real |__ADDRESS_OF_main::d3|)
+(define-fun _35 () Real (__BASE_ADDRESS_OF__ _34))
+(define-fun _36 () Bool (= _34 _35))
+(define-fun _37 () Real |main::d3@2|)
+(define-fun _38 () Bool (= _37 _22))
+(define-fun _39 () Bool (and _36 _38))
+(define-fun _40 () Bool (and _33 _39))
+(define-fun _41 () Real |__ADDRESS_OF_main::c1|)
+(define-fun _42 () Real (__BASE_ADDRESS_OF__ _41))
+(define-fun _43 () Bool (= _41 _42))
+(define-fun _44 () Bool (and _40 _43))
+(define-fun _45 () Real |__ADDRESS_OF_main::c2|)
+(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45))
+(define-fun _47 () Bool (= _45 _46))
+(define-fun _48 () Bool (and _44 _47))
+(define-fun _49 () Real |main::x1@3|)
+(define-fun _50 () Bool (<= _49 _7))
+(define-fun _51 () Bool (not _50))
+(define-fun _53 () Bool (and _48 _51))
+(define-fun _54 () Bool (and _48 _50))
+(define-fun _55 () Real |main::x2@3|)
+(define-fun _56 () Bool (<= _55 _7))
+(define-fun _57 () Bool (not _56))
+(define-fun _59 () Bool (and _53 _57))
+(define-fun _60 () Bool (and _53 _56))
+(define-fun _61 () Bool (or _54 _60))
+(define-fun _62 () Real |main::x3@3|)
+(define-fun _63 () Bool (<= _62 _7))
+(define-fun _67 () Bool (and _59 _63))
+(define-fun _68 () Bool (or _61 _67))
+(define-fun _69 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_0|)
+(define-fun _70 () Real (__BASE_ADDRESS_OF__ _69))
+(define-fun _71 () Bool (= _69 _70))
+(define-fun _72 () Bool (and _68 _71))
+(define-fun _73 () Bool (= _49 _7))
+(define-fun _75 () Bool (and _72 _73))
+(define-fun _76 () Bool (not _73))
+(define-fun _77 () Bool (and _72 _76))
+(define-fun _78 () Bool (= _55 _7))
+(define-fun _80 () Bool (and _77 _78))
+(define-fun _81 () Bool (not _78))
+(define-fun _82 () Bool (and _77 _81))
+(define-fun _83 () Bool (or _75 _80))
+(define-fun _84 () Bool (= _62 _7))
+(define-fun _86 () Bool (and _82 _84))
+(define-fun _87 () Bool (not _84))
+(define-fun _88 () Bool (and _82 _87))
+(define-fun _89 () Bool (or _83 _86))
+(define-fun _90 () Real |main::__CPAchecker_TMP_0@3|)
+(define-fun _91 () Bool (= _90 _7))
+(define-fun _92 () Bool (and _88 _91))
+(define-fun _93 () Bool (= _90 _22))
+(define-fun _94 () Bool (and _89 _93))
+(define-fun _95 () Bool (or _92 _94))
+(define-fun _96 () Real |__VERIFIER_assert::cond@2|)
+(define-fun _97 () Bool (= _90 _96))
+(define-fun _98 () Bool (and _95 _97))
+(define-fun _99 () Bool (= _96 _7))
+(define-fun _101 () Bool (and _98 _99))
+(declare-fun __ART__34@0 () Bool)
+(declare-fun |main::c2@3| () Real)
+(declare-fun __ART__24@0 () Bool)
+(declare-fun __ART__45@0 () Bool)
+(declare-fun |main::c1@3| () Real)
+(declare-fun __ART__23@0 () Bool)
+(declare-fun __ART__32@0 () Bool)
+(declare-fun __ART__36@0 () Bool)
+(declare-fun __ART__26@0 () Bool)
+(declare-fun __ART__53@0 () Bool)
+(declare-fun __ART__29@0 () Bool)
+(define-fun _64 () Bool (not _63))
+(define-fun _108 () Real |main::c1@3|)
+(define-fun _109 () Bool (= _108 _7))
+(define-fun _123 () Real |main::c2@3|)
+(define-fun _124 () Bool (= _123 _7))
+(define-fun _160 () Bool __ART__23@0)
+(define-fun _161 () Bool (= _51 _160))
+(define-fun _162 () Bool __ART__24@0)
+(define-fun _163 () Bool (= _57 _162))
+(define-fun _164 () Bool (and _161 _163))
+(define-fun _165 () Bool __ART__26@0)
+(define-fun _166 () Bool (= _64 _165))
+(define-fun _167 () Bool (and _164 _166))
+(define-fun _168 () Bool __ART__29@0)
+(define-fun _169 () Bool (= _109 _168))
+(define-fun _170 () Bool (and _167 _169))
+(define-fun _171 () Bool __ART__32@0)
+(define-fun _172 () Bool (= _73 _171))
+(define-fun _173 () Bool (and _170 _172))
+(define-fun _174 () Bool __ART__34@0)
+(define-fun _175 () Bool (= _78 _174))
+(define-fun _176 () Bool (and _173 _175))
+(define-fun _177 () Bool __ART__36@0)
+(define-fun _178 () Bool (= _84 _177))
+(define-fun _179 () Bool (and _176 _178))
+(define-fun _180 () Bool __ART__45@0)
+(define-fun _181 () Bool (= _99 _180))
+(define-fun _182 () Bool (and _179 _181))
+(define-fun _183 () Bool __ART__53@0)
+(define-fun _184 () Bool (= _124 _183))
+(define-fun _185 () Bool (and _182 _184))
+
+
+(push 1)
+(assert _101)
+(set-info :status sat)
+(check-sat)
+(push 1)
+(assert _185)
+(set-info :status sat)
+(check-sat)
+(pop 1)
+(pop 1)
+(exit)