From 6635f92842e00091c9c695a5325c0f79b862aebd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Mar 2020 14:10:39 -0700 Subject: [PATCH] fix #3618 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 2 +- src/sat/sat_solver.cpp | 9 ++++++--- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index fabe43629..dc2193168 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -490,7 +490,7 @@ namespace sat { break; } case ba_solver::xr_t: - NOT_IMPLEMENTED_YET(); + throw default_exception("local search is incompatible with enabling xor solving"); break; } } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 185cc2598..8b542097f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1278,8 +1278,12 @@ namespace sat { lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) { literal_vector _lits(num_lits, lits); for (literal lit : m_user_scope_literals) _lits.push_back(~lit); - SASSERT(m_local_search); - scoped_ptr _ptr = m_local_search; + struct scoped_ls { + solver& s; + scoped_ls(solver& s): s(s) {} + ~scoped_ls() { dealloc(s.m_local_search); s.m_local_search = nullptr; } + }; + scoped_ls _ls(*this); if (inconsistent()) return l_false; scoped_limits scoped_rl(rlimit()); SASSERT(m_local_search); @@ -1291,7 +1295,6 @@ namespace sat { m_model = m_local_search->get_model(); m_model_is_current = true; } - m_local_search = nullptr; return r; }