Fix minor bug and typo in boolean rewriter

One of the rewrites in the boolean rewriter had the condition `n[0] ==
tt && n[0] == ff`, which could never be true. Another rewrite covers the
same case but returns a `REWRITE_AGAIN` instead of a `REWRITE_DONE`.
This commit also fixes a minor typo.

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index cc9eb54b99036930080763f3f81912282197ef68..dc5f655aa3e058a9384200ec370a08258aad15ea 100644 (file)
--- 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