diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index 7e1cc79bb..ecf70a8c5 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -7,80 +7,13 @@
 # Author: Leonardo de Moura (leonardo)
 ############################################
 from mk_util import *
+from mk_project import *
 
 parse_options()
 check_eol()
+API_files = init_project_def()
 
-add_lib('util', [])
-add_lib('polynomial', ['util'], 'math/polynomial')
-add_lib('sat', ['util'])
-add_lib('nlsat', ['polynomial', 'sat'])
-add_lib('subpaving', ['util'], 'math/subpaving')
-add_lib('ast', ['util', 'polynomial'])
-add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
-# Simplifier module will be deleted in the future.
-# It has been replaced with rewriter module.
-add_lib('simplifier', ['rewriter'], 'ast/simplifier')
-# Model module should not depend on simplifier module. 
-# We must replace all occurrences of simplifier with rewriter.
-add_lib('model', ['rewriter', 'simplifier'])
-add_lib('tactic', ['ast', 'model'])
-# Old (non-modular) parameter framework. It has been subsumed by util\params.h.
-# However, it is still used by many old components.
-add_lib('old_params', ['model', 'simplifier'])
-add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier'])
-add_lib('substitution', ['ast'], 'ast/substitution')
-add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms')
-add_lib('parser_util', ['ast'], 'parsers/util')
-add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
-add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern')
-add_lib('macros', ['simplifier', 'old_params'], 'ast/macros')
-add_lib('grobner', ['ast'], 'math/grobner')
-add_lib('euclid', ['util'], 'math/euclid')
-add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker')
-add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster')
-add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 
-                'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
-add_lib('user_plugin', ['smt'], 'smt/user_plugin')
-add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
-add_lib('sat_tactic', ['tactic', 'sat'], 'tactic/sat')
-add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
-add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'tactic/nlsat')
-add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'tactic/subpaving')
-add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
-add_lib('fuzzing', ['ast'], 'test/fuzzing')
-add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
-add_lib('smt_tactic', ['smt'], 'tactic/smt')
-add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
-add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
-add_lib('aig', ['tactic'], 'tactic/aig')
-# 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('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogics')
-add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
-add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
-# TODO: delete SMT 1.0 frontend
-add_lib('smtparser', ['portfolio'], 'parsers/smt')
-add_lib('api', ['portfolio', 'user_plugin', 'smtparser'],
-        includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h'])
-add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
-add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
-API_files = ['z3_api.h']
-add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', 
-        reexports=['api'], 
-        dll_name='libz3', 
-        export_files=API_files)
-add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
-add_hlib('cpp', 'bindings/c++', includes2install=['z3++.h'])
-set_z3py_dir('bindings/python')
-# Examples
-add_cpp_example('cpp_example', 'c++') 
-add_c_example('c_example', 'c')
-add_c_example('maxsat')
-add_dotnet_example('dotnet_example', 'dotnet')
-add_z3py_example('python')
-
-update_version(4, 2, 0, 0)
+update_version()
 mk_auto_src()
 mk_bindings(API_files)
 mk_vs_proj('z3', ['shell'])
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
new file mode 100644
index 000000000..f0d5414d8
--- /dev/null
+++ b/scripts/mk_project.py
@@ -0,0 +1,83 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+# 
+# Z3 project configuration files
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+from mk_util import *
+
+# Z3 Project definition
+def init_project_def():
+    set_version(4, 2, 0, 0)
+    add_lib('util', [])
+    add_lib('polynomial', ['util'], 'math/polynomial')
+    add_lib('sat', ['util'])
+    add_lib('nlsat', ['polynomial', 'sat'])
+    add_lib('subpaving', ['util'], 'math/subpaving')
+    add_lib('ast', ['util', 'polynomial'])
+    add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
+    # Simplifier module will be deleted in the future.
+    # It has been replaced with rewriter module.
+    add_lib('simplifier', ['rewriter'], 'ast/simplifier')
+    # Model module should not depend on simplifier module. 
+    # We must replace all occurrences of simplifier with rewriter.
+    add_lib('model', ['rewriter', 'simplifier'])
+    add_lib('tactic', ['ast', 'model'])
+    # Old (non-modular) parameter framework. It has been subsumed by util\params.h.
+    # However, it is still used by many old components.
+    add_lib('old_params', ['model', 'simplifier'])
+    add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier'])
+    add_lib('substitution', ['ast'], 'ast/substitution')
+    add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms')
+    add_lib('parser_util', ['ast'], 'parsers/util')
+    add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
+    add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern')
+    add_lib('macros', ['simplifier', 'old_params'], 'ast/macros')
+    add_lib('grobner', ['ast'], 'math/grobner')
+    add_lib('euclid', ['util'], 'math/euclid')
+    add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker')
+    add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster')
+    add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 
+                    'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
+    add_lib('user_plugin', ['smt'], 'smt/user_plugin')
+    add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
+    add_lib('sat_tactic', ['tactic', 'sat'], 'tactic/sat')
+    add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
+    add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'tactic/nlsat')
+    add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'tactic/subpaving')
+    add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
+    add_lib('fuzzing', ['ast'], 'test/fuzzing')
+    add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
+    add_lib('smt_tactic', ['smt'], 'tactic/smt')
+    add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
+    add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
+    add_lib('aig', ['tactic'], 'tactic/aig')
+    # 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('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogics')
+    add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
+    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
+    # TODO: delete SMT 1.0 frontend
+    add_lib('smtparser', ['portfolio'], 'parsers/smt')
+    add_lib('api', ['portfolio', 'user_plugin', 'smtparser'],
+            includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h'])
+    add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
+    add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
+    API_files = ['z3_api.h']
+    add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', 
+            reexports=['api'], 
+            dll_name='libz3', 
+            export_files=API_files)
+    add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
+    add_hlib('cpp', 'bindings/c++', includes2install=['z3++.h'])
+    set_z3py_dir('bindings/python')
+    # Examples
+    add_cpp_example('cpp_example', 'c++') 
+    add_c_example('c_example', 'c')
+    add_c_example('maxsat')
+    add_dotnet_example('dotnet_example', 'dotnet')
+    add_z3py_example('py_example', 'python')
+    return API_files
+
+
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 275e4212d..76c6cc4f8 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -40,6 +40,21 @@ Z3PY_SRC_DIR=None
 VS_PROJ = False
 TRACE = False
 
+VER_MAJOR=None
+VER_MINOR=None
+VER_BUILD=None
+VER_REVISION=None
+
+def set_version(major, minor, build, revision):
+    global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION
+    VER_MAJOR = major
+    VER_MINOR = minor
+    VER_BUILD = build
+    VER_REVISION = revision
+
+def get_version():
+    return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
+
 def is_cr_lf(fname):
     # Check whether text files use cr/lf
     f = open(fname, 'r')
@@ -191,14 +206,6 @@ def set_z3py_dir(p):
     if VERBOSE:
         print "Python bindinds directory was detected."
 
-def add_z3py_example(p):
-    mk_dir(BUILD_DIR)
-    full = '%s/%s' % (EXAMPLE_DIR, p)
-    for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
-        shutil.copyfile('%s/%s' % (full, py), '%s/%s' % (BUILD_DIR, py))
-        if is_verbose():
-            print "Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)
-
 _UNIQ_ID = 0
 
 def mk_fresh_name(prefix):
@@ -217,6 +224,9 @@ _Processed_Headers = set()
 def get_component(name):
     return _Name2Component[name]
 
+def get_components():
+    return _Components
+
 # Return the directory where the python bindings are located.
 def get_z3py_dir():
     return Z3PY_SRC_DIR
@@ -361,6 +371,12 @@ class Component:
 
     def is_example(self):
         return False
+    
+    # Invoked when creating a (windows) distribution package using components at build_path, and
+    # storing them at dist_path
+    def mk_win_dist(self, build_path, dist_path):
+        return
+
 
 class LibComponent(Component):
     def __init__(self, name, path, deps, includes2install):
@@ -396,6 +412,12 @@ class LibComponent(Component):
         for include in self.includes2install:
             out.write('\t@rm -f $(PREFIX)/include/%s\n' % include)
 
+    def mk_win_dist(self, build_path, dist_path):
+        mk_dir('%s/include' % dist_path)
+        for include in self.includes2install:
+            shutil.copy('%s/%s' % (self.src_dir, include),
+                        '%s/include/%s' % (dist_path, include))        
+
 # "Library" containing only .h files. This is just a placeholder for includes files to be installed.
 class HLibComponent(LibComponent):
     def __init__(self, name, path, includes2install):
@@ -467,6 +489,12 @@ class ExeComponent(Component):
             exefile = '%s$(EXE_EXT)' % self.exe_name
             out.write('\t@rm -f $(PREFIX)/bin/%s\n' % exefile)
 
+    def mk_win_dist(self, build_path, dist_path):
+        if self.install:
+            mk_dir('%s/bin' % dist_path)
+            shutil.copy('%s/%s.exe' % (build_path, self.exe_name),
+                        '%s/bin/%s.exe' % (dist_path, self.exe_name))
+
 
 class DLLComponent(Component):
     def __init__(self, name, dll_name, path, deps, export_files, reexports, install):
@@ -538,6 +566,12 @@ class DLLComponent(Component):
             out.write('\t@rm -f $(PREFIX)/lib/%s\n' % dllfile)
             out.write('\t@rm -f %s/%s\n' % (PYTHON_PACKAGE_DIR, dllfile))
 
+    def mk_win_dist(self, build_path, dist_path):
+        if self.install:
+            mk_dir('%s/lib' % dist_path)
+            shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
+                        '%s/lib/%s.dll' % (dist_path, self.dll_name))
+
 class DotNetDLLComponent(Component):
     def __init__(self, name, dll_name, path, deps, assembly_info_dir):
         Component.__init__(self, name, path, deps)
@@ -583,6 +617,12 @@ class DotNetDLLComponent(Component):
     def has_assembly_info(self):
         return True
 
+    def mk_win_dist(self, build_path, dist_path):
+        # Assuming all DotNET dll should be in the distribution
+        mk_dir('%s/lib' % dist_path)
+        shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
+                    '%s/lib/%s.dll' % (dist_path, self.dll_name))
+
 class ExampleComponent(Component):
     def __init__(self, name, path):
         Component.__init__(self, name, path, [])
@@ -592,6 +632,7 @@ class ExampleComponent(Component):
     def is_example(self):
         return True
 
+
 class CppExampleComponent(ExampleComponent):
     def __init__(self, name, path):
         ExampleComponent.__init__(self, name, path)
@@ -666,6 +707,21 @@ class DotNetExampleComponent(ExampleComponent):
             out.write('\n')
             out.write('_ex_%s: %s\n\n' % (self.name, exefile))
 
+class PythonExampleComponent(ExampleComponent):
+    def __init__(self, name, path):
+        ExampleComponent.__init__(self, name, path)
+
+    # Python examples are just placeholders, we just copy the *.py files when mk_makefile is invoked.
+    # We don't need to include them in the :examples rule
+    def mk_makefile(self, out):
+        full = '%s/%s' % (EXAMPLE_DIR, self.path)
+        for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
+            shutil.copyfile('%s/%s' % (full, py), '%s/%s' % (BUILD_DIR, py))
+            if is_verbose():
+                print "Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)
+        out.write('_ex_%s: \n\n' % self.name)
+
+
 def reg_component(name, c):
     global _Id, _Components, _ComponentNames, _Name2Component
     c.id = _Id
@@ -708,6 +764,10 @@ def add_dotnet_example(name, path=None):
     c = DotNetExampleComponent(name, path)
     reg_component(name, c)
 
+def add_z3py_example(name, path=None):
+    c = PythonExampleComponent(name, path)
+    reg_component(name, c)
+
 # Copy configuration correct file to BUILD_DIR
 def cp_config_mk():
     if IS_WINDOW:
@@ -732,7 +792,7 @@ def mk_install(out):
     out.write('\t@mkdir -p $(PREFIX)/bin\n')
     out.write('\t@mkdir -p $(PREFIX)/include\n')
     out.write('\t@mkdir -p $(PREFIX)/lib\n')
-    for c in _Components:
+    for c in get_components():
         c.mk_install(out)
     out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
     out.write('\t@echo Z3 was successfully installed.\n')
@@ -740,7 +800,7 @@ def mk_install(out):
 
 def mk_uninstall(out):
     out.write('uninstall:\n')
-    for c in _Components:
+    for c in get_components():
         c.mk_uninstall(out)
     out.write('\t@rm -f %s/z3*.pyc\n' % PYTHON_PACKAGE_DIR)
     out.write('\t@echo Z3 was successfully uninstalled.\n')
@@ -757,7 +817,7 @@ def mk_makefile():
     out.write('include config.mk\n')
     # Generate :all rule
     out.write('all:')
-    for c in _Components:
+    for c in get_components():
         if c.main_component():
             out.write(' %s' % c.name)
     out.write('\n\t@echo Z3 was successfully built.\n')
@@ -766,12 +826,12 @@ def mk_makefile():
         out.write('\t@echo "    sudo make install"\n')
     # Generate :examples rule
     out.write('examples:')
-    for c in _Components:
+    for c in get_components():
         if c.is_example():
             out.write(' _ex_%s' % c.name)
     out.write('\n\t@echo Z3 examples were successfully built.\n')
     # Generate components
-    for c in _Components:
+    for c in get_components():
         c.mk_makefile(out)
     # Generate install/uninstall rules if not WINDOWS
     if not IS_WINDOW:
@@ -818,7 +878,13 @@ def mk_pat_db():
         print "Generated '%s/database.h'" % c.src_dir
 
 # Update version numbers
-def update_version(major, minor, build, revision):
+def update_version():
+    major = VER_MAJOR
+    minor = VER_MINOR
+    build = VER_BUILD
+    revision = VER_REVISION
+    if major == None or minor == None or build == None or revision == None:
+        raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
     if not ONLY_MAKEFILES:
         mk_version_dot_h(major, minor, build, revision)
         update_all_assembly_infos(major, minor, build, revision)
@@ -838,7 +904,7 @@ def mk_version_dot_h(major, minor, build, revision):
 
 # Update version number in AssemblyInfo.cs files
 def update_all_assembly_infos(major, minor, build, revision):
-    for c in _Components:
+    for c in get_components():
         if c.has_assembly_info():
             assembly = '%s/%s/AssemblyInfo.cs' % (c.src_dir, c.assembly_info_dir)
             if os.path.exists(assembly):
@@ -962,7 +1028,7 @@ def mk_install_tactic_cpp(cnames, path):
 
 def mk_all_install_tactic_cpps():
     if not ONLY_MAKEFILES:
-        for c in _Components:
+        for c in get_components():
             if c.require_install_tactics():
                 cnames = []
                 cnames.extend(c.deps)
@@ -995,7 +1061,7 @@ def mk_def_file(c):
 
 def mk_def_files():
     if not ONLY_MAKEFILES:
-        for c in _Components:
+        for c in get_components():
             if c.require_def_file():
                 mk_def_file(c)
 
@@ -1273,3 +1339,11 @@ def mk_vs_proj(name, components):
     f.write('</Project>\n')
     if is_verbose():
         print "Generated '%s'" % proj_name
+
+def mk_win_dist(build_path, dist_path):
+    for c in get_components():
+        c.mk_win_dist(build_path, dist_path)
+    # Add Z3Py to lib directory
+    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
+        shutil.copy('%s/%s' % (build_path, pyc),
+                    '%s/lib/%s' % (dist_path, pyc))
diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
new file mode 100644
index 000000000..1b30f0951
--- /dev/null
+++ b/scripts/mk_win_dist.py
@@ -0,0 +1,201 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+# 
+# Scripts for automatically generating 
+# Window distribution zip files.
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+import os
+import glob
+import re
+import getopt
+import sys
+import shutil
+import subprocess
+import zipfile
+from mk_exception import *
+from mk_project import *
+
+BUILD_DIR='build-dist'
+BUILD_X64_DIR='build-dist/x64'
+BUILD_X86_DIR='build-dist/x86'
+VERBOSE=True
+DIST_DIR='dist'
+
+def set_verbose(flag):
+    global VERBOSE
+    VERBOSE = flag
+
+def is_verbose():
+    return VERBOSE
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        os.makedirs(d)
+
+def set_build_dir(path):
+    global BUILD_DIR
+    BUILD_DIR = path
+    BUILD_X86_DIR = '%s/x86' % path
+    BUILD_X64_DIR = '%s/x64' % path
+    mk_dir(BUILD_X86_DIR)
+    mk_dir(BUILD_X64_DIR)
+
+def display_help():
+    print "mk_win_dist.py: Z3 Windows distribution generator\n"
+    print "This script generates the zip files containing executables, dlls, header files for Windows."
+    print "It must be executed from the Z3 root directory."
+    print "\nOptions:"
+    print "  -h, --help                    display this message."
+    print "  -s, --silent                  do not print verbose messages."
+    print "  -b <sudir>, --build=<subdir>  subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)."
+    exit(0)
+
+# Parse configuration option for mk_make script
+def parse_options():
+    path = BUILD_DIR
+    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hs', ['build=', 
+                                                                  'help',
+                                                                  'silent',
+                                                                  ])
+    for opt, arg in options:
+        if opt in ('-b', '--build'):
+            if arg == 'src':
+                raise MKException('The src directory should not be used to host the Makefile')
+            path = arg
+        elif opt in ('-s', '--silent'):
+            set_verbose(False)
+        elif opt in ('-h', '--help'):
+            display_help()
+        else:
+            raise MKException("Invalid command line option '%s'" % opt)
+    set_build_dir(path)
+
+# Check whether build directory already exists or not
+def check_build_dir(path):
+    return os.path.exists(path) and os.path.exists('%s/Makefile' % path)
+
+# Create a build directory using mk_make.py
+def mk_build_dir(path, x64):
+    if not check_build_dir(path):
+        opts = ["python", "scripts/mk_make.py", "-b", path]
+        if x64:
+            opts.append('-x')
+        if subprocess.call(opts) != 0:
+            raise MKException("Failed to generate build directory at '%s'" % path)
+    
+# Create build directories
+def mk_build_dirs():
+    mk_build_dir(BUILD_X86_DIR, False)
+    mk_build_dir(BUILD_X64_DIR, True)
+
+# Check if on Visual Studio command prompt
+def check_vc_cmd_prompt():
+    try:
+        subprocess.call(['cl'], stdin=subprocess.PIPE, stderr=subprocess.PIPE)
+    except:
+        raise MKException("You must execute the mk_win_dist.py script on a Visual Studio Command Prompt")
+
+def exec_cmds(cmds):
+    cmd_file = 'z3_tmp.cmd'
+    f = open(cmd_file, 'w')
+    for cmd in cmds:
+        f.write(cmd)
+        f.write('\n')
+    f.close()
+    res = 0
+    try:
+        res = subprocess.call(cmd_file, shell=True)
+    except:
+        res = 1
+    try:
+        os.erase(cmd_file)
+    except:
+        pass
+    return res
+
+# Compile Z3 (if x64 == True, then it builds it in x64 mode).
+def mk_z3_core(x64):
+    cmds = []
+    if x64:
+        cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
+        cmds.append('cd %s' % BUILD_X64_DIR)    
+    else:
+        cmds.append('"call %VCINSTALLDIR%vcvarsall.bat" x86')
+        cmds.append('cd %s' % BUILD_X86_DIR)
+    cmds.append('nmake')
+    if exec_cmds(cmds) != 0:
+        raise MKException("Failed to make z3, x64: %s" % x64)
+
+def mk_z3():
+    mk_z3_core(False)
+    mk_z3_core(True)
+
+def mk_dist_dir_core(x64):
+    major, minor, build, revision = get_version()
+    if x64:
+        platform = "x64"
+        build_path = BUILD_X64_DIR
+    else:
+        platform = "x86"
+        build_path = BUILD_X86_DIR
+    dist_path = '%s/z3-%s.%s.%s-%s' % (DIST_DIR, major, minor, build, platform)
+    mk_dir(dist_path)
+    mk_win_dist(build_path, dist_path)
+    if is_verbose():
+        print "Generated %s distribution folder at '%s'" % (platform, dist_path)
+
+def mk_dist_dir():
+    mk_dist_dir_core(False)
+    mk_dist_dir_core(True)
+
+ZIPOUT = None
+
+def mk_zip_visitor(pattern, dir, files):
+    for filename in files:
+        if fnmatch(filename, pattern):
+            fname = os.path.join(dir, filename)
+            if not os.path.isdir(fname):
+                ZIPOUT.write(fname)
+
+def mk_zip_core(x64):
+    global ZIPOUT
+    major, minor, build, revision = get_version()
+    if x64:
+        platform = "x64"
+    else:
+        platform = "x86"
+    dist_path = 'z3-%s.%s.%s-%s' % (major, minor, build, platform)
+    old = os.getcwd()
+    try:
+        os.chdir(DIST_DIR)
+        zfname = '%s.zip' % dist_path
+        ZIPOUT = zipfile.ZipFile(zfname, 'w')
+        os.path.walk(dist_path, mk_zip_visitor, '*')
+        if is_verbose():
+            print "Generated '%s'" % zfname
+    except:
+        pass
+    ZIPOUT = None
+    os.chdir(old)
+
+# Create a zip file for each platform
+def mk_zip():
+    mk_zip_core(False)
+    mk_zip_core(True)
+
+# Entry point
+def main():
+    if os.name != 'nt':
+        raise MKException("This script is for Windows only")
+    parse_options()
+    check_vc_cmd_prompt()
+    mk_build_dirs()
+    mk_z3()
+    init_project_def()
+    mk_dist_dir()
+    mk_zip()
+
+main()
+
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index b5485e35d..a19474ceb 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -56,11 +56,13 @@ void error(const char * msg) {
 }
 
 void display_usage() {
+    std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << " - ";
 #ifdef _AMD64_
-    std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << " - 64 bit]. (C) Copyright 2006 Microsoft Corp.\n";
+    std::cout << "64";
 #else
-    std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << " - 32 bit]. (C) Copyright 2006 Microsoft Corp.\n";
+    std::cout << "32";
 #endif
+    std::cout << " bit]. (C) Copyright 2006 Microsoft Corp.\n";
     std::cout << "Usage: z3 [options] [" << OPT << "file:]file\n";
     std::cout << "\nInput format:\n";
     std::cout << "  " << OPT << "smt        use parser for SMT input format.\n";
diff --git a/src/test/imdd.cpp b/src/test/imdd.cpp
index 12d23993e..bfaca274c 100644
--- a/src/test/imdd.cpp
+++ b/src/test/imdd.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #include"imdd.h"
 
-#ifndef _AMD64_
+#if !defined(_AMD64_) && defined(Z3DEBUG)
 
 static void tst0() {
     std::cout << "--------------------------------\n";