diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 0a58740d1..c09fc695d 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -327,7 +327,6 @@ class nla2bv_tactic : public tactic {
             }
             void operator()(app* n) { 
                 if (a.is_int(n) && is_uninterp_const(n)) {
-                    TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";);
                     m_vars.push_back(n);
                 }
                 else if (a.is_real(n) && is_uninterp_const(n)) {
@@ -371,7 +370,7 @@ class nla2bv_tactic : public tactic {
                 add_var(fe_var.vars()[i]);
             }
             if (!fe_var.is_supported()) return not_supported;
-            if (!fe_var.vars().empty()) return is_bool;
+            if (fe_var.vars().empty()) return is_bool;
             return has_num;
         }
         
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 528a6c048..a9a6032f1 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -117,11 +117,10 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
     return and_then(
         mk_report_verbose_tactic("(qfnia-tactic)", 10),
         mk_qfnia_premable(m, p),
-        mk_qfnia_sat_solver(m, p)
                 
-//        or_else(mk_qfnia_sat_solver(m, p),
-//                try_for(mk_qfnia_smt_solver(m, p), 2000),
-//                mk_qfnia_nlsat_solver(m, p),
-//                mk_qfnia_smt_solver(m, p))
+        or_else(mk_qfnia_sat_solver(m, p),
+                try_for(mk_qfnia_smt_solver(m, p), 2000),
+                mk_qfnia_nlsat_solver(m, p),
+                mk_qfnia_smt_solver(m, p))
         );
 }