diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index c1b2e7323..f7b8f2797 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -490,7 +490,7 @@ namespace nlsat {
         interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) {
             sign_table & table = m_sign_table_tmp;
             table.reset();
-            TRACE("nsat_evaluator", m_solver.display(tout, a) << "\n";);
+            TRACE("nsat_evaluator", m_solver.display(tout, *a) << "\n";);
             unsigned num_ps = a->size();
             var x = a->max_var();
             for (unsigned i = 0; i < num_ps; i++) {
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 471946b7b..c3563a6bc 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2644,6 +2644,7 @@ namespace nlsat {
                         del_clause(c, m_clauses);
                         if (!substitute_var(v, p, q))
                             return false;
+                        TRACE("nlsat", display(tout << "simplified\n"););
                         change = true;
                         break;
                     }
@@ -2686,21 +2687,29 @@ namespace nlsat {
                     ps.reset();
                     even.reset();
                     bool change = false;
+                    auto k = a1.get_kind();
                     for (unsigned i = 0; i < sz; ++i) {
                         poly * po = a1.p(i);
                         m_pm.substitute(po, x, q, p, pr);
-                        ps.push_back(pr);                                
-                        even.push_back(a1.is_even(i));
-                        change |= pr != po;
                         if (m_pm.is_zero(pr)) {
                             ps.reset();
                             even.reset();
                             change = true;
                             break;
                         }
+                        if (m_pm.is_const(pr)) {
+                            if (!a1.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) {
+                                k = atom::flip(k);
+                            }
+                            change = true;
+                            continue;
+                        }
+                        ps.push_back(pr);                                
+                        even.push_back(a1.is_even(i));
+                        change |= pr != po;
                     }        
                     if (!change) continue;
-                    literal l = mk_ineq_literal(a1.get_kind(), ps.size(), ps.c_ptr(), even.c_ptr()); 
+                    literal l = mk_ineq_literal(k, ps.size(), ps.c_ptr(), even.c_ptr()); 
                     if (a1.m_bool_var != l.var()) {                        
                         b2l.insert(a1.m_bool_var, l);
                         inc_ref(l);