diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 99b05beaf..735f835e0 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -695,6 +695,7 @@ namespace lp {
         }
     }
 
+    void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
         if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) 
             insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]);
         else 
@@ -1751,7 +1752,8 @@ namespace lp {
     }
     // clang-format off
     void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
-                const mpq& right_side,
+        lconstraint_kind kind,
+        const mpq& right_side,
         constraint_index constr_index,
         unsigned& equal_to_j) {
         update_column_type_and_bound(j, kind, right_side, constr_index);
@@ -1895,7 +1897,8 @@ namespace lp {
     }
     // clang-format off
     void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
-                lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
+        lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
+        lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
 
         mpq y_of_bound(0);
         switch (kind) {
@@ -1943,7 +1946,8 @@ namespace lp {
     }
     // clang-format off
     void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
-                lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
+        lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
+        lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
         mpq y_of_bound(0);
         switch (kind) {
         case LT:
@@ -2029,7 +2033,8 @@ namespace lp {
     }
     // clang-format off
     bool lar_solver::column_corresponds_to_term(unsigned j) const {
-            }
+        return tv::is_term(m_var_register.local_to_external(j));
+    }
 
     var_index lar_solver::to_column(unsigned ext_j) const {
         return m_var_register.external_to_local(ext_j);