diff options
| -rw-r--r-- | example.smt2 | 6 | ||||
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/example.smt2 b/example.smt2 new file mode 100644 index 000000000..ab3ad5aac --- /dev/null +++ b/example.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_AX) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(assert (not true)) +(check-sat) +(exit) diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index dc5f655aa..cceb6d49c 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -133,7 +133,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { switch(n.getKind()) { case kind::NOT: { - if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff); + //if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff); if (n[0] == ff) return RewriteResponse(REWRITE_DONE, tt); if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]); break; |