From 9f1530fdc0af619be4e86f7e153e25c5b627348b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Mar 2020 14:34:17 -0700 Subject: [PATCH] fix #3428 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 07a65563a..01507e517 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -207,9 +207,11 @@ class mbp::impl { continue; } m_visited.mark(e); - if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e)) { + if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e) && !m.canceled()) { expr_ref val = eval(e); TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";); + if (m.canceled()) + continue; SASSERT(m.is_true(val) || m.is_false(val)); if (!m_bool_visited.is_marked(e)) { fmls.push_back(m.is_true(val) ? e : mk_not(m, e)); @@ -229,7 +231,7 @@ class mbp::impl { expr_ref tmp(m); sub(fml, tmp); expr_ref val = eval(tmp); - SASSERT(m.is_true(val) || m.is_false(val)); + SASSERT(m.is_true(val) || m.is_false(val) || m.canceled()); fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp)); } return found_bool;