diff --git a/lib/pattern_inference_params.cpp b/lib/pattern_inference_params.cpp
deleted file mode 100644
index 38fc24dca..000000000
--- a/lib/pattern_inference_params.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pattern_inference_params.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-03-24.
-
-Revision History:
-
---*/
-#include"pattern_inference_params.h"
-
-void pattern_inference_params::register_params(ini_params & p) {
-    p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns, 
-                              "when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
-    p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns,
-                          "block looping patterns during pattern inference");
-    p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith), 
-                         "0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");
-    p.register_bool_param("PI_USE_DATABASE", m_pi_use_database);
-    p.register_unsigned_param("PI_ARITH_WEIGHT", m_pi_arith_weight, "default weight for quantifiers where the only available pattern has nested arithmetic terms.");
-    p.register_unsigned_param("PI_NON_NESTED_ARITH_WEIGHT", m_pi_non_nested_arith_weight, "default weight for quantifiers where the only available pattern has non nested arithmetic terms.");
-    p.register_bool_param("PI_PULL_QUANTIFIERS", m_pi_pull_quantifiers, "pull nested quantifiers, if no pattern was found.");
-    p.register_int_param("PI_NOPAT_WEIGHT", m_pi_nopat_weight, "set weight of quantifiers without patterns, if negative the weight is not changed.");
-    p.register_bool_param("PI_AVOID_SKOLEMS", m_pi_avoid_skolems);
-    p.register_bool_param("PI_WARNINGS", m_pi_warnings, "enable/disable warning messages in the pattern inference module.");
-}
-
-
diff --git a/mk_make.py b/mk_make.py
index 723fe4027..785275a0c 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -53,7 +53,7 @@ add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'frame
                 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
 add_lib('user_plugin', ['smt'])
 add_lib('core_tactics', ['framework', 'normal_forms'])
-add_lib('arith_tactics', ['core_tactics', 'assertion_set'])
+add_lib('arith_tactics', ['core_tactics', 'assertion_set', 'sat'])
 add_lib('sat_tactic', ['framework', 'sat'])
 add_lib('sat_strategy', ['assertion_set', 'sat_tactic'])
 # TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr.
diff --git a/lib/bv2int_rewriter.cpp b/src/arith_tactics/bv2int_rewriter.cpp
similarity index 100%
rename from lib/bv2int_rewriter.cpp
rename to src/arith_tactics/bv2int_rewriter.cpp
diff --git a/lib/bv2int_rewriter.h b/src/arith_tactics/bv2int_rewriter.h
similarity index 100%
rename from lib/bv2int_rewriter.h
rename to src/arith_tactics/bv2int_rewriter.h
diff --git a/lib/bv2real_rewriter.cpp b/src/arith_tactics/bv2real_rewriter.cpp
similarity index 100%
rename from lib/bv2real_rewriter.cpp
rename to src/arith_tactics/bv2real_rewriter.cpp
diff --git a/lib/bv2real_rewriter.h b/src/arith_tactics/bv2real_rewriter.h
similarity index 100%
rename from lib/bv2real_rewriter.h
rename to src/arith_tactics/bv2real_rewriter.h
diff --git a/lib/elim_term_ite_strategy.cpp b/src/arith_tactics/elim_term_ite_strategy.cpp
similarity index 100%
rename from lib/elim_term_ite_strategy.cpp
rename to src/arith_tactics/elim_term_ite_strategy.cpp
diff --git a/lib/elim_term_ite_strategy.h b/src/arith_tactics/elim_term_ite_strategy.h
similarity index 100%
rename from lib/elim_term_ite_strategy.h
rename to src/arith_tactics/elim_term_ite_strategy.h
diff --git a/lib/smt_formula_compiler.cpp b/src/arith_tactics/smt_formula_compiler.cpp
similarity index 100%
rename from lib/smt_formula_compiler.cpp
rename to src/arith_tactics/smt_formula_compiler.cpp
diff --git a/lib/smt_formula_compiler.h b/src/arith_tactics/smt_formula_compiler.h
similarity index 100%
rename from lib/smt_formula_compiler.h
rename to src/arith_tactics/smt_formula_compiler.h
diff --git a/lib/smt_solver_exp.cpp b/src/arith_tactics/smt_solver_exp.cpp
similarity index 100%
rename from lib/smt_solver_exp.cpp
rename to src/arith_tactics/smt_solver_exp.cpp
diff --git a/lib/smt_solver_exp.h b/src/arith_tactics/smt_solver_exp.h
similarity index 100%
rename from lib/smt_solver_exp.h
rename to src/arith_tactics/smt_solver_exp.h
diff --git a/lib/smt_solver_strategy.cpp b/src/arith_tactics/smt_solver_strategy.cpp
similarity index 100%
rename from lib/smt_solver_strategy.cpp
rename to src/arith_tactics/smt_solver_strategy.cpp
diff --git a/lib/smt_solver_strategy.h b/src/arith_tactics/smt_solver_strategy.h
similarity index 100%
rename from lib/smt_solver_strategy.h
rename to src/arith_tactics/smt_solver_strategy.h
diff --git a/lib/smt_solver_types.h b/src/arith_tactics/smt_solver_types.h
similarity index 100%
rename from lib/smt_solver_types.h
rename to src/arith_tactics/smt_solver_types.h
diff --git a/lib/elim_distinct.cpp b/src/assertion_set/elim_distinct.cpp
similarity index 100%
rename from lib/elim_distinct.cpp
rename to src/assertion_set/elim_distinct.cpp
diff --git a/lib/elim_distinct.h b/src/assertion_set/elim_distinct.h
similarity index 100%
rename from lib/elim_distinct.h
rename to src/assertion_set/elim_distinct.h
diff --git a/lib/reduce_args.cpp b/src/assertion_set/reduce_args.cpp
similarity index 100%
rename from lib/reduce_args.cpp
rename to src/assertion_set/reduce_args.cpp
diff --git a/lib/reduce_args.h b/src/assertion_set/reduce_args.h
similarity index 100%
rename from lib/reduce_args.h
rename to src/assertion_set/reduce_args.h
diff --git a/lib/shallow_context_simplifier.cpp b/src/assertion_set/shallow_context_simplifier.cpp
similarity index 100%
rename from lib/shallow_context_simplifier.cpp
rename to src/assertion_set/shallow_context_simplifier.cpp
diff --git a/lib/shallow_context_simplifier.h b/src/assertion_set/shallow_context_simplifier.h
similarity index 100%
rename from lib/shallow_context_simplifier.h
rename to src/assertion_set/shallow_context_simplifier.h
diff --git a/lib/cofactor_elim_term_ite.cpp b/src/core_tactics/cofactor_elim_term_ite.cpp
similarity index 100%
rename from lib/cofactor_elim_term_ite.cpp
rename to src/core_tactics/cofactor_elim_term_ite.cpp
diff --git a/lib/cofactor_elim_term_ite.h b/src/core_tactics/cofactor_elim_term_ite.h
similarity index 100%
rename from lib/cofactor_elim_term_ite.h
rename to src/core_tactics/cofactor_elim_term_ite.h
diff --git a/lib/cofactor_term_ite_tactic.cpp b/src/core_tactics/cofactor_term_ite_tactic.cpp
similarity index 100%
rename from lib/cofactor_term_ite_tactic.cpp
rename to src/core_tactics/cofactor_term_ite_tactic.cpp
diff --git a/lib/cofactor_term_ite_tactic.h b/src/core_tactics/cofactor_term_ite_tactic.h
similarity index 100%
rename from lib/cofactor_term_ite_tactic.h
rename to src/core_tactics/cofactor_term_ite_tactic.h
diff --git a/lib/symmetry_reduce_tactic.cpp b/src/core_tactics/symmetry_reduce_tactic.cpp
similarity index 100%
rename from lib/symmetry_reduce_tactic.cpp
rename to src/core_tactics/symmetry_reduce_tactic.cpp
diff --git a/lib/symmetry_reduce_tactic.h b/src/core_tactics/symmetry_reduce_tactic.h
similarity index 100%
rename from lib/symmetry_reduce_tactic.h
rename to src/core_tactics/symmetry_reduce_tactic.h
diff --git a/lib/assertion_stack.cpp b/src/dead/assertion_stack.cpp
similarity index 100%
rename from lib/assertion_stack.cpp
rename to src/dead/assertion_stack.cpp
diff --git a/lib/assertion_stack.h b/src/dead/assertion_stack.h
similarity index 100%
rename from lib/assertion_stack.h
rename to src/dead/assertion_stack.h
diff --git a/lib/parameters.h b/src/dead/parameters.h
similarity index 100%
rename from lib/parameters.h
rename to src/dead/parameters.h
diff --git a/lib/smt_classifier.h b/src/dead/smt_classifier.h
similarity index 100%
rename from lib/smt_classifier.h
rename to src/dead/smt_classifier.h
diff --git a/lib/st_cmds.h b/src/dead/st_cmds.h
similarity index 100%
rename from lib/st_cmds.h
rename to src/dead/st_cmds.h
diff --git a/lib/dbg_cmds.cpp b/src/extra_cmds/dbg_cmds.cpp
similarity index 100%
rename from lib/dbg_cmds.cpp
rename to src/extra_cmds/dbg_cmds.cpp
diff --git a/lib/dbg_cmds.h b/src/extra_cmds/dbg_cmds.h
similarity index 100%
rename from lib/dbg_cmds.h
rename to src/extra_cmds/dbg_cmds.h
diff --git a/lib/polynomial_cmds.cpp b/src/extra_cmds/polynomial_cmds.cpp
similarity index 100%
rename from lib/polynomial_cmds.cpp
rename to src/extra_cmds/polynomial_cmds.cpp
diff --git a/lib/polynomial_cmds.h b/src/extra_cmds/polynomial_cmds.h
similarity index 100%
rename from lib/polynomial_cmds.h
rename to src/extra_cmds/polynomial_cmds.h
diff --git a/lib/subpaving_cmds.cpp b/src/extra_cmds/subpaving_cmds.cpp
similarity index 100%
rename from lib/subpaving_cmds.cpp
rename to src/extra_cmds/subpaving_cmds.cpp
diff --git a/lib/subpaving_cmds.h b/src/extra_cmds/subpaving_cmds.h
similarity index 100%
rename from lib/subpaving_cmds.h
rename to src/extra_cmds/subpaving_cmds.h
diff --git a/lib/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp
similarity index 100%
rename from lib/datalog_parser.cpp
rename to src/muz_qe/datalog_parser.cpp
diff --git a/lib/datalog_parser.h b/src/muz_qe/datalog_parser.h
similarity index 100%
rename from lib/datalog_parser.h
rename to src/muz_qe/datalog_parser.h
diff --git a/src/arith_tactics/vsubst_tactic.cpp b/src/muz_qe/vsubst_tactic.cpp
similarity index 100%
rename from src/arith_tactics/vsubst_tactic.cpp
rename to src/muz_qe/vsubst_tactic.cpp
diff --git a/src/arith_tactics/vsubst_tactic.h b/src/muz_qe/vsubst_tactic.h
similarity index 100%
rename from src/arith_tactics/vsubst_tactic.h
rename to src/muz_qe/vsubst_tactic.h