diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
index 47b9e0505..1b633be70 100644
--- a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
+++ b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
@@ -42,26 +42,28 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
     else
         factor = mk_skip_tactic();
 
-    return and_then(and_then(using_params(mk_simplify_tactic(m, p),
-                                          main_p),
-                             using_params(mk_purify_arith_tactic(m, p),
-                                          purify_p),
-                             mk_propagate_values_tactic(m, p),
-                             mk_solve_eqs_tactic(m, p),
-                             using_params(mk_purify_arith_tactic(m, p),
-                                          purify_p),
-                             mk_elim_uncnstr_tactic(m, p),
-                             mk_elim_term_ite_tactic(m, p)),
-                    and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
-                             factor,
-                             mk_solve_eqs_tactic(m, p),
-                             using_params(mk_purify_arith_tactic(m, p),
-                                          purify_p),
-                             using_params(mk_simplify_tactic(m, p),
-                                          main_p),
-                             mk_tseitin_cnf_core_tactic(m, p),
-                             using_params(mk_simplify_tactic(m, p),
-                                          main_p),
-                             mk_nlsat_tactic(m, p)));
+    return and_then(
+        mk_report_verbose_tactic("(qfnra-nlsat-tactic)", 10),
+        and_then(using_params(mk_simplify_tactic(m, p),
+                              main_p),
+                 using_params(mk_purify_arith_tactic(m, p),
+                              purify_p),
+                 mk_propagate_values_tactic(m, p),
+                 mk_solve_eqs_tactic(m, p),
+                 using_params(mk_purify_arith_tactic(m, p),
+                              purify_p),
+                 mk_elim_uncnstr_tactic(m, p),
+                 mk_elim_term_ite_tactic(m, p)),
+        and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
+            factor,
+            mk_solve_eqs_tactic(m, p),
+            using_params(mk_purify_arith_tactic(m, p),
+                         purify_p),
+            using_params(mk_simplify_tactic(m, p),
+                         main_p),
+            mk_tseitin_cnf_core_tactic(m, p),
+            using_params(mk_simplify_tactic(m, p),
+                         main_p),
+            mk_nlsat_tactic(m, p)));
 }
 
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index a85e95b57..932ca597f 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -492,7 +492,7 @@ namespace smt {
         m_params.m_arith_eq2ineq       = true;
         m_params.m_arith_reflect       = false; 
         m_params.m_arith_propagate_eqs = false; 
-        m_params.m_nnf_cnf             = false;
+        m_params.m_nnf_cnf             = false;        
         setup_lra_arith();
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3bdd2d784..3b6af0be5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -298,13 +298,15 @@ class theory_lra::imp {
 
     void init_solver() {
         if (m_solver) return;
-        lp_params lp(ctx().get_params());
-        m_solver = alloc(lp::lar_solver); 
+
+        reset_variable_values();
         m_theory_var2var_index.reset();
+        m_solver = alloc(lp::lar_solver); 
+        lp_params lp(ctx().get_params());
         m_solver->settings().set_resource_limit(m_resource_limit);
         m_solver->settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lp.simplex_strategy());
-        reset_variable_values();
         m_solver->settings().bound_propagation() = BP_NONE != propagation_mode();
+        m_solver->settings().m_enable_hnf = lp.enable_hnf();
         m_solver->set_track_pivoted_rows(lp.bprop_on_pivoted_rows());
 
         // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
@@ -2712,7 +2714,6 @@ public:
         if (dump_lemmas()) {
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
             (void)id;
-            //SASSERT(id != 55);
         }
     }
 
@@ -2732,7 +2733,6 @@ public:
         if (dump_lemmas()) {                
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
             (void)id;
-            // SASSERT(id != 71);
         }
     }
 
diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index 36ee89a1b..4c5c17bd5 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -127,6 +127,43 @@ public:
     }
 };
 
+struct has_nlmul {
+    struct found {};
+    ast_manager& m;
+    arith_util   a;
+    has_nlmul(ast_manager& m):m(m), a(m) {}
+    
+    void throw_found(expr* e) {
+        TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(m.get_sort(e), m) << "\n";);
+        SASSERT(false);
+        throw found();
+    }
+
+    void operator()(var *) { }
+
+    void operator()(quantifier *) { }
+
+    void operator()(app * n) {
+        family_id fid = n->get_family_id();
+        if (fid == a.get_family_id()) {
+            switch (n->get_decl_kind()) {
+            case OP_MUL:
+                if (n->get_num_args() != 2 || !a.is_numeral(n->get_arg(0)))
+                    throw_found(n);
+                break;
+            case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
+                if (!a.is_numeral(n->get_arg(1)))
+                    throw_found(n);
+				break;
+            case OP_POWER:
+                throw_found(n);
+            default:
+                break;
+            }
+        }
+    }
+};
+
 probe * mk_arith_avg_degree_probe() {
     return alloc(arith_degree_probe, true);
 }
@@ -441,13 +478,13 @@ struct is_non_nira_functor {
                 if (m_linear) {
                     if (n->get_num_args() != 2)
                         throw_found(n);
-                    if (!u.is_numeral(n->get_arg(0)))
+                    if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1))) 
                         throw_found(n);
                 }
                 return;
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
                 if (m_linear && !u.is_numeral(n->get_arg(1)))
-                    throw_found(n);
+                    throw_found(n); 
                 return;
             case OP_IS_INT:
                 if (m_real)
@@ -478,27 +515,27 @@ struct is_non_nira_functor {
 
 static bool is_qfnia(goal const & g) {
     is_non_nira_functor p(g.m(), true, false, false, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_qfnra(goal const & g) {
     is_non_nira_functor p(g.m(), false, true, false, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_nia(goal const & g) {
     is_non_nira_functor p(g.m(), true, false, true, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_nra(goal const & g) {
     is_non_nira_functor p(g.m(), false, true, true, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_nira(goal const & g) {
     is_non_nira_functor p(g.m(), true, true, true, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_lra(goal const & g) {
@@ -560,12 +597,16 @@ struct is_non_qfufnra_functor {
                 }
                 return;
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
-                if (!u.is_numeral(n->get_arg(1)))
+                if (!u.is_numeral(n->get_arg(1))) {
+                    TRACE("arith", tout << "non-linear " << expr_ref(n, m) << "\n";);
                     throw_found();
+                }
                 return;
             case OP_POWER: 
-                if (!u.is_numeral(n->get_arg(1)))
+                if (!u.is_numeral(n->get_arg(1))) {
+                    TRACE("arith", tout << "non-linear " << expr_ref(n, m) << "\n";);
                     throw_found();
+                }
                 m_has_nonlinear = true;
                 return;
             case OP_IS_INT:
@@ -574,6 +615,7 @@ struct is_non_qfufnra_functor {
                 throw_found();
                 return;
             default:
+                TRACE("arith", tout << "non-linear " << expr_ref(n, m) << "\n";);
                 throw_found();
             }
         } 
diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp
index 947a41111..605232772 100644
--- a/src/tactic/fpa/qffplra_tactic.cpp
+++ b/src/tactic/fpa/qffplra_tactic.cpp
@@ -26,6 +26,23 @@ tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p) {
     return st;
 }
 
+struct is_fpa_function {
+    struct found {};
+    ast_manager & m;
+    fpa_util      fu;
+    
+    is_fpa_function(ast_manager & _m) : m(_m), fu(m) {}
+
+    void operator()(var *) { }
+
+    void operator()(quantifier *) { }
+
+    void operator()(app * n) {
+        if (n->get_family_id() == fu.get_family_id()) 
+            throw found();
+    }
+};
+
 struct is_non_qffplra_predicate {
     struct found {};
     ast_manager & m;
@@ -61,7 +78,9 @@ struct is_non_qffplra_predicate {
 class is_qffplra_probe : public probe {
 public:
     result operator()(goal const & g) override {
-        return !test<is_non_qffplra_predicate>(g);
+        return 
+            test<is_fpa_function>(g) && 
+            !test<is_non_qffplra_predicate>(g);
     }
 
     ~is_qffplra_probe() override {}
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 2ef49229a..b92e08006 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -110,9 +110,11 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
 
 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
 
-    return and_then(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),
-                            mk_qfnia_smt_solver(m, 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),
+                mk_qfnia_smt_solver(m, p)));
 }
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index e58abb4fd..1d0d20c33 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -600,6 +600,9 @@ lia_move int_solver::make_hnf_cut() {
 }
 
 lia_move int_solver::hnf_cut() {
+    if (!settings().m_enable_hnf) {
+        return lia_move::undef;
+    }
     if ((m_number_of_calls) % settings().hnf_cut_period() == 0) {
         return make_hnf_cut();
     }
diff --git a/src/util/lp/lp_params.pyg b/src/util/lp/lp_params.pyg
index 7731536f0..1ef788241 100644
--- a/src/util/lp/lp_params.pyg
+++ b/src/util/lp/lp_params.pyg
@@ -5,6 +5,7 @@ def_module_params('lp',
                    ('min', BOOL, False, 'minimize cost'),
                    ('print_stats', BOOL, False, 'print statistic'),
                    ('simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
+                   ('enable_hnf', BOOL, True, 'enable hnf cuts'),
                    ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation')
                           ))           
 
diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h
index 4e99ecc82..dd19df23a 100644
--- a/src/util/lp/lp_settings.h
+++ b/src/util/lp/lp_settings.h
@@ -197,6 +197,7 @@ public:
     bool             m_int_patch_only_integer_values;
     unsigned         limit_on_rows_for_hnf_cutter;
     unsigned         limit_on_columns_for_hnf_cutter;
+    bool             m_enable_hnf;
 
 
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }
@@ -263,7 +264,8 @@ public:
                     m_int_pivot_fixed_vars_from_basis(false),
                     m_int_patch_only_integer_values(true),
                     limit_on_rows_for_hnf_cutter(75),
-                    limit_on_columns_for_hnf_cutter(150)
+                    limit_on_columns_for_hnf_cutter(150),
+                    m_enable_hnf(true)
     {}
 
     void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }