diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index e02245fbb..498f71e02 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -250,6 +250,8 @@ namespace nla {
     // z < 0 & x < 0 => -x <= -z
     bool grobner::propagate_quotients(dd::solver::equation const& eq) {
         dd::pdd const& p = eq.poly();
+        dd::pdd_eval eval;
+        eval.var2val() = [&](unsigned j) { return val(j); };
         if (p.is_linear())
             return false;
         if (p.is_val())
@@ -260,15 +262,17 @@ namespace nla {
         for (auto v : p.free_vars())
             if (!c().var_is_int(v))
                 return false;
+        if (eval(p) == 0)
+            return false;
         tracked_uint_set nl_vars;
+        rational d(1);
         for (auto const& m : p) {
+            d = lcm(d, denominator(m.coeff));
             if (m.vars.size() == 1)
                 continue;
             for (auto j : m.vars)
                 nl_vars.insert(j);
         }
-        dd::pdd_eval eval;
-        eval.var2val() = [&](unsigned j) { return val(j); };
 
         for (auto v : nl_vars) {
             auto& m = p.manager();
@@ -276,9 +280,16 @@ namespace nla {
             p.factor(v, 1, lc, r);
             if (!r.is_linear())
                 continue;
+            if (d != 1) {
+                lc *= d;
+                r *= d;
+            }
             auto v_value = val(v);
             auto r_value = eval(r);
             auto lc_value = eval(lc);
+            SASSERT(v_value.is_int());
+            SASSERT(r_value.is_int());
+            SASSERT(lc_value.is_int());
             if (r_value == 0) {
                 if (v_value == 0)
                     continue;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3bccd0918..a4e861008 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1660,9 +1660,6 @@ public:
                 return FC_CONTINUE;
             }
 
-            if (st == FC_GIVEUP)
-                IF_VERBOSE(0, display(verbose_stream()));
-
             if (!int_undef && !check_bv_terms())
                 return FC_CONTINUE;