diff --git a/include/klee/Solver/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h
index 3bf6a2e192..3440764589 100644
--- a/include/klee/Solver/IncompleteSolver.h
+++ b/include/klee/Solver/IncompleteSolver.h
@@ -79,7 +79,7 @@ class StagedSolverImpl : public SolverImpl {
                            bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index addb9f55c6..a19f4f26e6 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -191,7 +191,7 @@ class Solver {
   getRange(const Query &, time::Span timeout = time::Span());
 
   virtual std::string getConstraintLog(const Query &query);
-  virtual void setCoreSolverTimeout(time::Span timeout);
+  virtual void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
 
   /// @brief Notify the solver that the state with specified id has been
   /// terminated
diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h
index ba389a34dc..69b7a64bef 100644
--- a/include/klee/Solver/SolverCmdLine.h
+++ b/include/klee/Solver/SolverCmdLine.h
@@ -41,6 +41,8 @@ extern llvm::cl::opt<bool> LogTimedOutQueries;
 
 extern llvm::cl::opt<std::string> MaxCoreSolverTime;
 
+extern llvm::cl::opt<unsigned> MaxCoreSolverMemory;
+
 extern llvm::cl::opt<bool> UseForkedCoreSolver;
 
 extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h
index 016711ba4d..24a6fdd627 100644
--- a/include/klee/Solver/SolverImpl.h
+++ b/include/klee/Solver/SolverImpl.h
@@ -120,7 +120,7 @@ class SolverImpl {
     return {};
   }
 
-  virtual void setCoreSolverTimeout(time::Span) {}
+  virtual void setCoreSolverLimits(time::Span, unsigned) {}
 
   virtual void notifyStateTermination(std::uint32_t id) = 0;
 };
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 6014b1b33a..b06d2fee5b 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -543,8 +543,10 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
   }
 
   coreSolverTimeout = time::Span{MaxCoreSolverTime};
-  if (coreSolverTimeout)
+  if (coreSolverTimeout) {
     UseForkedCoreSolver = true;
+  }
+  coreSolverMemoryLimit = MaxCoreSolverMemory;
   std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse);
   if (!coreSolver) {
     klee_error("Failed to create core solver\n");
@@ -1358,9 +1360,10 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     condition = maxStaticPctChecks(current, condition);
 
   time::Span timeout = coreSolverTimeout;
+  unsigned memoryLimit = coreSolverMemoryLimit;
   if (isSeeding)
     timeout *= static_cast<unsigned>(it->second.size());
-  solver->setTimeout(timeout);
+  solver->setLimits(timeout, memoryLimit);
 
   bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true;
   if (!isInternal) {
@@ -1368,6 +1371,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     shouldCheckFalseBlock = canReachSomeTargetFromBlock(current, ifFalseBlock);
   }
   PartialValidity res = PartialValidity::None;
+
   bool terminateEverything = false, success = true;
   if (!shouldCheckTrueBlock) {
     bool mayBeFalse = false;
@@ -1402,7 +1406,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     success = solver->evaluate(current.constraints.cs(), condition, res,
                                current.queryMetaData);
   }
-  solver->setTimeout(time::Span());
+  solver->setLimits(time::Span(), 0);
   if (!success) {
     current.pc = current.prevPC;
     terminateStateOnSolverError(current, "Query timed out (fork).");
@@ -1614,11 +1618,11 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
                                          siie = it->second.end();
          siit != siie; ++siit) {
       bool res;
-      solver->setTimeout(coreSolverTimeout);
+      solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
       bool success = solver->mustBeFalse(state.constraints.cs(),
                                          siit->assignment.evaluate(condition),
                                          res, state.queryMetaData);
-      solver->setTimeout(time::Span());
+      solver->setLimits(time::Span(), 0);
       assert(success && "FIXME: Unhandled solver failure");
       (void)success;
       if (res) {
@@ -1687,9 +1691,9 @@ void Executor::bindArgument(KFunction *kf, unsigned index,
 
 ref<Expr> Executor::toUnique(const ExecutionState &state, ref<Expr> e) {
   ref<Expr> result = e;
-  solver->setTimeout(coreSolverTimeout);
+  solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
   solver->tryGetUnique(state.constraints.cs(), e, result, state.queryMetaData);
-  solver->setTimeout(time::Span());
+  solver->setLimits(time::Span(), 0);
   return result;
 }
 
@@ -5493,11 +5497,11 @@ void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal,
   /* If size greater then upper bound for size, then we will follow
   the malloc semantic and return NULL. Otherwise continue execution. */
   PartialValidity inBounds;
-  solver->setTimeout(coreSolverTimeout);
+  solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
   bool success =
       solver->evaluate(state.constraints.cs(), upperBoundSizeConstraint,
                        inBounds, state.queryMetaData);
-  solver->setTimeout(time::Span());
+  solver->setLimits(time::Span(), 0);
   if (!success) {
     terminateStateOnSolverError(state, "Query timed out (resolve)");
     return;
@@ -5798,21 +5802,21 @@ bool Executor::computeSizes(
   objects = constraints.gatherSymcretizedArrays();
   findObjects(symbolicSizesSum, objects);
 
-  solver->setTimeout(coreSolverTimeout);
+  solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
   bool success = solver->getResponse(
       constraints,
       UgtExpr::create(symbolicSizesSum,
                       ConstantExpr::create(SymbolicAllocationThreshold,
                                            symbolicSizesSum->getWidth())),
       response, metaData);
-  solver->setTimeout(time::Span());
+  solver->setLimits(time::Span(), 0);
 
   if (!response->tryGetInitialValuesFor(objects, values)) {
     /* Receive model with a smallest sum as possible. */
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     success = solver->getMinimalUnsignedValue(constraints, symbolicSizesSum,
                                               minimalSumValue, metaData);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
     assert(success);
 
     /* We can simply query the solver to get value of size, but
@@ -5822,9 +5826,9 @@ bool Executor::computeSizes(
     ConstraintSet minimized = constraints;
     minimized.addConstraint(EqExpr::create(symbolicSizesSum, minimalSumValue));
 
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     success = solver->getInitialValues(minimized, objects, values, metaData);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
   }
   return success;
 }
@@ -6005,10 +6009,10 @@ bool Executor::resolveMemoryObjects(
     if (!onlyLazyInitialize || !mayLazyInitialize) {
       ResolutionList rl;
 
-      solver->setTimeout(coreSolverTimeout);
+      solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
       incomplete = state.addressSpace.resolve(state, solver.get(), basePointer,
                                               rl, 0, coreSolverTimeout);
-      solver->setTimeout(time::Span());
+      solver->setLimits(time::Span(), 0);
 
       for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie;
            ++i) {
@@ -6023,10 +6027,10 @@ bool Executor::resolveMemoryObjects(
     }
 
     if (mayLazyInitialize) {
-      solver->setTimeout(coreSolverTimeout);
+      solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
       bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds,
                                        mayLazyInitialize, state.queryMetaData);
-      solver->setTimeout(time::Span());
+      solver->setLimits(time::Span(), 0);
       if (!success) {
         return false;
       } else if (mayLazyInitialize) {
@@ -6091,10 +6095,10 @@ bool Executor::checkResolvedMemoryObjects(
             .simplified;
 
     PartialValidity result;
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     bool success = solver->evaluate(state.constraints.cs(), inBounds, result,
                                     state.queryMetaData);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
     if (!success) {
       return false;
     }
@@ -6155,10 +6159,10 @@ bool Executor::checkResolvedMemoryObjects(
                                .simplified;
 
       bool mayBeInBounds;
-      solver->setTimeout(coreSolverTimeout);
+      solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
       bool success = solver->mayBeTrue(state.constraints.cs(), inBounds,
                                        mayBeInBounds, state.queryMetaData);
-      solver->setTimeout(time::Span());
+      solver->setLimits(time::Span(), 0);
       if (!success) {
         return false;
       }
@@ -6180,10 +6184,10 @@ bool Executor::checkResolvedMemoryObjects(
   }
 
   if (mayBeOutOfBound) {
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds,
                                      mayBeOutOfBound, state.queryMetaData);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
     if (!success) {
       return false;
     }
@@ -6210,10 +6214,10 @@ bool Executor::makeGuard(ExecutionState &state,
     }
   }
 
-  solver->setTimeout(coreSolverTimeout);
+  solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
   bool success = solver->mayBeTrue(state.constraints.cs(), guard, mayBeInBounds,
                                    state.queryMetaData);
-  solver->setTimeout(time::Span());
+  solver->setLimits(time::Span(), 0);
   if (!success) {
     return false;
   }
@@ -6318,7 +6322,7 @@ void Executor::executeMemoryOperation(
     idFastResult = *state->resolvedPointers[base].begin();
   } else {
     ObjectPair idFastOp;
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
 
     if (!state->addressSpace.resolveOne(*state, solver.get(), address, idFastOp,
                                         success, haltExecution)) {
@@ -6327,7 +6331,7 @@ void Executor::executeMemoryOperation(
           cast<ConstantPointerExpr>(address), idFastOp);
     }
 
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
 
     if (success) {
       idFastResult = idFastOp.first;
@@ -6352,16 +6356,16 @@ void Executor::executeMemoryOperation(
                    .simplified;
 
     ref<SolverResponse> response;
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     bool success = solver->getResponse(state->constraints.cs(), inBounds,
                                        response, state->queryMetaData);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
     if (!success) {
       state->pc = state->prevPC;
       terminateStateOnSolverError(*state, "Query timed out (bounds check).");
       return;
     }
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
 
     bool mustBeInBounds = !isa<InvalidResponse>(response);
     if (mustBeInBounds) {
@@ -6414,10 +6418,10 @@ void Executor::executeMemoryOperation(
              allLeafsAreConstant(address)) {
     ObjectPair idFastOp;
 
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     state->addressSpace.resolveOne(*state, solver.get(), basePointer, idFastOp,
                                    success, haltExecution);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
 
     if (!success) {
       terminateStateOnTargetError(*state, ReachWithError::UseAfterFree);
@@ -6684,11 +6688,11 @@ ref<const MemoryObject> Executor::lazyInitializeObject(
           sizeExpr, Expr::createPointer(MaxSymbolicAllocationSize));
     }
     bool mayBeInBounds;
-    solver->setTimeout(coreSolverTimeout);
+    solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
     bool success = solver->mayBeTrue(state.constraints.cs(),
                                      AndExpr::create(lowerBound, upperBound),
                                      mayBeInBounds, state.queryMetaData);
-    solver->setTimeout(time::Span());
+    solver->setLimits(time::Span(), 0);
     if (!success) {
       return nullptr;
     }
@@ -7430,7 +7434,7 @@ bool isMakeSymbolicSymbol(const klee::Symbolic &symb) {
 }
 
 bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
-  solver->setTimeout(coreSolverTimeout);
+  solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
 
   PathConstraints extendedConstraints(state.constraints);
 
@@ -7504,11 +7508,11 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
   std::vector<const Array *> objects(objectSet.begin(), objectSet.end());
 
   ref<SolverResponse> response;
-  solver->setTimeout(coreSolverTimeout);
+  solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
   bool success =
       solver->getResponse(extendedConstraints.cs(), Expr::createFalse(),
                           response, state.queryMetaData);
-  solver->setTimeout(time::Span());
+  solver->setLimits(time::Span(), 0);
   if (!success || !isa<InvalidResponse>(response)) {
     klee_warning("unable to compute initial values (invalid constraints?)!");
     ExprPPrinter::printQuery(llvm::errs(), state.constraints.cs(),
@@ -7588,14 +7592,14 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
 
     ref<Expr> concretizationCondition = Expr::createFalse();
     for (const auto &concretization : concretizations) {
-      solver->setTimeout(coreSolverTimeout);
+      solver->setLimits(coreSolverTimeout, coreSolverMemoryLimit);
       success = solver->getResponse(
           extendedConstraints.cs(),
           OrExpr::create(Expr::createIsZero(EqExpr::create(
                              concretization.first, concretization.second)),
                          concretizationCondition),
           response, state.queryMetaData);
-      solver->setTimeout(time::Span());
+      solver->setLimits(time::Span(), 0);
 
       if (auto invalidResponse = dyn_cast<InvalidResponse>(response)) {
         concretizationCondition =
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index d0d4adc20b..0dacaef9a7 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -224,6 +224,10 @@ class Executor : public Interpreter {
   /// (e.g. for a single STP query)
   time::Span coreSolverTimeout;
 
+  /// The soft maximum memory to allow for a core SMT-sovler to use.
+  /// (e.g. for a single STP query)
+  unsigned coreSolverMemoryLimit;
+
   /// Maximum time to allow for a single instruction.
   time::Span maxInstructionTime;
 
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 6cff49d410..b3c122da0b 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -44,7 +44,9 @@ class TimingSolver {
       : solver(std::move(solver)), optimizer(optimizer),
         simplifyExprs(_simplifyExprs) {}
 
-  void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); }
+  void setLimits(time::Span t, unsigned m) {
+    solver->setCoreSolverLimits(t, m);
+  }
 
   std::string getConstraintLog(const Query &query) {
     return solver->getConstraintLog(query);
diff --git a/lib/Solver/AlphaEquivalenceSolver.cpp b/lib/Solver/AlphaEquivalenceSolver.cpp
index 8e3df97617..8da1e345c1 100644
--- a/lib/Solver/AlphaEquivalenceSolver.cpp
+++ b/lib/Solver/AlphaEquivalenceSolver.cpp
@@ -41,7 +41,7 @@ class AlphaEquivalenceSolver : public SolverImpl {
                            bool &isValid);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &);
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
   ValidityCore changeVersion(const ValidityCore &validityCore,
                              AlphaBuilder &builder);
@@ -213,8 +213,9 @@ std::string AlphaEquivalenceSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void AlphaEquivalenceSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
+void AlphaEquivalenceSolver::setCoreSolverLimits(time::Span timeout,
+                                                 unsigned memoryLimit) {
+  solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void AlphaEquivalenceSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index 6363096fed..1290e071b6 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -44,7 +44,7 @@ class AssignmentValidatingSolver : public SolverImpl {
                      std::vector<SparseStorageImpl<unsigned char>> &values);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
@@ -187,8 +187,9 @@ std::string AssignmentValidatingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void AssignmentValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
-  return solver->impl->setCoreSolverTimeout(timeout);
+void AssignmentValidatingSolver::setCoreSolverLimits(time::Span timeout,
+                                                     unsigned memoryLimit) {
+  return solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void AssignmentValidatingSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/BitwuzlaSolver.cpp b/lib/Solver/BitwuzlaSolver.cpp
index bcb544b7d0..fabde85809 100644
--- a/lib/Solver/BitwuzlaSolver.cpp
+++ b/lib/Solver/BitwuzlaSolver.cpp
@@ -237,6 +237,7 @@ class BitwuzlaSolverImpl : public SolverImpl {
 
 private:
   time::Span timeout;
+  unsigned memoryLimit;
   SolverImpl::SolverRunStatus runStatusCode;
 
   bool internalRunSolver(const ConstraintQuery &query, BitwuzlaSolverEnv &env,
@@ -272,7 +273,13 @@ class BitwuzlaSolverImpl : public SolverImpl {
 public:
   std::string getConstraintLog(const Query &) final;
   SolverImpl::SolverRunStatus getOperationStatusCode() final;
-  void setCoreSolverTimeout(time::Span _timeout) final { timeout = _timeout; }
+  void setCoreSolverLimits(time::Span _timeout, unsigned _memoryLimit) final {
+    timeout = _timeout;
+    memoryLimit = _memoryLimit;
+    if (memoryLimit) {
+      solverParameters.set(Option::MEMORY_LIMIT, memoryLimit);
+    }
+  }
   void enableUnsatCore() {
     solverParameters.set(Option::PRODUCE_UNSAT_CORES, true);
   }
@@ -296,8 +303,6 @@ BitwuzlaSolverImpl::BitwuzlaSolverImpl()
     : runStatusCode(SolverImpl::SOLVER_RUN_STATUS_FAILURE) {
   solverParameters.set(Option::PRODUCE_MODELS, true);
 
-  setCoreSolverTimeout(timeout);
-
   if (ProduceUnsatCore) {
     enableUnsatCore();
   } else {
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index f14d7bdc7b..bb4f472aef 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -87,7 +87,7 @@ class CachingSolver : public SolverImpl {
                            bool &isValid);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
@@ -297,8 +297,9 @@ std::string CachingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void CachingSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
+void CachingSolver::setCoreSolverLimits(time::Span timeout,
+                                        unsigned memoryLimit) {
+  solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void CachingSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index de6809d6ef..e3e86a3c39 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -102,7 +102,7 @@ class CexCachingSolver : public SolverImpl {
                            bool &isValid);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &query) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
@@ -429,8 +429,9 @@ std::string CexCachingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void CexCachingSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
+void CexCachingSolver::setCoreSolverLimits(time::Span timeout,
+                                           unsigned memoryLimit) {
+  solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void CexCachingSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp
index 9d918d32fe..1f471d2388 100644
--- a/lib/Solver/ConcretizingSolver.cpp
+++ b/lib/Solver/ConcretizingSolver.cpp
@@ -57,7 +57,7 @@ class ConcretizingSolver : public SolverImpl {
       std::vector<SparseStorageImpl<unsigned char>> &values, bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &);
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 
 private:
@@ -575,8 +575,9 @@ SolverImpl::SolverRunStatus ConcretizingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
-void ConcretizingSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->setCoreSolverTimeout(timeout);
+void ConcretizingSolver::setCoreSolverLimits(time::Span timeout,
+                                             unsigned memoryLimit) {
+  solver->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void ConcretizingSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 7027ee010e..b04f592663 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -149,8 +149,9 @@ std::string StagedSolverImpl::getConstraintLog(const Query &query) {
   return secondary->impl->getConstraintLog(query);
 }
 
-void StagedSolverImpl::setCoreSolverTimeout(time::Span timeout) {
-  secondary->impl->setCoreSolverTimeout(timeout);
+void StagedSolverImpl::setCoreSolverLimits(time::Span timeout,
+                                           unsigned memoryLimit) {
+  secondary->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void StagedSolverImpl::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index b5c1d69718..eb60222251 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -47,7 +47,7 @@ class IndependentSolver : public SolverImpl {
                            bool &isValid);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
@@ -344,8 +344,9 @@ std::string IndependentSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void IndependentSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
+void IndependentSolver::setCoreSolverLimits(time::Span timeout,
+                                            unsigned memoryLimit) {
+  solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void IndependentSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index cff8fc2f3b..d3d1c7a093 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -92,7 +92,9 @@ template <typename SolverContext> class MetaSMTSolverImpl : public SolverImpl {
                     bool optimizeDivides);
 
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; }
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit) {
+    _timeout = timeout;
+  }
   void notifyStateTermination(std::uint32_t) {}
 
   bool computeTruth(const Query &, bool &isValid);
@@ -438,8 +440,9 @@ std::string MetaSMTSolver<SolverContext>::getConstraintLog(const Query &query) {
 }
 
 template <typename SolverContext>
-void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(time::Span timeout) {
-  impl->setCoreSolverTimeout(timeout);
+void MetaSMTSolver<SolverContext>::setCoreSolverLimits(time::Span timeout,
+                                                       unsigned memoryLimit) {
+  impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 std::unique_ptr<Solver> createMetaSMTSolver() {
diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h
index d9e5554ff4..a9d078acb1 100644
--- a/lib/Solver/MetaSMTSolver.h
+++ b/lib/Solver/MetaSMTSolver.h
@@ -23,7 +23,7 @@ template <typename SolverContext> class MetaSMTSolver : public Solver {
   virtual ~MetaSMTSolver();
 
   std::string getConstraintLog(const Query &) final;
-  virtual void setCoreSolverTimeout(time::Span timeout);
+  virtual void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
 };
 
 /// createMetaSMTSolver - Create a solver using the metaSMT backend set by
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 71cf6aa216..06184ac399 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -316,8 +316,9 @@ std::string QueryLoggingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void QueryLoggingSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
+void QueryLoggingSolver::setCoreSolverLimits(time::Span timeout,
+                                             unsigned memoryLimit) {
+  solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void QueryLoggingSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index b5b3d11439..99babc55a4 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -75,7 +75,7 @@ class QueryLoggingSolver : public SolverImpl {
                            bool &isValid);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index 98b80ac20d..f3c6bc2972 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -99,7 +99,7 @@ class STPSolverImpl : public SolverImpl {
   ~STPSolverImpl() override;
 
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout) override {
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit) override {
     this->timeout = timeout;
   }
   void notifyStateTermination(std::uint32_t) override {}
@@ -483,8 +483,8 @@ std::string STPSolver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
 }
 
-void STPSolver::setCoreSolverTimeout(time::Span timeout) {
-  impl->setCoreSolverTimeout(timeout);
+void STPSolver::setCoreSolverLimits(time::Span timeout, unsigned memoryLimit) {
+  impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 } // namespace klee
diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h
index 873ed3dbd6..f8244ddc2f 100644
--- a/lib/Solver/STPSolver.h
+++ b/lib/Solver/STPSolver.h
@@ -29,10 +29,10 @@ class STPSolver : public Solver {
   /// format.
   std::string getConstraintLog(const Query &) final;
 
-  /// setCoreSolverTimeout - Set constraint solver timeout delay to the given
+  /// setCoreSolverLimits - Set constraint solver timeout delay to the given
   /// value; 0
   /// is off.
-  virtual void setCoreSolverTimeout(time::Span timeout);
+  virtual void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
 };
 } // namespace klee
 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 98c830f0df..c6491707c8 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -38,8 +38,8 @@ std::string Solver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
 }
 
-void Solver::setCoreSolverTimeout(time::Span timeout) {
-  impl->setCoreSolverTimeout(timeout);
+void Solver::setCoreSolverLimits(time::Span timeout, unsigned memoryLimit) {
+  impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 bool Solver::evaluate(const Query &query, PartialValidity &result) {
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index 2f36e881ec..54e7902869 100644
--- a/lib/Solver/SolverCmdLine.cpp
+++ b/lib/Solver/SolverCmdLine.cpp
@@ -91,6 +91,11 @@ cl::opt<std::string> MaxCoreSolverTime(
         "Enables --use-forked-solver"),
     cl::cat(SolvingCat));
 
+cl::opt<unsigned> MaxCoreSolverMemory(
+    "max-solver-memory",
+    cl::desc("Set soft memory limit for core SMT solver (default=0 (off))"),
+    cl::init(0), cl::cat(SolvingCat));
+
 cl::opt<bool> UseForkedCoreSolver(
     "use-forked-solver",
     cl::desc("Run the core SMT solver in a forked process (default=true)"),
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index ce0c3fd437..f07f6d6a31 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -42,7 +42,7 @@ class ValidatingSolver : public SolverImpl {
                            bool &isValid);
   SolverRunStatus getOperationStatusCode();
   std::string getConstraintLog(const Query &) final;
-  void setCoreSolverTimeout(time::Span timeout);
+  void setCoreSolverLimits(time::Span timeout, unsigned memoryLimit);
   void notifyStateTermination(std::uint32_t id);
 };
 
@@ -223,8 +223,9 @@ std::string ValidatingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
-  solver->impl->setCoreSolverTimeout(timeout);
+void ValidatingSolver::setCoreSolverLimits(time::Span timeout,
+                                           unsigned memoryLimit) {
+  solver->impl->setCoreSolverLimits(timeout, memoryLimit);
 }
 
 void ValidatingSolver::notifyStateTermination(std::uint32_t id) {
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index bf94993bdf..8a4a3d1bf9 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -216,10 +216,12 @@ class Z3SolverImpl : public SolverImpl {
 private:
   Z3BuilderType builderType;
   time::Span timeout;
+  unsigned memoryLimit;
   SolverImpl::SolverRunStatus runStatusCode;
   std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile;
   // Parameter symbols
   ::Z3_symbol timeoutParamStrSymbol;
+  ::Z3_symbol maxMemoryParamStrSymbol;
   ::Z3_symbol unsatCoreParamStrSymbol;
 
   bool internalRunSolver(const ConstraintQuery &query, Z3SolverEnv &env,
@@ -259,8 +261,9 @@ class Z3SolverImpl : public SolverImpl {
 public:
   std::string getConstraintLog(const Query &) final;
   SolverImpl::SolverRunStatus getOperationStatusCode() final;
-  void setCoreSolverTimeout(time::Span _timeout) final {
+  void setCoreSolverLimits(time::Span _timeout, unsigned _memoryLimit) final {
     timeout = _timeout;
+    memoryLimit = _memoryLimit;
 
     auto timeoutInMilliSeconds =
         static_cast<unsigned>((timeout.toMicroseconds() / 1000));
@@ -268,6 +271,10 @@ class Z3SolverImpl : public SolverImpl {
       timeoutInMilliSeconds = UINT_MAX;
     Z3_params_set_uint(builder->ctx, solverParameters, timeoutParamStrSymbol,
                        timeoutInMilliSeconds);
+    if (memoryLimit) {
+      Z3_params_set_uint(builder->ctx, solverParameters,
+                         maxMemoryParamStrSymbol, memoryLimit);
+    }
   }
   void enableUnsatCore() {
     Z3_params_set_bool(builder->ctx, solverParameters, unsatCoreParamStrSymbol,
@@ -312,7 +319,9 @@ Z3SolverImpl::Z3SolverImpl(Z3BuilderType type)
   solverParameters = Z3_mk_params(builder->ctx);
   Z3_params_inc_ref(builder->ctx, solverParameters);
   timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout");
-  setCoreSolverTimeout(timeout);
+  maxMemoryParamStrSymbol =
+      Z3_mk_string_symbol(builder->ctx, "memory_high_watermark_mb");
+  setCoreSolverLimits(timeout, memoryLimit);
   unsatCoreParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "unsat_core");
 
   // HACK: This changes Z3's handling of the `to_ieee_bv` function so that
diff --git a/scripts/kleef b/scripts/kleef
index dd7bc29bcc..e46c0cf6e7 100755
--- a/scripts/kleef
+++ b/scripts/kleef
@@ -38,6 +38,7 @@ def klee_options(
         "--max-solvers-approx-tree-inc=16",
         # Just use half of the memory in case we have to fork
         f"--max-memory={int(max_memory * 0.7)}",
+        f"--max-solver-memory={int(max_memory * 0.7)}",
         "--libc=klee",
         "--skip-not-lazy-initialized",
         f"--output-dir={test_output_dir}",  # Output files into specific directory
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 98cf20dcf9..583d81fe1d 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -198,8 +198,9 @@ static bool EvaluateInputAST(const char *Filename, const llvm::MemoryBuffer *MB,
 
   if (CoreSolverToUse != DUMMY_SOLVER) {
     const time::Span maxCoreSolverTime(MaxCoreSolverTime);
-    if (maxCoreSolverTime) {
-      coreSolver->setCoreSolverTimeout(maxCoreSolverTime);
+    const unsigned maxCoreSolverMemory(MaxCoreSolverMemory);
+    if (maxCoreSolverTime || maxCoreSolverMemory) {
+      coreSolver->setCoreSolverLimits(maxCoreSolverTime, maxCoreSolverMemory);
     }
   }
 
diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp
index cdc2ea2808..5537210352 100644
--- a/unittests/Solver/Z3SolverTest.cpp
+++ b/unittests/Solver/Z3SolverTest.cpp
@@ -27,7 +27,7 @@ class Z3SolverTest : public ::testing::Test {
   std::unique_ptr<Solver> Z3Solver_;
 
   Z3SolverTest() : Z3Solver_(createCoreSolver(CoreSolverType::Z3_SOLVER)) {
-    Z3Solver_->setCoreSolverTimeout(time::Span("10s"));
+    Z3Solver_->setCoreSolverLimits(time::Span("10s"), 0);
   }
 };