mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3623

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 12:36:59 -07:00
parent 2b5247a37b
commit 78626c57d5
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/sat_local_search.cpp
View file

@ -167,9 +167,10 @@ namespace sat {
init_goodvars(); init_goodvars();
set_best_unsat(); set_best_unsat();
for (bool_var v : m_units) { unsigned sz = m_units.size();
for (unsigned i = 0; !m_is_unsat && i < m_units.size(); ++i) {
bool_var v = m_units[i];
propagate(literal(v, !cur_solution(v))); propagate(literal(v, !cur_solution(v)));
if (m_is_unsat) break;
} }
if (m_is_unsat) { if (m_is_unsat) {
IF_VERBOSE(0, verbose_stream() << "unsat during reinit\n"); IF_VERBOSE(0, verbose_stream() << "unsat during reinit\n");