#5324

Z3Prover · Jun 8, 2021 · fb6cd8e · fb6cd8e
1 parent bdf6a17
commit fb6cd8e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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;