diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 2e7b2ef8cf..9e9d1add14 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1125,8 +1125,10 @@ namespace lp {
 
     void lar_solver::explain_fixed_column(unsigned j, explanation& ex) {
         SASSERT(column_is_fixed(j));
-        auto* deps = get_bound_constraint_witnesses_for_column(j);
-        for (auto ci : flatten(deps))
+        const column& ul = m_imp->m_columns[j];
+        m_imp->m_tmp_dependencies.reset();
+        m_imp->m_dependencies.linearize(ul.lower_bound_witness(), ul.upper_bound_witness(), m_imp->m_tmp_dependencies);
+        for (auto ci : m_imp->m_tmp_dependencies)
             ex.push_back(ci);
     }
 
diff --git a/src/util/dependency.h b/src/util/dependency.h
index 5837e575b6..55d88291ac 100644
--- a/src/util/dependency.h
+++ b/src/util/dependency.h
@@ -234,6 +234,22 @@ public:
         m_todo.reset();
     }
 
+    // Linearize the union of two dependencies without allocating a join node.
+    void linearize(dependency * d1, dependency * d2, vector<value, false> & vs) const {
+        SASSERT(m_todo.empty());
+        if (d1) {
+            d1->mark();
+            m_todo.push_back(d1);
+        }
+        if (d2 && !d2->is_marked()) {
+            d2->mark();
+            m_todo.push_back(d2);
+        }
+        if (!m_todo.empty())
+            linearize_todo(m_todo, vs);
+        m_todo.reset();
+    }
+
     void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) const {
         if (deps.empty())
             return;
@@ -333,6 +349,10 @@ public:
         return m_dep_manager.linearize(d, vs);
     }    
 
+    void linearize(dependency * d1, dependency * d2, vector<value, false> & vs) const {
+        return m_dep_manager.linearize(d1, d2, vs);
+    }    
+
     static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) {
         dep_manager::s_linearize(d, vs);
         return vs;