diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 056df3b69..50cd31661 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -563,18 +563,15 @@ bool core::var_is_fixed(lpvar j) const {
 bool core::var_is_free(lpvar j) const {
     return lra.column_is_free(j);
 }
-
     
 std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
     lra.print_term_as_indices(in.term(), out);
-    out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs();
-    return out;
+    return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs();
 }
 
 std::ostream & core::print_var(lpvar j, std::ostream & out) const {
-    if (is_monic_var(j)) {
+    if (is_monic_var(j)) 
         print_monic(m_emons[j], out);
-    }
         
     lra.print_column_info(j, out);
     signed_var jr = m_evars.find(j);
@@ -1524,9 +1521,11 @@ void core::add_bounds() {
         lpvar i = m_to_refine[(k + r) % sz];
         auto const& m = m_emons[i];
         for (lpvar j : m.vars()) {
-            if (!var_is_free(j)) continue;
+            if (!var_is_free(j))
+                continue;
             // split the free variable (j <= 0, or j > 0), and return
-            m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));  
+            m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
+            TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n");                  
             ++lp_settings().stats().m_nla_add_bounds;
             return;
         }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 2921e5018..ebfe93dfe 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1443,7 +1443,6 @@ namespace arith {
         case lp::NE: is_eq = true;     sign = true;  break;
         default: UNREACHABLE();
         }
-        TRACE("arith", tout << "is_lower: " << is_lower << " sign " << sign << "\n";);
         // TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
         // then term is used instead of ineq.m_term
         sat::literal lit;
@@ -1452,6 +1451,7 @@ namespace arith {
         else 
             lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
 
+        TRACE("arith", tout << "is_lower: " << is_lower << " sign " << sign << " " << ctx.literal2expr(lit) << "\n";);
         return sign ? ~lit : lit;                                            
     }
 
@@ -1488,6 +1488,14 @@ namespace arith {
             auto lit = mk_ineq_literal(ineq);
             ctx.mark_relevant(lit);
             s().set_phase(lit);
+            // force trichotomy axiom for equality literals
+            if (ineq.cmp() == lp::EQ) {
+                nla::lemma l;
+                l.push_back(ineq);
+                l.push_back(nla::ineq(lp::LT, ineq.term(), ineq.rs()));
+                l.push_back(nla::ineq(lp::GT, ineq.term(), ineq.rs()));
+                false_case_of_check_nla(l);
+            }
         }
         for (const nla::lemma& l : m_nla->lemmas())
             false_case_of_check_nla(l);