diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-13 08:28:56 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-13 08:28:56 -0600 |
| commit | acbe543869918eb2d88779f0f98bfd18b82282d3 (patch) | |
| tree | 13c51723dcaf4c7c56da2f7cc076c45a034f214c /src/preprocessing/passes | |
| parent | b212e64555954532b93db2b64a863d107a4a127d (diff) | |
Do not call ppRewrite on Boolean equalities (#5762)
Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.
Fixes #5761.
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/theory_rewrite_eq.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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); |