mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
parent
bdf6a17b89
commit
fb6cd8e132
|
@ -76,8 +76,9 @@ namespace arith {
|
|||
}
|
||||
|
||||
bool solver::unit_propagate() {
|
||||
TRACE("arith", tout << "unit propagate\n";);
|
||||
m_model_is_initialized = false;
|
||||
if (!m_new_eq && m_new_bounds.empty() && m_asserted_qhead == m_asserted.size())
|
||||
if (!m_solver->has_changed_columns() && !m_new_eq && m_new_bounds.empty() && m_asserted_qhead == m_asserted.size())
|
||||
return false;
|
||||
|
||||
m_new_eq = false;
|
||||
|
|
Loading…
Reference in a new issue