From d1854ab4d263abde358699839d65ce44285342ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2017 15:24:40 -0800 Subject: [PATCH] fix assertion in model converter for incremental mode Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_simplifier.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 05c89fba7..fac4cface 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -46,7 +46,7 @@ namespace sat { UNREACHABLE(); throw solver_exception("flipping assumption"); } - if (m_solver && m_solver->is_external(v)) { + if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) { std::cout << "flipping external v" << v << "\n"; UNREACHABLE(); throw solver_exception("flipping external"); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 6d578b4f9..c101e3a29 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -970,11 +970,12 @@ namespace sat { } void insert(literal l) { + VERIFY(process_var(l.var())); m_queue.insert(l); } bool process_var(bool_var v) { - return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); + return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); } void operator()() {