diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 4bccdf6bb..b9641c869 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -55,7 +55,6 @@ def init_project_def():
     add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
-    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic'], 'tactic/fpa')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
     add_lib('qe', ['smt','sat'], 'qe')
     add_lib('duality', ['smt', 'interp', 'qe'])
@@ -71,6 +70,7 @@ def init_project_def():
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
     add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
     add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
+    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 4854b3c07..12c127a37 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -23,6 +23,8 @@ Notes:
 #include"fpa2bv_tactic.h"
 #include"smt_tactic.h"
 #include"propagate_values_tactic.h"
+#include"probe_arith.h"
+#include"qfnra_tactic.h"
 
 #include"qffp_tactic.h"
 
@@ -40,10 +42,13 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
                                      mk_propagate_values_tactic(m, p),
                                      using_params(mk_simplify_tactic(m, p), simp_p),                                 
                                      mk_bit_blaster_tactic(m, p),
-                                     using_params(mk_simplify_tactic(m, p), simp_p),                                 
+                                     using_params(mk_simplify_tactic(m, p), simp_p),
                                      cond(mk_is_propositional_probe(),
                                         mk_sat_tactic(m, p),
-                                        mk_smt_tactic(p)),
+                                        cond(mk_is_qfnra_probe(),
+                                            mk_qfnra_tactic(m, p),
+                                            mk_smt_tactic(p))
+                                        ),
                                      mk_fail_if_undecided_tactic())));
 
     st->updt_params(p);