diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 60184962f..b72b88f55 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1380,72 +1380,6 @@ namespace lp {
         return m_mpq_lar_core_solver.column_is_free(j);
     }
 
-    // column is at lower or upper bound, lower and upper bound are different.
-    // the lower/upper bound is not strict.
-    // the LP obtained by making the bound strict is infeasible
-    // -> the column has to be fixed
-    bool lar_solver::is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
-        if (column_is_fixed(j))
-            return false;
-        mpq val;
-        if (!has_value(j, val))
-            return false;
-        lp::lconstraint_kind k;
-        if (column_has_upper_bound(j) &&
-            get_upper_bound(j).x == val) {
-            push();   
-            k = column_is_int(j) ? LE : LT;
-            auto ci = mk_var_bound(j, k, column_is_int(j) ? val - 1 : val);
-            update_column_type_and_bound(j, k, column_is_int(j) ? val - 1 : val, ci);
-            auto st = find_feasible_solution();
-            bool infeasible = st == lp_status::INFEASIBLE;
-            if (infeasible) {
-                explanation exp;
-                get_infeasibility_explanation(exp);
-                unsigned_vector cis;
-                exp.remove(ci);
-                verbose_stream() << "tight upper bound " << j << " " << val << "\n";
-                bounds.push_back({exp, j, true, val});
-            }
-            pop(1);
-            return infeasible;            
-        }
-        if (column_has_lower_bound(j) &&
-            get_lower_bound(j).x == val) {
-            push();
-            k = column_is_int(j) ? GE : GT;
-            auto ci = mk_var_bound(j, k, column_is_int(j) ? val + 1 : val);
-            update_column_type_and_bound(j, k, column_is_int(j) ? val + 1 : val, ci);
-            auto st = find_feasible_solution();
-            bool infeasible = st == lp_status::INFEASIBLE;
-            if (infeasible) {
-                explanation exp;
-                get_infeasibility_explanation(exp);
-                exp.remove(ci);
-                verbose_stream() << "tight lower bound " << j << " " << val << "\n";
-                bounds.push_back({exp, j, false, val});
-            }
-            pop(1);
-            return infeasible;
-        }
-        
-        return false;
-    }
-
-    bool lar_solver::has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
-        verbose_stream() << "has-fixed-at-bound\n";
-        for (unsigned j = 0; j < A_r().m_columns.size(); ++j) {
-            auto ci = column_index(j);
-            if (is_fixed_at_bound(ci, bounds)) 
-                verbose_stream() << "fixed " << j << "\n";
-        }
-        verbose_stream() << "num fixed " << bounds.size() << "\n";
-        if (!bounds.empty())
-            find_feasible_solution();
-        return !bounds.empty();
-    }
-
-
     // below is the initialization functionality of lar_solver
 
     bool lar_solver::strategy_is_undecided() const {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index a257ae4e8..96af2d4ce 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -364,9 +364,6 @@ class lar_solver : public column_namer {
                 }
     }
 
-    bool is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
-    bool has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
-
     bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
     inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
     bool external_is_used(unsigned) const;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 5372a3b33..b21424e65 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1659,10 +1659,7 @@ public:
         unsigned old_idx = m_final_check_idx;
         switch (is_sat) {
         case l_true:
-            TRACE("arith", display(tout));
-
-            // if (lp().has_fixed_at_bound()) // explain and propagate.
-
+            TRACE("arith", display(tout));            
 #if 0
             m_dist.reset();
             m_dist.push(0, 1);