diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h
index dcc68d8e1..b8c705891 100644
--- a/src/nlsat/nlsat_types.h
+++ b/src/nlsat/nlsat_types.h
@@ -115,12 +115,13 @@ namespace nlsat {
         switch (k) {
         case atom::kind::EQ: return out << "=";
         case atom::kind::LT: return out << "<";
+        case atom::kind::GT: return out << ">";
         case atom::kind::ROOT_EQ: return out << "= root";
         case atom::kind::ROOT_LT: return out << "< root";
         case atom::kind::ROOT_LE: return out << "<= root";
         case atom::kind::ROOT_GT: return out << "> root";
         case atom::kind::ROOT_GE: return out << ">= root";
-        default: UNREACHABLE();
+        default: return out << (int)k;
         }
         return out;
     }
diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp
index fb9e85b8b..a76cd1213 100644
--- a/src/nlsat/tactic/goal2nlsat.cpp
+++ b/src/nlsat/tactic/goal2nlsat.cpp
@@ -29,7 +29,7 @@ Notes:
 #include"expr2var.h"
 #include"arith_decl_plugin.h"
 #include"tactic.h"
-#include"ast_smt2_pp.h"
+#include"ast_pp.h"
 #include"polynomial.h"
 #include"algebraic_numbers.h"
 
@@ -126,7 +126,7 @@ struct goal2nlsat::imp {
         m_qm.neg(d2);
         polynomial_ref p(m_pm);
         p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2);
-        TRACE("goal2nlsat_bug", tout << "p: " << p << "\nk: " << k << "\n";);
+        TRACE("goal2nlsat_bug", tout << mk_pp(f, m) << " p: " << p << "\nk: " << k << "\n";);
         if (is_const(p)) {
             int sign;
             if (is_zero(p))
@@ -194,7 +194,7 @@ struct goal2nlsat::imp {
                 switch (to_app(f)->get_decl_kind()) {
                 case OP_TRUE:
                 case OP_FALSE:
-                    TRACE("goal2nlsat", tout << "f: " << mk_ismt2_pp(f, m) << "\n";);
+                    TRACE("goal2nlsat", tout << "f: " << mk_pp(f, m) << "\n";);
                     throw tactic_exception("apply simplify before applying nlsat");
                 case OP_AND:
                 case OP_OR:
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 7318ba06a..2846fd03e 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include "ast_util.h"
 #include "tseitin_cnf_tactic.h"
 #include "expr_safe_replace.h"
+#include "ast_pp.h"
 
 namespace qe {
 
@@ -285,6 +286,7 @@ namespace qe {
             }
             nlsat::var_vector vs;
             m_solver.vars(l, vs);
+            TRACE("qe", m_solver.display(tout, l); tout << "\n";);
             for (unsigned i = 0; i < vs.size(); ++i) {
                 level.merge(m_rvar2level[vs[i]]);
             }
@@ -542,15 +544,20 @@ namespace qe {
                     }
                     else if (m_t2x.is_var(v)) {
                         nlsat::var w = m_t2x.to_var(v);
+                        TRACE("qe", tout << mk_pp(v, m) << " |-> " << w << "\n";);
                         m_bound_rvars.back().push_back(w);
                         m_rvar2level.setx(w, lvl, max_level());
                     }
+                    else {
+                        TRACE("qe", tout << mk_pp(v, m) << " not found\n";);
+                    }
                 }
             }
             init_var2expr();
             m_is_true = nlsat::literal(m_a2b.to_var(is_true), false);
             // insert literals from arithmetical sub-formulas
             nlsat::atom_vector const& atoms = m_solver.get_atoms();
+            TRACE("qe", m_solver.display(tout); );
             for (unsigned i = 0; i < atoms.size(); ++i) {
                 if (atoms[i]) {
                     get_level(nlsat::literal(i, false));
diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp
index 2bb9ef75c..75fbcc3f4 100644
--- a/src/tactic/smtlogics/nra_tactic.cpp
+++ b/src/tactic/smtlogics/nra_tactic.cpp
@@ -38,7 +38,7 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
     return and_then(mk_simplify_tactic(m, p),
                     mk_nnf_tactic(m, p),
                     mk_propagate_values_tactic(m, p),
-                    mk_qe_lite_tactic(m), 
+                    //mk_qe_lite_tactic(m), 
                     mk_qe_tactic(m, p),
                     cond(mk_is_qfnra_probe(),
                          or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),