diff options
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); |