diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 420256e59..d2aa164eb 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -152,11 +152,11 @@ namespace sat { void update_prefix(literal l) { bool_var x = l.var(); - unsigned p = m_prefix[x].m_prefix; - if (m_prefix[x].m_length >= m_trail_lim.size() || + unsigned p = m_vprefix[x].m_prefix; + if (m_vprefix[x].m_length >= m_trail_lim.size() || ((p | m_prefix) != m_prefix)) { - m_prefix[x].m_length = m_trail_lim.size(); - m_prefix[x].m_prefix = m_prefix; + m_vprefix[x].m_length = m_trail_lim.size(); + m_vprefix[x].m_prefix = m_prefix; } } diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index f4dee3061..23558ea44 100644 --- a/src/test/sat_local_search.cpp +++ b/src/test/sat_local_search.cpp @@ -76,7 +76,9 @@ void tst_sat_local_search(char ** argv, int argc, int& i) { reslimit limit; params_ref params; sat::solver solver(params, limit); - sat::local_search local_search(solver); + sat::local_search local_search; + + local_search.import(solver, true); char const* file_name = argv[i + 1]; ++i;