From acbe543869918eb2d88779f0f98bfd18b82282d3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 13 Jan 2021 08:28:56 -0600 Subject: 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 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/preprocessing/passes/theory_rewrite_eq.cpp') 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); -- cgit v1.2.3