From acbe543869918eb2d88779f0f98bfd18b82282d3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 13 Jan 2021 08:28:56 -0600 Subject: [PATCH] Do not call ppRewrite on Boolean equalities (#5762) Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true. Fixes #5761. --- src/preprocessing/passes/theory_rewrite_eq.cpp | 3 ++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/arith/issue5761-ppr.smt2 | 9 +++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/arith/issue5761-ppr.smt2 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) -- 2.30.2