From 55c285c0df6aaa31ed6ce54ca3f805bb7788aae9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Mar 2020 14:01:00 -0700 Subject: [PATCH] fix #3620 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 104927a63..185cc2598 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1276,6 +1276,8 @@ 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; if (inconsistent()) return l_false; @@ -1284,7 +1286,7 @@ namespace sat { m_local_search->add(*this); m_local_search->updt_params(m_params); scoped_rl.push_child(&(m_local_search->rlimit())); - lbool r = m_local_search->check(num_lits, lits, nullptr); + lbool r = m_local_search->check(_lits.size(), _lits.c_ptr(), nullptr); if (r == l_true) { m_model = m_local_search->get_model(); m_model_is_current = true;