From 361964f1738ae1026b5df7ac4e2d88cc284ce1ab Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 30 Dec 2019 12:24:06 -0800
Subject: [PATCH] fix arith errors add_row for nex grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_common.cpp  | 10 +++++-----
 src/math/lp/nla_grobner.cpp |  4 ++++
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index a4a2f37f5..72c2a974e 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -134,7 +134,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
             dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
             dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
         }
-        return cn.mk_scalar(c().m_lar_solver.column_lower_bound(j).x);
+        return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x);
     }
     if (!c().is_monic_var(j)) {
         c().insert_to_active_var_set(j);
@@ -144,13 +144,13 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
     nex_creator::mul_factory mf(cn);
     mf *= coeff;
     for (lpvar k : m.vars()) {
-        if (c().var_is_fixed(j)) {
+        if (c().var_is_fixed(k)) {
             if (dep_manager) {
-                c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+                c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
                 dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
                 dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
             }
-            mf *= c().m_lar_solver.column_lower_bound(j).x;
+            mf *= c().m_lar_solver.column_lower_bound(k).x;
         } else {
             c().insert_to_active_var_set(k);
             mf *= cn.mk_var(k);
@@ -184,8 +184,8 @@ template <typename T> u_dependency* common::create_sum_from_row(const T& row,
                 dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
             if (uc + 1) 
                 dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));                    
-            sum += e;
         }
+        sum += e;
     }
     return dep;
 }
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index bb4a43e8f..e9c0821ee 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -726,6 +726,10 @@ std::ostream& grobner_core::display_dependency(std::ostream& out, u_dependency*
 
 #ifdef Z3DEBUG
 bool grobner_core::test_find_b(const nex* ab, const nex_mul* b) {
+    if (ab->is_var()) {
+        return b->size() == 0 || (b->get_degree() == 1 && b->get_child_exp(0)->to_var().var() ==
+                                  ab->to_var().var());
+    }
     nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul();
     nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, *b);
     ab_clone.m_coeff = rational(1);