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 68006b67ff721c894a3d982ade3503385400be78..190b336842d210da066c040702301955bdfe7131 100644 (file)
--- 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 ea0b3b9e34d72eeb307047c2c2a9b89b87684a7f..a2e070dafd00edd612afc0518032de10a80e1f78 100644 (file)
--- 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 (file)
index 0000000..264807a
--- /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)