From eed6f3a1fee9cbfe68e15acb50a84cf2cab7bc2c Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Wed, 19 Oct 2016 02:58:59 -0700 Subject: [PATCH] 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. --- src/theory/booleans/theory_bool_rewriter.cpp | 4 ++-- 1 file 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 -- 2.30.2