diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 2b4dc05dd..a97e2b125 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3014,7 +3014,7 @@ namespace smt {
         bool was_consistent = !inconsistent();
         try {
             internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
-        } catch (cancel_exception&) {
+        } catch (oom_exception&) {
             throw default_exception("Resource limits hit in push");
         }
         if (!m.inc())
@@ -3629,7 +3629,7 @@ namespace smt {
 
         try {
             internalize_assertions();
-        } catch (cancel_exception&) {
+        } catch (oom_exception&) {
             return l_undef;
         }
         expr_ref_vector theory_assumptions(m);
@@ -3702,7 +3702,7 @@ namespace smt {
                 add_theory_assumptions(asms);
                 TRACE("unsat_core_bug", tout << asms << '\n';);
                 init_assumptions(asms);
-            } catch (cancel_exception&) {
+            } catch (oom_exception&) {
                 return l_undef;
             }
             TRACE("before_search", display(tout););
@@ -3729,7 +3729,7 @@ namespace smt {
                 // introducing proxies: if (!validate_assumptions(asms)) return l_undef;
                 for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
                 init_assumptions(asms);
-            } catch (cancel_exception&) {
+            } catch (oom_exception&) {
                 return l_undef;
             }
             for (auto const& clause : clauses) init_clause(clause);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index d44da1e87..865d140e5 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -63,8 +63,8 @@ namespace smt {
     class model_generator;
     class context;
 
-    struct cancel_exception : public std::exception {
-        char const * what() const noexcept override { return "smt-canceled"; }
+    struct oom_exception : public z3_error {
+        oom_exception() : z3_error(ERR_MEMOUT) {}
     };
 
     struct enode_pp {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 5cfb4a8a8..ccdfc5ccb 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -354,7 +354,7 @@ namespace smt {
     */
     void context::internalize(expr * n, bool gate_ctx) {
         if (memory::above_high_watermark())
-            throw cancel_exception();
+            throw oom_exception();
         internalize_deep(n);
         internalize_rec(n, gate_ctx);
     }