diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 2d39e3287a..be1b701223 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include "util/file_path.h"
 #include "util/scoped_timer.h"
 #include "util/file_path.h"
+#include "util/memory_manager.h"
 #include "ast/ast_pp.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
@@ -514,6 +515,15 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_solver_reset(c, s);
         RESET_ERROR_CODE();
+        struct scoped_memory_limit_reset {
+            size_t m_prev_max;
+            scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) {
+                memory::set_max_size(0);
+            }
+            ~scoped_memory_limit_reset() {
+                memory::set_max_size(m_prev_max);
+            }
+        } scoped_max_memory;
         to_solver(s)->m_solver = nullptr;
         to_solver(s)->m_cmd_context = nullptr;
         if (to_solver(s)->m_pp) to_solver(s)->m_pp->reset();
diff --git a/src/test/memory.cpp b/src/test/memory.cpp
index 58e8855b64..e751f29553 100644
--- a/src/test/memory.cpp
+++ b/src/test/memory.cpp
@@ -11,6 +11,8 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/trace.h"
 
 static bool oom = false;
+static unsigned oom_handler_calls = 0;
+static Z3_error_code oom_handler_last_code = Z3_OK;
 
 
 static void err_handler(Z3_context c, Z3_error_code e) {
@@ -18,6 +20,11 @@ static void err_handler(Z3_context c, Z3_error_code e) {
     throw std::bad_alloc();
 }
 
+static void err_handler_noexcept(Z3_context, Z3_error_code e) {
+    ++oom_handler_calls;
+    oom_handler_last_code = e;
+}
+
 static void hit_me(char const* wm) {
     Z3_config cfg;
     Z3_context ctx;
@@ -49,6 +56,37 @@ static void hit_me(char const* wm) {
     Z3_del_config(cfg);
 }
 
+static void solver_reset_after_oom(char const* wm) {
+    Z3_config cfg;
+    Z3_context ctx;
+
+    oom_handler_calls = 0;
+    oom_handler_last_code = Z3_OK;
+
+    cfg = Z3_mk_config();
+    if (!cfg) {
+        return;
+    }
+    Z3_global_param_set("MEMORY_MAX_SIZE", wm);
+    ctx = Z3_mk_context(cfg);
+    if (ctx) {
+        Z3_set_error_handler(ctx, &err_handler_noexcept);
+        Z3_solver s = Z3_mk_solver(ctx);
+        Z3_symbol p = Z3_mk_string_symbol(ctx, "p");
+        Z3_ast b = Z3_mk_const(ctx, p, Z3_mk_bool_sort(ctx));
+        Z3_solver_assert(ctx, s, b);
+        Z3_solver_check(ctx, s);
+        for (unsigned i = 1; oom_handler_last_code != Z3_MEMOUT_FAIL; ++i) {
+            Z3_mk_bv_sort(ctx, i);
+        }
+        VERIFY(oom_handler_last_code == Z3_MEMOUT_FAIL);
+        VERIFY(oom_handler_calls > 0);
+        Z3_solver_reset(ctx, s);
+        Z3_del_context(ctx);
+    }
+    Z3_del_config(cfg);
+}
+
 void tst_memory() {    
     hit_me("10");
     Z3_reset_memory();
@@ -56,5 +94,8 @@ void tst_memory() {
     Z3_reset_memory();
     hit_me("30");
     Z3_reset_memory();
+    solver_reset_after_oom("30");
+    Z3_reset_memory();
+    Z3_global_param_set("MEMORY_MAX_SIZE", "0");
 
 }
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index eddadb989c..6fbf175e0e 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -143,6 +143,11 @@ void memory::set_max_size(size_t max_size) {
     g_memory_max_size = max_size;
 }
 
+size_t memory::get_max_size() {
+    lock_guard lock(*g_memory_mux);
+    return g_memory_max_size <= 0 ? 0 : static_cast<size_t>(g_memory_max_size);
+}
+
 void memory::set_max_alloc_count(size_t max_count) {
     g_memory_max_alloc_count = max_count;
 }
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 1d9a604afb..c90198b398 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -55,6 +55,7 @@ public:
     static void set_high_watermark(size_t watermak);
     static bool above_high_watermark();
     static void set_max_size(size_t max_size);
+    static size_t get_max_size();
     static void set_max_alloc_count(size_t max_count);
     static void finalize(bool shutdown = true);
     static void display_max_usage(std::ostream& os);
@@ -157,4 +158,3 @@ inline std::ostream & operator<<(std::ostream & out, mem_stat const & m) {
 }
 
 
-