diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 1144922bfb..d743c5342d 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1135,15 +1135,7 @@ namespace lp {
 
     // Linearize the bound witnesses of all fixed columns in the row together, so the
     // mark bits walk each dependency sub-DAG shared between columns only once.
-    // When lp.batch_explain_fixed_in_row is disabled, fall back to explaining each
-    // fixed column independently (the pre-batching behavior).
     void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) {
-        if (!settings().batch_explain_fixed_in_row()) {
-            for (auto const& c : get_row(row))
-                if (column_is_fixed(c.var()))
-                    explain_fixed_column(c.var(), ex);
-            return;
-        }
         auto& witnesses = m_imp->m_tmp_witnesses;
         witnesses.reset();
         for (auto const& c : get_row(row)) {
diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg
index 89c9730bc0..29a10c2d52 100644
--- a/src/math/lp/lp_params_helper.pyg
+++ b/src/math/lp/lp_params_helper.pyg
@@ -15,6 +15,5 @@ def_module_params(module_name='lp',
                           ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'),
                           ('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'),
                           ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
-                          ('batch_explain_fixed_in_row', BOOL, True, 'linearize the bound witnesses of all fixed columns in a row in a single dependency pass (de-duplicating shared sub-DAGs) instead of explaining each fixed column independently'),
                          ))
                          
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index 14e60a5b9f..affc299788 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -46,7 +46,6 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_dio_calls_period_decrease = lp_p.dio_calls_period_decrease();
     m_dio_run_gcd = lp_p.dio_run_gcd();
     m_random_hammers = lp_p.random_hammers();
-    m_batch_explain_fixed_in_row = lp_p.batch_explain_fixed_in_row();
     m_lcube = lp_p.lcube();
     m_lcube_flips = lp_p.lcube_flips();
     unsigned hammer_period = lp_p.int_hammer_period();
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 5aeb645b78..bc1f2044f5 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -268,7 +268,6 @@ private:
     unsigned         m_dio_calls_period_decrease = 2;
     bool             m_dio_run_gcd = true;
     bool             m_random_hammers = true;
-    bool             m_batch_explain_fixed_in_row = true;
     bool             m_lcube = true;
     unsigned         m_lcube_flips = 16;
 public:
@@ -280,8 +279,6 @@ public:
     unsigned & dio_calls_period_decrease() { return m_dio_calls_period_decrease; }
     bool random_hammers() const { return m_random_hammers; }
     bool & random_hammers() { return m_random_hammers; }
-    bool batch_explain_fixed_in_row() const { return m_batch_explain_fixed_in_row; }
-    bool & batch_explain_fixed_in_row() { return m_batch_explain_fixed_in_row; }
     bool print_external_var_name() const { return m_print_external_var_name; }
     bool propagate_eqs() const { return m_propagate_eqs;}
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }