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

build break

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-04 16:58:03 -08:00
parent 5d8d42b1fa
commit 0a9ee6c640
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/opt/opt_lns.cpp
View file

@ -103,7 +103,7 @@ namespace opt {
for (unsigned i = 0; i < m_unprocessed.size(); ++i) { for (unsigned i = 0; i < m_unprocessed.size(); ++i) {
if (mdl->is_false(unprocessed(i))) { if (mdl->is_false(unprocessed(i))) {
expr_ref tmp(m_unprocessed.get(j), m); expr_ref tmp(m_unprocessed.get(j), m);
m_unprocessed[j++] = m_unprocessed[i]; m_unprocessed[j++] = m_unprocessed.get(i);
m_unprocessed[i] = tmp; m_unprocessed[i] = tmp;
break; break;
} }
@ -111,7 +111,7 @@ namespace opt {
for (unsigned i = j; i < m_unprocessed.size(); ++i) { for (unsigned i = j; i < m_unprocessed.size(); ++i) {
if (mdl->is_true(unprocessed(i))) { if (mdl->is_true(unprocessed(i))) {
expr_ref tmp(m_unprocessed.get(j), m); expr_ref tmp(m_unprocessed.get(j), m);
m_unprocessed[j++] = m_unprocessed[i]; m_unprocessed[j++] = m_unprocessed.get(i);
m_unprocessed[i] = tmp; m_unprocessed[i] = tmp;
} }
} }
@ -200,7 +200,6 @@ namespace opt {
unsigned num_improved = 0; unsigned num_improved = 0;
unsigned max_conflicts = m_max_conflicts; unsigned max_conflicts = m_max_conflicts;
while (m.inc()) { while (m.inc()) {
unsigned hard = m_hardened.size();
unsigned reward = improve_step(mdl); unsigned reward = improve_step(mdl);
if (reward == 0) if (reward == 0)
break; break;