From 719c5dd911196322b18870e782da06c307887645 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Mar 2020 12:14:28 -0700 Subject: [PATCH] fix #3342 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index e784fd76d..0a2ca2b93 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -98,6 +98,8 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg continue; } if (m().is_false(arg)) { + neg_lits.reset(); + pos_lits.reset(); result = m().mk_false(); return BR_DONE; } @@ -107,6 +109,8 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg continue; } if (pos_lits.is_marked(atom)) { + neg_lits.reset(); + pos_lits.reset(); result = m().mk_false(); return BR_DONE; } @@ -118,6 +122,8 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg continue; } if (neg_lits.is_marked(arg)) { + neg_lits.reset(); + pos_lits.reset(); result = m().mk_false(); return BR_DONE; } @@ -184,6 +190,8 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; if (m().is_true(arg)) { + neg_lits.reset(); + pos_lits.reset(); result = m().mk_true(); return BR_DONE; } @@ -198,6 +206,8 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args continue; } if (pos_lits.is_marked(atom)) { + neg_lits.reset(); + pos_lits.reset(); result = m().mk_true(); return BR_DONE; } @@ -209,6 +219,8 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args continue; } if (neg_lits.is_marked(arg)) { + neg_lits.reset(); + pos_lits.reset(); result = m().mk_true(); return BR_DONE; } @@ -222,6 +234,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args neg_lits.reset(); pos_lits.reset(); + unsigned sz = buffer.size(); switch(sz) {