diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index de542f3c4..23ae179e2 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -24,7 +24,6 @@ Notes:
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "smt/tactic/smt_tactic.h"
-// include"mip_tactic.h"
 #include "tactic/arith/add_bounds_tactic.h"
 #include "tactic/arith/pb2bv_tactic.h"
 #include "tactic/arith/lia2pb_tactic.h"
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 5374ba1c1..d967660ce 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -102,13 +102,17 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
                     mk_fail_if_undecided_tactic());
 }
 
-tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
     params_ref simp_p = p;
     simp_p.set_bool("som", true); // expand into sums of monomials
+    return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic());
+}
+
+tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
 
     return and_then(mk_qfnia_premable(m, p),
-                    or_else(mk_qfnia_nlsat_solver(m, p),
-                            mk_qfnia_sat_solver(m, p),
-                            and_then(using_params(mk_simplify_tactic(m), simp_p),
-                                     mk_smt_tactic())));
+                    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)));
 }