diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a829cb200..d7b81b424 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1119,7 +1119,6 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
     }
     std::ostringstream buffer;
     buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
-    INVOKE_DEBUGGER();
     throw ast_exception(buffer.str());
 }
 
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index cc6cedac7..0ea0de103 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -995,7 +995,7 @@ namespace nlsat {
             unsigned sz = cls.size();
             for (unsigned i = 0; i < sz; i++) {
                 literal l = cls[i];
-                SASSERT(m_atoms[l.var()] == 0);
+                SASSERT(m_atoms[l.var()] == nullptr);
                 SASSERT(value(l) != l_true);
                 if (value(l) == l_false)
                     continue;
@@ -1085,13 +1085,13 @@ namespace nlsat {
                 checkpoint();
                 if (value(l) == l_false)
                     continue;
+                TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";);
                 SASSERT(value(l) == l_undef);
                 SASSERT(max_var(l) == m_xk);
                 bool_var b = l.var();
                 atom * a   = m_atoms[b];
                 SASSERT(a != nullptr);
                 interval_set_ref curr_set(m_ism);
-                TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";);
                 curr_set = m_evaluator.infeasible_intervals(a, l.sign());
                 TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n";);
                 if (m_ism.is_empty(curr_set)) {
@@ -1151,7 +1151,7 @@ namespace nlsat {
            If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0
         */
         bool process_clause(clause const & cls, bool satisfy_learned) {
-            TRACE("nlsat", display(tout << "processing clause: ", cls) << "sat: " << is_satisfied(cls) << "\n";);
+            TRACE("nlsat", display(tout << "processing clause: ", cls) << " sat: " << is_satisfied(cls) << "\n";);
             if (is_satisfied(cls))
                 return true;
             if (m_xk == null_var)
diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp
index 42ae36564..04f7f9d06 100644
--- a/src/nlsat/tactic/goal2nlsat.cpp
+++ b/src/nlsat/tactic/goal2nlsat.cpp
@@ -251,6 +251,7 @@ struct goal2nlsat::imp {
     }
 
     void operator()(goal const & g) {
+        TRACE("goal2nlsat", g.display(tout););
         if (has_term_ite(g))
             throw tactic_exception("eliminate term-ite before applying nlsat");
         unsigned sz = g.size();
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index f9ceaa26d..1074b9679 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -165,7 +165,7 @@ namespace qe {
                 lits.push_back(~l);
                 break;
             default:
-                UNREACHABLE();
+                lits.push_back(l);
                 break; 
             }
         }