ensure bounds propagation on changed columns after nla propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/lar_solver.cpp

@@ -1067,6 +1067,8 @@ namespace lp {
     }
 
     bool lar_solver::init_model() const {
+        CTRACE("lar_solver_model",!m_columns_with_changed_bounds.empty(), tout << "non-empty changed bounds\n");
+        TRACE("lar_solver_model", tout << get_status() << "\n");
         if (get_status() != lp_status::OPTIMAL && get_status() != lp_status::FEASIBLE)
             return false;
         if (!m_columns_with_changed_bounds.empty())

src/smt/theory_lra.cpp

@@ -2115,8 +2115,9 @@ class theory_lra::imp {
         flush_bound_axioms();
         // disabled in master:
         propagate_nla(); 
-        if (!can_propagate_core())
+        if (!can_propagate_core()) 
             return false;
+
         m_new_def = false;        
         while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
             auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
@@ -2160,6 +2161,7 @@ class theory_lra::imp {
             m_nla->propagate();
             add_lemmas();
             add_equalities();
+            propagate_bounds_with_lp_solver();
         }
     }
 
@@ -2210,9 +2212,6 @@ class theory_lra::imp {
     }
 
     void propagate_bounds_with_lp_solver() {
-        if (!should_propagate()) 
-            return;
-
         m_bp.init();
         lp().propagate_bounds_for_touched_rows(m_bp);
 
@@ -2224,13 +2223,11 @@ class theory_lra::imp {
             // verbose_stream() << "unsat\n";
         }
         else {
-            unsigned count = 0, prop = 0;
             for (auto& ib : m_bp.ibounds()) {
                 m.inc();
                 if (ctx().inconsistent())
                     break;
-                ++prop;
-                count += propagate_lp_solver_bound(ib);
+                propagate_lp_solver_bound(ib);
             }
         }
     }