diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 150770bb6..c08b0774f 100755
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -63,7 +63,7 @@ bool intervals::get_lemma(monomial const& m) {
             svector<lp::constraint_index> expl;
             m_dep_manager.linearize(signs_a.m_upper_dep, expl); 
             _().current_expl().add_expl(expl);
-            llc cmp = m_config.lower_is_open(a)? llc::LT: llc::LE;
+            llc cmp = m_config.upper_is_open(a)? llc::LT: llc::LE;
             mk_ineq(m.var(), cmp,  ub.x);
             TRACE("nla_solver", _().print_lemma(tout); );
             return true;
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 87f13ced5..4d318eec6 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -118,12 +118,12 @@ 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),
-        or_else(mk_qfnia_sat_solver(m, p),
-             try_for(mk_qfnia_smt_solver(m, p), 2000),
-            mk_qfnia_nlsat_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))
-            )
+            // )
         ;
 }