diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index d93a13129..01f9e687e 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -11,7 +11,7 @@ Version 4.4
 
 - Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one.
 
-- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, and Codeplex users rsas, clockish, Heizmann.
+- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, and Stackoverflow users user297886.
 
 
 Version 4.3.2
diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 0d8a3ceb3..e48c23905 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -975,6 +975,15 @@ void substitute_example() {
     std::cout << new_f << std::endl;
 }
 
+void extract_example() {
+    std::cout << "extract example\n";
+    context c;
+    expr x(c);
+    x = c.constant("x", c.bv_sort(32));
+    expr y = x.extract(21, 10);
+    std::cout << y << " " << y.hi() << " " << y.lo() << "\n";
+}
+
 int main() {
     try {
         demorgan(); std::cout << "\n";
@@ -1013,6 +1022,7 @@ int main() {
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";
+        extract_example(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 2ed420c20..0f4fdb216 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1376,6 +1376,7 @@ class MLComponent(Component):
             sub_dir = os.path.join('api', 'ml')
             mk_dir(os.path.join(BUILD_DIR, sub_dir))
             api_src = get_component(API_COMPONENT).to_src_dir
+            out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it.
             for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
                 out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
                 str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
@@ -1412,7 +1413,7 @@ class MLComponent(Component):
                       (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'), 
                        os.path.join(sub_dir, 'z3native_stubs.c'), 
                        get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'));
-            out.write('\t$(CC) $(CXXFLAGS) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % 
+            out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % 
                       (OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs')))
 
             out.write('%s: %s %s %s$(SO_EXT)' % (
@@ -1695,7 +1696,7 @@ def mk_config():
             'OBJ_EXT=.obj\n'
             'LIB_EXT=.lib\n'
             'AR=lib\n'
-            'AR_FLAGS=/nologo\n'
+            'AR_FLAGS=/nologo /LTCG\n'
             'AR_OUTFLAG=/OUT:\n'
             'EXE_EXT=.exe\n'
             'LINK=cl\n'
@@ -1713,16 +1714,16 @@ def mk_config():
                 'SLINK_FLAGS=/nologo /LDd\n')
             if not VS_X64:
                 config.write(
-                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
+                    'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
+                    'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
+                    'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
             else:
                 config.write(
-                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
+                    'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
+                    'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
+                    'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
         else:
             # Windows Release mode
             config.write(
@@ -1732,16 +1733,16 @@ def mk_config():
                 extra_opt = '%s /D _TRACE' % extra_opt
             if not VS_X64:
                 config.write(
-                    'CXXFLAGS=/nologo /c /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
+                    'CXXFLAGS=/nologo /c /GL /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
+                    'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
+                    'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
             else:
                 config.write(
-                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt)
+                    'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt)
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
-                    'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')
+                    'LINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
+                    'SLINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')
 
         # End of Windows VS config.mk
         if is_verbose():
@@ -1782,7 +1783,7 @@ def mk_config():
                 FOCI2 = False
         if GIT_HASH:
             CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
-        CXXFLAGS = '%s -c' % CXXFLAGS
+        CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
         HAS_OMP = test_openmp(CXX)
         if HAS_OMP:
             CXXFLAGS = '%s -fopenmp -mfpmath=sse' % CXXFLAGS
@@ -2104,7 +2105,7 @@ def mk_pat_db():
     c = get_component(PATTERN_COMPONENT)
     fin  = open(os.path.join(c.src_dir, 'database.smt2'), 'r')
     fout = open(os.path.join(c.src_dir, 'database.h'), 'w')
-    fout.write('char const * g_pattern_database =\n')
+    fout.write('static char const g_pattern_database[] =\n')
     for line in fin:
         fout.write('"%s\\n"\n' % line.strip('\n'))
     fout.write(';\n')
diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index 3a95fb730..33d7a3eab 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -39,7 +39,7 @@ def mk_dir(d):
         os.makedirs(d)
 
 def set_build_dir(path):
-    global BUILD_DIR
+    global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR
     BUILD_DIR = path
     BUILD_X86_DIR = os.path.join(path, 'x86')
     BUILD_X64_DIR = os.path.join(path, 'x64')
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 889044d1f..93800237e 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -642,6 +642,7 @@ def mk_java():
     java_wrapper.write('#ifdef __cplusplus\n')
     java_wrapper.write('extern "C" {\n')
     java_wrapper.write('#endif\n\n')
+    java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n')
     java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n')
     java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW)                                   \\\n')
     java_wrapper.write('  T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n')
@@ -688,13 +689,13 @@ def mk_java():
     java_wrapper.write('  // upon errors, but the actual error handling is done by throwing exceptions in the\n')
     java_wrapper.write('  // wrappers below.\n')
     java_wrapper.write('}\n\n')
-    java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str)
+    java_wrapper.write('DLL_VIS JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str)
     java_wrapper.write('{\n')
     java_wrapper.write('  Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n')
     java_wrapper.write('}\n\n')
     java_wrapper.write('')
     for name, result, params in _dotnet_decls:
-        java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
+        java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
         i = 0;
         for param in params:
             java_wrapper.write(', ')
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index b9c6230b7..20ef9ba7f 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -300,7 +300,7 @@ extern "C" {
         Z3_CATCH_RETURN(-1);
     }
     
-    char const * Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s) {
+    Z3_API char const * Z3_get_symbol_string(Z3_context c, Z3_symbol s) {
         Z3_TRY;
         LOG_Z3_get_symbol_string(c, s);
         RESET_ERROR_CODE();
@@ -823,7 +823,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    char const * Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a) {
+    Z3_API char const * Z3_ast_to_string(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_ast_to_string(c, a);
         RESET_ERROR_CODE();
@@ -866,11 +866,11 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    char const * Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s) {
+    Z3_API char const * Z3_sort_to_string(Z3_context c, Z3_sort s) {
         return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(s));
     }
 
-    char const * Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) {
+    Z3_API char const * Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) {
         return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(f));
     }
 
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 3408cdf3c..49fa10d94 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -548,12 +548,12 @@ extern "C" {
         }
     }
 
-    char const * Z3_API Z3_get_error_msg(Z3_error_code err) {
+    Z3_API char const * Z3_get_error_msg(Z3_error_code err) {
         LOG_Z3_get_error_msg(err);
         return _get_error_msg_ex(0, err);
     }
 
-    char const * Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
+    Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
         LOG_Z3_get_error_msg_ex(c, err);
         return _get_error_msg_ex(c, err);
     }
@@ -577,7 +577,7 @@ extern "C" {
     
 };
 
-ast_manager & Z3_API Z3_get_manager(__in Z3_context c) {
+Z3_API ast_manager& Z3_get_manager(__in Z3_context c) {
     return mk_c(c)->m();
 }
 
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index dd689dcb0..38d726761 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -293,10 +293,10 @@ extern "C" {
         else {
             model_ref _m;
             m_solver.get()->get_model(_m);
-            Z3_model_ref *crap = alloc(Z3_model_ref);
-            crap->m_model = _m.get();
-            mk_c(c)->save_object(crap);
-            *model = of_model(crap);
+            Z3_model_ref *tmp_val = alloc(Z3_model_ref);
+            tmp_val->m_model = _m.get();
+            mk_c(c)->save_object(tmp_val);
+            *model = of_model(tmp_val);
         }
 
         *out_interp = of_ast_vector(v);
@@ -490,8 +490,8 @@ extern "C" {
         try {
             std::string foo(filename);
             if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){
-                Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
-                Z3_app app = Z3_to_app(ctx, ass);
+                Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
+                Z3_app app = Z3_to_app(ctx, assrts);
                 int nconjs = Z3_get_app_num_args(ctx, app);
                 assertions.resize(nconjs);
                 for (int k = 0; k < nconjs; k++)
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index f0c31d800..0ae1a9948 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -651,7 +651,7 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
-    char const * Z3_API Z3_model_to_string(Z3_context c, Z3_model m) {
+    Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) {
         Z3_TRY;
         LOG_Z3_model_to_string(c, m);
         RESET_ERROR_CODE();
diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp
index 4170852a9..727005186 100644
--- a/src/api/api_quant.cpp
+++ b/src/api/api_quant.cpp
@@ -507,7 +507,7 @@ extern "C" {
         return (Z3_ast)(p); 
     }    
 
-    char const * Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
+    Z3_API char const * Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
         return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
     }
     
diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp
index b81fb2f2c..7e994a0e2 100644
--- a/src/api/api_solver_old.cpp
+++ b/src/api/api_solver_old.cpp
@@ -297,7 +297,7 @@ extern "C" {
         Z3_CATCH;
     }
 
-    char const * Z3_API Z3_context_to_string(Z3_context c) {
+    Z3_API char const * Z3_context_to_string(Z3_context c) {
         Z3_TRY;
         LOG_Z3_context_to_string(c);
         RESET_ERROR_CODE();
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 7380e52f1..f43ba83e5 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -866,6 +866,9 @@ namespace z3 {
         friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
 
         friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
+        expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
+        unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); } 
+        unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); } 
 
         /**
            \brief Return a simplified version of this expression.
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 4b330ff86..db3f46bfd 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -176,9 +176,9 @@ public class Solver extends Z3Object
      **/
     public int getNumAssertions() throws Z3Exception
     {
-        ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        return ass.size();
+        return assrts.size();
     }
 
     /**
@@ -188,12 +188,12 @@ public class Solver extends Z3Object
      **/
     public BoolExpr[] getAssertions() throws Z3Exception
     {
-        ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        int n = ass.size();
+        int n = assrts.size();
         BoolExpr[] res = new BoolExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject());
+            res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
         return res;
     }
 
diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h
index a4a0cb4be..7a0b6857c 100644
--- a/src/api/z3_macros.h
+++ b/src/api/z3_macros.h
@@ -35,7 +35,11 @@
 #endif
 
 #ifndef Z3_API
-#define Z3_API
+# ifdef __GNUC__
+#  define Z3_API __attribute__ ((visibility ("default")))
+# else
+#  define Z3_API
+# endif
 #endif 
 
 #ifndef DEFINE_TYPE
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index b28b640bb..805f3070f 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -34,9 +34,9 @@ Revision History:
 // ---------------------------------------
 // smt_renaming
 
-const static char* m_predef_names[] = {
+static const char m_predef_names[][8] = {
     "=", ">=", "<=", "+", "-", "*", ">", "<", "!=", "or", "and", "implies", "not", "iff", "xor",
-    "true", "false", "forall", "exists", "let", "flet", NULL
+    "true", "false", "forall", "exists", "let", "flet"
 };
 
 symbol smt_renaming::fix_symbol(symbol s, int k) {
@@ -120,8 +120,8 @@ bool smt_renaming::all_is_legal(char const* s) {
 }
 
 smt_renaming::smt_renaming() {
-    for (const char **p = m_predef_names; *p; ++p) {
-        symbol s(*p);
+    for (unsigned i = 0; i < ARRAYSIZE(m_predef_names); ++i) {
+        symbol s(m_predef_names[i]);
         m_translate.insert(s, s);
         m_rev_translate.insert(s, s);
     }
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index 9bdaf4959..6268c761d 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -26,8 +26,6 @@ Notes:
 
 template<typename Config>
 class poly_rewriter : public Config {
-public:
-    static char const * g_ste_blowup_msg;
 protected:
     typedef typename Config::numeral numeral; 
     sort *   m_curr_sort;
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 036221f96..0a00a7199 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -22,9 +22,6 @@ Notes:
 #include"ast_ll_pp.h"
 #include"ast_smt2_pp.h"
 
-template<typename Config>
-char const * poly_rewriter<Config>::g_ste_blowup_msg = "sum of monomials blowup";
-
 
 template<typename Config>
 void poly_rewriter<Config>::updt_params(params_ref const & _p) {
@@ -356,7 +353,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
         TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " ";
               tout << "\n";);
         if (sum.size() > m_som_blowup)
-            throw rewriter_exception(g_ste_blowup_msg);
+            throw rewriter_exception("sum of monomials blowup");
         m_args.reset();
         for (unsigned i = 0; i < num_args; i++) {
             expr * const * v = sums[i];
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f5937955d..0c60d876b 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1185,6 +1185,7 @@ void cmd_context::reset(bool finalize) {
     restore_assertions(0);
     if (m_solver)
         m_solver = 0;
+    m_scopes.reset();
     m_pp_env = 0;
     m_dt_eh  = 0;
     if (m_manager) {
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index f87c8d264..13f6f5be3 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -24,6 +24,16 @@ Notes:
 #include"solver.h"
 
 context_params::context_params() {
+    m_unsat_core     = false;
+    m_model          = true;
+    m_model_validate = false;
+    m_auto_config    = true;
+    m_proof          = false;
+    m_trace          = false;
+    m_debug_ref_count = false;
+    m_smtlib2_compliant = false;
+    m_well_sorted_check = false;
+    m_timeout = UINT_MAX;
     updt_params();
 }
 
@@ -98,17 +108,17 @@ void context_params::updt_params() {
 }
 
 void context_params::updt_params(params_ref const & p) {
-    m_timeout           = p.get_uint("timeout", UINT_MAX);
-    m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
-    m_auto_config       = p.get_bool("auto_config", true);
-    m_proof             = p.get_bool("proof", false);
-    m_model             = p.get_bool("model", true);
-    m_model_validate    = p.get_bool("model_validate", false);
-    m_trace             = p.get_bool("trace", false);
+    m_timeout           = p.get_uint("timeout", m_timeout);
+    m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check));
+    m_auto_config       = p.get_bool("auto_config", m_auto_config);
+    m_proof             = p.get_bool("proof", m_proof);
+    m_model             = p.get_bool("model", m_model);
+    m_model_validate    = p.get_bool("model_validate", m_model_validate);
+    m_trace             = p.get_bool("trace", m_trace);
     m_trace_file_name   = p.get_str("trace_file_name", "z3.log");
-    m_unsat_core        = p.get_bool("unsat_core", false);
-    m_debug_ref_count   = p.get_bool("debug_ref_count", false);
-    m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false);
+    m_unsat_core        = p.get_bool("unsat_core", m_unsat_core);
+    m_debug_ref_count   = p.get_bool("debug_ref_count", m_debug_ref_count);
+    m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant);
 }
 
 void context_params::collect_param_descrs(param_descrs & d) {
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index e2a5d05dc..eefb3b85f 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -1131,10 +1131,10 @@ namespace Duality {
           }
           std::vector<expr> *cnsts[2] = { &child->getTerms(), &assumptions->getTerms() };
           for (unsigned i = 0; i < assumps.size(); i++) {
-              expr &ass = assumps[i];
-              expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass;
+              expr &as = assumps[i];
+              expr alit = (as.is_app() && as.decl().get_decl_kind() == Implies) ? as.arg(0) : as;
               bool isA = map.find(alit) != map.end();
-              cnsts[isA ? 0 : 1]->push_back(ass);
+              cnsts[isA ? 0 : 1]->push_back(as);
           }
       }
       else
@@ -3221,12 +3221,12 @@ done:
     std::vector<expr> assumps, core, conjuncts;
     AssertEdgeCache(edge,assumps);
     for(unsigned i = 0; i < edge->Children.size(); i++){
-      expr ass = GetAnnotation(edge->Children[i]);
+      expr as = GetAnnotation(edge->Children[i]);
       std::vector<expr> clauses;
-      if(!ass.is_true()){
-	CollectConjuncts(ass.arg(1),clauses);
+      if(!as.is_true()){
+	CollectConjuncts(as.arg(1),clauses);
 	for(unsigned j = 0; j < clauses.size(); j++)
-	  GetAssumptionLits(ass.arg(0) || clauses[j],assumps);
+	  GetAssumptionLits(as.arg(0) || clauses[j],assumps);
       }
     }
     expr fmla = GetAnnotation(node);
diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp
index 389a64b6c..9c08a0e31 100755
--- a/src/interp/iz3scopes.cpp
+++ b/src/interp/iz3scopes.cpp
@@ -165,7 +165,7 @@ scopes::range scopes::range_glb(const range &rng1, const range &rng2){
 	  return bar.first->second;
 	  //std::pair<hash_set<scopes::range_lo>::iterator,bool> bar = rt->unique.insert(foo);
 	  // const range_lo *baz = &*(bar.first); 
-	  // return (range_lo *)baz; // exit const hell
+	  // return (range_lo *)baz; // coerce const
   }
 
   scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index ae4c657bd..9110014bf 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -276,8 +276,8 @@ expr * func_interp::get_interp() const {
     return r;
 }
 
-func_interp * func_interp::translate(ast_translation & translator) const {
-    func_interp * new_fi = alloc(func_interp, m_manager, m_arity);
+func_interp * func_interp::translate(ast_translation & translator) const {    
+    func_interp * new_fi = alloc(func_interp, translator.to(), m_arity);
 
     ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
     ptr_vector<func_entry>::const_iterator end = m_entries.end();
diff --git a/src/model/model.cpp b/src/model/model.cpp
index a6b9695b4..73a39a8eb 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -74,6 +74,7 @@ void model::register_decl(func_decl * d, expr * v) {
 
 void model::register_decl(func_decl * d, func_interp * fi) {
     SASSERT(d->get_arity() > 0);
+    SASSERT(&fi->m() == &m_manager);
     decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
     if (entry->get_data().m_value == 0) {
         // new entry
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 017bac724..1849903c5 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -884,14 +884,15 @@ namespace datalog {
     struct uninterpreted_function_finder_proc {
         ast_manager& m;
         datatype_util m_dt;
+        dl_decl_util  m_dl;
         bool m_found;
         func_decl* m_func;
         uninterpreted_function_finder_proc(ast_manager& m): 
-            m(m), m_dt(m), m_found(false), m_func(0) {}
+            m(m), m_dt(m), m_dl(m), m_found(false), m_func(0) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) { }
         void operator()(app * n) {
-            if (is_uninterp(n)) {
+            if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) {
                 m_found = true;
                 m_func = n->get_decl();
             }
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 60a10190a..7344f187c 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -828,7 +828,7 @@ namespace datalog {
             SASSERT(&expl_singleton->get_plugin()==m_er_plugin);
             m_e_fact_relation = static_cast<explanation_relation *>(expl_singleton);
         }
-        func_decl_set const& predicates = m_context.get_predicates();
+        func_decl_set predicates(m_context.get_predicates());
         decl_set::iterator it = predicates.begin();
         decl_set::iterator end = predicates.end();
         for (; it!=end; ++it) {
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 9421b26df..7fcca9ce2 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -734,6 +734,7 @@ namespace datalog {
 
     relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src, 
             const relation_base * delta) { 
+        TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << "\n";); 
         relation_union_fn * res = tgt.get_plugin().mk_union_fn(tgt, src, delta);
         if(!res && &tgt.get_plugin()!=&src.get_plugin()) {
             res = src.get_plugin().mk_union_fn(tgt, src, delta);
diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h
index 00a92748a..72448f026 100644
--- a/src/muz/rel/karr_relation.h
+++ b/src/muz/rel/karr_relation.h
@@ -45,7 +45,7 @@ namespace datalog {
         {}            
         
         virtual bool can_handle_signature(const relation_signature & sig) {
-            return true;
+            return get_manager().get_context().karr();
         }
 
         static symbol get_name() { return symbol("karr_relation"); }
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index b5f6521b8..6314d6fad 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -19,6 +19,7 @@ Revision History:
 #include<memory.h>
 #include"sat_clause.h"
 #include"z3_exception.h"
+#include"trace.h"
 
 namespace sat {
 
@@ -173,6 +174,7 @@ namespace sat {
     }
 
     void clause_allocator::del_clause(clause * cls) {
+        TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());
         size_t size = clause::get_obj_size(cls->m_capacity);
 #ifdef _AMD64_
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index a2c1c7871..6a7ca6280 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -128,6 +128,11 @@ namespace sat {
             if (j == 0) {
                 // empty clause
                 m_solver.set_conflict(justification());
+                for (; it != end; ++it) {
+                    *it2 = *it;
+                    it2++;
+                }
+                cs.set_end(it2);
                 return;
             }
             TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index b5d9f1550..d0052b8c2 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -207,6 +207,24 @@ namespace sat {
         }
         return true;
     }
+
+    bool integrity_checker::check_disjoint_clauses() const {
+        uint_set ids;
+        clause_vector::const_iterator it  = s.m_clauses.begin();
+        clause_vector::const_iterator end = s.m_clauses.end();
+        for (; it != end; ++it) {
+            ids.insert((*it)->id());
+        }
+        it = s.m_learned.begin();
+        end = s.m_learned.end();
+        for (; it != end; ++it) {
+            if (ids.contains((*it)->id())) {
+                TRACE("sat", tout << "Repeated clause: " << (*it)->id() << "\n";);
+                return false;
+            }
+        }
+        return true;
+    }
     
     bool integrity_checker::operator()() const {
         if (s.inconsistent())
@@ -216,6 +234,7 @@ namespace sat {
         SASSERT(check_watches());
         SASSERT(check_bool_vars());
         SASSERT(check_reinit_stack());
+        SASSERT(check_disjoint_clauses());
         return true;
     }
 };
diff --git a/src/sat/sat_integrity_checker.h b/src/sat/sat_integrity_checker.h
index fc3da8c5d..8aa9340c0 100644
--- a/src/sat/sat_integrity_checker.h
+++ b/src/sat/sat_integrity_checker.h
@@ -36,6 +36,7 @@ namespace sat {
         bool check_bool_vars() const;
         bool check_watches() const;
         bool check_reinit_stack() const;
+        bool check_disjoint_clauses() const;
         bool operator()() const;
     };
 };
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 219b9f278..e67043c04 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -227,6 +227,7 @@ namespace sat {
     }
 
     void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
+        TRACE("sat", tout << "cleanup_clauses\n";);
         clause_vector::iterator it  = cs.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = cs.end();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index f898130af..5c0d60260 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -50,7 +50,10 @@ namespace sat {
     }
 
     solver::~solver() {
+        SASSERT(check_invariant());
+        TRACE("sat", tout << "Delete clauses\n";);
         del_clauses(m_clauses.begin(), m_clauses.end());
+        TRACE("sat", tout << "Delete learned\n";);
         del_clauses(m_learned.begin(), m_learned.end());
     }
 
@@ -1121,6 +1124,7 @@ namespace sat {
        \brief GC (the second) half of the clauses in the database.
     */
     void solver::gc_half(char const * st_name) {
+        TRACE("sat", tout << "gc\n";);
         unsigned sz     = m_learned.size();
         unsigned new_sz = sz/2;
         unsigned j      = new_sz;
@@ -1145,6 +1149,7 @@ namespace sat {
        \brief Use gc based on dynamic psm. Clauses are initially frozen.
     */
     void solver::gc_dyn_psm() {
+        TRACE("sat", tout << "gc\n";);
         // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
         // that I may miss some propagations for reactivated clauses.
         SASSERT(scope_lvl() == 0);
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 2a64c9cd5..72f1d5770 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -89,7 +89,7 @@ namespace sat {
         clause_vector           m_learned;
         unsigned                m_num_frozen;
         vector<watch_list>      m_watches;
-        svector<lbool>          m_assignment;
+        char_vector             m_assignment;
         svector<justification>  m_justification; 
         svector<char>           m_decision;
         svector<char>           m_mark;
@@ -200,8 +200,8 @@ namespace sat {
         bool is_external(bool_var v) const { return m_external[v] != 0; }
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         unsigned scope_lvl() const { return m_scope_lvl; }
-        lbool value(literal l) const { return m_assignment[l.index()]; }
-        lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
+        lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
+        lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
         unsigned lvl(bool_var v) const { return m_level[v]; }
         unsigned lvl(literal l) const { return m_level[l.var()]; }
         void assign(literal l, justification j) {
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 1acfcdf57..faf5ce0ef 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() {
     proof_ref_vector new_prs1(m_manager);
     expr_ref_vector  new_exprs2(m_manager);
     proof_ref_vector new_prs2(m_manager);
-    unsigned i  = m_asserted_qhead;
+    unsigned i  = 0;
     unsigned sz = m_asserted_formulas.size();
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
diff --git a/src/smt/database.h b/src/smt/database.h
index 1975fe3c3..69843f434 100644
--- a/src/smt/database.h
+++ b/src/smt/database.h
@@ -1,4 +1,4 @@
-static char const * g_pattern_database =
+static char const g_pattern_database[] =
 "(benchmark patterns \n"
 " :status unknown \n"
 " :logic ALL \n"
diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp
index 2e94c376d..c559e2b9b 100644
--- a/src/smt/params/dyn_ack_params.cpp
+++ b/src/smt/params/dyn_ack_params.cpp
@@ -17,16 +17,14 @@ Revision History:
 
 --*/
 #include"dyn_ack_params.h"
+#include"smt_params_helper.hpp"
 
-#if 0
-void dyn_ack_params::register_params(ini_params & p) {
-    p.register_int_param("dack", 0, 2, reinterpret_cast<int&>(m_dack), 
-                         "0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution.");
-    p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities");
-    p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded");
-    p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict");
-    p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict).");
-    p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay);
-}
-#endif
-
+void dyn_ack_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_dack = static_cast<dyn_ack_strategy>(p.dack());
+    m_dack_eq = p.dack_eq();
+    m_dack_factor = p.dack_factor();
+    m_dack_threshold = p.dack_threshold();
+    m_dack_gc = p.dack_gc();
+    m_dack_gc_inv_decay = p.dack_gc_inv_decay();
+}
\ No newline at end of file
diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h
index 9f7ce578c..95b5aff8a 100644
--- a/src/smt/params/dyn_ack_params.h
+++ b/src/smt/params/dyn_ack_params.h
@@ -19,6 +19,8 @@ Revision History:
 #ifndef _DYN_ACK_PARAMS_H_
 #define _DYN_ACK_PARAMS_H_
 
+#include"params.h"
+
 enum dyn_ack_strategy {
     DACK_DISABLED,
     DACK_ROOT, // congruence is the root of the conflict
@@ -34,15 +36,17 @@ struct dyn_ack_params {
     double           m_dack_gc_inv_decay;
 
 public:
-    dyn_ack_params():
+    dyn_ack_params(params_ref const & p = params_ref()) :
         m_dack(DACK_ROOT),
         m_dack_eq(false),
         m_dack_factor(0.1),
         m_dack_threshold(10),
         m_dack_gc(2000), 
         m_dack_gc_inv_decay(0.8) {
+        updt_params(p);
     }
 
+    void updt_params(params_ref const & _p);
 };
 
 
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 18619c8ec..2f8d9c1ee 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
 
 void smt_params::updt_params(params_ref const & p) {
     preprocessor_params::updt_params(p);
+    dyn_ack_params::updt_params(p);
     qi_params::updt_params(p);
     theory_arith_params::updt_params(p);
     theory_bv_params::updt_params(p);
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 869b8cdc4..39818e621 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -45,5 +45,11 @@ def_module_params(module_name='smt',
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
                           ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
                           ('array.weak', BOOL, False, 'weak array theory'),
-                          ('array.extensional', BOOL, True, 'extensional array theory')
+                          ('array.extensional', BOOL, True, 'extensional array theory'),
+						  ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
+						  ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
+						  ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
+						  ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
+						  ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
+						  ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
                           ))
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index d78b82cc6..a4e97380b 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -236,8 +236,8 @@ namespace smt {
         params_ref ps          = m_imp->params();
         #pragma omp critical (smt_kernel)
         {
-            dealloc(m_imp);
-            m_imp = alloc(imp, _m, fps, ps);
+            m_imp->~imp();
+            m_imp = new (m_imp) imp(_m, fps, ps);
         }
     }
 
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index b76fb6c74..f824cb3f1 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -361,8 +361,8 @@ namespace smt {
             context & ctx        = m_imp->m_context;
             smt_params & p = m_imp->m_params;
             quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
-            dealloc(m_imp);
-            m_imp = alloc(imp, *this, ctx, p, plugin);
+            m_imp->~imp();
+            m_imp = new (m_imp) imp(*this, ctx, p, plugin);
             plugin->set_manager(*this);
         }
     }
diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index 98f659fe0..fc7358f3d 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -555,8 +555,12 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
         mc = 0;
 }
 
-lbool sls_engine::operator()() {
+lbool sls_engine::operator()() {    
     m_tracker.initialize(m_assertions);
+    m_tracker.reset(m_assertions);
+    if (m_restart_init)
+        m_tracker.randomize(m_assertions);
+
     lbool res = l_undef;
 
     do {
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index 1490b9628..cf96cb295 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -25,13 +25,12 @@ Revision History:
 #define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
 
 void bit_vector::expand_to(unsigned new_capacity) {
-    unsigned * new_data     = alloc_svect(unsigned, new_capacity);
-    memset(new_data, 0, new_capacity * sizeof(unsigned));
-    if (m_capacity > 0) {
-        memcpy(new_data, m_data, m_capacity * sizeof(unsigned));
-        dealloc_svect(m_data);
+    if (m_data) {
+        m_data = (unsigned*)memory::reallocate(m_data, new_capacity * sizeof(unsigned));
+    } else {
+        m_data = alloc_svect(unsigned, new_capacity);
     }
-    m_data     = new_data;
+    memset(m_data + m_capacity, 0, (new_capacity - m_capacity) * sizeof(unsigned));
     m_capacity = new_capacity;
 }
 
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 0ccdeae9e..6738ba0aa 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -87,9 +87,7 @@ public:
     }
 
     ~bit_vector() {
-        if (m_data) {
-            dealloc_svect(m_data);
-        }
+        dealloc_svect(m_data);
     }
     
     void reset() {
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 45088d5d4..e911ff505 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -60,7 +60,7 @@ static void throw_out_of_memory() {
 }
 
 #ifdef PROFILE_MEMORY
-unsigned g_synch_counter = 0;
+static unsigned g_synch_counter = 0;
 class mem_usage_report {
 public:
     ~mem_usage_report() { 
@@ -173,6 +173,7 @@ void memory::display_i_max_usage(std::ostream & os) {
               << "\n";
 }
 
+#if _DEBUG
 void memory::deallocate(char const * file, int line, void * p) {
     deallocate(p);
     TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";););
@@ -183,6 +184,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
     TRACE("memory", tout << "alloc " << std::hex << r << std::dec << " " << file << ":" << line << " " << obj << " " << s << "\n";);
     return r;
 }
+#endif
 
 #if defined(_WINDOWS) || defined(_USE_THREAD_LOCAL)
 // ==================================
@@ -250,6 +252,24 @@ void * memory::allocate(size_t s) {
     return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
 }
 
+void* memory::reallocate(void *p, size_t s) {
+    size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
+    size_t sz = *sz_p;
+    void *real_p = reinterpret_cast<void*>(sz_p);
+    s = s + sizeof(size_t); // we allocate an extra field!
+
+    g_memory_thread_alloc_size += s - sz;
+    if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
+        synchronize_counters(true);
+    }
+
+    void *r = realloc(real_p, s);
+    if (r == 0)
+        throw_out_of_memory();
+    *(static_cast<size_t*>(r)) = s;
+    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+}
+
 #else
 // ==================================
 // ==================================
@@ -290,5 +310,29 @@ void * memory::allocate(size_t s) {
     *(static_cast<size_t*>(r)) = s;
     return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
 }
+
+void* memory::reallocate(void *p, size_t s) {
+    size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
+    size_t sz      = *sz_p;
+    void * real_p  = reinterpret_cast<void*>(sz_p);
+    s = s + sizeof(size_t); // we allocate an extra field!
+    bool out_of_mem = false;
+    #pragma omp critical (z3_memory_manager)
+    {
+        g_memory_alloc_size += s - sz;
+        if (g_memory_alloc_size > g_memory_max_used_size)
+            g_memory_max_used_size = g_memory_alloc_size;
+        if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
+            out_of_mem = true;
+    }
+    if (out_of_mem)
+        throw_out_of_memory();
+
+    void *r = realloc(real_p, s);
+    if (r == 0)
+        throw_out_of_memory();
+    *(static_cast<size_t*>(r)) = s;
+    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+}
  
 #endif
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 2cabc70b7..bd912828e 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -23,6 +23,24 @@ Revision History:
 #include<ostream>
 #include"z3_exception.h"
 
+#ifndef __has_builtin
+# define __has_builtin(x) 0
+#endif
+
+#ifdef __GNUC__
+# if (__GNUC__ * 100 + __GNUC_MINOR__) >= 409 || __has_builtin(returns_nonnull)
+#  define GCC_RET_NON_NULL __attribute__((returns_nonnull))
+# else
+#  define GCC_RET_NON_NULL
+# endif
+# define ALLOC_ATTR __attribute__((malloc)) GCC_RET_NON_NULL
+#elif defined(_WINDOWS)
+# define ALLOC_ATTR __declspec(restrict)
+#else
+# define ALLOC_ATTR
+#endif
+
+
 class out_of_memory_error : public z3_error {
 public:
     out_of_memory_error();
@@ -39,9 +57,12 @@ public:
     static void display_max_usage(std::ostream& os);
     static void display_i_max_usage(std::ostream& os);
     static void deallocate(void* p);
-    static void* allocate(size_t s);
+    static ALLOC_ATTR void* allocate(size_t s);
+    static ALLOC_ATTR void* reallocate(void *p, size_t s);
+#if _DEBUG
     static void deallocate(char const* file, int line, void* p);
-    static void* allocate(char const* file, int line, char const* obj, size_t s);
+    static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
+#endif
     static unsigned long long get_allocation_size();
     static unsigned long long get_max_used_memory();
     // temporary hack to avoid out-of-memory crash in z3.exe
@@ -74,6 +95,9 @@ void dealloc(T * ptr) {
 
 #endif
 
+template<typename T>
+ALLOC_ATTR T * alloc_vect(unsigned sz);
+
 template<typename T>
 T * alloc_vect(unsigned sz) {
     T * r = static_cast<T*>(memory::allocate(sizeof(T) * sz));
diff --git a/src/util/util.cpp b/src/util/util.cpp
index eb9acb385..c4b729adb 100644
--- a/src/util/util.cpp
+++ b/src/util/util.cpp
@@ -19,7 +19,7 @@ Revision History:
 
 #include"util.h"
 
-unsigned g_verbosity_level = 0;
+static unsigned g_verbosity_level = 0;
 
 void set_verbosity_level(unsigned lvl) {
     g_verbosity_level = lvl;
@@ -40,7 +40,7 @@ std::ostream& verbose_stream() {
 }
 
 
-void (*g_fatal_error_handler)(int) = 0;
+static void (*g_fatal_error_handler)(int) = 0;
 
 void fatal_error(int error_code) {
     if (g_fatal_error_handler) {
diff --git a/src/util/vector.h b/src/util/vector.h
index 9370a4eed..dc08a63b3 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -71,18 +71,12 @@ class vector {
             SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
             SZ new_capacity = (3 * old_capacity + 1) >> 1;
             SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
-            SZ size         = reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
             if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
                 throw default_exception("Overflow encountered when expanding vector");
             }
-            SZ * mem        = reinterpret_cast<SZ*>(memory::allocate(new_capacity_T));
-            *mem                  = new_capacity; 
-            mem ++;
-            *mem                  = size;         
-            mem++;
-            memcpy(mem, m_data, size * sizeof(T));
-            free_memory();
-            m_data                = reinterpret_cast<T *>(mem);
+            SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
+            *mem    = new_capacity;
+            m_data  = reinterpret_cast<T *>(mem + 2);
         }
     }