diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 96a1c97a3..7ee8fb9d8 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -260,20 +260,9 @@ struct solver::imp {
             out.close();
         }
 
-        lbool r = l_undef;
         statistics& st = m_nla_core.lp_settings().stats().m_st;
-        try {
-            r = m_nlsat->check();
-        }
-        catch (z3_exception&) {
-            if (m_limit.is_canceled()) {
-                r = l_undef;
-            }
-            else {
-                m_nlsat->collect_statistics(st);
-                throw;
-            }
-        }
+        lbool r = m_nlsat->check();
+
         m_nlsat->collect_statistics(st);
         TRACE(nra, tout << "nra result " << r << "\n");
         CTRACE(nra, false,
@@ -406,25 +395,15 @@ struct solver::imp {
         setup_assignment_solver();
         lbool r = l_undef;
         statistics &st = m_nla_core.lp_settings().stats().m_st;
-        nlsat::literal_vector clause;
-        try {
-            nlsat::assignment rvalues(m_nlsat->am());
-            for (auto [j, x] : m_lp2nl) {
-                scoped_anum a(am());
-                am().set(a, m_nla_core.val(j).to_mpq());
-                rvalues.set(x, a);
-            }
-            r = m_nlsat->check(rvalues, clause);
-        } 
-        catch (z3_exception &) {
-            if (m_limit.is_canceled()) {
-                r = l_undef;
-            } 
-            else {
-                m_nlsat->collect_statistics(st);
-                throw;
-            }
+        nlsat::literal_vector clause;        
+        nlsat::assignment rvalues(m_nlsat->am());
+        for (auto [j, x] : m_lp2nl) {
+            scoped_anum a(am());
+            am().set(a, m_nla_core.val(j).to_mpq());
+            rvalues.set(x, a);
         }
+        r = m_nlsat->check(rvalues, clause);
+        
         m_nlsat->collect_statistics(st);
         switch (r) {
         case l_true:
@@ -657,20 +636,8 @@ struct solver::imp {
                 add_ub(lra.get_upper_bound(v), w, lra.get_column_upper_bound_witness(v));
         }
         
-        lbool r = l_undef;
-        statistics& st = m_nla_core.lp_settings().stats().m_st;
-        try {
-            r = m_nlsat->check();
-        }
-        catch (z3_exception&) {
-            if (m_limit.is_canceled()) {
-                r = l_undef;
-            }
-            else {
-                m_nlsat->collect_statistics(st);
-                throw;
-            }
-        }
+        lbool r = m_nlsat->check();
+        statistics &st = m_nla_core.lp_settings().stats().m_st;
         m_nlsat->collect_statistics(st);
         
         switch (r) {
@@ -719,18 +686,8 @@ struct solver::imp {
                 add_ub(lra.get_upper_bound(v), w);
         }
         
-        lbool r = l_undef;
-        try {
-            r = m_nlsat->check();
-        }
-        catch (z3_exception&) {
-            if (m_limit.is_canceled()) {
-                r = l_undef;
-            }
-            else {
-                throw;
-            }
-        }
+        
+        lbool r = m_nlsat->check();
 
         if (r == l_true)
             return r;
@@ -959,19 +916,68 @@ solver::~solver() {
 
 
 lbool solver::check() {
-    return m_imp->check();
+    try {
+        return m_imp->check();
+    } 
+    catch (z3_exception &) {
+        statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
+        m_imp->m_nlsat->collect_statistics(st);
+        if (m_imp->m_limit.is_canceled()) {
+            return l_undef;
+        }
+        else {
+            throw;
+        }
+    }
 }
 
 lbool solver::check(vector<dd::pdd> const& eqs) {
-    return m_imp->check(eqs);
+    try {
+        return m_imp->check(eqs);
+    } 
+    catch (z3_exception &) {
+        statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
+        m_imp->m_nlsat->collect_statistics(st);
+        if (m_imp->m_limit.is_canceled()) {
+            return l_undef;
+        }
+        else {
+            throw;
+        }
+    }
 }
 
 lbool solver::check(dd::solver::equation_vector const& eqs) {
-    return m_imp->check(eqs);
+    try {
+        return m_imp->check(eqs);
+    } 
+    catch (z3_exception &) {
+        statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
+        m_imp->m_nlsat->collect_statistics(st);
+        if (m_imp->m_limit.is_canceled()) {
+            return l_undef;
+        }
+        else {
+            throw;
+        }
+    }
 }
 
 lbool solver::check_assignment() {
-    return m_imp->check_assignment();
+    try {
+        return m_imp->check_assignment();
+    } 
+    catch (z3_exception &) {
+        statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
+        m_imp->m_nlsat->collect_statistics(st);
+        IF_VERBOSE(0, verbose_stream() << "check-assignment\n");
+        if (m_imp->m_limit.is_canceled()) {
+            return l_undef;
+        }
+        else {
+            throw;
+        }
+    }
 }
 
 bool solver::need_check() {
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index f3c36dc4c..9bc47af1e 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -96,7 +96,8 @@ static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
     params_ref simp_p = p;
     simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits.
 
-    return and_then(using_params(mk_simplify_tactic(m), simp_p),
+    return and_then(mk_report_verbose_tactic("(qfnia-sat)", 2),
+                    using_params(mk_simplify_tactic(m), simp_p),
                     mk_nla2bv_tactic(m, nia2sat_p),
                     skip_if_failed(mk_qfnia_bv_solver(m, p)),
                     mk_fail_if_undecided_tactic());
@@ -107,7 +108,8 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
     simp_p.set_bool("som", true); // expand into sums of monomials
     simp_p.set_bool("factor", false);
 
-    return and_then(using_params(mk_simplify_tactic(m), simp_p),
+    return and_then(mk_report_verbose_tactic("(qfnia-nlsat)", 2),
+                    using_params(mk_simplify_tactic(m), simp_p),
                     try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000),
                     mk_fail_if_undecided_tactic());
 }
@@ -115,14 +117,14 @@ static tactic * mk_qfnia_nlsat_solver(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(
+    return and_then(mk_report_verbose_tactic("(qfnia-smt)", 2),
         using_params(mk_simplify_tactic(m), simp_p), 
         mk_smt_tactic(m));
 }
 
 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
     return and_then(
-        mk_report_verbose_tactic("(qfnia-tactic)", 10),
+        mk_report_verbose_tactic("(qfnia-tactic)", 2),
         mk_qfnia_preamble(m, p),
         or_else(mk_qfnia_sat_solver(m, p),
                 try_for(mk_qfnia_smt_solver(m, p), 2000),