From fb6cd8e1320197d36d0ccdb6dfb2b2d5a29ea73a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Jun 2021 15:15:02 -0700 Subject: [PATCH] #5324 --- src/sat/smt/arith_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 6b3dc752a..308691c6e 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -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;