diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 9d2aa653b..0e7fcf521 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -24,7 +24,6 @@ def init_project_def():
     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')    
@@ -33,10 +32,10 @@ def init_project_def():
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('model',  ['macros'])
     add_lib('converters', ['model'], 'ast/converters')
-    add_lib('ast_sls', ['ast','normal_forms','converters','smt_params','euf'], 'ast/sls')
+    add_lib('ast_sls', ['ast','normal_forms','converters','params','euf'], 'ast/sls')
     add_lib('sat', ['params', 'util', 'dd', 'ast_sls', 'grobner'])    
     add_lib('nlsat', ['polynomial', 'sat'])
-    add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp')
+    add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'params'], 'math/lp')
     add_lib('bit_blaster',  ['rewriter'], 'ast/rewriter/bit_blaster')
     add_lib('substitution', ['rewriter'], 'ast/substitution')
     add_lib('proofs', ['rewriter'], 'ast/proofs')
@@ -44,7 +43,7 @@ def init_project_def():
     add_lib('tactic', ['simplifiers'])
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
     add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')
-    add_lib('solver', ['params', 'smt_params', 'model', 'tactic', 'qe_lite', 'proofs'])
+    add_lib('solver', ['params', 'params', 'model', 'tactic', 'qe_lite', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
@@ -53,13 +52,13 @@ def init_project_def():
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
-    add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite', 'simplifiers', 'solver'], 'solver/assertions')
+    add_lib('solver_assertions', ['pattern','params','cmd_context','qe_lite', 'simplifiers', 'solver'], 'solver/assertions')
     add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
 
-    add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
+    add_lib('proto_model', ['model', 'rewriter', 'params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'solver_assertions',
                     'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
-    add_lib('sat_smt', ['sat', 'ast_sls', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
+    add_lib('sat_smt', ['sat', 'ast_sls', 'euf', 'smt', 'tactic', 'solver', 'params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
     add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')    
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
diff --git a/scripts/release.yml b/scripts/release.yml
index 3c79de5e4..e5a334131 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -579,7 +579,7 @@ stages:
         tagSource: 'userSpecifiedTag'
         tag: 'z3-$(ReleaseVersion)'
         title: 'z3-$(ReleaseVersion)'
-        releaseNotesSource: 'input'
+        releaseNotesSource: 'inline'
         releaseNotes: '$(ReleaseVersion) release'
         assets: '$(Agent.TempDirectory)/*.*'
         isDraft: true
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 071436200..82283dbb0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -57,7 +57,6 @@ add_subdirectory(ast/simplifiers)
 add_subdirectory(tactic)
 add_subdirectory(qe/mbp)
 add_subdirectory(qe/lite)
-add_subdirectory(smt/params)
 add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)
 add_subdirectory(sat)
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 2838bcb05..c17c0089b 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -32,7 +32,7 @@ Revision History:
 #include "ast/recfun_decl_plugin.h"
 #include "ast/special_relations_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/smt_kernel.h"
 #include "smt/smt_solver.h"
 #include "cmd_context/tactic_manager.h"
diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h
index 152f5bc76..7f1ceb9bb 100644
--- a/src/api/api_datalog.h
+++ b/src/api/api_datalog.h
@@ -20,7 +20,7 @@ Revision History:
 
 #include "api/z3.h"
 #include "ast/ast.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/smt_kernel.h"
 #include "api/api_util.h"
 
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 67886f3bd..1337562a3 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -55,6 +55,7 @@ Mam optimization?
 #include "ast/simplifiers/euf_completion.h"
 #include "ast/shared_occs.h"
 #include "params/tactic_params.hpp"
+#include "params/smt_params_helper.hpp"
 
 namespace euf {
 
@@ -111,6 +112,18 @@ namespace euf {
         }
     };
 
+    struct completion::scoped_generation {
+        completion& c;
+        unsigned m_generation = 0;
+        scoped_generation(completion& c, unsigned g): c(c) {
+            m_generation = c.m_generation;
+            c.m_generation = g;
+        }
+        ~scoped_generation() {
+            c.m_generation = m_generation;
+        }
+    };
+
     void completion::push() {
         if (m_side_condition_solver)
             m_side_condition_solver->push();
@@ -287,23 +300,26 @@ namespace euf {
         if (body.empty())
             add_constraint(head, d);
         else {
-            // create a new rule. 
-            // add all (one is actually enough) parts of the body to watch list.
-            auto r = alloc(conditional_rule, body, head, d);
+            euf::enode_vector _body;
+            for (auto* f : body)
+                _body.push_back(m_egraph.find(f)->get_root());
+            auto r = alloc(conditional_rule, _body, head, d);
             m_rules.push_back(r);
             get_trail().push(new_obj_trail(r));
             get_trail().push(push_back_vector(m_rules));
-            for (auto f : body) {
-                auto n = m_egraph.find(f)->get_root();
-                if (m.is_not(n->get_expr()))
-                    n = n->get_arg(0)->get_root();
-                m_rule_watch.reserve(n->get_id() + 1);
-                m_rule_watch[n->get_id()].push_back(r);
-                get_trail().push(push_watch_rule(m_rule_watch, n->get_id()));
-            }
+            insert_watch(_body[0], r);
         }
     }
 
+    void completion::insert_watch(enode* n, conditional_rule* r) {
+        n = n->get_root();
+        if (m.is_not(n->get_expr()))
+            n = n->get_arg(0)->get_root();
+        m_rule_watch.reserve(n->get_id() + 1);
+        m_rule_watch[n->get_id()].push_back(r);
+        get_trail().push(push_watch_rule(m_rule_watch, n->get_id()));
+    }
+
     void completion::propagate_all_rules() {
         for (auto* r : m_rules)
             if (!r->m_in_queue)
@@ -324,16 +340,20 @@ namespace euf {
     void completion::propagate_rule(conditional_rule& r) {
         if (!r.m_active)
             return;
-        for (auto* f : r.m_body) {
-            switch (eval_cond(f, r.m_dep)) {
+        for (unsigned i = r.m_watch_index; i < r.m_body.size(); ++i) {
+            auto* f = r.m_body.get(i);       
+            switch (eval_cond(f->get_expr(), r.m_dep)) {
             case l_true:
+                get_trail().push(value_trail(r.m_watch_index));
+                ++r.m_watch_index;
                 break;
             case l_false:
                 get_trail().push(value_trail(r.m_active));
                 r.m_active = false;
                 return;
             default:
-                break;
+                insert_watch(f, &r);
+                return;                
             }
         }
         if (r.m_body.empty()) {
@@ -349,10 +369,15 @@ namespace euf {
             return;
         var_subst subst(m);
         expr_ref_vector _binding(m);
-        for (unsigned i = 0; i < q->get_num_decls(); ++i)
+        unsigned max_generation = 0;
+        for (unsigned i = 0; i < q->get_num_decls(); ++i) {
             _binding.push_back(binding[i]->get_expr());
+            max_generation = std::max(max_generation, binding[i]->generation());
+        }
         expr_ref r = subst(q->get_expr(), _binding);
         IF_VERBOSE(12, verbose_stream() << "add " << r << "\n");
+
+        scoped_generation sg(*this, max_generation + 1);
         add_constraint(r, get_dependency(q));
         propagate_rules();
         m_should_propagate = true;
@@ -419,7 +444,7 @@ namespace euf {
                 continue;
             }
             if (!is_app(e)) {
-                m_nodes_to_canonize.push_back(m_egraph.mk(e, 0, 0, nullptr));
+                m_nodes_to_canonize.push_back(m_egraph.mk(e, m_generation, 0, nullptr));
                 m_todo.pop_back();
                 continue;
             }
@@ -433,7 +458,7 @@ namespace euf {
                     m_todo.push_back(arg);
             }
             if (sz == m_todo.size()) {
-                m_nodes_to_canonize.push_back(m_egraph.mk(e, 0, m_args.size(), m_args.data()));
+                m_nodes_to_canonize.push_back(m_egraph.mk(e, m_generation, m_args.size(), m_args.data()));
                 m_todo.pop_back();
             }
         }
diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h
index fb0b866e5..e7f231eed 100644
--- a/src/ast/simplifiers/euf_completion.h
+++ b/src/ast/simplifiers/euf_completion.h
@@ -52,12 +52,13 @@ namespace euf {
         };
 
         struct conditional_rule {
-            expr_ref_vector m_body;
+            euf::enode_vector m_body;
             expr_ref m_head;
             expr_dependency* m_dep;
+            unsigned m_watch_index = 0;
             bool m_active = true;
             bool m_in_queue = false;
-            conditional_rule(expr_ref_vector& b, expr_ref& h, expr_dependency* d) :
+            conditional_rule(euf::enode_vector& b, expr_ref& h, expr_dependency* d) :
                 m_body(b), m_head(h), m_dep(d) {}
         };
 
@@ -78,6 +79,7 @@ namespace euf {
         bool                   m_has_new_eq = false;
         bool                   m_should_propagate = false;
         unsigned               m_max_instantiations = std::numeric_limits<unsigned>::max();
+        unsigned               m_generation = 0;
         vector<ptr_vector<conditional_rule>> m_rule_watch;
             
         enode* mk_enode(expr* e);
@@ -104,6 +106,7 @@ namespace euf {
 
         void add_rule(expr* f, expr_dependency* d);
         void watch_rule(enode* root, enode* other);
+        void insert_watch(enode* n, conditional_rule* r);
         void propagate_rule(conditional_rule& r);
         void propagate_rules();
         void propagate_all_rules();
@@ -111,6 +114,8 @@ namespace euf {
         ptr_vector<conditional_rule> m_propagation_queue;
         struct push_watch_rule;
 
+        struct scoped_generation;
+
         bool is_gt(expr* a, expr* b) const;
     public:
         completion(ast_manager& m, dependent_expr_state& fmls);
diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt
index bfe8175e0..12692b54c 100644
--- a/src/ast/sls/CMakeLists.txt
+++ b/src/ast/sls/CMakeLists.txt
@@ -26,5 +26,5 @@ z3_add_component(ast_sls
     euf
     converters
     normal_forms
-    smt_params
+    params
 )
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 57ddb793a..58cd32834 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -26,7 +26,7 @@ Author:
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 
 namespace sls {
 
diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
index 209beae22..a51d3bf1a 100644
--- a/src/ast/sls/sls_smt_plugin.cpp
+++ b/src/ast/sls/sls_smt_plugin.cpp
@@ -20,7 +20,7 @@ Author:
 #include "ast/for_each_expr.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/ast_pp.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 
 namespace sls {
 
diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 41b3d55dc..8774a4529 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -42,7 +42,7 @@ z3_add_component(lp
     util
     polynomial
     nlsat
-    smt_params
+    params
   PYG_FILES
     lp_params_helper.pyg
 )
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 33eb4bb6a..68c97cec3 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -3,7 +3,7 @@
   Author: Nikolaj Bjorner, Lev Nachmanson
 */
 #include "math/lp/lar_solver.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 #include "lar_solver.h"
 
 
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index 3a49f6d5b..48b064567 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -20,7 +20,7 @@ Revision History:
 #include "math/lp/lp_params_helper.hpp"
 #include <memory>
 #include "util/vector.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 #include "math/lp/lp_settings_def.h"
 template bool lp::vectors_are_equal<lp::mpq>(vector<lp::mpq > const&, vector<lp::mpq> const&);
 
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index ea591e8a5..955adeb07 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -27,7 +27,7 @@
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_intervals.h"
 #include "nlsat/nlsat_solver.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 
 namespace nra {
     class solver;
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 360378e78..d8269e7f6 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -15,7 +15,7 @@
 #include "util/map.h"
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 
 
 namespace nra {
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 3479fef0d..394b217df 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -32,7 +32,7 @@ Revision History:
 #include "util/trail.h"
 #include "ast/converters/model_converter.h"
 #include "model/model2expr.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "muz/base/dl_rule_transformer.h"
 #include "ast/expr_functors.h"
 #include "muz/base/dl_engine_base.h"
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index ce1b4f638..e4a595c95 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -23,7 +23,7 @@ Revision History:
 #include "muz/rel/doc.h"
 #include "smt/smt_kernel.h"
 #include "ast/rewriter/expr_safe_replace.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 
diff --git a/src/muz/spacer/spacer_legacy_mbp.cpp b/src/muz/spacer/spacer_legacy_mbp.cpp
index 31614ed91..067192cd5 100644
--- a/src/muz/spacer/spacer_legacy_mbp.cpp
+++ b/src/muz/spacer/spacer_legacy_mbp.cpp
@@ -23,7 +23,7 @@ Notes:
 #include "ast/rewriter/bool_rewriter.h"
 #include "muz/base/dl_util.h"
 #include "ast/for_each_expr.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "model/model.h"
 #include "util/ref_vector.h"
 #include "ast/rewriter/rewriter.h"
diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp
index ce6198f0f..5d8bdb4ce 100644
--- a/src/muz/spacer/spacer_legacy_mev.cpp
+++ b/src/muz/spacer/spacer_legacy_mev.cpp
@@ -10,7 +10,7 @@ Copyright (c) 2017 Arie Gurfinkel
 #include "ast/rewriter/bool_rewriter.h"
 #include "muz/base/dl_util.h"
 #include "ast/for_each_expr.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "model/model.h"
 #include "util/ref_vector.h"
 #include "ast/rewriter/rewriter.h"
diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 76f480078..cf63f1aab 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -24,7 +24,7 @@ Revision History:
 
 #include "ast/rewriter/expr_replacer.h"
 
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 
 #include "model/model.h"
 #include "model/model_pp.h"
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 53f0384d2..dd75f86e8 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -50,7 +50,7 @@ Notes:
 #include "model/model_evaluator.h"
 #include "model/model_pp.h"
 #include "model/model_smt2_pp.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 
 #include "qe/lite/qel.h"
 #include "qe/mbp/mbp_plugin.h"
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index bacd8da7d..e60bbfae6 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -26,7 +26,7 @@ Notes:
 #include "util/params.h"
 #include "solver/solver_na2as.h"
 #include "smt/smt_kernel.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/smt_types.h"
 #include "smt/theory_opt.h"
 #include "ast/converters/generic_model_converter.h"
diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt
index 3ecf00dd4..b587b99ef 100644
--- a/src/params/CMakeLists.txt
+++ b/src/params/CMakeLists.txt
@@ -1,7 +1,17 @@
 z3_add_component(params
   SOURCES
-    pattern_inference_params.cpp
     context_params.cpp
+    dyn_ack_params.cpp	
+    pattern_inference_params.cpp
+    preprocessor_params.cpp
+    qi_params.cpp
+    smt_params.cpp
+    theory_arith_params.cpp
+    theory_array_params.cpp
+    theory_bv_params.cpp
+    theory_pb_params.cpp
+    theory_seq_params.cpp
+    theory_str_params.cpp        
   COMPONENT_DEPENDENCIES
     util
   PYG_FILES
@@ -17,6 +27,7 @@ z3_add_component(params
     sat_params.pyg
     seq_rewriter_params.pyg
     sls_params.pyg
+    smt_params_helper.pyg
     solver_params.pyg
     tactic_params.pyg
   EXTRA_REGISTER_MODULE_HEADERS
diff --git a/src/smt/params/dyn_ack_params.cpp b/src/params/dyn_ack_params.cpp
similarity index 91%
rename from src/smt/params/dyn_ack_params.cpp
rename to src/params/dyn_ack_params.cpp
index 57645903d..8e922a84d 100644
--- a/src/smt/params/dyn_ack_params.cpp
+++ b/src/params/dyn_ack_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/dyn_ack_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/dyn_ack_params.h"
+#include "params/smt_params_helper.hpp"
 
 void dyn_ack_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/dyn_ack_params.h b/src/params/dyn_ack_params.h
similarity index 100%
rename from src/smt/params/dyn_ack_params.h
rename to src/params/dyn_ack_params.h
diff --git a/src/smt/params/preprocessor_params.cpp b/src/params/preprocessor_params.cpp
similarity index 95%
rename from src/smt/params/preprocessor_params.cpp
rename to src/params/preprocessor_params.cpp
index b6b80a34e..ea389219d 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/params/preprocessor_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/preprocessor_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/preprocessor_params.h"
+#include "params/smt_params_helper.hpp"
 
 void preprocessor_params::updt_local_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/preprocessor_params.h b/src/params/preprocessor_params.h
similarity index 100%
rename from src/smt/params/preprocessor_params.h
rename to src/params/preprocessor_params.h
diff --git a/src/smt/params/qi_params.cpp b/src/params/qi_params.cpp
similarity index 96%
rename from src/smt/params/qi_params.cpp
rename to src/params/qi_params.cpp
index d6b22d9f1..708208ba2 100644
--- a/src/smt/params/qi_params.cpp
+++ b/src/params/qi_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/qi_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/qi_params.h"
+#include "params/smt_params_helper.hpp"
 
 void qi_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/qi_params.h b/src/params/qi_params.h
similarity index 100%
rename from src/smt/params/qi_params.h
rename to src/params/qi_params.h
diff --git a/src/smt/params/smt_params.cpp b/src/params/smt_params.cpp
similarity index 99%
rename from src/smt/params/smt_params.cpp
rename to src/params/smt_params.cpp
index f54f129c3..1471dcd98 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/params/smt_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/smt_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params.h"
+#include "params/smt_params_helper.hpp"
 #include "util/gparams.h"
 #include "params/solver_params.hpp"
 
diff --git a/src/smt/params/smt_params.h b/src/params/smt_params.h
similarity index 95%
rename from src/smt/params/smt_params.h
rename to src/params/smt_params.h
index 7a14aa1da..cc4082715 100644
--- a/src/smt/params/smt_params.h
+++ b/src/params/smt_params.h
@@ -19,16 +19,16 @@ Revision History:
 #pragma once
 
 #include "ast/static_features.h"
-#include "smt/params/dyn_ack_params.h"
-#include "smt/params/qi_params.h"
-#include "smt/params/theory_arith_params.h"
-#include "smt/params/theory_array_params.h"
-#include "smt/params/theory_bv_params.h"
-#include "smt/params/theory_str_params.h"
-#include "smt/params/theory_seq_params.h"
-#include "smt/params/theory_pb_params.h"
-#include "smt/params/theory_datatype_params.h"
-#include "smt/params/preprocessor_params.h"
+#include "params/dyn_ack_params.h"
+#include "params/qi_params.h"
+#include "params/theory_arith_params.h"
+#include "params/theory_array_params.h"
+#include "params/theory_bv_params.h"
+#include "params/theory_str_params.h"
+#include "params/theory_seq_params.h"
+#include "params/theory_pb_params.h"
+#include "params/theory_datatype_params.h"
+#include "params/preprocessor_params.h"
 #include "params/context_params.h"
 
 enum phase_selection {
diff --git a/src/smt/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
similarity index 100%
rename from src/smt/params/smt_params_helper.pyg
rename to src/params/smt_params_helper.pyg
diff --git a/src/smt/params/theory_arith_params.cpp b/src/params/theory_arith_params.cpp
similarity index 97%
rename from src/smt/params/theory_arith_params.cpp
rename to src/params/theory_arith_params.cpp
index 5d973a63e..fdb7a71b4 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/params/theory_arith_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/theory_arith_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/theory_arith_params.h"
+#include "params/smt_params_helper.hpp"
 #include "params/arith_rewriter_params.hpp"
 
 void theory_arith_params::updt_params(params_ref const & _p) {
diff --git a/src/smt/params/theory_arith_params.h b/src/params/theory_arith_params.h
similarity index 100%
rename from src/smt/params/theory_arith_params.h
rename to src/params/theory_arith_params.h
diff --git a/src/smt/params/theory_array_params.cpp b/src/params/theory_array_params.cpp
similarity index 90%
rename from src/smt/params/theory_array_params.cpp
rename to src/params/theory_array_params.cpp
index 2283be256..816f3db32 100644
--- a/src/smt/params/theory_array_params.cpp
+++ b/src/params/theory_array_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/theory_array_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/theory_array_params.h"
+#include "params/smt_params_helper.hpp"
 
 void theory_array_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/theory_array_params.h b/src/params/theory_array_params.h
similarity index 100%
rename from src/smt/params/theory_array_params.h
rename to src/params/theory_array_params.h
diff --git a/src/smt/params/theory_bv_params.cpp b/src/params/theory_bv_params.cpp
similarity index 92%
rename from src/smt/params/theory_bv_params.cpp
rename to src/params/theory_bv_params.cpp
index 8a3ddcf37..18acde202 100644
--- a/src/smt/params/theory_bv_params.cpp
+++ b/src/params/theory_bv_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/theory_bv_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/theory_bv_params.h"
+#include "params/smt_params_helper.hpp"
 #include "params/bv_rewriter_params.hpp"
 
 void theory_bv_params::updt_params(params_ref const & _p) {
diff --git a/src/smt/params/theory_bv_params.h b/src/params/theory_bv_params.h
similarity index 100%
rename from src/smt/params/theory_bv_params.h
rename to src/params/theory_bv_params.h
diff --git a/src/smt/params/theory_datatype_params.h b/src/params/theory_datatype_params.h
similarity index 93%
rename from src/smt/params/theory_datatype_params.h
rename to src/params/theory_datatype_params.h
index b16f4254a..4bfe83b5a 100644
--- a/src/smt/params/theory_datatype_params.h
+++ b/src/params/theory_datatype_params.h
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 
 struct theory_datatype_params {
     unsigned   m_dt_lazy_splits;
diff --git a/src/smt/params/theory_pb_params.cpp b/src/params/theory_pb_params.cpp
similarity index 87%
rename from src/smt/params/theory_pb_params.cpp
rename to src/params/theory_pb_params.cpp
index 2df8d6fee..30a168b49 100644
--- a/src/smt/params/theory_pb_params.cpp
+++ b/src/params/theory_pb_params.cpp
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include "smt/params/theory_pb_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/theory_pb_params.h"
+#include "params/smt_params_helper.hpp"
 
 void theory_pb_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/theory_pb_params.h b/src/params/theory_pb_params.h
similarity index 100%
rename from src/smt/params/theory_pb_params.h
rename to src/params/theory_pb_params.h
diff --git a/src/smt/params/theory_seq_params.cpp b/src/params/theory_seq_params.cpp
similarity index 83%
rename from src/smt/params/theory_seq_params.cpp
rename to src/params/theory_seq_params.cpp
index 290b2631d..54bf69162 100644
--- a/src/smt/params/theory_seq_params.cpp
+++ b/src/params/theory_seq_params.cpp
@@ -14,8 +14,8 @@ Revision History:
 
 --*/
 
-#include "smt/params/theory_seq_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/theory_seq_params.h"
+#include "params/smt_params_helper.hpp"
 
 void theory_seq_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/theory_seq_params.h b/src/params/theory_seq_params.h
similarity index 100%
rename from src/smt/params/theory_seq_params.h
rename to src/params/theory_seq_params.h
diff --git a/src/smt/params/theory_str_params.cpp b/src/params/theory_str_params.cpp
similarity index 96%
rename from src/smt/params/theory_str_params.cpp
rename to src/params/theory_str_params.cpp
index 7f84a6cbe..b256af715 100644
--- a/src/smt/params/theory_str_params.cpp
+++ b/src/params/theory_str_params.cpp
@@ -15,8 +15,8 @@ Revision History:
 
 --*/
 
-#include "smt/params/theory_str_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/theory_str_params.h"
+#include "params/smt_params_helper.hpp"
 
 void theory_str_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
diff --git a/src/smt/params/theory_str_params.h b/src/params/theory_str_params.h
similarity index 100%
rename from src/smt/params/theory_str_params.h
rename to src/params/theory_str_params.h
diff --git a/src/qe/qe.h b/src/qe/qe.h
index 05251a2e0..2fd36596d 100644
--- a/src/qe/qe.h
+++ b/src/qe/qe.h
@@ -21,7 +21,7 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "util/statistics.h"
 #include "util/lbool.h"
 #include "ast/expr_functors.h"
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 334999411..2fac002d0 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -20,6 +20,7 @@ Notes:
 
 --*/
 
+#include "params/smt_params.h"
 #include "ast/expr_abstract.h"
 #include "ast/ast_util.h"
 #include "ast/occurs.h"
@@ -31,7 +32,6 @@ Notes:
 #include "model/model_evaluator.h"
 #include "model/model_evaluator_params.hpp"
 #include "smt/smt_kernel.h"
-#include "smt/params/smt_params.h"
 #include "smt/smt_solver.h"
 #include "solver/solver.h"
 #include "solver/mus.h"
diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index 02aa22806..d66410879 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -52,6 +52,6 @@ z3_add_component(sat_smt
     ast
     euf
     mbp
-    smt_params
+    params
 )
 
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index b6749d99f..12ace1a24 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -31,7 +31,7 @@ Author:
 #include "sat/smt/user_solver.h"
 #include "sat/smt/euf_relevancy.h"
 #include "sat/smt/euf_proof_checker.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 
 
 namespace euf {
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 86a719d18..15bca05da 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -20,7 +20,7 @@ Author:
 #include "sat/smt/sat_smt.h"
 #include "ast/euf/euf_egraph.h"
 #include "model/model.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 
 namespace euf {
 
diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 5025483e7..5599b15ee 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -21,7 +21,7 @@ Revision History:
 #include<time.h>
 #include<signal.h>
 #include "util/stopwatch.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/reg_decl_plugins.h"
 #include "muz/rel/dl_compiler.h"
diff --git a/src/smt/dyn_ack.h b/src/smt/dyn_ack.h
index 7f33e57e5..00c220c43 100644
--- a/src/smt/dyn_ack.h
+++ b/src/smt/dyn_ack.h
@@ -19,7 +19,7 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
-#include "smt/params/dyn_ack_params.h"
+#include "params/dyn_ack_params.h"
 #include "util/obj_hashtable.h"
 #include "util/obj_pair_hashtable.h"
 #include "util/obj_triple_hashtable.h"
diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h
index 4478245f9..9cda34b0b 100644
--- a/src/smt/expr_context_simplifier.h
+++ b/src/smt/expr_context_simplifier.h
@@ -20,7 +20,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/obj_hashtable.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/smt_kernel.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/bool_rewriter.h"
diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt
deleted file mode 100644
index d7ebb2be2..000000000
--- a/src/smt/params/CMakeLists.txt
+++ /dev/null
@@ -1,18 +0,0 @@
-z3_add_component(smt_params
-  SOURCES
-    dyn_ack_params.cpp
-    preprocessor_params.cpp
-    qi_params.cpp
-    smt_params.cpp
-    theory_arith_params.cpp
-    theory_array_params.cpp
-    theory_bv_params.cpp
-    theory_pb_params.cpp
-    theory_seq_params.cpp
-    theory_str_params.cpp
-  COMPONENT_DEPENDENCIES
-    params
-    ast
-  PYG_FILES
-    smt_params_helper.pyg
-)
diff --git a/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt
index 4ade7e538..ba894f2cf 100644
--- a/src/smt/proto_model/CMakeLists.txt
+++ b/src/smt/proto_model/CMakeLists.txt
@@ -4,5 +4,5 @@ z3_add_component(proto_model
   COMPONENT_DEPENDENCIES
     model
     rewriter
-    smt_params
+    params
 )
diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h
index 27589eee3..7265875ef 100644
--- a/src/smt/qi_queue.h
+++ b/src/smt/qi_queue.h
@@ -25,7 +25,7 @@ Revision History:
 #include "smt/smt_checker.h"
 #include "smt/smt_quantifier.h"
 #include "smt/fingerprints.h"
-#include "smt/params/qi_params.h"
+#include "params/qi_params.h"
 #include "ast/cost_evaluator.h"
 #include "util/statistics.h"
 
diff --git a/src/smt/smt_case_split_queue.h b/src/smt/smt_case_split_queue.h
index a84b5ea4f..5c1b8c8ee 100644
--- a/src/smt/smt_case_split_queue.h
+++ b/src/smt/smt_case_split_queue.h
@@ -20,7 +20,7 @@ Revision History:
 
 #include "smt/smt_types.h"
 #include "util/heap.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 
 namespace smt {
     class context;
diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h
index 0d645f76f..96de16e48 100644
--- a/src/smt/smt_conflict_resolution.h
+++ b/src/smt/smt_conflict_resolution.h
@@ -24,7 +24,7 @@ Revision History:
 #include "smt/smt_enode.h"
 #include "smt/dyn_ack.h"
 #include "util/obj_pair_hashtable.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "util/obj_pair_hashtable.h"
 #include "util/map.h"
 #include "smt/watch_list.h"
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index a0df5c52f..85efd5620 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -21,7 +21,7 @@ Revision History:
 #include "smt/smt_lookahead.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_util.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params_helper.hpp"
 
 namespace smt {
 
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 46d51f9a0..fec9e2df5 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -24,8 +24,8 @@ Revision History:
 #include "ast/ast.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/normal_forms/defined_names.h"
-#include "smt/params/qi_params.h"
-#include "smt/params/smt_params.h"
+#include "params/qi_params.h"
+#include "params/smt_params.h"
 
 class proto_model;
 class model;
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index 90f7419d4..a42c465f5 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -19,7 +19,7 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 
 struct static_features;
 namespace smt {
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 6eff267e4..f7737b8a6 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -23,8 +23,8 @@ Notes:
 #include "ast/ast_pp.h"
 #include "ast/func_decl_dependencies.h"
 #include "smt/smt_kernel.h"
-#include "smt/params/smt_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params.h"
+#include "params/smt_params_helper.hpp"
 #include "solver/solver_na2as.h"
 #include "solver/mus.h"
 
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index f34f0c98b..f5a7a18ab 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -29,7 +29,7 @@ and V is a value (true or false) and x is a subterm
 
 #include "smt/tactic/ctx_solver_simplify_tactic.h"
 #include "ast/arith_decl_plugin.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/smt_kernel.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/mk_simplified_app.h"
diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 587ed9b56..7d01ce2ce 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -21,8 +21,8 @@ Notes:
 #include "ast/ast_util.h"
 #include "ast/ast_ll_pp.h"
 #include "smt/smt_kernel.h"
-#include "smt/params/smt_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params.h"
+#include "params/smt_params_helper.hpp"
 #include "smt/smt_solver.h"
 #include "tactic/tactic.h"
 #include "tactic/tactical.h"
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index e2bc5e7a4..3cfb870a1 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -30,7 +30,7 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "model/numeral_factory.h"
 #include "smt/smt_theory.h"
-#include "smt/params/theory_arith_params.h"
+#include "params/theory_arith_params.h"
 #include "smt/arith_eq_adapter.h"
 #include "smt/smt_context.h"
 #include "smt/old_interval.h"
diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h
index b170b88e9..9fc9dd44d 100644
--- a/src/smt/theory_array.h
+++ b/src/smt/theory_array.h
@@ -19,7 +19,7 @@ Revision History:
 #pragma once
 
 #include "smt/theory_array_base.h"
-#include "smt/params/theory_array_params.h"
+#include "params/theory_array_params.h"
 #include "util/union_find.h"
 
 namespace smt {
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 0a7d4bbb2..f46a9ce70 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -24,7 +24,7 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "model/numeral_factory.h"
 #include "smt/smt_theory.h"
-#include "smt/params/theory_bv_params.h"
+#include "params/theory_bv_params.h"
 
 namespace smt {
     
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index d64cc9388..8a61ce5bd 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -24,7 +24,7 @@ Revision History:
 #include "ast/datatype_decl_plugin.h"
 #include "model/datatype_factory.h"
 #include "smt/smt_theory.h"
-#include "smt/params/theory_datatype_params.h"
+#include "params/theory_datatype_params.h"
 
 namespace smt {
     class theory_datatype : public theory {
diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index 0a2987f8d..45ec93c08 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -21,7 +21,7 @@ TODO: eager equality propagation
 #pragma once
 
 #include "smt/theory_arith.h"
-#include "smt/params/theory_arith_params.h"
+#include "params/theory_arith_params.h"
 #include "ast/arith_decl_plugin.h"
 #include "smt/arith_eq_adapter.h"
 #include "smt/theory_opt.h"
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index a613c8012..9a818bc10 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -32,7 +32,7 @@ Revision History:
 #include "smt/smt_theory.h"
 #include "smt/diff_logic.h"
 #include "smt/smt_justification.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/arith_eq_adapter.h"
 #include "smt/smt_model_generator.h"
 #include "smt/smt_clause.h"
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index f713877b3..353f4aeeb 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -25,7 +25,7 @@ Notes:
 #include "ast/pb_decl_plugin.h"
 #include "smt/smt_clause.h"
 #include "smt/smt_b_justification.h"
-#include "smt/params/theory_pb_params.h"
+#include "params/theory_pb_params.h"
 #include "math/simplex/simplex.h"
 
 namespace smt {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 47d69345a..f462beff7 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -27,7 +27,7 @@
 #include "ast/seq_decl_plugin.h"
 #include "model/value_factory.h"
 #include "smt/smt_theory.h"
-#include "smt/params/theory_str_params.h"
+#include "params/theory_str_params.h"
 #include "smt/smt_model_generator.h"
 #include "smt/smt_arith_value.h"
 #include "smt/smt_kernel.h"
diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt
index 4c5f8b428..86316c86e 100644
--- a/src/solver/CMakeLists.txt
+++ b/src/solver/CMakeLists.txt
@@ -17,7 +17,7 @@ z3_add_component(solver
   COMPONENT_DEPENDENCIES
     model
     tactic
-    smt_params
+    params
     qe_lite
   PYG_FILES
     combined_solver_params.pyg
diff --git a/src/solver/assertions/CMakeLists.txt b/src/solver/assertions/CMakeLists.txt
index a1348fca2..c060eb6f9 100644
--- a/src/solver/assertions/CMakeLists.txt
+++ b/src/solver/assertions/CMakeLists.txt
@@ -3,7 +3,7 @@ z3_add_component(solver_assertions
     asserted_formulas.cpp
   COMPONENT_DEPENDENCIES
     smt2parser
-    smt_params
+    params
     qe_lite
     solver
 )
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index 7c50ad1e1..262499ff4 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -37,7 +37,7 @@ Revision History:
 #include "ast/normal_forms/pull_quant.h"
 #include "ast/normal_forms/elim_term_ite.h"
 #include "ast/pattern/pattern_inference.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "qe/lite/qe_lite_tactic.h"
 
 
diff --git a/src/solver/solver_preprocess.cpp b/src/solver/solver_preprocess.cpp
index 1ac7bb8b4..e91c63d79 100644
--- a/src/solver/solver_preprocess.cpp
+++ b/src/solver/solver_preprocess.cpp
@@ -41,7 +41,7 @@ Notes:
 #include "ast/simplifiers/flatten_clauses.h"
 #include "ast/simplifiers/bound_simplifier.h"
 #include "ast/simplifiers/cnf_nnf.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "solver/solver_preprocess.h"
 #include "qe/lite/qe_lite_tactic.h"
 
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 4b8e28366..09568f330 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -24,8 +24,8 @@ Notes:
 #include "solver/tactic2solver.h"
 #include "solver/solver_na2as.h"
 #include "solver/mus.h"
-#include "smt/params/smt_params.h"
-#include "smt/params/smt_params_helper.hpp"
+#include "params/smt_params.h"
+#include "params/smt_params_helper.hpp"
 
 
 /**
diff --git a/src/test/arith_simplifier_plugin.cpp b/src/test/arith_simplifier_plugin.cpp
index 639fda765..be61f6aa6 100644
--- a/src/test/arith_simplifier_plugin.cpp
+++ b/src/test/arith_simplifier_plugin.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "smt/arith_eq_solver.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include <iostream>
 
 typedef rational numeral;
diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp
index d1d81245e..352e1cd88 100644
--- a/src/test/check_assumptions.cpp
+++ b/src/test/check_assumptions.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "util/memory_manager.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/ast.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
diff --git a/src/test/datalog_parser.cpp b/src/test/datalog_parser.cpp
index ee69bff8b..ef3dcbf36 100644
--- a/src/test/datalog_parser.cpp
+++ b/src/test/datalog_parser.cpp
@@ -9,7 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/arith_decl_plugin.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/reg_decl_plugins.h"
 #include <iostream>
 
diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp
index e0827ba28..1b9bed786 100644
--- a/src/test/dl_context.cpp
+++ b/src/test/dl_context.cpp
@@ -9,7 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 #include "muz/fp/datalog_parser.h"
 #include "muz/base/dl_context.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "muz/fp/dl_register_engine.h"
 
 using namespace datalog;
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index 34dc7e020..8adca3ed6 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -9,7 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "muz/rel/dl_table_relation.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "util/stopwatch.h"
 #include "ast/reg_decl_plugins.h"
 #include "muz/rel/dl_relation_manager.h"
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index e05bc07f5..24581e4fd 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -13,7 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/sorting_network.h"
 #include "smt/smt_kernel.h"
 #include "model/model_smt2_pp.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/ast_util.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/th_rewriter.h"
diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp
index c66681c1b..a1a8d7e4e 100644
--- a/src/test/expr_substitution.cpp
+++ b/src/test/expr_substitution.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "ast/expr_substitution.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/substitution/substitution.h"
 #include "ast/substitution/unifier.h"
 #include "ast/bv_decl_plugin.h"
diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp
index 415a5772c..37607e853 100644
--- a/src/test/model_retrieval.cpp
+++ b/src/test/model_retrieval.cpp
@@ -6,7 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 
 #include "ast/ast.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "smt/smt_context.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp
index 8772fec92..c73a04e8d 100644
--- a/src/test/pb2bv.cpp
+++ b/src/test/pb2bv.cpp
@@ -12,7 +12,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/rewriter/pb2bv_rewriter.h"
 #include "smt/smt_kernel.h"
 #include "model/model_smt2_pp.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/ast_util.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index a505006a2..cd3b52553 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "ast/ast.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "qe/qe.h"
 #include "ast/ast_pp.h"
 #include "util/lbool.h"
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index 08c857809..416faf061 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "ast/ast.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "qe/qe.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index f67e76a04..5c171bb78 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -13,7 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/ast_util.h"
 #include "model/model_smt2_pp.h"
 #include "smt/smt_kernel.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include <iostream>
 
 struct ast_ext {
diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp
index 848223613..6bb022aad 100644
--- a/src/test/substitution.cpp
+++ b/src/test/substitution.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "ast/expr_substitution.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/substitution/substitution.h"
 #include "ast/substitution/unifier.h"
 #include "ast/bv_decl_plugin.h"
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 79fc5ff43..5f4ea1049 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -13,7 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/sorting_network.h"
 #include "smt/smt_kernel.h"
 #include "model/model_smt2_pp.h"
-#include "smt/params/smt_params.h"
+#include "params/smt_params.h"
 #include "ast/ast_util.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/th_rewriter.h"