mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

restart after sat solution

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-06 09:21:35 -08:00
parent 03a4920f3d
commit c1c26f0726
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/sat_solver.cpp
View file

@ -1351,9 +1351,15 @@ namespace sat {
scoped_rl.push_child(&(m_local_search->rlimit()));
m_local_search->rlimit().push(500000);
m_local_search->reinit(*this);
m_local_search->check(_lits.size(), _lits.data(), nullptr);
lbool r = m_local_search->check(_lits.size(), _lits.data(), nullptr);
for (unsigned i = 0; i < m_phase.size(); ++i)
m_best_phase[i] = m_local_search->get_value(i);
if (r == l_true) {
m_conflicts_since_restart = 0;
m_conflicts_since_gc = 0;
m_next_simplify = std::max(m_next_simplify, m_conflicts_since_init + 1);
do_restart(true);
}
}