diff --git a/mk_make.py b/mk_make.py
index 288f4dfbc..2896f6828 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -51,9 +51,13 @@ add_lib('proof_checker', ['rewriter', 'spc'])
 add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'framework', 'assertion_set'])
 add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'framework', 
                 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
+add_lib('user_ext', ['smt'])
+add_lib('core_tactics', ['framework', 'normal_forms'])
+add_lib('arith_tactics', ['core_tactics', 'assertion_set'])
 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.
 add_lib('muz_qe', ['smt', 'sat', 'smt2parser'])
+add_lib('aig', ['framework', 'assertion_set'])
 # TODO: delete SMT 1.0 frontend
 add_lib('smtparser', ['api_headers', 'smt', 'spc'])
diff --git a/lib/aig.cpp b/src/aig/aig.cpp
similarity index 100%
rename from lib/aig.cpp
rename to src/aig/aig.cpp
diff --git a/lib/aig.h b/src/aig/aig.h
similarity index 100%
rename from lib/aig.h
rename to src/aig/aig.h
diff --git a/lib/aig_tactic.cpp b/src/aig/aig_tactic.cpp
similarity index 100%
rename from lib/aig_tactic.cpp
rename to src/aig/aig_tactic.cpp
diff --git a/lib/aig_tactic.h b/src/aig/aig_tactic.h
similarity index 100%
rename from lib/aig_tactic.h
rename to src/aig/aig_tactic.h
diff --git a/lib/api_arith.cpp b/src/api/api_arith.cpp
similarity index 100%
rename from lib/api_arith.cpp
rename to src/api/api_arith.cpp
diff --git a/lib/api_array.cpp b/src/api/api_array.cpp
similarity index 100%
rename from lib/api_array.cpp
rename to src/api/api_array.cpp
diff --git a/lib/api_ast.cpp b/src/api/api_ast.cpp
similarity index 100%
rename from lib/api_ast.cpp
rename to src/api/api_ast.cpp
diff --git a/lib/api_ast_map.cpp b/src/api/api_ast_map.cpp
similarity index 100%
rename from lib/api_ast_map.cpp
rename to src/api/api_ast_map.cpp
diff --git a/lib/api_ast_map.h b/src/api/api_ast_map.h
similarity index 100%
rename from lib/api_ast_map.h
rename to src/api/api_ast_map.h
diff --git a/lib/api_ast_vector.cpp b/src/api/api_ast_vector.cpp
similarity index 100%
rename from lib/api_ast_vector.cpp
rename to src/api/api_ast_vector.cpp
diff --git a/lib/api_ast_vector.h b/src/api/api_ast_vector.h
similarity index 100%
rename from lib/api_ast_vector.h
rename to src/api/api_ast_vector.h
diff --git a/lib/api_bv.cpp b/src/api/api_bv.cpp
similarity index 100%
rename from lib/api_bv.cpp
rename to src/api/api_bv.cpp
diff --git a/lib/api_commands.cpp b/src/api/api_commands.cpp
similarity index 100%
rename from lib/api_commands.cpp
rename to src/api/api_commands.cpp
diff --git a/lib/api_config_params.cpp b/src/api/api_config_params.cpp
similarity index 100%
rename from lib/api_config_params.cpp
rename to src/api/api_config_params.cpp
diff --git a/lib/api_config_params.h b/src/api/api_config_params.h
similarity index 100%
rename from lib/api_config_params.h
rename to src/api/api_config_params.h
diff --git a/lib/api_context.cpp b/src/api/api_context.cpp
similarity index 100%
rename from lib/api_context.cpp
rename to src/api/api_context.cpp
diff --git a/lib/api_context.h b/src/api/api_context.h
similarity index 100%
rename from lib/api_context.h
rename to src/api/api_context.h
diff --git a/lib/api_datalog.cpp b/src/api/api_datalog.cpp
similarity index 100%
rename from lib/api_datalog.cpp
rename to src/api/api_datalog.cpp
diff --git a/lib/api_datalog.h b/src/api/api_datalog.h
similarity index 100%
rename from lib/api_datalog.h
rename to src/api/api_datalog.h
diff --git a/lib/api_datatype.cpp b/src/api/api_datatype.cpp
similarity index 100%
rename from lib/api_datatype.cpp
rename to src/api/api_datatype.cpp
diff --git a/lib/api_goal.cpp b/src/api/api_goal.cpp
similarity index 100%
rename from lib/api_goal.cpp
rename to src/api/api_goal.cpp
diff --git a/lib/api_goal.h b/src/api/api_goal.h
similarity index 100%
rename from lib/api_goal.h
rename to src/api/api_goal.h
diff --git a/lib/api_log.cpp b/src/api/api_log.cpp
similarity index 100%
rename from lib/api_log.cpp
rename to src/api/api_log.cpp
diff --git a/lib/api_log_macros.cpp b/src/api/api_log_macros.cpp
similarity index 100%
rename from lib/api_log_macros.cpp
rename to src/api/api_log_macros.cpp
diff --git a/lib/api_log_macros.h b/src/api/api_log_macros.h
similarity index 100%
rename from lib/api_log_macros.h
rename to src/api/api_log_macros.h
diff --git a/lib/api_model.cpp b/src/api/api_model.cpp
similarity index 100%
rename from lib/api_model.cpp
rename to src/api/api_model.cpp
diff --git a/lib/api_model.h b/src/api/api_model.h
similarity index 100%
rename from lib/api_model.h
rename to src/api/api_model.h
diff --git a/lib/api_numeral.cpp b/src/api/api_numeral.cpp
similarity index 100%
rename from lib/api_numeral.cpp
rename to src/api/api_numeral.cpp
diff --git a/lib/api_params.cpp b/src/api/api_params.cpp
similarity index 100%
rename from lib/api_params.cpp
rename to src/api/api_params.cpp
diff --git a/lib/api_parsers.cpp b/src/api/api_parsers.cpp
similarity index 100%
rename from lib/api_parsers.cpp
rename to src/api/api_parsers.cpp
diff --git a/lib/api_poly.cpp b/src/api/api_poly.cpp
similarity index 100%
rename from lib/api_poly.cpp
rename to src/api/api_poly.cpp
diff --git a/lib/api_poly.h b/src/api/api_poly.h
similarity index 100%
rename from lib/api_poly.h
rename to src/api/api_poly.h
diff --git a/lib/api_quant.cpp b/src/api/api_quant.cpp
similarity index 100%
rename from lib/api_quant.cpp
rename to src/api/api_quant.cpp
diff --git a/lib/api_solver.cpp b/src/api/api_solver.cpp
similarity index 100%
rename from lib/api_solver.cpp
rename to src/api/api_solver.cpp
diff --git a/lib/api_solver.h b/src/api/api_solver.h
similarity index 100%
rename from lib/api_solver.h
rename to src/api/api_solver.h
diff --git a/lib/api_solver_old.cpp b/src/api/api_solver_old.cpp
similarity index 100%
rename from lib/api_solver_old.cpp
rename to src/api/api_solver_old.cpp
diff --git a/lib/api_stats.cpp b/src/api/api_stats.cpp
similarity index 100%
rename from lib/api_stats.cpp
rename to src/api/api_stats.cpp
diff --git a/lib/api_stats.h b/src/api/api_stats.h
similarity index 100%
rename from lib/api_stats.h
rename to src/api/api_stats.h
diff --git a/lib/api_tactic.cpp b/src/api/api_tactic.cpp
similarity index 100%
rename from lib/api_tactic.cpp
rename to src/api/api_tactic.cpp
diff --git a/lib/api_tactic.h b/src/api/api_tactic.h
similarity index 100%
rename from lib/api_tactic.h
rename to src/api/api_tactic.h
diff --git a/lib/api_user_theory.cpp b/src/api/api_user_theory.cpp
similarity index 100%
rename from lib/api_user_theory.cpp
rename to src/api/api_user_theory.cpp
diff --git a/lib/api_util.h b/src/api/api_util.h
similarity index 100%
rename from lib/api_util.h
rename to src/api/api_util.h
diff --git a/lib/add_bounds.cpp b/src/arith_tactics/add_bounds.cpp
similarity index 100%
rename from lib/add_bounds.cpp
rename to src/arith_tactics/add_bounds.cpp
diff --git a/lib/add_bounds.h b/src/arith_tactics/add_bounds.h
similarity index 100%
rename from lib/add_bounds.h
rename to src/arith_tactics/add_bounds.h
diff --git a/lib/add_bounds_tactic.cpp b/src/arith_tactics/add_bounds_tactic.cpp
similarity index 100%
rename from lib/add_bounds_tactic.cpp
rename to src/arith_tactics/add_bounds_tactic.cpp
diff --git a/lib/add_bounds_tactic.h b/src/arith_tactics/add_bounds_tactic.h
similarity index 100%
rename from lib/add_bounds_tactic.h
rename to src/arith_tactics/add_bounds_tactic.h
diff --git a/lib/bound_manager.cpp b/src/arith_tactics/bound_manager.cpp
similarity index 100%
rename from lib/bound_manager.cpp
rename to src/arith_tactics/bound_manager.cpp
diff --git a/lib/bound_manager.h b/src/arith_tactics/bound_manager.h
similarity index 100%
rename from lib/bound_manager.h
rename to src/arith_tactics/bound_manager.h
diff --git a/lib/bound_propagator.cpp b/src/arith_tactics/bound_propagator.cpp
similarity index 100%
rename from lib/bound_propagator.cpp
rename to src/arith_tactics/bound_propagator.cpp
diff --git a/lib/bound_propagator.h b/src/arith_tactics/bound_propagator.h
similarity index 100%
rename from lib/bound_propagator.h
rename to src/arith_tactics/bound_propagator.h
diff --git a/lib/degree_shift_tactic.cpp b/src/arith_tactics/degree_shift_tactic.cpp
similarity index 100%
rename from lib/degree_shift_tactic.cpp
rename to src/arith_tactics/degree_shift_tactic.cpp
diff --git a/lib/degree_shift_tactic.h b/src/arith_tactics/degree_shift_tactic.h
similarity index 100%
rename from lib/degree_shift_tactic.h
rename to src/arith_tactics/degree_shift_tactic.h
diff --git a/lib/diff_neq_tactic.cpp b/src/arith_tactics/diff_neq_tactic.cpp
similarity index 100%
rename from lib/diff_neq_tactic.cpp
rename to src/arith_tactics/diff_neq_tactic.cpp
diff --git a/lib/diff_neq_tactic.h b/src/arith_tactics/diff_neq_tactic.h
similarity index 100%
rename from lib/diff_neq_tactic.h
rename to src/arith_tactics/diff_neq_tactic.h
diff --git a/lib/fix_dl_var_tactic.cpp b/src/arith_tactics/fix_dl_var_tactic.cpp
similarity index 100%
rename from lib/fix_dl_var_tactic.cpp
rename to src/arith_tactics/fix_dl_var_tactic.cpp
diff --git a/lib/fix_dl_var_tactic.h b/src/arith_tactics/fix_dl_var_tactic.h
similarity index 100%
rename from lib/fix_dl_var_tactic.h
rename to src/arith_tactics/fix_dl_var_tactic.h
diff --git a/lib/fm_tactic.cpp b/src/arith_tactics/fm_tactic.cpp
similarity index 100%
rename from lib/fm_tactic.cpp
rename to src/arith_tactics/fm_tactic.cpp
diff --git a/lib/fm_tactic.h b/src/arith_tactics/fm_tactic.h
similarity index 100%
rename from lib/fm_tactic.h
rename to src/arith_tactics/fm_tactic.h
diff --git a/lib/lia2pb_tactic.cpp b/src/arith_tactics/lia2pb_tactic.cpp
similarity index 100%
rename from lib/lia2pb_tactic.cpp
rename to src/arith_tactics/lia2pb_tactic.cpp
diff --git a/lib/lia2pb_tactic.h b/src/arith_tactics/lia2pb_tactic.h
similarity index 100%
rename from lib/lia2pb_tactic.h
rename to src/arith_tactics/lia2pb_tactic.h
diff --git a/lib/linear_equation.cpp b/src/arith_tactics/linear_equation.cpp
similarity index 100%
rename from lib/linear_equation.cpp
rename to src/arith_tactics/linear_equation.cpp
diff --git a/lib/linear_equation.h b/src/arith_tactics/linear_equation.h
similarity index 100%
rename from lib/linear_equation.h
rename to src/arith_tactics/linear_equation.h
diff --git a/lib/lu.cpp b/src/arith_tactics/lu.cpp
similarity index 100%
rename from lib/lu.cpp
rename to src/arith_tactics/lu.cpp
diff --git a/lib/lu.h b/src/arith_tactics/lu.h
similarity index 100%
rename from lib/lu.h
rename to src/arith_tactics/lu.h
diff --git a/lib/mip_tactic.cpp b/src/arith_tactics/mip_tactic.cpp
similarity index 100%
rename from lib/mip_tactic.cpp
rename to src/arith_tactics/mip_tactic.cpp
diff --git a/lib/mip_tactic.h b/src/arith_tactics/mip_tactic.h
similarity index 100%
rename from lib/mip_tactic.h
rename to src/arith_tactics/mip_tactic.h
diff --git a/lib/nla2bv_tactic.cpp b/src/arith_tactics/nla2bv_tactic.cpp
similarity index 100%
rename from lib/nla2bv_tactic.cpp
rename to src/arith_tactics/nla2bv_tactic.cpp
diff --git a/lib/nla2bv_tactic.h b/src/arith_tactics/nla2bv_tactic.h
similarity index 100%
rename from lib/nla2bv_tactic.h
rename to src/arith_tactics/nla2bv_tactic.h
diff --git a/lib/normalize_bounds_tactic.cpp b/src/arith_tactics/normalize_bounds_tactic.cpp
similarity index 100%
rename from lib/normalize_bounds_tactic.cpp
rename to src/arith_tactics/normalize_bounds_tactic.cpp
diff --git a/lib/normalize_bounds_tactic.h b/src/arith_tactics/normalize_bounds_tactic.h
similarity index 100%
rename from lib/normalize_bounds_tactic.h
rename to src/arith_tactics/normalize_bounds_tactic.h
diff --git a/lib/pb2bv_model_converter.cpp b/src/arith_tactics/pb2bv_model_converter.cpp
similarity index 100%
rename from lib/pb2bv_model_converter.cpp
rename to src/arith_tactics/pb2bv_model_converter.cpp
diff --git a/lib/pb2bv_model_converter.h b/src/arith_tactics/pb2bv_model_converter.h
similarity index 100%
rename from lib/pb2bv_model_converter.h
rename to src/arith_tactics/pb2bv_model_converter.h
diff --git a/lib/pb2bv_tactic.cpp b/src/arith_tactics/pb2bv_tactic.cpp
similarity index 100%
rename from lib/pb2bv_tactic.cpp
rename to src/arith_tactics/pb2bv_tactic.cpp
diff --git a/lib/pb2bv_tactic.h b/src/arith_tactics/pb2bv_tactic.h
similarity index 100%
rename from lib/pb2bv_tactic.h
rename to src/arith_tactics/pb2bv_tactic.h
diff --git a/lib/probe_arith.cpp b/src/arith_tactics/probe_arith.cpp
similarity index 100%
rename from lib/probe_arith.cpp
rename to src/arith_tactics/probe_arith.cpp
diff --git a/lib/probe_arith.h b/src/arith_tactics/probe_arith.h
similarity index 100%
rename from lib/probe_arith.h
rename to src/arith_tactics/probe_arith.h
diff --git a/lib/propagate_ineqs_tactic.cpp b/src/arith_tactics/propagate_ineqs_tactic.cpp
similarity index 100%
rename from lib/propagate_ineqs_tactic.cpp
rename to src/arith_tactics/propagate_ineqs_tactic.cpp
diff --git a/lib/propagate_ineqs_tactic.h b/src/arith_tactics/propagate_ineqs_tactic.h
similarity index 100%
rename from lib/propagate_ineqs_tactic.h
rename to src/arith_tactics/propagate_ineqs_tactic.h
diff --git a/lib/purify_arith_tactic.cpp b/src/arith_tactics/purify_arith_tactic.cpp
similarity index 100%
rename from lib/purify_arith_tactic.cpp
rename to src/arith_tactics/purify_arith_tactic.cpp
diff --git a/lib/purify_arith_tactic.h b/src/arith_tactics/purify_arith_tactic.h
similarity index 100%
rename from lib/purify_arith_tactic.h
rename to src/arith_tactics/purify_arith_tactic.h
diff --git a/lib/recover_01_tactic.cpp b/src/arith_tactics/recover_01_tactic.cpp
similarity index 100%
rename from lib/recover_01_tactic.cpp
rename to src/arith_tactics/recover_01_tactic.cpp
diff --git a/lib/recover_01_tactic.h b/src/arith_tactics/recover_01_tactic.h
similarity index 100%
rename from lib/recover_01_tactic.h
rename to src/arith_tactics/recover_01_tactic.h
diff --git a/lib/vsubst_tactic.cpp b/src/arith_tactics/vsubst_tactic.cpp
similarity index 100%
rename from lib/vsubst_tactic.cpp
rename to src/arith_tactics/vsubst_tactic.cpp
diff --git a/lib/vsubst_tactic.h b/src/arith_tactics/vsubst_tactic.h
similarity index 100%
rename from lib/vsubst_tactic.h
rename to src/arith_tactics/vsubst_tactic.h
diff --git a/lib/ctx_simplify_tactic.cpp b/src/core_tactics/ctx_simplify_tactic.cpp
similarity index 99%
rename from lib/ctx_simplify_tactic.cpp
rename to src/core_tactics/ctx_simplify_tactic.cpp
index 9b4ca6c54..91334fd5c 100644
--- a/lib/ctx_simplify_tactic.cpp
+++ b/src/core_tactics/ctx_simplify_tactic.cpp
@@ -18,7 +18,7 @@ Notes:
 --*/
 #include"ctx_simplify_tactic.h"
 #include"mk_simplified_app.h"
-#include"num_occurs.h"
+#include"num_occurs_goal.h"
 #include"cooperate.h"
 #include"ast_ll_pp.h"
 #include"ast_smt2_pp.h"
@@ -51,7 +51,7 @@ struct ctx_simplify_tactic::imp {
     unsigned                    m_scope_lvl;
     unsigned                    m_depth;                  
     unsigned                    m_num_steps;
-    num_occurs                  m_occs;
+    num_occurs_goal             m_occs;
     mk_simplified_app           m_mk_app;
     unsigned long long          m_max_memory;
     unsigned                    m_max_depth;
diff --git a/lib/ctx_simplify_tactic.h b/src/core_tactics/ctx_simplify_tactic.h
similarity index 100%
rename from lib/ctx_simplify_tactic.h
rename to src/core_tactics/ctx_simplify_tactic.h
diff --git a/lib/distribute_forall_tactic.cpp b/src/core_tactics/distribute_forall_tactic.cpp
similarity index 100%
rename from lib/distribute_forall_tactic.cpp
rename to src/core_tactics/distribute_forall_tactic.cpp
diff --git a/lib/distribute_forall_tactic.h b/src/core_tactics/distribute_forall_tactic.h
similarity index 100%
rename from lib/distribute_forall_tactic.h
rename to src/core_tactics/distribute_forall_tactic.h
diff --git a/lib/elim_uncnstr_tactic.cpp b/src/core_tactics/elim_uncnstr_tactic.cpp
similarity index 100%
rename from lib/elim_uncnstr_tactic.cpp
rename to src/core_tactics/elim_uncnstr_tactic.cpp
diff --git a/lib/elim_uncnstr_tactic.h b/src/core_tactics/elim_uncnstr_tactic.h
similarity index 100%
rename from lib/elim_uncnstr_tactic.h
rename to src/core_tactics/elim_uncnstr_tactic.h
diff --git a/lib/nnf_tactic.cpp b/src/core_tactics/nnf_tactic.cpp
similarity index 100%
rename from lib/nnf_tactic.cpp
rename to src/core_tactics/nnf_tactic.cpp
diff --git a/lib/nnf_tactic.h b/src/core_tactics/nnf_tactic.h
similarity index 100%
rename from lib/nnf_tactic.h
rename to src/core_tactics/nnf_tactic.h
diff --git a/lib/occf_tactic.cpp b/src/core_tactics/occf_tactic.cpp
similarity index 100%
rename from lib/occf_tactic.cpp
rename to src/core_tactics/occf_tactic.cpp
diff --git a/lib/occf_tactic.h b/src/core_tactics/occf_tactic.h
similarity index 100%
rename from lib/occf_tactic.h
rename to src/core_tactics/occf_tactic.h
diff --git a/lib/propagate_values_tactic.cpp b/src/core_tactics/propagate_values_tactic.cpp
similarity index 100%
rename from lib/propagate_values_tactic.cpp
rename to src/core_tactics/propagate_values_tactic.cpp
diff --git a/lib/propagate_values_tactic.h b/src/core_tactics/propagate_values_tactic.h
similarity index 100%
rename from lib/propagate_values_tactic.h
rename to src/core_tactics/propagate_values_tactic.h
diff --git a/lib/simplify_tactic.cpp b/src/core_tactics/simplify_tactic.cpp
similarity index 100%
rename from lib/simplify_tactic.cpp
rename to src/core_tactics/simplify_tactic.cpp
diff --git a/lib/simplify_tactic.h b/src/core_tactics/simplify_tactic.h
similarity index 100%
rename from lib/simplify_tactic.h
rename to src/core_tactics/simplify_tactic.h
diff --git a/lib/solve_eqs_tactic.cpp b/src/core_tactics/solve_eqs_tactic.cpp
similarity index 100%
rename from lib/solve_eqs_tactic.cpp
rename to src/core_tactics/solve_eqs_tactic.cpp
diff --git a/lib/solve_eqs_tactic.h b/src/core_tactics/solve_eqs_tactic.h
similarity index 100%
rename from lib/solve_eqs_tactic.h
rename to src/core_tactics/solve_eqs_tactic.h
diff --git a/lib/split_clause_tactic.cpp b/src/core_tactics/split_clause_tactic.cpp
similarity index 100%
rename from lib/split_clause_tactic.cpp
rename to src/core_tactics/split_clause_tactic.cpp
diff --git a/lib/split_clause_tactic.h b/src/core_tactics/split_clause_tactic.h
similarity index 100%
rename from lib/split_clause_tactic.h
rename to src/core_tactics/split_clause_tactic.h
diff --git a/lib/tseitin_cnf_tactic.cpp b/src/core_tactics/tseitin_cnf_tactic.cpp
similarity index 100%
rename from lib/tseitin_cnf_tactic.cpp
rename to src/core_tactics/tseitin_cnf_tactic.cpp
diff --git a/lib/tseitin_cnf_tactic.h b/src/core_tactics/tseitin_cnf_tactic.h
similarity index 100%
rename from lib/tseitin_cnf_tactic.h
rename to src/core_tactics/tseitin_cnf_tactic.h
diff --git a/src/muz_qe/dl_simplifier_plugin.cpp b/src/dead/dl_simplifier_plugin.cpp
similarity index 100%
rename from src/muz_qe/dl_simplifier_plugin.cpp
rename to src/dead/dl_simplifier_plugin.cpp
diff --git a/src/muz_qe/dl_simplifier_plugin.h b/src/dead/dl_simplifier_plugin.h
similarity index 100%
rename from src/muz_qe/dl_simplifier_plugin.h
rename to src/dead/dl_simplifier_plugin.h
diff --git a/lib/smt_trail.h b/src/dead/smt_trail.h
similarity index 100%
rename from lib/smt_trail.h
rename to src/dead/smt_trail.h
diff --git a/lib/tactic2solver.cpp b/src/framework/tactic2solver.cpp
similarity index 100%
rename from lib/tactic2solver.cpp
rename to src/framework/tactic2solver.cpp
diff --git a/lib/tactic2solver.h b/src/framework/tactic2solver.h
similarity index 100%
rename from lib/tactic2solver.h
rename to src/framework/tactic2solver.h
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index b64bf3925..288aaf5bb 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -44,7 +44,6 @@ Revision History:
 #include"dl_compiler.h"
 #include"dl_instruction.h"
 #include"dl_context.h"
-#include"dl_simplifier_plugin.h"
 #include"dl_smt_relation.h"
 #ifndef _EXTERNAL_RELEASE
 #include"dl_skip_table.h"
diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp
index 6494bd223..b4c78cb01 100644
--- a/src/muz_qe/pdr_farkas_learner.cpp
+++ b/src/muz_qe/pdr_farkas_learner.cpp
@@ -29,7 +29,7 @@ Revision History:
 #include "pdr_util.h"
 #include "pdr_farkas_learner.h"
 #include "th_rewriter.h"
-#include "smtparser.h"
+// #include "smtparser.h"
 #include "pdr_interpolant_provider.h"
 #include "ast_ll_pp.h"
 #include "arith_bounds_tactic.h"
@@ -858,6 +858,8 @@ namespace pdr {
 
 
     void farkas_learner::test(char const* filename)  {
+#if 0
+        // [Leo]: disabled because it uses an external component: SMT 1.0 parser
         if (!filename) {
             test();
             return;
@@ -886,6 +888,7 @@ namespace pdr {
         expr_ref_vector lemmas(m);
         bool res = fl.get_lemma_guesses(A, B, lemmas);        
         std::cout << "lemmas: " << pp_cube(lemmas, m) << "\n";
+#endif
     }
 };
 
diff --git a/lib/mk_simplified_app.cpp b/src/rewriter/mk_simplified_app.cpp
similarity index 100%
rename from lib/mk_simplified_app.cpp
rename to src/rewriter/mk_simplified_app.cpp
diff --git a/lib/mk_simplified_app.h b/src/rewriter/mk_simplified_app.h
similarity index 100%
rename from lib/mk_simplified_app.h
rename to src/rewriter/mk_simplified_app.h
diff --git a/lib/user_decl_plugin.cpp b/src/user_ext/user_decl_plugin.cpp
similarity index 100%
rename from lib/user_decl_plugin.cpp
rename to src/user_ext/user_decl_plugin.cpp
diff --git a/lib/user_decl_plugin.h b/src/user_ext/user_decl_plugin.h
similarity index 100%
rename from lib/user_decl_plugin.h
rename to src/user_ext/user_decl_plugin.h
diff --git a/lib/user_simplifier_plugin.cpp b/src/user_ext/user_simplifier_plugin.cpp
similarity index 100%
rename from lib/user_simplifier_plugin.cpp
rename to src/user_ext/user_simplifier_plugin.cpp
diff --git a/lib/user_simplifier_plugin.h b/src/user_ext/user_simplifier_plugin.h
similarity index 100%
rename from lib/user_simplifier_plugin.h
rename to src/user_ext/user_simplifier_plugin.h
diff --git a/lib/user_smt_theory.cpp b/src/user_ext/user_smt_theory.cpp
similarity index 100%
rename from lib/user_smt_theory.cpp
rename to src/user_ext/user_smt_theory.cpp
diff --git a/lib/user_smt_theory.h b/src/user_ext/user_smt_theory.h
similarity index 100%
rename from lib/user_smt_theory.h
rename to src/user_ext/user_smt_theory.h