diff --git a/src/math/lp/nla_bounds.cpp b/src/math/lp/nla_bounds.cpp
index 18aada476..c7a49896d 100644
--- a/src/math/lp/nla_bounds.cpp
+++ b/src/math/lp/nla_bounds.cpp
@@ -69,12 +69,13 @@ namespace nla {
             auto i(ineq(j, lp::lconstraint_kind::LE, rational(value)));
             TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
             c().add_literal(i);
-        }
+        } 
         else {
             auto i(ineq(j, lp::lconstraint_kind::GE, rational(value)));
             TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
             c().add_literal(i);
         }
+        IF_VERBOSE(2, verbose_stream() << "unit bound j" << j << " = " << value << "\n");
         return true;
     }
 
diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp
index a990f560d..0d3708f25 100644
--- a/src/math/lp/nla_stellensatz.cpp
+++ b/src/math/lp/nla_stellensatz.cpp
@@ -156,7 +156,7 @@ namespace nla {
         new_lemma &= ex2;
         for (auto const &ineq : ineqs)
             new_lemma |= ineq;
-        IF_VERBOSE(5, verbose_stream() << "unsat \n" << new_lemma << "\n");
+        IF_VERBOSE(2, verbose_stream() << "stellensatz unsat \n" << new_lemma << "\n");
         TRACE(arith, tout << "unsat\n" << new_lemma << "\n");
         c().lra_solver().settings().stats().m_nla_stellensatz++;
     }
@@ -396,7 +396,7 @@ namespace nla {
     rational stellensatz::mvalue(lp::lar_term const &t) const {
         rational r(0);
         for (auto cv : t)
-            r += c().val(cv.j()) * cv.coeff();
+            r += m_values[cv.j()] * cv.coeff();
         return r;
     }
 
@@ -549,14 +549,13 @@ namespace nla {
         for (auto ci : constraints.indices()) 
             insert_monomials_from_constraint(ci);                    
 
-        auto &constraints = m_solver.lra().constraints();
         unsigned initial_false_constraints = m_false_constraints.size();
         for (unsigned it = 0; it < m_false_constraints.size(); ++it) {
             if (it > 10 * initial_false_constraints)
                 break;
             auto ci1 = m_false_constraints[it];
             auto const &con = constraints[ci1];
-            lpvar j = find_max_lex_monomial(con.lhs());
+            auto [j, coeff] = find_max_lex_monomial(con.lhs());
             if (j == lp::null_lpvar)
                 continue;
             auto vars = m_mon2vars[j];
@@ -564,7 +563,6 @@ namespace nla {
                 continue;
 
             for (auto v : vars) {
-
                 if (v >= m_occurs.size())
                     continue;
                 for (unsigned cidx = 0; cidx < m_occurs[v].size(); ++cidx) {
@@ -725,6 +723,8 @@ namespace nla {
             hi_sign = -hi_sign;       
         lp::lar_term lhs;
         rational rhs;
+        VERIFY(coeff_lo != 0);
+        VERIFY(coeff_hi != 0);
         for (auto const& cv : con_lo.lhs()) {
             auto j = mk_monomial(quot_lo, cv.j());
             auto coeff = lo_sign * cv.coeff() / coeff_lo;
@@ -759,7 +759,7 @@ namespace nla {
                    display_constraint(verbose_stream() << hi << ": ", hi) << "\n";
                    verbose_stream() << "rhs " << con_lo.rhs() << " " << con_hi.rhs() << "\n");
         if (lhs.size() == 0) {
-            IF_VERBOSE(2, verbose_stream() << rhs << " " << "empty\n");
+            IF_VERBOSE(2, verbose_stream() << "0 <= " << rhs << "\n");
             return;
         }
         resolvent_justification just(r);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 1695f5e41..e56043573 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1039,7 +1039,7 @@ namespace arith {
             break;
         }
 
-        if (!check_delayed_eqs())
+        if (false && !check_delayed_eqs())
             return sat::check_result::CR_CONTINUE;
 
         switch (check_nla()) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 15c60f0a2..475dcfc79 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3477,9 +3477,6 @@ public:
             set_evidence(ev.ci(), m_core, m_eqs);
         if (m_eqs.empty() && all_of(m_core, [&](literal l) { return ctx().get_assignment(l) == l_false; }))
             is_conflict = true;
-        for (auto l : m_core) {
-            IF_VERBOSE(1, verbose_stream() << l << " " << ctx().get_assignment(l) << "\n");
-        }
 
         TRACE(arith_conflict,
               tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");