diff options
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index cc9eb54b9..dc5f655aa 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -168,7 +168,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } case kind::IMPLIES: { if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); - if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); break; @@ -259,7 +259,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // XOR true x return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); } else if(n[1] == tt) { - // XCR x true + // XOR x true return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } else if(n[0] == ff) { // XOR false x |