Fix type issue in arith rewrite equality (#3972)

Fixes #3952 and fixes #3940 and fixes #3941 and fixes #3968.

3 files changed, 68 insertions, 11 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 786296b15..6c226bb61 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1301,18 +1301,21 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
 Node TheoryArithPrivate::ppRewrite(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
-  if (atom.getKind() == kind::EQUAL  && options::arithRewriteEq()) {
-    Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-    Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-    leq = ppRewriteTerms(leq);
-    geq = ppRewriteTerms(geq);
-    Node rewritten = Rewriter::rewrite(leq.andNode(geq));
-    Debug("arith::preprocess") << "arith::preprocess() : returning "
-                               << rewritten << endl;
-    return rewritten;
-  } else {
-    return ppRewriteTerms(atom);
+  if (options::arithRewriteEq())
+  {
+    if (atom.getKind() == kind::EQUAL && atom[0].getType().isReal())
+    {
+      Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+      Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+      leq = ppRewriteTerms(leq);
+      geq = ppRewriteTerms(geq);
+      Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+      Debug("arith::preprocess")
+          << "arith::preprocess() : returning " << rewritten << endl;
+      return rewritten;
+    }
   }
+  return ppRewriteTerms(atom);
 }
 
 Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d96360ad6..0edbd094d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1173,6 +1173,7 @@ set(regress_1_tests
   regress1/arith/div.06.smt2
   regress1/arith/div.08.smt2
   regress1/arith/div.09.smt2
+  regress1/arith/issue3952-rew-eq.smt2
   regress1/arith/miplib3.cvc
   regress1/arith/mod.02.smt2
   regress1/arith/mod.03.smt2
diff --git a/test/regress/regress1/arith/issue3952-rew-eq.smt2 b/test/regress/regress1/arith/issue3952-rew-eq.smt2
new file mode 100644
index 000000000..9a14251a0
--- /dev/null
+++ b/test/regress/regress1/arith/issue3952-rew-eq.smt2
@@ -0,0 +1,53 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic QF_UFNIA)
+(set-option :check-models true)
+(set-option :produce-models true)
+(set-option :arith-rewrite-equalities true)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const v5 Bool)
+(declare-const i3 Int)
+(declare-const i4 Int)
+(declare-const i5 Int)
+(declare-const i7 Int)
+(declare-const i8 Int)
+(declare-const i10 Int)
+(declare-const i11 Int)
+(declare-const i13 Int)
+(declare-const i15 Int)
+(declare-const i16 Int)
+(declare-const i17 Int)
+(push 1)
+(assert (< i15 i8))
+(declare-const v6 Bool)
+(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2))
+(push 1)
+(declare-const v7 Bool)
+(declare-const i18 Int)
+(push 1)
+(declare-const v8 Bool)
+(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2))
+(declare-const v9 Bool)
+(declare-const i19 Int)
+(assert (xor (<= (- i4 i3 i10 i7) 65) (not v5) (and (<= i18 i11) v6 (distinct v6 (or v1 v2 v0 v5) (< i15 i8) v3 v2 v1 (< i15 i8) v6 v3 v3) (or v1 v2 v0 v5)) v7 (not v5) (= 128 i11)))
+(push 1)
+(declare-const v10 Bool)
+(assert (=> v9 v1))
+(assert (not v5))
+(declare-const v11 Bool)
+(declare-const i20 Int)
+(declare-const i21 Int)
+(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2))
+(push 1)
+(assert (= v10 (=> (<= i18 i11) (distinct 67 i18)) v1 v6 (<= (- i4 i3 i10 i7) 65) (xor (<= (- i4 i3 i10 i7) 65) (not v5) (and (<= i18 i11) v6 (distinct v6 (or v1 v2 v0 v5) (< i15 i8) v3 v2 v1 (< i15 i8) v6 v3 v3) (or v1 v2 v0 v5)) v7 (not v5) (= 128 i11)) v8))
+(push 1)
+(check-sat)
+(push 1)
+(push 1)
+(pop 1)
+(check-sat)