diff --git a/mk_make.py b/mk_make.py
new file mode 100644
index 000000000..35c06b4c5
--- /dev/null
+++ b/mk_make.py
@@ -0,0 +1,161 @@
+import os
+import glob
+
+BUILD_DIR='build-test'
+SRC_DIR='src'
+MODES=['Debug', 'Release']
+PLATFORMS=['Win32', 'x64']
+VS_COMMON_OPTIONS='WIN32;_WINDOWS;ASYNC_COMMANDS'
+VS_DBG_OPTIONS='Z3DEBUG;_TRACE;_DEBUG'
+VS_RELEASE_OPTIONS='NDEBUG;_EXTERNAL_RELEASE'
+
+def is_debug(mode):
+    return mode == 'Debug'
+
+def is_x64(platform):
+    return platform == 'x64'
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        os.makedirs(d)
+
+# Initialization
+mk_dir(BUILD_DIR)
+
+def module_src_dir(name):
+    return '%s%s%s' % (SRC_DIR, os.sep, name)
+
+def module_build_dir(name):
+    return '%s%s%s' % (BUILD_DIR, os.sep, name)
+
+def vs_header(f):
+    f.write(
+'<?xml version="1.0" encoding="utf-8"?>\n'
+'<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
+
+GUI = 0
+Name2GUI = {}
+
+def vs_project_configurations(f, name):
+    global GUI, Name2GUI
+    f.write('  <ItemGroup Label="ProjectConfigurations">\n')
+    for mode in MODES:
+        for platform in PLATFORMS:
+            f.write('    <ProjectConfiguration Include="%s|%s">\n' % (mode, platform))
+            f.write('      <Configuration>%s</Configuration>\n' % mode)
+            f.write('      <Platform>%s</Platform>\n' % platform)
+            f.write('    </ProjectConfiguration>\n')
+    f.write('  </ItemGroup>\n')
+
+    f.write('   <PropertyGroup Label="Globals">\n')
+    f.write('    <ProjectGuid>{00000000-0000-0000-000--%s}</ProjectGuid>\n' % GUI)
+    f.write('    <ProjectName>%s</ProjectName>\n' % name)
+    f.write('    <Keyword>Win32Proj</Keyword>\n')
+    f.write('  </PropertyGroup>\n')
+    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
+    Name2GUI[name] = GUI
+    GUI = GUI + 1
+
+def vs_lib_configurations(f, name):
+    for mode in MODES:
+        for platform in PLATFORMS:
+            f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'" Label="Configuration">\n' % (mode, platform))
+            f.write('    <ConfigurationType>StaticLibrary</ConfigurationType>\n')
+            f.write('    <CharacterSet>Unicode</CharacterSet>\n')
+            f.write('    <UseOfMfc>false</UseOfMfc>\n')
+            f.write('  </PropertyGroup>\n')
+
+    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
+    f.write('  <ImportGroup Label="ExtensionSettings">\n')
+    f.write('   </ImportGroup>\n')
+    f.write('   <ImportGroup Label="PropertySheets">\n')
+    f.write('    <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" />  </ImportGroup>\n')
+    f.write('  <PropertyGroup Label="UserMacros" />\n')
+
+    f.write('  <PropertyGroup>\n')
+    for mode in MODES:
+        for platform in PLATFORMS:
+            if is_x64(platform):
+                f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>\n' % 
+                        (mode, platform))
+            else:
+                f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">$(SolutionDir)$(Configuration)\</OutDir>\n' % (mode, platform))
+    for mode in MODES:
+        for platform in PLATFORMS:
+            f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">%s</TargetName>\n' % (mode, platform, name))
+            f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">.lib</TargetExt>\n' % (mode, platform))
+    f.write('  </PropertyGroup>\n')
+
+def vs_compilation_options(f, name, deps):
+    for mode in MODES:
+        for platform in PLATFORMS:
+            f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">\n' % (mode, platform))
+            if is_x64(platform):
+                f.write('    <Midl>\n')
+                f.write('      <TargetEnvironment>X64</TargetEnvironment>\n')
+                f.write('    </Midl>\n')
+            f.write('    <ClCompile>\n')
+            if is_debug(mode):
+                f.write('      <Optimization>Disabled</Optimization>\n')
+            else:
+                f.write('      <Optimization>Full</Optimization>\n')
+            options = VS_COMMON_OPTIONS
+            if is_debug(mode):
+                options = "%s;%s" % (options, VS_DBG_OPTIONS)
+            else:
+                options = "%s;%s" % (options, VS_RELEASE_OPTIONS)
+            if is_x64(platform):
+                options = "%s;_AMD64_" % options
+            f.write('      <PreprocessorDefinitions>%s;%%(PreprocessorDefinitions)</PreprocessorDefinitions>\n' % options)
+            if is_debug(mode):
+                f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
+                f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
+                f.write('      <WarningLevel>Level3</WarningLevel>\n')
+            f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
+            f.write('      <OpenMPSupport>true</OpenMPSupport>\n')
+            f.write('      <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n')
+            f.write('      <AdditionalIncludeDirectories>')
+            f.write('..\..\src\%s' % name)
+            for dep in deps:
+                f.write(';..\..\src\%s' % dep)
+            f.write('</AdditionalIncludeDirectories>\n')
+            f.write('    </ClCompile>\n')
+            f.write('    <Link>\n')
+            f.write('      <OutputFile>$(OutDir)%s.lib</OutputFile>\n' % name)
+            f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
+            if is_x64(platform):
+                f.write('      <TargetMachine>MachineX64</TargetMachine>\n')
+            else:
+                f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
+            f.write('    </Link>\n')
+            f.write('  </ItemDefinitionGroup>\n')
+
+def add_vs_cpps(f, name):
+    f.write('  <ItemGroup>\n')
+    srcs = module_src_dir(name)
+    for cppfile in glob.glob(os.path.join(srcs, '*.cpp')):
+       f.write('    <ClCompile Include="..%s..%s%s" />\n' % (os.sep, os.sep, cppfile))
+    f.write('  </ItemGroup>\n')
+
+def vs_footer(f):
+    f.write(
+'  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n'
+'  <ImportGroup Label="ExtensionTargets">\n'
+'  </ImportGroup>\n'
+'</Project>\n')
+   
+def add_lib(name, deps):
+    module_dir = module_build_dir(name)
+    mk_dir(module_dir)
+
+    vs_proj = open('%s%s%s.vcxproj' % (module_dir, os.sep, name), 'w')
+    vs_header(vs_proj)
+    vs_project_configurations(vs_proj, name)
+    vs_lib_configurations(vs_proj, name)
+    vs_compilation_options(vs_proj, name, deps)
+    add_vs_cpps(vs_proj, name)
+    vs_footer(vs_proj)
+
+add_lib('util', [])
+add_lib('polynomial', ['util'])
+add_lib('ast', ['util', 'polynomial'])
diff --git a/lib/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
similarity index 100%
rename from lib/arith_decl_plugin.cpp
rename to src/ast/arith_decl_plugin.cpp
diff --git a/lib/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
similarity index 100%
rename from lib/arith_decl_plugin.h
rename to src/ast/arith_decl_plugin.h
diff --git a/lib/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
similarity index 100%
rename from lib/array_decl_plugin.cpp
rename to src/ast/array_decl_plugin.cpp
diff --git a/lib/array_decl_plugin.h b/src/ast/array_decl_plugin.h
similarity index 100%
rename from lib/array_decl_plugin.h
rename to src/ast/array_decl_plugin.h
diff --git a/lib/ast.cpp b/src/ast/ast.cpp
similarity index 100%
rename from lib/ast.cpp
rename to src/ast/ast.cpp
diff --git a/lib/ast.h b/src/ast/ast.h
similarity index 100%
rename from lib/ast.h
rename to src/ast/ast.h
diff --git a/lib/ast_list.h b/src/ast/ast_list.h
similarity index 100%
rename from lib/ast_list.h
rename to src/ast/ast_list.h
diff --git a/lib/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
similarity index 100%
rename from lib/ast_ll_pp.cpp
rename to src/ast/ast_ll_pp.cpp
diff --git a/lib/ast_ll_pp.h b/src/ast/ast_ll_pp.h
similarity index 100%
rename from lib/ast_ll_pp.h
rename to src/ast/ast_ll_pp.h
diff --git a/lib/ast_pp.cpp b/src/ast/ast_pp.cpp
similarity index 100%
rename from lib/ast_pp.cpp
rename to src/ast/ast_pp.cpp
diff --git a/lib/ast_pp.h b/src/ast/ast_pp.h
similarity index 100%
rename from lib/ast_pp.h
rename to src/ast/ast_pp.h
diff --git a/lib/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
similarity index 100%
rename from lib/ast_smt2_pp.cpp
rename to src/ast/ast_smt2_pp.cpp
diff --git a/lib/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
similarity index 100%
rename from lib/ast_smt2_pp.h
rename to src/ast/ast_smt2_pp.h
diff --git a/lib/ast_util.cpp b/src/ast/ast_util.cpp
similarity index 100%
rename from lib/ast_util.cpp
rename to src/ast/ast_util.cpp
diff --git a/lib/ast_util.h b/src/ast/ast_util.h
similarity index 100%
rename from lib/ast_util.h
rename to src/ast/ast_util.h
diff --git a/lib/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
similarity index 100%
rename from lib/bv_decl_plugin.cpp
rename to src/ast/bv_decl_plugin.cpp
diff --git a/lib/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
similarity index 100%
rename from lib/bv_decl_plugin.h
rename to src/ast/bv_decl_plugin.h
diff --git a/lib/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
similarity index 100%
rename from lib/datatype_decl_plugin.cpp
rename to src/ast/datatype_decl_plugin.cpp
diff --git a/lib/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
similarity index 100%
rename from lib/datatype_decl_plugin.h
rename to src/ast/datatype_decl_plugin.h
diff --git a/lib/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
similarity index 100%
rename from lib/dl_decl_plugin.cpp
rename to src/ast/dl_decl_plugin.cpp
diff --git a/lib/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h
similarity index 100%
rename from lib/dl_decl_plugin.h
rename to src/ast/dl_decl_plugin.h
diff --git a/lib/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
similarity index 100%
rename from lib/float_decl_plugin.cpp
rename to src/ast/float_decl_plugin.cpp
diff --git a/lib/float_decl_plugin.h b/src/ast/float_decl_plugin.h
similarity index 100%
rename from lib/float_decl_plugin.h
rename to src/ast/float_decl_plugin.h
diff --git a/lib/for_each_ast.h b/src/ast/for_each_ast.h
similarity index 100%
rename from lib/for_each_ast.h
rename to src/ast/for_each_ast.h
diff --git a/lib/format.cpp b/src/ast/format.cpp
similarity index 100%
rename from lib/format.cpp
rename to src/ast/format.cpp
diff --git a/lib/format.h b/src/ast/format.h
similarity index 100%
rename from lib/format.h
rename to src/ast/format.h
diff --git a/lib/pp.cpp b/src/ast/pp.cpp
similarity index 100%
rename from lib/pp.cpp
rename to src/ast/pp.cpp
diff --git a/lib/pp.h b/src/ast/pp.h
similarity index 100%
rename from lib/pp.h
rename to src/ast/pp.h
diff --git a/lib/pp_params.cpp b/src/ast/pp_params.cpp
similarity index 100%
rename from lib/pp_params.cpp
rename to src/ast/pp_params.cpp
diff --git a/lib/pp_params.h b/src/ast/pp_params.h
similarity index 100%
rename from lib/pp_params.h
rename to src/ast/pp_params.h
diff --git a/lib/recurse_expr.h b/src/ast/recurse_expr.h
similarity index 100%
rename from lib/recurse_expr.h
rename to src/ast/recurse_expr.h
diff --git a/lib/recurse_expr_def.h b/src/ast/recurse_expr_def.h
similarity index 100%
rename from lib/recurse_expr_def.h
rename to src/ast/recurse_expr_def.h
diff --git a/lib/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
similarity index 100%
rename from lib/seq_decl_plugin.cpp
rename to src/ast/seq_decl_plugin.cpp
diff --git a/lib/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
similarity index 100%
rename from lib/seq_decl_plugin.h
rename to src/ast/seq_decl_plugin.h
diff --git a/lib/shared_occs.cpp b/src/ast/shared_occs.cpp
similarity index 100%
rename from lib/shared_occs.cpp
rename to src/ast/shared_occs.cpp
diff --git a/lib/shared_occs.h b/src/ast/shared_occs.h
similarity index 100%
rename from lib/shared_occs.h
rename to src/ast/shared_occs.h
diff --git a/lib/algebraic_numbers.cpp b/src/polynomial/algebraic_numbers.cpp
similarity index 100%
rename from lib/algebraic_numbers.cpp
rename to src/polynomial/algebraic_numbers.cpp
diff --git a/lib/algebraic_numbers.h b/src/polynomial/algebraic_numbers.h
similarity index 100%
rename from lib/algebraic_numbers.h
rename to src/polynomial/algebraic_numbers.h
diff --git a/lib/linear_eq_solver.h b/src/polynomial/linear_eq_solver.h
similarity index 100%
rename from lib/linear_eq_solver.h
rename to src/polynomial/linear_eq_solver.h
diff --git a/lib/polynomial.cpp b/src/polynomial/polynomial.cpp
similarity index 100%
rename from lib/polynomial.cpp
rename to src/polynomial/polynomial.cpp
diff --git a/lib/polynomial.h b/src/polynomial/polynomial.h
similarity index 100%
rename from lib/polynomial.h
rename to src/polynomial/polynomial.h
diff --git a/lib/polynomial_cache.cpp b/src/polynomial/polynomial_cache.cpp
similarity index 100%
rename from lib/polynomial_cache.cpp
rename to src/polynomial/polynomial_cache.cpp
diff --git a/lib/polynomial_cache.h b/src/polynomial/polynomial_cache.h
similarity index 100%
rename from lib/polynomial_cache.h
rename to src/polynomial/polynomial_cache.h
diff --git a/lib/polynomial_factorization.cpp b/src/polynomial/polynomial_factorization.cpp
similarity index 100%
rename from lib/polynomial_factorization.cpp
rename to src/polynomial/polynomial_factorization.cpp
diff --git a/lib/polynomial_factorization.h b/src/polynomial/polynomial_factorization.h
similarity index 100%
rename from lib/polynomial_factorization.h
rename to src/polynomial/polynomial_factorization.h
diff --git a/lib/polynomial_primes.h b/src/polynomial/polynomial_primes.h
similarity index 100%
rename from lib/polynomial_primes.h
rename to src/polynomial/polynomial_primes.h
diff --git a/lib/polynomial_var2value.h b/src/polynomial/polynomial_var2value.h
similarity index 100%
rename from lib/polynomial_var2value.h
rename to src/polynomial/polynomial_var2value.h
diff --git a/lib/sexpr2upolynomial.cpp b/src/polynomial/sexpr2upolynomial.cpp
similarity index 100%
rename from lib/sexpr2upolynomial.cpp
rename to src/polynomial/sexpr2upolynomial.cpp
diff --git a/lib/sexpr2upolynomial.h b/src/polynomial/sexpr2upolynomial.h
similarity index 100%
rename from lib/sexpr2upolynomial.h
rename to src/polynomial/sexpr2upolynomial.h
diff --git a/lib/upolynomial.cpp b/src/polynomial/upolynomial.cpp
similarity index 100%
rename from lib/upolynomial.cpp
rename to src/polynomial/upolynomial.cpp
diff --git a/lib/upolynomial.h b/src/polynomial/upolynomial.h
similarity index 100%
rename from lib/upolynomial.h
rename to src/polynomial/upolynomial.h
diff --git a/lib/upolynomial_factorization.cpp b/src/polynomial/upolynomial_factorization.cpp
similarity index 100%
rename from lib/upolynomial_factorization.cpp
rename to src/polynomial/upolynomial_factorization.cpp
diff --git a/lib/upolynomial_factorization.h b/src/polynomial/upolynomial_factorization.h
similarity index 100%
rename from lib/upolynomial_factorization.h
rename to src/polynomial/upolynomial_factorization.h
diff --git a/lib/upolynomial_factorization_int.h b/src/polynomial/upolynomial_factorization_int.h
similarity index 100%
rename from lib/upolynomial_factorization_int.h
rename to src/polynomial/upolynomial_factorization_int.h
diff --git a/lib/cmd_context_types.cpp b/src/util/cmd_context_types.cpp
similarity index 100%
rename from lib/cmd_context_types.cpp
rename to src/util/cmd_context_types.cpp
diff --git a/lib/cmd_context_types.h b/src/util/cmd_context_types.h
similarity index 100%
rename from lib/cmd_context_types.h
rename to src/util/cmd_context_types.h
diff --git a/lib/cooperate.cpp b/src/util/cooperate.cpp
similarity index 100%
rename from lib/cooperate.cpp
rename to src/util/cooperate.cpp
diff --git a/lib/cooperate.h b/src/util/cooperate.h
similarity index 100%
rename from lib/cooperate.h
rename to src/util/cooperate.h
diff --git a/lib/error_codes.h b/src/util/error_codes.h
similarity index 100%
rename from lib/error_codes.h
rename to src/util/error_codes.h
diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h
index 008333b0b..217b58567 100644
--- a/src/util/mpq_inf.h
+++ b/src/util/mpq_inf.h
@@ -21,7 +21,6 @@ Revision History:
 
 #include"mpq.h"
 #include"hash.h"
-#include"params.h"
 
 typedef std::pair<mpq, mpq> mpq_inf;
 
@@ -32,12 +31,12 @@ class mpq_inf_manager {
 public:
     typedef mpq_inf numeral;
 
-    mpq_inf_manager(mpq_manager<SYNCH> & _m, params_ref const & p = params_ref()):m(_m) {
-        updt_params(p);
+    mpq_inf_manager(mpq_manager<SYNCH> & _m, double inf = 0.0001):m(_m) {
+        set_inf(inf);
     }
 
-    void updt_params(params_ref const & p) {
-        m_inf = p.get_double(":infinitesimal-as-double", 0.00001);
+    void set_inf(double inf) {
+        m_inf = inf;
     }
 
     enum inf_kind { NEG=-1, ZERO, POS };
diff --git a/lib/params.cpp b/src/util/params.cpp
similarity index 80%
rename from lib/params.cpp
rename to src/util/params.cpp
index bcb3ce078..ae7f0c830 100644
--- a/lib/params.cpp
+++ b/src/util/params.cpp
@@ -17,7 +17,6 @@ Notes:
 
 --*/
 #include"params.h"
-#include"ast.h"
 #include"rational.h"
 #include"symbol.h"
 #include"dictionary.h"
@@ -158,11 +157,9 @@ class params {
             char const *  m_str_value;
             char const *  m_sym_value;
             rational *    m_rat_value;
-            ast *         m_ast_value;
         };
     };
     typedef std::pair<symbol, value> entry;
-    ast_manager *  m_manager;
     svector<entry> m_entries;
     unsigned       m_ref_count;
     
@@ -170,7 +167,7 @@ class params {
     void del_values();
 
 public:
-    params():m_manager(0), m_ref_count(0) {}
+    params():m_ref_count(0) {}
     ~params() {
         reset();
     }
@@ -178,8 +175,6 @@ public:
     void inc_ref() { m_ref_count++; }
     void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
 
-    void set_manager(ast_manager & m);
-
     bool empty() const { return m_entries.empty(); }
     bool contains(symbol const & k) const;
     bool contains(char const * k) const;
@@ -213,12 +208,6 @@ public:
     rational get_rat(char const * k, rational const & _default) const; 
     symbol get_sym(symbol const & k, symbol const & _default) const;
     symbol get_sym(char const * k, symbol const & _default) const;
-    expr * get_expr(symbol const & k, expr * _default) const;
-    expr * get_expr(char const * k, expr * _default) const;
-    func_decl * get_func_decl(symbol const & k, func_decl * _default) const;
-    func_decl * get_func_decl(char const * k, func_decl * _default) const;
-    sort * get_sort(symbol const & k, sort * _default) const;
-    sort * get_sort(char const * k, sort * _default) const;
 
     // setters
     void set_bool(symbol const & k, bool v);
@@ -233,12 +222,6 @@ public:
     void set_rat(char const * k, rational const & v); 
     void set_sym(symbol const & k, symbol const & v);
     void set_sym(char const * k, symbol const & v);
-    void set_expr(symbol const & k, expr * v);
-    void set_expr(char const * k, expr * v);
-    void set_func_decl(symbol const & k, func_decl * v);
-    void set_func_decl(char const * k, func_decl * v);
-    void set_sort(symbol const & k, sort * v);
-    void set_sort(char const * k, sort * v);
 
     void display(std::ostream & out) const {
         out << "(params";
@@ -265,11 +248,6 @@ public:
             case CPK_STRING:
                 out << " " << it->second.m_str_value;
                 break;
-            case CPK_EXPR:
-            case CPK_FUNC_DECL:
-            case CPK_SORT:
-                out << " #" << it->second.m_ast_value->get_id();
-                break;
             default:
                 UNREACHABLE();
                 break;
@@ -344,15 +322,6 @@ void params_ref::copy_core(params const * src) {
         case CPK_STRING:
             m_params->set_str(it->first, it->second.m_str_value);
             break;
-        case CPK_EXPR:
-            m_params->set_expr(it->first, static_cast<expr*>(it->second.m_ast_value));
-            break;
-        case CPK_FUNC_DECL:
-            m_params->set_func_decl(it->first, static_cast<func_decl*>(it->second.m_ast_value));
-            break;
-        case CPK_SORT:
-            m_params->set_sort(it->first, static_cast<sort*>(it->second.m_ast_value));
-            break;
         default:
             UNREACHABLE();
             break;
@@ -369,7 +338,6 @@ void params_ref::init() {
         params * old = m_params;
         m_params = alloc(params);
         m_params->inc_ref();
-        m_params->m_manager = old->m_manager;
         copy_core(old);
         old->dec_ref();
     }
@@ -385,12 +353,6 @@ double params_ref::get_double(symbol const & k, double _default) const { return
 double params_ref::get_double(char const * k, double _default) const { return m_params ? m_params->get_double(k, _default) : _default; }
 char const * params_ref::get_str(symbol const & k, char const * _default) const { return m_params ? m_params->get_str(k, _default) : _default; }
 char const * params_ref::get_str(char const * k, char const * _default) const { return m_params ? m_params->get_str(k, _default) : _default; }
-expr * params_ref::get_expr(symbol const & k, expr * _default) const { return m_params ? m_params->get_expr(k, _default) : _default; }
-expr * params_ref::get_expr(char const * k, expr * _default) const { return m_params ? m_params->get_expr(k, _default) : _default; }
-func_decl * params_ref::get_func_decl(symbol const & k, func_decl * _default) const { return m_params ? m_params->get_func_decl(k, _default) : _default; }
-func_decl * params_ref::get_func_decl(char const * k, func_decl * _default) const { return m_params ? m_params->get_func_decl(k, _default) : _default; }
-sort * params_ref::get_sort(symbol const & k, sort * _default) const { return m_params ? m_params->get_sort(k, _default) : _default; }
-sort * params_ref::get_sort(char const * k, sort * _default) const { return m_params ? m_params->get_sort(k, _default) : _default; }
 
 rational params_ref::get_rat(symbol const & k, rational const & _default) const { 
     return m_params ? m_params->get_rat(k, _default) : _default; 
@@ -408,11 +370,6 @@ symbol params_ref::get_sym(char const * k, symbol const & _default) const {
     return m_params ? m_params->get_sym(k, _default) : _default; 
 }
 
-void params_ref::set_manager(ast_manager & m) {
-    init();
-    m_params->set_manager(m);
-}
-
 bool params_ref::empty() const {
     if (!m_params)
         return true;
@@ -506,35 +463,6 @@ void params_ref::set_sym(char const * k, symbol const & v) {
     m_params->set_sym(k, v);
 }
 
-void params_ref::set_expr(symbol const & k, expr * v) {
-    init();
-    m_params->set_expr(k, v);
-}
-
-void params_ref::set_expr(char const * k, expr * v) {
-    init();
-    m_params->set_expr(k, v);
-}
-
-void params_ref::set_func_decl(symbol const & k, func_decl * v) {
-    init();
-    m_params->set_func_decl(k, v);
-}
-
-void params_ref::set_func_decl(char const * k, func_decl * v) {
-    init();
-    m_params->set_func_decl(k, v);
-}
-
-void params_ref::set_sort(symbol const & k, sort * v) {
-    init();
-    m_params->set_sort(k, v);
-}
-
-void params_ref::set_sort(char const * k, sort * v) {
-    init();
-    m_params->set_sort(k, v);
-}
 
 void params::del_value(entry & e) {
     switch (e.second.m_kind) {
@@ -542,21 +470,11 @@ void params::del_value(entry & e) {
         if (e.second.m_kind == CPK_NUMERAL)
             dealloc(e.second.m_rat_value);
         break;
-    case CPK_EXPR:
-    case CPK_SORT:
-    case CPK_FUNC_DECL:
-        SASSERT(m_manager);
-        m_manager->dec_ref(e.second.m_ast_value);
-        return;
     default:
         return;
     }
 }
 
-void params::set_manager(ast_manager & m) {
-    m_manager = &m;
-}
-
 #define TRAVERSE_ENTRIES(CODE) {                        \
     svector<entry>::iterator it  = m_entries.begin();   \
     svector<entry>::iterator end = m_entries.end();     \
@@ -696,30 +614,6 @@ symbol params::get_sym(char const * k, symbol const & _default) const {
     GET_VALUE(return symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);, CPK_SYMBOL);
 }
 
-expr * params::get_expr(symbol const & k, expr * _default) const {
-    GET_VALUE(return static_cast<expr*>(it->second.m_ast_value);, CPK_EXPR);
-}
-
-expr * params::get_expr(char const * k, expr * _default) const {
-    GET_VALUE(return static_cast<expr*>(it->second.m_ast_value);, CPK_EXPR);
-}
-
-func_decl * params::get_func_decl(symbol const & k, func_decl * _default) const {
-    GET_VALUE(return static_cast<func_decl*>(it->second.m_ast_value);, CPK_FUNC_DECL);
-}
-
-func_decl * params::get_func_decl(char const * k, func_decl * _default) const {
-    GET_VALUE(return static_cast<func_decl*>(it->second.m_ast_value);, CPK_FUNC_DECL);
-}
-
-sort * params::get_sort(symbol const & k, sort * _default) const {
-    GET_VALUE(return static_cast<sort*>(it->second.m_ast_value);, CPK_SORT);
-}
-
-sort * params::get_sort(char const * k, sort * _default) const {
-    GET_VALUE(return static_cast<sort*>(it->second.m_ast_value);, CPK_SORT);
-}
-
 #define SET_VALUE(MATCH_CODE, ADD_CODE) {       \
     TRAVERSE_ENTRIES(if (it->first == k) {      \
         MATCH_CODE                              \
@@ -820,44 +714,3 @@ void params::set_sym(char const * k, symbol const & v) {
     SET_SYM_VALUE();
 }
 
-#define SET_AST_VALUE(KIND) {                   \
-    SASSERT(m_manager);                         \
-    m_manager->inc_ref(v);                      \
-    SET_VALUE({                                 \
-        del_value(*it);                         \
-        it->second.m_kind      = KIND;          \
-        it->second.m_ast_value = v;             \
-    },                                          \
-    {                                           \
-        entry new_entry;                        \
-        new_entry.first  = symbol(k);           \
-        new_entry.second.m_kind = KIND;         \
-        new_entry.second.m_ast_value = v;       \
-        m_entries.push_back(new_entry);         \
-    })}
-
-
-void params::set_expr(symbol const & k, expr * v) {
-    SET_AST_VALUE(CPK_EXPR);
-}
- 
-void params::set_expr(char const * k, expr * v) {
-    SET_AST_VALUE(CPK_EXPR);
-}
-
-void params::set_func_decl(symbol const & k, func_decl * v) {
-    SET_AST_VALUE(CPK_FUNC_DECL);
-}
-
-void params::set_func_decl(char const * k, func_decl * v) {
-    SET_AST_VALUE(CPK_FUNC_DECL);
-}
-
-void params::set_sort(symbol const & k, sort * v) {
-    SET_AST_VALUE(CPK_SORT);
-}
-
-void params::set_sort(char const * k, sort * v) {
-    SET_AST_VALUE(CPK_SORT);
-}
-
diff --git a/lib/params.h b/src/util/params.h
similarity index 81%
rename from lib/params.h
rename to src/util/params.h
index f2a5e4da8..66c4e7c7a 100644
--- a/lib/params.h
+++ b/src/util/params.h
@@ -21,8 +21,6 @@ Notes:
 
 #include"cmd_context_types.h"
 #include"vector.h"
-class ast;
-class ast_manager;
 
 typedef cmd_arg_kind param_kind;
 
@@ -56,14 +54,6 @@ public:
     rational get_rat(char const * k, rational const & _default) const;
     symbol get_sym(symbol const & k, symbol const & _default) const;
     symbol get_sym(char const * k, symbol const & _default) const;
-    expr * get_expr(symbol const & k, expr * _default) const;
-    expr * get_expr(char const * k, expr * _default) const;
-    func_decl * get_func_decl(symbol const & k, func_decl * _default) const;
-    func_decl * get_func_decl(char const * k, func_decl * _default) const;
-    sort * get_sort(symbol const & k, sort * _default) const;
-    sort * get_sort(char const * k, sort * _default) const;
-
-    void set_manager(ast_manager & m);
 
     bool empty() const;
     bool contains(symbol const & k) const;
@@ -85,12 +75,6 @@ public:
     void set_rat(char const * k, rational const & v); 
     void set_sym(symbol const & k, symbol const & v);
     void set_sym(char const * k, symbol const & v);
-    void set_expr(symbol const & k, expr * v);
-    void set_expr(char const * k, expr * v);
-    void set_func_decl(symbol const & k, func_decl * v);
-    void set_func_decl(char const * k, func_decl * v);
-    void set_sort(symbol const & k, sort * v);
-    void set_sort(char const * k, sort * v);
 
     void display(std::ostream & out) const;
 
diff --git a/lib/skip_list_base.h b/src/util/skip_list_base.h
similarity index 100%
rename from lib/skip_list_base.h
rename to src/util/skip_list_base.h
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 6b5d396f8..24d17ddfa 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -20,7 +20,7 @@ Notes:
 #include"map.h"
 #include"str_hashtable.h"
 #include"buffer.h"
-#include"ast_smt2_pp.h"
+#include"smt2_util.h"
 #include<iomanip>
 
 void statistics::update(char const * key, unsigned inc) {
diff --git a/lib/z3_exception.cpp b/src/util/z3_exception.cpp
similarity index 100%
rename from lib/z3_exception.cpp
rename to src/util/z3_exception.cpp
diff --git a/lib/z3_exception.h b/src/util/z3_exception.h
similarity index 100%
rename from lib/z3_exception.h
rename to src/util/z3_exception.h
diff --git a/lib/z3_omp.h b/src/util/z3_omp.h
similarity index 100%
rename from lib/z3_omp.h
rename to src/util/z3_omp.h