From ca9ed38ff54f7e31ac00b42354bc63ae7d123908 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 2 Jan 2020 12:01:01 -0800
Subject: [PATCH] add dependencies only for fixed variablse in
 add_row_to_pdd_grobner()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

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));