diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 45ad7e71c..5842acdfa 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -907,9 +907,9 @@ namespace nlsat {
             TRACE("nlsat_explain", tout << "adding literals for "; display_var(tout, y); tout << " -> ";
                   m_am.display_decimal(tout, y_val); tout << "\n";);
             polynomial_ref p_lower(m_pm);
-            unsigned i_lower;
+            unsigned i_lower = UINT_MAX;
             polynomial_ref p_upper(m_pm);
-            unsigned i_upper;
+            unsigned i_upper = UINT_MAX;
             polynomial_ref p(m_pm);
             unsigned sz = ps.size();
             for (unsigned k = 0; k < sz; k++) {
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
index d07dd84a3..aeca2a363 100644
--- a/src/nlsat/nlsat_interval_set.cpp
+++ b/src/nlsat/nlsat_interval_set.cpp
@@ -78,6 +78,7 @@ namespace nlsat {
             auto s = am.compare(i.m_lower, i.m_upper);
             TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper);
                   tout << "\ns: " << s << "\n";);
+            (void)s;
             SASSERT(s <= 0);
             SASSERT(!is_zero(s) || !i.m_lower_open && !i.m_upper_open);            
         }
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 0925daf32..62855b8aa 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1795,7 +1795,7 @@ namespace nlsat {
         }
 
         void resolve_clause(bool_var b, clause const & c) {
-            TRACE("nlsat_resolve", tout << "resolving clause for b: " << b << "\n";);
+            TRACE("nlsat_resolve", tout << "resolving clause for b: " << b << "\n"; display(tout, c) << "\n";);
             resolve_clause(b, c.size(), c.c_ptr());
             m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions);
         }