diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index 1f4e4942e..059382be4 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -63,16 +63,17 @@ add_lib('bv_tactics', ['tactic'])
 add_lib('fuzzing', ['ast'])
 add_lib('fpa', ['core_tactics', 'bit_blaster', 'sat_tactic'])
 add_lib('smt_tactic', ['smt'])
+add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'])
 add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'])
-add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic'])
-# TODO: rewrite ufbv_strategy as a tactic and move to smtlogic_tactics.
-add_lib('ufbv_strategy', ['assertion_set', 'normal_forms', 'macros', 'smt_tactic', 'rewriter'])
+add_lib('aig', ['cmd_context', 'assertion_set'])
 # 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', ['cmd_context', 'assertion_set'])
+add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'])
+# TODO: rewrite ufbv_strategy as a tactic and move to smtlogic_tactics.
+add_lib('ufbv_strategy', ['assertion_set', 'normal_forms', 'macros', 'smt_tactic', 'rewriter'])
 add_lib('portfolio', ['smtlogic_tactics', 'ufbv_strategy', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'])
 # TODO: delete SMT 1.0 frontend
-add_lib('smtparser', ['api_headers', 'smt', 'spc', 'portfolio'])
-add_lib('api', ['portfolio', 'user_plugin', 'smtparser'])
+add_lib('api', ['portfolio', 'user_plugin'])
+add_exe('shell', ['api', 'sat', 'extra_cmds'])
 
 mk_vs_solution()
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 658f266c2..9e6853795 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -41,8 +41,10 @@ Name2GUI = {}
 def mk_gui_str(id):
     return '4D2F40D8-E5F9-473B-B548-%012d' % id
 
+MODULES = []
 HEADERS = []
 LIBS = []
+EXES = []
 DEPS = {}
 
 class MKException(Exception):
@@ -73,6 +75,17 @@ def module_src_dir(name):
 def module_build_dir(name):
     return '%s%s%s' % (BUILD_DIR, os.sep, name)
 
+LIB_KIND = 0
+EXE_KIND = 1
+
+def get_extension(kind):
+    if kind == LIB_KIND:
+        return 'lib'
+    elif kind == EXE_KIND:
+        return 'exe'
+    else:
+        raise MKException('unknown kind %s' % kind)
+
 def vs_header(f):
     f.write(
 '<?xml version="1.0" encoding="utf-8"?>\n'
@@ -98,11 +111,16 @@ def vs_project_configurations(f, name):
     Name2GUI[name] = GUI
     GUI = GUI + 1
 
-def vs_lib_configurations(f, name):
+def vs_configurations(f, name, kind):
     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')
+            if kind == LIB_KIND:
+                f.write('    <ConfigurationType>StaticLibrary</ConfigurationType>\n')
+            elif kind == EXE_KIND:
+                f.write('    <ConfigurationType>Application</ConfigurationType>\n')
+            else:
+                raise MKException("unknown kind %s" % kind)
             f.write('    <CharacterSet>Unicode</CharacterSet>\n')
             f.write('    <UseOfMfc>false</UseOfMfc>\n')
             f.write('  </PropertyGroup>\n')
@@ -125,10 +143,10 @@ def vs_lib_configurations(f, name):
     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('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">.%s</TargetExt>\n' % (mode, platform, get_extension(kind)))
     f.write('  </PropertyGroup>\n')
 
-def vs_compilation_options(f, name, deps):
+def vs_compilation_options(f, name, deps, kind):
     for mode in MODES:
         for platform in PLATFORMS:
             f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">\n' % (mode, platform))
@@ -163,12 +181,21 @@ def vs_compilation_options(f, name, deps):
             f.write('</AdditionalIncludeDirectories>\n')
             f.write('    </ClCompile>\n')
             f.write('    <Link>\n')
-            f.write('      <OutputFile>$(OutDir)%s.lib</OutputFile>\n' % name)
+            f.write('      <OutputFile>$(OutDir)%s.%s</OutputFile>\n' % (name, get_extension(kind)))
             f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
             if is_x64(platform):
                 f.write('      <TargetMachine>MachineX64</TargetMachine>\n')
             else:
                 f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
+            if kind == EXE_KIND:
+                f.write('<AdditionalDependencies>kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib')
+                for dep in deps:
+                    f.write(';$(OutDir)%s.lib' % dep)
+                    # if is_x64(platform):
+                    #    f.write(';..\%s\%s\%s\%s.lib' % (dep, platform, mode, dep))
+                    # else:
+                    #    f.write(';..\%s\%s\%s.lib' % (dep, mode, dep))
+                f.write(';%(AdditionalDependencies)</AdditionalDependencies>\n')
             f.write('    </Link>\n')
             f.write('  </ItemDefinitionGroup>\n')
 
@@ -187,7 +214,7 @@ def vs_footer(f):
 '</Project>\n')
 
 def check_new_component(name):
-    if (name in HEADERS) or (name in LIBS):
+    if (name in HEADERS) or (name in LIBS) or (name in EXES):
         raise MKException("Component '%s' was already defined" % name)
 
 # Add a directory containing only .h files
@@ -211,9 +238,15 @@ def find_all_deps(name, deps):
             raise MKException("Unknown component '%s' at '%s'." % (dep, name))
     return new_deps
 
-def add_lib(name, deps):
+def add_component(name, deps, kind):
     check_new_component(name)
-    LIBS.append(name)
+    if kind == LIB_KIND:
+        LIBS.append(name)
+    elif kind == EXE_KIND:
+        EXES.append(name)
+    else:
+        raise MKException("unknown kind %s" % kind)
+    MODULES.append(name)
     deps = find_all_deps(name, deps)
     DEPS[name] = deps
     print "Dependencies for '%s': %s" % (name, deps)
@@ -224,11 +257,17 @@ def add_lib(name, deps):
     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)
+    vs_configurations(vs_proj, name, kind)
+    vs_compilation_options(vs_proj, name, deps, kind)
     add_vs_cpps(vs_proj, name)
     vs_footer(vs_proj)
 
+def add_lib(name, deps):
+    add_component(name, deps, LIB_KIND)
+
+def add_exe(name, deps):
+    add_component(name, deps, EXE_KIND)
+
 def is_lib(name):
     # Add DLL dependency
     return name in LIBS
@@ -238,8 +277,7 @@ def mk_vs_solution():
     sln.write('\n')
     sln.write("Microsoft Visual Studio Solution File, Format Version 11.00\n")
     sln.write("# Visual Studio 2010\n")
-    modules = LIBS
-    for module in modules:
+    for module in MODULES:
         gui = Name2GUI[module]
         deps = DEPS[module]
         sln.write('Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "%s", "%s%s%s.vcxproj", "{%s}"\n' %
@@ -259,7 +297,7 @@ def mk_vs_solution():
             sln.write('   %s|%s = %s|%s\n' % (mode, platform, mode, platform))
     sln.write('EndGlobalSection\n')
     sln.write('GlobalSection(ProjectConfigurationPlatforms) = postSolution\n')
-    for module in modules:
+    for module in MODULES:
         gui = Name2GUI[module]
         for mode in MODES:
             for platform in PLATFORMS:
diff --git a/src/smtparser/expr_pattern_match.cpp b/src/api/expr_pattern_match.cpp
similarity index 100%
rename from src/smtparser/expr_pattern_match.cpp
rename to src/api/expr_pattern_match.cpp
diff --git a/src/smtparser/expr_pattern_match.h b/src/api/expr_pattern_match.h
similarity index 100%
rename from src/smtparser/expr_pattern_match.h
rename to src/api/expr_pattern_match.h
diff --git a/src/smtparser/smtlib.cpp b/src/api/smtlib.cpp
similarity index 100%
rename from src/smtparser/smtlib.cpp
rename to src/api/smtlib.cpp
diff --git a/src/smtparser/smtlib.h b/src/api/smtlib.h
similarity index 100%
rename from src/smtparser/smtlib.h
rename to src/api/smtlib.h
diff --git a/src/smtparser/smtlib_solver.cpp b/src/api/smtlib_solver.cpp
similarity index 100%
rename from src/smtparser/smtlib_solver.cpp
rename to src/api/smtlib_solver.cpp
diff --git a/src/smtparser/smtlib_solver.h b/src/api/smtlib_solver.h
similarity index 100%
rename from src/smtparser/smtlib_solver.h
rename to src/api/smtlib_solver.h
diff --git a/src/smtparser/smtparser.cpp b/src/api/smtparser.cpp
similarity index 100%
rename from src/smtparser/smtparser.cpp
rename to src/api/smtparser.cpp
diff --git a/src/smtparser/smtparser.h b/src/api/smtparser.h
similarity index 100%
rename from src/smtparser/smtparser.h
rename to src/api/smtparser.h
diff --git a/shell/simple_sat.cpp b/src/dead/simple_sat.cpp
similarity index 100%
rename from shell/simple_sat.cpp
rename to src/dead/simple_sat.cpp
diff --git a/shell/simple_sat.h b/src/dead/simple_sat.h
similarity index 100%
rename from shell/simple_sat.h
rename to src/dead/simple_sat.h
diff --git a/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
similarity index 100%
rename from shell/datalog_frontend.cpp
rename to src/shell/datalog_frontend.cpp
diff --git a/shell/datalog_frontend.h b/src/shell/datalog_frontend.h
similarity index 100%
rename from shell/datalog_frontend.h
rename to src/shell/datalog_frontend.h
diff --git a/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
similarity index 100%
rename from shell/dimacs_frontend.cpp
rename to src/shell/dimacs_frontend.cpp
diff --git a/shell/dimacs_frontend.h b/src/shell/dimacs_frontend.h
similarity index 100%
rename from shell/dimacs_frontend.h
rename to src/shell/dimacs_frontend.h
diff --git a/shell/main.cpp b/src/shell/main.cpp
similarity index 100%
rename from shell/main.cpp
rename to src/shell/main.cpp
diff --git a/shell/options.h b/src/shell/options.h
similarity index 100%
rename from shell/options.h
rename to src/shell/options.h
diff --git a/shell/resource.h b/src/shell/resource.h
similarity index 100%
rename from shell/resource.h
rename to src/shell/resource.h
diff --git a/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
similarity index 100%
rename from shell/smtlib_frontend.cpp
rename to src/shell/smtlib_frontend.cpp
diff --git a/shell/smtlib_frontend.h b/src/shell/smtlib_frontend.h
similarity index 100%
rename from shell/smtlib_frontend.h
rename to src/shell/smtlib_frontend.h
diff --git a/shell/z3_log_frontend.cpp b/src/shell/z3_log_frontend.cpp
similarity index 100%
rename from shell/z3_log_frontend.cpp
rename to src/shell/z3_log_frontend.cpp
diff --git a/shell/z3_log_frontend.h b/src/shell/z3_log_frontend.h
similarity index 100%
rename from shell/z3_log_frontend.h
rename to src/shell/z3_log_frontend.h