diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 2da7b0f21a6..a979359f303 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -21,10 +21,10 @@ def init_project_def():
     add_lib('hilbert', ['util'], 'math/hilbert')
     add_lib('automata', ['util'], 'math/automata')
     add_lib('params', ['util'])
-    add_lib('smt_params', ['params'], 'smt/params')
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
+    add_lib('smt_params', ['ast', 'params'], 'smt/params')
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('euf', ['ast'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt
index 0be62f82013..d7ebb2be2d0 100644
--- a/src/smt/params/CMakeLists.txt
+++ b/src/smt/params/CMakeLists.txt
@@ -12,6 +12,7 @@ z3_add_component(smt_params
     theory_str_params.cpp
   COMPONENT_DEPENDENCIES
     params
+    ast
   PYG_FILES
     smt_params_helper.pyg
 )
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 2636d29f38e..37249fdaca2 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -292,6 +292,18 @@ void smt_params::setup_QF_LIA(static_features const& st) {
     }
 }
 
+void smt_params::setup_QF_UFIDL() {
+    m_relevancy_lvl = 0;
+    m_arith_reflect = false;
+    m_nnf_cnf = false;
+    m_arith_eq_bounds = true;
+    m_arith_eq2ineq = true;
+    // m_params.m_phase_selection  = PS_THEORY;
+    m_restart_strategy = RS_GEOMETRIC;
+    m_restart_factor = 1.5;
+    m_restart_adaptive = false;
+}
+
 void smt_params::setup_QF_UFLIA() {
     m_relevancy_lvl       = 0;
     m_arith_reflect       = false; 
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 96e8c9ceb79..07b6b609553 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -274,6 +274,8 @@ struct smt_params : public preprocessor_params,
 
     void setup_QF_LIA(static_features const& st);
 
+    void setup_QF_UFIDL();
+
     void setup_QF_UFLIA();
 
     void setup_QF_UFLRA();
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index ef5f5493cff..aed515ef066 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -377,15 +377,7 @@ namespace smt {
 
     void setup::setup_QF_UFIDL() {
         TRACE("setup", tout << "setup_QF_UFIDL()\n";);
-        m_params.m_relevancy_lvl    = 0;
-        m_params.m_arith_reflect    = false;
-        m_params.m_nnf_cnf          = false;
-        m_params.m_arith_eq_bounds  = true;
-        m_params.m_arith_eq2ineq    = true;
-        // m_params.m_phase_selection  = PS_THEORY;
-        m_params.m_restart_strategy = RS_GEOMETRIC;
-        m_params.m_restart_factor   = 1.5;
-        m_params.m_restart_adaptive = false;
+        m_params.setup_QF_UFIDL();
         setup_lra_arith();
     }
 
@@ -624,8 +616,6 @@ namespace smt {
         }
     }
 
-
-
     void setup::setup_arith() {
         static_features    st(m_manager);
         IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);