projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9da056f) | patch
Fix minor bug and typo in boolean rewriter
authorAndres Notzli <andres.noetzli@gmail.com>
Wed, 19 Oct 2016 09:58:59 +0000 (02:58 -0700)
committerAndres Notzli <andres.noetzli@gmail.com>
Wed, 19 Oct 2016 09:58:59 +0000 (02:58 -0700)
commiteed6f3a1fee9cbfe68e15acb50a84cf2cab7bc2c
tree6addb6865f825c2846a76329ccad8329f4a37f4ftree
parent9da056f71c0c4a8ed5afd01c300e9c86cfcf5601commit | diff
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 diff | blob | history