From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Jan 2021 14:28:56 +0000 (-0600)
Subject: Do not call ppRewrite on Boolean equalities (#5762)
X-Git-Tag: cvc5-1.0.0~2381
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=acbe543869918eb2d88779f0f98bfd18b82282d3;p=cvc5.git

Do not call ppRewrite on Boolean equalities (#5762)

Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.

Fixes #5761.
---

diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 68006b67f..190b33684 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -59,7 +59,8 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
 
     if (it == visited.end())
     {
-      if (cur.getKind() == kind::EQUAL)
+      // don't consider Boolean equality
+      if (cur.getKind() == kind::EQUAL && !cur[0].getType().isBoolean())
       {
         // For example, (= x y) ---> (and (>= x y) (<= x y))
         theory::TrustNode trn = te->ppRewriteEquality(cur);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ea0b3b9e3..a2e070daf 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -59,6 +59,7 @@ set(regress_0_tests
   regress0/arith/issue4367.smt2
   regress0/arith/issue4525.smt2
   regress0/arith/issue5219-conflict-rewrite.smt2
+  regress0/arith/issue5761-ppr.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc
diff --git a/test/regress/regress0/arith/issue5761-ppr.smt2 b/test/regress/regress0/arith/issue5761-ppr.smt2
new file mode 100644
index 000000000..264807afb
--- /dev/null
+++ b/test/regress/regress0/arith/issue5761-ppr.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --arith-rewrite-equalities -i
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-const i4 Int)
+(declare-const v9 Bool)
+(assert (= v9 (< (- i4) 1)))
+(push)
+(check-sat)