diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp
index 72c486c24..4f5eb5ed0 100644
--- a/src/tactic/portfolio/default_tactic.cpp
+++ b/src/tactic/portfolio/default_tactic.cpp
@@ -44,8 +44,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
                                         cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                         cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
                                         cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
-                                        cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
-                                             mk_smt_tactic())))))))))))),
+                                        //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
+                                             mk_smt_tactic()))))))))))),
                                p);
     return st;
 }
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 27d7433e8..c868fdcb9 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -86,8 +86,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_qffpbv_tactic(m, p);
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
-    else if (logic=="QF_UFNRA")
-        return mk_qfufnra_tactic(m, p);
+    //else if (logic=="QF_UFNRA")
+    //    return mk_qfufnra_tactic(m, p);
     else 
         return mk_default_tactic(m, p);
 }