diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 2913d81d1..adcd47b8c 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1538,13 +1538,11 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lp
 
 
 dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
-    unsigned lc, uc;
-    m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
-    if (lc != null_lpvar)
-        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
-    if (uc != null_lpvar) 
-        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
     if (var_is_fixed(j)) {
+        unsigned lc, uc;
+        m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
+        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
         return m_pdd_manager.mk_val(c *  m_lar_solver.column_lower_bound(j).x);
     }
 
@@ -1556,6 +1554,7 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
     const monic& m = emons()[j];
     for (lpvar k : m.vars()) {
         if (var_is_fixed(k)) {
+            unsigned lc, uc;
             r *= m_pdd_manager.mk_val(m_lar_solver.column_lower_bound(k).x);           
             m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
             dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));