diff --git a/clang/lib/Verify/Backend/CVC5Backend.cpp b/clang/lib/Verify/Backend/CVC5Backend.cpp
index 3a53d58e3f..a4bca829d6 100644
--- a/clang/lib/Verify/Backend/CVC5Backend.cpp
+++ b/clang/lib/Verify/Backend/CVC5Backend.cpp
@@ -30,6 +30,7 @@
 #else
 #include <cerrno>
 #include <csignal>
+#include <sys/resource.h>
 #include <sys/wait.h>
 #endif
 
@@ -1505,15 +1506,9 @@ class SMTLibEncoder {
 static VerifyResult querySizeLimitResult(const ObligationModule &Module,
                                          uint64_t MaxQueryNodes,
                                          llvm::StringRef BackendName) {
-  VerifyResult Result;
-  if (MaxQueryNodes == 0 || obligationModuleNodeCount(Module) <= MaxQueryNodes)
-    return Result;
-  Result.Status = VerifyStatus::Unresolved;
-  Result.Reason = VerifyReason::QuerySizeLimit;
-  Result.Message = "canonical obligation module exceeds query node budget " +
-                   std::to_string(MaxQueryNodes);
-  Result.BackendName = BackendName.str();
-  return Result;
+  if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, BackendName))
+    return std::move(*Limited);
+  return VerifyResult();
 }
 
 static std::optional<std::string>
@@ -2404,7 +2399,8 @@ CVC5VerifyBackend::CVC5VerifyBackend(const BackendExecutionOptions &Execution)
     : TimeoutMs(Execution.SolverTimeoutMs),
       CollectionTimeoutMs(Execution.CollectionTimeoutMs),
       CertifyTimeoutMs(Execution.CertifyTimeoutMs),
-      ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs),
+      ResourceLimit(Execution.SolverResourceLimit),
+      MemoryLimitMB(Execution.MemoryLimitMB), Jobs(Execution.Jobs),
       Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes),
       IntegerEncoding(Execution.IntegerEncoding) {
   llvm::StringRef Requested = Execution.CVC5Path.empty()
@@ -2431,6 +2427,7 @@ struct SolverRun {
 
 static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                          unsigned TimeoutMs, unsigned ResourceLimit,
+                         uint64_t MemoryLimitMB = 0,
                          const std::atomic<bool> *Cancelled = nullptr);
 
 /// Whether the cvc5 at \p SolverPath prints a sequence value last element
@@ -2473,6 +2470,7 @@ static bool printsSequencesReversed(const std::string &SolverPath) {
 
 static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                          unsigned TimeoutMs, unsigned ResourceLimit,
+                         uint64_t MemoryLimitMB,
                          const std::atomic<bool> *Cancelled) {
   SolverRun Run;
   VerifyResult &Result = Run.Failure;
@@ -2530,9 +2528,27 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                                                 ErrorPath.str()};
   std::string InvocationError;
   bool ExecutionFailed = false;
+  // On Windows the limit bounds the process's committed memory. On POSIX
+  // hosts a limit makes ExecuteNoWait fork rather than spawn, and fork runs
+  // Z3's fork handlers, which wait for the timers of every check running in
+  // the process; the limit is set on the spawned process instead.
+#if defined(_WIN32)
+  const unsigned SpawnLimit = static_cast<unsigned>(
+      std::min<uint64_t>(MemoryLimitMB, std::numeric_limits<unsigned>::max()));
+#else
+  const unsigned SpawnLimit = 0;
+#endif
   llvm::sys::ProcessInfo Process =
-      llvm::sys::ExecuteNoWait(SolverPath, Args, std::nullopt, Redirects, 0,
-                               &InvocationError, &ExecutionFailed);
+      llvm::sys::ExecuteNoWait(SolverPath, Args, std::nullopt, Redirects,
+                               SpawnLimit, &InvocationError, &ExecutionFailed);
+#if defined(__linux__)
+  // What cvc5 allocates: its data segment and private writable mappings.
+  if (MemoryLimitMB != 0 && Process.Pid != llvm::sys::ProcessInfo::InvalidPid) {
+    struct rlimit Data;
+    Data.rlim_cur = Data.rlim_max = static_cast<rlim_t>(MemoryLimitMB) << 20;
+    (void)::prlimit(Process.Pid, RLIMIT_DATA, &Data, nullptr);
+  }
+#endif
   if (ExecutionFailed || Process.Pid == llvm::sys::ProcessInfo::InvalidPid) {
     Result.Reason = VerifyReason::SolverInvocationFailure;
     Result.Message = InvocationError.empty() ? "cannot start cvc5 process"
@@ -2615,6 +2631,25 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
     return Run;
   }
   if (ExitCode != 0) {
+    std::string OutputError;
+    std::optional<std::string> StandardOutput =
+        readSolverOutput(OutputPath, OutputError, MaxSolverOutputBytes);
+    // An allocation past the limit fails, and cvc5 reports it as an error
+    // ((error "std::bad_alloc")) or aborts on it (std::bad_alloc, or its SAT
+    // solver's Minisat::OutOfMemoryException).
+    auto outOfMemory = [](llvm::StringRef Text) {
+      return Text.contains("bad_alloc") || Text.contains("OutOfMemory");
+    };
+    if (outOfMemory(*StandardError) ||
+        (StandardOutput && outOfMemory(*StandardOutput))) {
+      Result.Reason = VerifyReason::SolverMemoryLimit;
+      Result.Message = "cvc5 ran out of memory";
+      if (MemoryLimitMB != 0)
+        Result.Message += ": each cvc5 process may use " +
+                          std::to_string(MemoryLimitMB) +
+                          " MB (--memory-limit)";
+      return Run;
+    }
     Result.Reason = VerifyReason::SolverInvocationFailure;
     Result.Message = "cvc5 exited with status " + std::to_string(ExitCode);
     if (!InvocationError.empty())
@@ -2622,9 +2657,7 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
     if (!StandardError->empty())
       Result.Message += ": " + diagnosticText(*StandardError);
     // cvc5 reports a script it rejects on standard output.
-    std::string OutputError;
-    if (std::optional<std::string> StandardOutput =
-            readSolverOutput(OutputPath, OutputError, MaxSolverOutputBytes))
+    if (StandardOutput)
       for (llvm::StringRef Rest = *StandardOutput; !Rest.empty();) {
         auto [Line, Next] = Rest.split('\n');
         if (Line.trim().starts_with("(error")) {
@@ -2802,8 +2835,8 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
       }
       Budget = static_cast<unsigned>(Remaining);
     }
-    SolverRun Run =
-        runCVC5(SolverPath, *Script, Budget, ResourceLimit, &Cancelled);
+    SolverRun Run = runCVC5(SolverPath, *Script, Budget, ResourceLimit,
+                            MemoryLimitMB, &Cancelled);
     auto giveUp = [&](llvm::StringRef Outcome) {
       RefinementDecision Exhausted = Refinement.exhausted(Outcome);
       Result.Reason = Exhausted.Reason;
diff --git a/clang/lib/Verify/Backend/CVC5Backend.h b/clang/lib/Verify/Backend/CVC5Backend.h
index 875d38fa26..3f7badb7a6 100644
--- a/clang/lib/Verify/Backend/CVC5Backend.h
+++ b/clang/lib/Verify/Backend/CVC5Backend.h
@@ -30,6 +30,7 @@ class CVC5VerifyBackend : public VerifyBackend {
   /// Set by cancel(): the running process is stopped and no other starts.
   std::atomic<bool> Cancelled{false};
   unsigned ResourceLimit;
+  uint64_t MemoryLimitMB;
   unsigned Jobs;
   llvm::StdThreadPool *Pool;
   std::optional<std::chrono::steady_clock::time_point> Deadline;
diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp
index 6bebcbc018..ac40f84d34 100644
--- a/clang/lib/Verify/Backend/Obligation.cpp
+++ b/clang/lib/Verify/Backend/Obligation.cpp
@@ -1,11 +1,13 @@
 //===--- Obligation.cpp ---------------------------------------------------===//
 #include "LogicTerms.h"
 #include "ObligationLowering.h"
+#include "ObligationSimplify.h"
 #include "SpecAxioms.h"
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Error.h"
+#include "llvm/Support/MathExtras.h"
 #include <algorithm>
 #include <tuple>
 
@@ -2159,7 +2161,8 @@ class ObligationBuilder {
     return std::move(Result);
   }
 
-  llvm::Expected<ObligationModule> buildPassive(const PassiveProgram &P) {
+  llvm::Expected<ObligationModule> buildPassive(const PassiveProgram &P,
+                                                uint64_t MaxNodes) {
     ObligationModule M;
     M.FunctionName = P.FunctionName;
     M.FunctionIdentity = P.FunctionIdentity;
@@ -2272,6 +2275,37 @@ class ObligationBuilder {
       return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s",
                                      ConstructionError.c_str());
 
+    // The goals' size is known before any is built: each is its condition
+    // under a negated copy of every assumption before it (a Not and an Or
+    // each), each query is its goal negated, and the complete goal joins the
+    // goals by And, with its query.
+    uint64_t Prefix = 0, Goals = 0, GoalCount = 0;
+    auto assumed = [&](const VCExpr *Assumption) {
+      Prefix =
+          llvm::SaturatingAdd(Prefix, logicNodeCount(Assumption), uint64_t(2));
+    };
+    auto goal = [&](const VCExpr *Condition) {
+      Goals = llvm::SaturatingAdd(Goals, Prefix, logicNodeCount(Condition));
+      ++GoalCount;
+    };
+    for (const auto &Entry : EntryAssumes)
+      assumed(Entry.get());
+    for (const LoweredStmt &Stmt : Stmts) {
+      if (Stmt.Kind == PassiveStmt::Assume)
+        assumed(Stmt.Cond.get());
+      else
+        goal(Stmt.Cond.get());
+    }
+    for (const auto &Exit : ExitAsserts)
+      goal(std::get<1>(Exit).get());
+    const uint64_t GoalNodes =
+        GoalCount == 0
+            ? 3
+            : llvm::SaturatingAdd(llvm::SaturatingMultiply(Goals, uint64_t(4)),
+                                  3 * GoalCount - 1);
+    if (MaxNodes != 0 && GoalNodes > MaxNodes)
+      return ObligationSizeError::obligations(GoalNodes, MaxNodes);
+
     std::vector<const VCExpr *> Assumptions;
     for (const auto &Entry : EntryAssumes)
       Assumptions.push_back(Entry.get());
@@ -2324,10 +2358,13 @@ class ObligationBuilder {
 
     M.CorrectnessGoal = buildCompleteGoal(M.Obligations);
     M.CounterexampleQuery = vcNot(cloneVCExpr(M.CorrectnessGoal.get()));
+    assert(GoalNodes == obligationModuleNodeCount(M) &&
+           "the goals' size was not predicted exactly");
 
     SpecAxiomContext AxiomContext{P.SpecFunctions, P.SpecFuel, P.HiddenSpecs,
                                   P.RevealedSpecs};
-    if (llvm::Error Error = materializeLogicFunctions(M, AxiomContext))
+    if (llvm::Error Error =
+            materializeLogicFunctions(M, AxiomContext, MaxNodes, GoalNodes))
       return std::move(Error);
 
     auto RequiredFeatures = validateObligationModule(M);
@@ -2588,14 +2625,32 @@ verify::validateObligationModule(const ObligationModule &M) {
   return RequiredFeatures;
 }
 
+char ObligationSizeError::ID = 0;
+
+llvm::Error ObligationSizeError::obligations(uint64_t Nodes, uint64_t Limit) {
+  return llvm::make_error<ObligationSizeError>(
+      "the proof obligations", Nodes, Limit,
+      "each check repeats every assumption before it, so split the function "
+      "or raise the limit");
+}
+
+void ObligationSizeError::log(llvm::raw_ostream &OS) const {
+  OS << What << " would take at least " << Nodes
+     << " expression nodes, more than the limit of " << Limit
+     << " (--max-query-nodes): " << Advice;
+}
+
 llvm::Expected<ObligationModule>
-verify::buildObligationModule(const PassiveProgram &P) {
+verify::buildObligationModule(const PassiveProgram &P, uint64_t MaxNodes) {
   ObligationBuilder B(P.ResultVarName,
                       P.OldHeapName.empty() ? std::string(VHeapName) + "_0"
                                             : P.OldHeapName,
                       P.CallerIntMode, P.HeapVariables,
                       /*ForceCallerMode=*/false, &P.SpecFunctions);
-  auto Module = B.buildPassive(P);
+  if (const auto &Over = P.TooLarge)
+    return llvm::make_error<ObligationSizeError>(Over->What, Over->Nodes,
+                                                 Over->Limit, Over->Advice);
+  auto Module = B.buildPassive(P, MaxNodes);
   if (Module) {
     Module->AssumedPosts = P.AssumedPosts;
     Module->AssumedUnfoldings = P.AssumedUnfoldings;
diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h
index ba16118533..463f109f4a 100644
--- a/clang/lib/Verify/Backend/Obligation.h
+++ b/clang/lib/Verify/Backend/Obligation.h
@@ -3,6 +3,7 @@
 #ifndef LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H
 #define LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H
 
+#include "../IR/NodeBudget.h"
 #include "clang/Basic/SourceLocation.h"
 #include "llvm/Support/Error.h"
 #include <cstdint>
@@ -217,7 +218,7 @@ class LogicExpr {
   /// archives.
   std::vector<std::unique_ptr<LogicExpr>> Patterns;
 
-  explicit LogicExpr(Kind K) : K(K) {}
+  explicit LogicExpr(Kind K) : K(K) { NodeBudget::count(); }
 };
 
 // Compatibility name for the Z3/spec adapters while they migrate internally.
diff --git a/clang/lib/Verify/Backend/ObligationLowering.h b/clang/lib/Verify/Backend/ObligationLowering.h
index 591892fc06..2a4af2f327 100644
--- a/clang/lib/Verify/Backend/ObligationLowering.h
+++ b/clang/lib/Verify/Backend/ObligationLowering.h
@@ -10,8 +10,37 @@
 namespace clang {
 namespace verify {
 
+/// Something a function's verification builds would have more expression
+/// nodes than the limit allows (--max-query-nodes), found before or as it
+/// was built: the obligations, each repeating every assumption before it
+/// (their size is known before any is built), or a spec's definition
+/// unfolded as deep as its fuel.
+class ObligationSizeError : public llvm::ErrorInfo<ObligationSizeError> {
+public:
+  static char ID;
+  ObligationSizeError(std::string What, uint64_t Nodes, uint64_t Limit,
+                      std::string Advice)
+      : What(std::move(What)), Nodes(Nodes), Limit(Limit),
+        Advice(std::move(Advice)) {}
+  /// The obligations of a module of \p Nodes nodes.
+  static llvm::Error obligations(uint64_t Nodes, uint64_t Limit);
+  void log(llvm::raw_ostream &OS) const override;
+  std::error_code convertToErrorCode() const override {
+    return llvm::inconvertibleErrorCode();
+  }
+  std::string What;
+  /// At least this many: a construction stops once it passes the limit.
+  uint64_t Nodes;
+  uint64_t Limit;
+  std::string Advice;
+};
+
+/// With \p MaxNodes, a module that would have more nodes than that (as
+/// obligationModuleNodeCount counts them) is an ObligationSizeError, before
+/// its goals are built. So is a program one of whose constructions passed
+/// its limit (PassiveProgram::TooLarge).
 llvm::Expected<ObligationModule>
-buildObligationModule(const PassiveProgram &Program);
+buildObligationModule(const PassiveProgram &Program, uint64_t MaxNodes = 0);
 
 ObligationKind obligationKind(ProofObligationKind Kind);
 
diff --git a/clang/lib/Verify/Backend/SpecAxioms.cpp b/clang/lib/Verify/Backend/SpecAxioms.cpp
index e95be6beaf..188dd79b83 100644
--- a/clang/lib/Verify/Backend/SpecAxioms.cpp
+++ b/clang/lib/Verify/Backend/SpecAxioms.cpp
@@ -1,8 +1,10 @@
 //===--- SpecAxioms.cpp - Verus-style spec defining axioms ----------------===//
 #include "SpecAxioms.h"
 #include "../Transform/SpecInline.h"
+#include "LogicTerms.h"
 #include "ObligationLowering.h"
 #include "llvm/Support/Error.h"
+#include "llvm/Support/MathExtras.h"
 
 using namespace clang;
 using namespace verify;
@@ -114,7 +116,9 @@ static const VFunction *findSpecFunction(const FunctionMap &Functions,
 }
 
 llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
-                                              const SpecAxiomContext &Ctx) {
+                                              const SpecAxiomContext &Ctx,
+                                              uint64_t MaxNodes,
+                                              uint64_t Nodes) {
   // The functions the query reaches; then, for a counterexample check only,
   // those their unfoldings and postconditions apply, where a failure leaves
   // the function out instead of failing the module.
@@ -153,6 +157,20 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
         Module.LogicFunctions.try_emplace(Identity, std::move(Declaration));
     (void)Inserted;
     LogicFunctionDecl &Owned = It->second;
+    // Its definitions join the module's nodes once all are lowered.
+    uint64_t Own = 0;
+    auto count = [&](const LogicExpr *Definition) -> llvm::Error {
+      Own = llvm::SaturatingAdd(Own, logicNodeCount(Definition));
+      const uint64_t Total = llvm::SaturatingAdd(Nodes, Own);
+      if (MaxNodes != 0 && Total > MaxNodes)
+        return llvm::make_error<ObligationSizeError>(
+            "the proof obligations with the definitions of the specs they "
+            "apply",
+            Total, MaxNodes,
+            "lower the fuel cppverify::reveal_with_fuel gives, split the "
+            "function, or raise the limit");
+      return llvm::Error::success();
+    };
     const std::string DefinitionHeap = Spec->ReadsHeap
                                            ? std::string(VSpecHeapName)
                                            : std::string(VHeapName) + "_0";
@@ -223,13 +241,26 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
       return llvm::createStringError(
           llvm::inconvertibleErrorCode(),
           "spec step definition result sort mismatch: %s", Spec->Name.c_str());
+    if (llvm::Error Error = count(Owned.StepDefinition.get()))
+      return Error;
     collectReferencedLogicFunctions(Owned.StepDefinition.get(), Pending);
 
     const unsigned MaxDepth =
         Spec->NeedsDecreasesCheck ? Fuel : std::min(Fuel, 1U);
     Owned.DefinitionFuel = MaxDepth;
     for (unsigned Depth = 1; Depth <= MaxDepth; ++Depth) {
-      std::unique_ptr<VExpr> Body = unfoldSpecDefinition(*Spec, Ctx, Depth);
+      std::unique_ptr<VExpr> Body;
+      {
+        NodeBudget Unfolding;
+        Body = unfoldSpecDefinition(*Spec, Ctx, Depth);
+        if (Unfolding.exceeded())
+          return llvm::make_error<ObligationSizeError>(
+              "the definition of " + Spec->Name + " unfolded " +
+                  std::to_string(Depth) + " levels deep",
+              Unfolding.built(), Unfolding.limit(),
+              "lower its fuel (cppverify::reveal_with_fuel), or raise the "
+              "limit");
+      }
       if (!Body)
         continue;
       auto Lowered = lowerLogicExpr(Body.get(), "", DefinitionHeap,
@@ -245,6 +276,8 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
         return llvm::createStringError(
             llvm::inconvertibleErrorCode(),
             "spec definition result sort mismatch: %s", Spec->Name.c_str());
+      if (llvm::Error Error = count(Definition.get()))
+        return Error;
       collectReferencedLogicFunctions(Definition.get(), Pending);
       Owned.DefinitionLevels.push_back(std::move(Definition));
     }
@@ -262,6 +295,7 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
         Owned.Decreases.push_back(std::move(*Lowered));
       }
     }
+    Nodes = llvm::SaturatingAdd(Nodes, Own);
     return llvm::Error::success();
   };
   std::set<std::string> Pending;
diff --git a/clang/lib/Verify/Backend/SpecAxioms.h b/clang/lib/Verify/Backend/SpecAxioms.h
index 23614adbbb..8b7dc1bf94 100644
--- a/clang/lib/Verify/Backend/SpecAxioms.h
+++ b/clang/lib/Verify/Backend/SpecAxioms.h
@@ -36,8 +36,15 @@ std::unique_ptr<VExpr> unfoldSpecBodyForAxiom(const VFunction &Spec,
 
 /// Materialize all logical function declarations and finite definition levels
 /// reachable from Module into its owned backend-neutral representation.
+/// With \p MaxNodes, the definitions may bring the module from \p Nodes to
+/// at most that many nodes (as obligationModuleNodeCount counts them): each
+/// is counted as it is lowered, and one past the limit is an
+/// ObligationSizeError, or left out when only a counterexample check needs
+/// it.
 llvm::Error materializeLogicFunctions(ObligationModule &Module,
-                                      const SpecAxiomContext &Ctx);
+                                      const SpecAxiomContext &Ctx,
+                                      uint64_t MaxNodes = 0,
+                                      uint64_t Nodes = 0);
 
 } // namespace verify
 } // namespace clang
diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp
index afd6b07247..35f9350638 100644
--- a/clang/lib/Verify/Backend/VerifyBackend.cpp
+++ b/clang/lib/Verify/Backend/VerifyBackend.cpp
@@ -230,17 +230,8 @@ class PortfolioVerifyBackend : public VerifyBackend {
     CVC5->setDeadline(D);
   }
   VerifyResult verifyModule(const ObligationModule &Module) override {
-    if (MaxQueryNodes != 0 &&
-        obligationModuleNodeCount(Module) > MaxQueryNodes) {
-      VerifyResult Result;
-      Result.Status = VerifyStatus::Unresolved;
-      Result.Reason = VerifyReason::QuerySizeLimit;
-      Result.Message =
-          "canonical obligation module exceeds query node budget " +
-          std::to_string(MaxQueryNodes);
-      Result.BackendName = "portfolio";
-      return Result;
-    }
+    if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, "portfolio"))
+      return std::move(*Limited);
 
     std::vector<VerifyResult> Z3Results;
     std::vector<VerifyResult> CVC5Results;
@@ -392,6 +383,24 @@ verify::parseMachineIntegerEncoding(llvm::StringRef Name) {
   return std::nullopt;
 }
 
+std::optional<VerifyResult>
+verify::moduleSizeLimit(const ObligationModule &Module, uint64_t MaxNodes,
+                        llvm::StringRef BackendName) {
+  if (MaxNodes == 0)
+    return std::nullopt;
+  const uint64_t Nodes = obligationModuleNodeCount(Module);
+  if (Nodes <= MaxNodes)
+    return std::nullopt;
+  VerifyResult Result;
+  Result.Status = VerifyStatus::Unresolved;
+  Result.Reason = VerifyReason::QuerySizeLimit;
+  Result.Message = "the obligation module has " + std::to_string(Nodes) +
+                   " expression nodes, more than the limit of " +
+                   std::to_string(MaxNodes) + " (--max-query-nodes)";
+  Result.BackendName = BackendName.str();
+  return Result;
+}
+
 llvm::StringRef verify::verifyReasonCode(VerifyReason Reason) {
   switch (Reason) {
   case VerifyReason::None:
@@ -402,6 +411,8 @@ llvm::StringRef verify::verifyReasonCode(VerifyReason Reason) {
     return "solver.timeout";
   case VerifyReason::SolverResourceLimit:
     return "solver.resource-limit";
+  case VerifyReason::SolverMemoryLimit:
+    return "solver.memory-limit";
   case VerifyReason::SolverUnknown:
     return "solver.unknown";
   case VerifyReason::SolverUnavailable:
@@ -681,17 +692,8 @@ class RaceVerifyBackend : public VerifyBackend {
     CVC5->setDeadline(D);
   }
   VerifyResult verifyModule(const ObligationModule &Module) override {
-    if (MaxQueryNodes != 0 &&
-        obligationModuleNodeCount(Module) > MaxQueryNodes) {
-      VerifyResult Result;
-      Result.Status = VerifyStatus::Unresolved;
-      Result.Reason = VerifyReason::QuerySizeLimit;
-      Result.Message =
-          "canonical obligation module exceeds query node budget " +
-          std::to_string(MaxQueryNodes);
-      Result.BackendName = "race";
-      return Result;
-    }
+    if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, "race"))
+      return std::move(*Limited);
     resume();
     VerifyResult Z3Result;
     VerifyResult CVC5Result;
diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h
index 00e7678705..ffa2f59c0d 100644
--- a/clang/lib/Verify/Backend/VerifyBackend.h
+++ b/clang/lib/Verify/Backend/VerifyBackend.h
@@ -36,6 +36,8 @@ enum class VerifyReason {
   Counterexample,
   SolverTimeout,
   SolverResourceLimit,
+  /// The solver ran out of the memory --memory-limit gives it.
+  SolverMemoryLimit,
   SolverUnknown,
   SolverUnavailable,
   SolverInvocationFailure,
@@ -77,6 +79,12 @@ enum class VerifyReason {
 
 llvm::StringRef verifyReasonCode(VerifyReason Reason);
 
+/// Limits what Z3 allocates in this process to \p MegaBytes, its queries
+/// together; 0 removes the limit. A check runs until its watchdog, polling
+/// every 10 ms, finds the limit passed, and its query then ends Unresolved
+/// with SolverMemoryLimit. Call it before any query runs.
+void setZ3MemoryLimit(uint64_t MegaBytes);
+
 /// Stops verification for the rest of the process (Ctrl-C): queries running
 /// end unresolved and none starts. Safe to call from a signal handler.
 void requestInterrupt();
@@ -238,6 +246,13 @@ llvm::StringRef machineIntegerEncodingName(MachineIntegerEncoding Encoding);
 std::optional<MachineIntegerEncoding>
 parseMachineIntegerEncoding(llvm::StringRef Name);
 
+/// Unresolved with QuerySizeLimit when \p Module has more than \p MaxNodes
+/// expression nodes, as a module from an archive or one a backend derives
+/// may; a source module is refused before it is built.
+std::optional<VerifyResult> moduleSizeLimit(const ObligationModule &Module,
+                                            uint64_t MaxNodes,
+                                            llvm::StringRef BackendName);
+
 struct BackendExecutionOptions {
   unsigned SolverTimeoutMs = 0;
   /// Per-query timeout for modules over sequences, sets, multisets, or
@@ -256,6 +271,9 @@ struct BackendExecutionOptions {
   llvm::StdThreadPool *Pool = nullptr;
   /// Maximum canonical expression nodes in a module; 0 disables it.
   uint64_t MaxQueryNodes = 0;
+  /// The megabytes each cvc5 process may allocate; 0 disables the limit.
+  /// Z3's limit is process-wide: setZ3MemoryLimit.
+  uint64_t MemoryLimitMB = 0;
   MachineIntegerEncoding IntegerEncoding = MachineIntegerEncoding::Auto;
   /// Do not retry a whole-module query after individual obligations are
   /// unresolved. Interactive fallback backends can consume those unresolved
diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp
index 305b45949c..27e62848dd 100644
--- a/clang/lib/Verify/Backend/Z3Encode.cpp
+++ b/clang/lib/Verify/Backend/Z3Encode.cpp
@@ -41,15 +41,7 @@ constexpr unsigned Z3ProofCacheAdapterVersion = 2;
 
 std::optional<VerifyResult> querySizeLimitResult(const ObligationModule &Module,
                                                  uint64_t MaxQueryNodes) {
-  if (MaxQueryNodes == 0 || obligationModuleNodeCount(Module) <= MaxQueryNodes)
-    return std::nullopt;
-  VerifyResult Result;
-  Result.Status = VerifyStatus::Unresolved;
-  Result.Reason = VerifyReason::QuerySizeLimit;
-  Result.Message = "canonical obligation module exceeds query node budget " +
-                   std::to_string(MaxQueryNodes);
-  Result.BackendName = "z3";
-  return Result;
+  return moduleSizeLimit(Module, MaxQueryNodes, "z3");
 }
 
 std::optional<std::string> sourceModelValue(const z3::expr &Value,
@@ -139,6 +131,44 @@ z3::params solverParams(z3::context &Ctx) {
 
 } // namespace
 
+namespace {
+/// The limit setZ3MemoryLimit gave Z3, for messages.
+std::atomic<uint64_t> Z3MemoryLimitMB{0};
+
+std::string z3MemoryMessage() {
+  const uint64_t Limit = Z3MemoryLimitMB.load();
+  if (Limit == 0)
+    return "Z3 ran out of memory";
+  return "Z3 reached the memory limit: its queries share " +
+         std::to_string(Limit) + " MB (--memory-limit)";
+}
+} // namespace
+
+// Each check's watchdog enforces the limit, so a check it stops is known to
+// have stopped for memory. Z3's own limits do not say so: its hard one,
+// memory_max_size, fails whichever allocation passes it in any context of
+// the process, Z3_mk_context's included, which then returns no context; its
+// high watermark stops the search where it is checked, often reporting only
+// canceled, and frees what the check took before it returns.
+void verify::setZ3MemoryLimit(uint64_t MegaBytes) {
+  Z3MemoryLimitMB = MegaBytes;
+}
+
+/// Z3's allocations, every query's together, are over the limit.
+static bool overMemoryLimit() {
+  const uint64_t Limit = Z3MemoryLimitMB.load();
+  return Limit != 0 && Z3_get_estimated_alloc_size() > (Limit << 20);
+}
+
+/// Z3 says a check that returned unknown ran out of memory, as when an
+/// allocation fails.
+static bool memoryReason(const z3::solver &S) {
+  const std::string Reason = S.reason_unknown();
+  return llvm::StringRef(Reason).contains("memout") ||
+         llvm::StringRef(Reason).contains("max. memory") ||
+         llvm::StringRef(Reason).contains("out of memory");
+}
+
 namespace {
 /// The encoder of each live Z3 context, for its error handler.
 std::mutex APIErrorLock;
@@ -166,14 +196,19 @@ void Z3Encoder::recordAPIError(Z3_context Context, Z3_error_code Code) {
     if (auto It = APIErrorEncoders.find(Context); It != APIErrorEncoders.end())
       Encoder = It->second;
   }
-  if (!Encoder || Encoder->Checking || !Encoder->APIError.empty())
+  if (!Encoder)
+    return;
+  // A check reports other errors as unknown, but not why.
+  if (Code == Z3_MEMOUT_FAIL)
+    Encoder->OutOfMemory = true;
+  if (Encoder->Checking || !Encoder->APIError.empty())
     return;
   Encoder->APIError = Z3_get_error_msg(Context, Code);
   Encoder->markEncodingFailure("Z3 reported an error: " + Encoder->APIError);
 }
 
 VerifyResult Z3Encoder::withAPIError(VerifyResult Result) {
-  if (APIError.empty())
+  if (APIError.empty() && !OutOfMemory)
     return Result;
   {
     std::lock_guard<std::mutex> Guard(CheckLock);
@@ -182,6 +217,11 @@ VerifyResult Z3Encoder::withAPIError(VerifyResult Result) {
   }
   VerifyResult Failed;
   Failed.Status = VerifyStatus::Unresolved;
+  if (OutOfMemory) {
+    Failed.Reason = VerifyReason::SolverMemoryLimit;
+    Failed.Message = z3MemoryMessage();
+    return Failed;
+  }
   Failed.Reason = VerifyReason::EncodingFailure;
   Failed.Message = "Z3 reported an error: " + APIError;
   return Failed;
@@ -1794,20 +1834,26 @@ z3::check_result Z3Encoder::check(z3::solver &S, unsigned Ms) {
   using Clock = std::chrono::steady_clock;
   {
     std::lock_guard<std::mutex> Guard(CheckLock);
-    if (Stopped || interruptRequested())
+    if (Stopped || OutOfMemory || interruptRequested())
       return z3::unknown;
     CheckFinished = false;
   }
   Checking = true;
   // Z3 forgets a cancellation that arrives inside one of its nested resource
   // scopes (leaving the scope clears it), whether from its own timeout or
-  // from interrupt(). A check past its time, stopped, or interrupted by
-  // Ctrl-C, which the watchdog polls for, is therefore interrupted again
-  // until it returns.
+  // from interrupt(). A check past its time, stopped, interrupted by Ctrl-C,
+  // or past the memory limit, which the watchdog polls for, is therefore
+  // interrupted again until it returns.
   constexpr std::chrono::milliseconds Grace(100);
   constexpr std::chrono::milliseconds Interval(50);
+  // How often the memory limit is polled: what a check allocates in this
+  // time is how far it can pass the limit.
+  constexpr std::chrono::milliseconds MemoryInterval(10);
+  const auto Poll = Z3MemoryLimitMB.load() != 0 ? MemoryInterval : Interval;
   bool TimedOut = false;
   bool Interrupted = false;
+  bool OverLimit = false;
+  z3::check_result Result = z3::unknown;
   std::thread Watchdog([&] {
     std::unique_lock<std::mutex> Lock(CheckLock);
     const auto Limit =
@@ -1815,13 +1861,15 @@ z3::check_result Z3Encoder::check(z3::solver &S, unsigned Ms) {
                 : Clock::now() + std::chrono::milliseconds(Ms) + Grace;
     auto Next = Limit;
     while (!CheckFinished) {
-      if (Stopped || interruptRequested() || Clock::now() >= Next) {
+      OverLimit = OverLimit || overMemoryLimit();
+      if (Stopped || OverLimit || interruptRequested() ||
+          Clock::now() >= Next) {
         TimedOut = TimedOut || Clock::now() >= Limit;
         Ctx.interrupt();
         Interrupted = true;
         Next = Clock::now() + Interval;
       }
-      CheckChanged.wait_until(Lock, std::min(Next, Clock::now() + Interval));
+      CheckChanged.wait_until(Lock, std::min(Next, Clock::now() + Poll));
     }
   });
   auto Join = llvm::make_scope_exit([&] {
@@ -1839,8 +1887,11 @@ z3::check_result Z3Encoder::check(z3::solver &S, unsigned Ms) {
       (void)Reset.check();
     }
     Checking = false;
+    if (Result == z3::unknown && (OverLimit || memoryReason(S)))
+      OutOfMemory = true;
   });
-  return S.check();
+  Result = S.check();
+  return Result;
 }
 
 std::optional<z3::expr>
@@ -3804,7 +3855,8 @@ VerifyResult Z3VerifyBackend::verifyModule(const ObligationModule &Module) {
       Result.Status == VerifyStatus::Unresolved &&
       (Result.Reason == VerifyReason::SolverTimeout ||
        Result.Reason == VerifyReason::SolverUnknown ||
-       Result.Reason == VerifyReason::SolverResourceLimit)) {
+       Result.Reason == VerifyReason::SolverResourceLimit ||
+       Result.Reason == VerifyReason::SolverMemoryLimit)) {
     IntegerEncoding = MachineIntegerEncoding::Auto;
     VerifyResult Retry = verifyModuleDirect(Module);
     IntegerEncoding = MachineIntegerEncoding::BitVector;
diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h
index ff1473e81f..7cf3cd9bc5 100644
--- a/clang/lib/Verify/Backend/Z3Encode.h
+++ b/clang/lib/Verify/Backend/Z3Encode.h
@@ -56,9 +56,14 @@ class Z3Encoder {
   /// The first error a Z3 call reported outside a check, which a check
   /// reports itself as unknown. Z3 returns a null term and goes on.
   std::string APIError;
+  /// Z3 ran out of memory here, in a check or another call: its allocations,
+  /// every context's together, reached setZ3MemoryLimit. Later checks return
+  /// unknown at once.
+  bool OutOfMemory = false;
   bool Checking = false;
   static void recordAPIError(Z3_context Context, Z3_error_code Code);
-  /// \p Result, unless a Z3 call failed in this unstopped encoder.
+  /// \p Result, unless a Z3 call failed or ran out of memory in this
+  /// unstopped encoder.
   VerifyResult withAPIError(VerifyResult Result);
   VerifyResult decideModule(const ObligationModule &Module,
                             const LogicExpr *Query,
diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt
index d13eed30f3..654c7235b0 100644
--- a/clang/lib/Verify/CMakeLists.txt
+++ b/clang/lib/Verify/CMakeLists.txt
@@ -24,6 +24,7 @@ get_property(_cppverify_z3_ep GLOBAL PROPERTY CPPVERIFY_Z3_EP_TARGET)
 add_clang_library(clangVerify
   IR/VExpr.cpp
   IR/VStmt.cpp
+  IR/NodeBudget.cpp
   Frontend/ASTConverter.cpp
   Transform/Passivize.cpp
   Transform/Inductive.cpp
diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index a9161a3329..0d75db39dc 100644
--- a/clang/lib/Verify/Driver/Verifier.cpp
+++ b/clang/lib/Verify/Driver/Verifier.cpp
@@ -1077,6 +1077,20 @@ struct VerifyDiagnostic {
   bool Hidden = false;
 };
 
+/// The backend a lowering reports, as lower-only names it.
+static std::string backendName(BackendKind Kind) {
+  return Kind == BackendKind::CVC5        ? "cvc5"
+         : Kind == BackendKind::Portfolio ? "portfolio"
+         : Kind == BackendKind::Race      ? "race"
+                                          : "z3";
+}
+
+static std::string lowerFailure(BackendKind Kind) {
+  return Kind == BackendKind::Z3 || Kind == BackendKind::BMC
+             ? "Z3 lowering failed: "
+             : "backend lowering failed: ";
+}
+
 static std::string backendSuffix(const VerifyResult &Result) {
   std::string Suffix;
   if (!Result.BackendName.empty()) {
@@ -1579,6 +1593,7 @@ class Verifier {
   void checkCalleeRecommendsOnFailure(const VFunction &Caller,
                                       const FunctionMap &FnMap,
                                       VerifyBackend &Backend) {
+    NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes);
     std::vector<const VSpecCallExpr *> Calls;
     collectSpecCallsInFunction(Caller, Calls);
     for (const VSpecCallExpr *C : Calls) {
@@ -1606,7 +1621,7 @@ class Verifier {
       if (PP.ExitAsserts.empty())
         continue;
       PP.CallerIntMode = Caller.IntMode;
-      auto Module = buildObligationModule(PP);
+      auto Module = buildObligationModule(PP, Opts.MaxQueryNodes);
       if (!Module) {
         Diags.push_back({VerifyDiagnostic::Unresolved,
                          "recommends lowering failed for " + Caller.Name +
@@ -1795,12 +1810,15 @@ class Verifier {
       LeanOut = LeanFile.get();
     }
 
+    // Z3 runs in this process, so its limit covers all its queries.
+    setZ3MemoryLimit(Opts.MemoryLimitMB);
     BackendExecutionOptions Execution;
     Execution.SolverTimeoutMs = Opts.SolverTimeoutMs;
     Execution.CollectionTimeoutMs = Opts.CollectionTimeoutMs;
     Execution.CertifyTimeoutMs = Opts.CertifyTimeoutMs;
     Execution.SolverResourceLimit = Opts.SolverResourceLimit;
     Execution.MaxQueryNodes = Opts.MaxQueryNodes;
+    Execution.MemoryLimitMB = Opts.MemoryLimitMB;
     Execution.IntegerEncoding = Opts.IntegerEncoding;
     Execution.SkipWholeModuleRetry = !Opts.LeanFallbackProjectPath.empty();
     Execution.CVC5Path = Opts.CVC5Path;
@@ -1989,6 +2007,29 @@ class Verifier {
                                        R, &In, Label, Kind});
         explainUnsettled(R, In, Checked);
       };
+      // What the function's verification builds is bounded by the node
+      // limit. Past it the function is too large: a verdict, which the
+      // verdicts relying on its contract take into account.
+      NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes);
+      auto tooLarge = [&](const VFunction &In,
+                          const ObligationSizeError &Size) {
+        VerifyResult Limited;
+        Limited.Status = VerifyStatus::Unresolved;
+        Limited.Reason = VerifyReason::QuerySizeLimit;
+        Limited.BackendName = backendName(Opts.Backend);
+        Limited.Message = Size.message();
+        AllOk = false;
+        AnyFailed = true;
+        if (!Opts.LowerOnly && !In.IsProof)
+          FailedCallers.insert(In.Identity);
+        std::string Message =
+            (Opts.LowerOnly ? lowerFailure(Opts.Backend) : std::string()) +
+            In.Name + backendSuffix(Limited) + " (" + Limited.Message + ")";
+        Diags.push_back({Opts.LowerOnly ? VerifyDiagnostic::Error
+                                        : VerifyDiagnostic::Unresolved,
+                         std::move(Message), In.DeclLoc, In.Name,
+                         std::move(Limited)});
+      };
       llvm::raw_string_ostream DumpStream(Run.Dump);
       llvm::raw_ostream *DumpOS = this->DumpOS ? &DumpStream : nullptr;
       std::unique_ptr<VerifyBackend> OwnBackend;
@@ -2021,7 +2062,7 @@ class Verifier {
       Passivizer P;
       P.setFunctionMap(InterfaceMap);
       auto proves = [&](PassiveProgram Smoke) {
-        auto Lowered = buildObligationModule(Smoke);
+        auto Lowered = buildObligationModule(Smoke, Opts.MaxQueryNodes);
         if (!Lowered) {
           llvm::consumeError(Lowered.takeError());
           return false;
@@ -2035,8 +2076,10 @@ class Verifier {
                VerifyStatus::Verified;
       };
       auto unreachable = [&](const PassiveProgram &Program, bool EntryOnly) {
-        auto Lowered = buildObligationModule(smokeProgram(
-            Program, EntryOnly ? 0 : Program.Stmts.size(), falseGoal()));
+        auto Lowered = buildObligationModule(
+            smokeProgram(Program, EntryOnly ? 0 : Program.Stmts.size(),
+                         falseGoal()),
+            Opts.MaxQueryNodes);
         if (!Lowered) {
           llvm::consumeError(Lowered.takeError());
           return false;
@@ -2146,11 +2189,20 @@ class Verifier {
                  SourceLocation(), Fn->Name});
           if (!UBError) {
             SpecInliner Inliner(FnMap, PreparedFn->SpecFuel);
+            NodeBudget Inlining;
             if (isDeductiveBackend(Opts.Backend) ||
                 Opts.Backend == BackendKind::Lean)
               Inliner.prepareFunctionAxiomatic(*PreparedFn);
             else
               Inliner.prepareFunction(*PreparedFn);
+            if (Inlining.exceeded()) {
+              tooLarge(*Fn, ObligationSizeError(
+                                "its specs inlined as deep as their fuel",
+                                Inlining.built(), Inlining.limit(),
+                                "lower the fuel cppverify::reveal_with_fuel "
+                                "gives, or raise the limit"));
+              continue;
+            }
           }
           WorkFn = &*PreparedFn;
           if (!UBError && Opts.Backend == BackendKind::BMC && Opts.LowerOnly) {
@@ -2182,7 +2234,8 @@ class Verifier {
           if (!Missing.empty()) {
             ReadsError = "calls " + Missing +
                          ", which reads the heap without a reads clause";
-          } else if (auto Lowered = buildObligationModule(ReadsPP)) {
+          } else if (auto Lowered =
+                         buildObligationModule(ReadsPP, Opts.MaxQueryNodes)) {
             if (auto Simplified = simplifyObligationModule(std::move(*Lowered)))
               ReadsModule = std::move(*Simplified);
             else
@@ -2280,7 +2333,8 @@ class Verifier {
           std::string PostError;
           if (auto Lowered = buildObligationModule(
                   withClauseProofs(buildSpecPostChecks(*Fn, FnMap), *Fn,
-                                   {VFunction::ClauseProof::Post}, FnMap))) {
+                                   {VFunction::ClauseProof::Post}, FnMap),
+                  Opts.MaxQueryNodes)) {
             if (auto Simplified = simplifyObligationModule(std::move(*Lowered)))
               PostModule = std::move(*Simplified);
             else
@@ -2395,7 +2449,8 @@ class Verifier {
           std::string Error;
           if (auto Lowered = buildObligationModule(
                   withClauseProofs(buildInductionChecks(*Fn, FnMap), *Fn,
-                                   {VFunction::ClauseProof::Post}, FnMap))) {
+                                   {VFunction::ClauseProof::Post}, FnMap),
+                  Opts.MaxQueryNodes)) {
             if (auto Simplified = simplifyObligationModule(std::move(*Lowered)))
               Induction = std::move(*Simplified);
             else
@@ -2495,7 +2550,8 @@ class Verifier {
                                   Kind>{VFunction::ClauseProof::Post,
                                         VFunction::ClauseProof::Decreases},
               FnMap);
-          auto DecModuleOrErr = buildObligationModule(DecPP);
+          auto DecModuleOrErr =
+              buildObligationModule(DecPP, Opts.MaxQueryNodes);
           // A spec's postcondition is proved with its termination.
           const std::string &Shown = Step ? Fn->InductiveStepOf : Fn->Name;
           const bool Quiet = Fn->IsBuiltin || Step;
@@ -2672,7 +2728,8 @@ class Verifier {
             Passivizer BoundPassivizer;
             BoundPassivizer.setFunctionMap(InterfaceMap);
             PassiveProgram BoundProgram = BoundPassivizer.run(*UnrolledFn);
-            auto BoundModuleOrErr = buildObligationModule(BoundProgram);
+            auto BoundModuleOrErr =
+                buildObligationModule(BoundProgram, Opts.MaxQueryNodes);
             if (!BoundModuleOrErr) {
               AllOk = false;
               AnyFailed = true;
@@ -2749,14 +2806,23 @@ class Verifier {
           Module = std::move(*BMCModule);
           Simplification = BMCSimplification;
         } else {
-          auto ModuleOrErr = buildObligationModule(PP);
+          auto ModuleOrErr = buildObligationModule(PP, Opts.MaxQueryNodes);
           if (!ModuleOrErr) {
             AllOk = false;
             AnyFailed = true;
-            Diags.push_back({VerifyDiagnostic::Unresolved,
-                             "obligation lowering failed: " + Fn->Name + " (" +
-                                 llvm::toString(ModuleOrErr.takeError()) +
-                                 ")"});
+            bool Limited = false;
+            llvm::Error Error = llvm::handleErrors(
+                ModuleOrErr.takeError(), [&](const ObligationSizeError &Size) {
+                  tooLarge(*Fn, Size);
+                  Limited = true;
+                });
+            if (Limited)
+              llvm::consumeError(std::move(Error));
+            else
+              Diags.push_back({VerifyDiagnostic::Unresolved,
+                               "obligation lowering failed: " + Fn->Name +
+                                   " (" + llvm::toString(std::move(Error)) +
+                                   ")"});
             continue;
           }
           auto SimplifiedModule = simplifyObligationModule(
@@ -2813,12 +2879,7 @@ class Verifier {
           if (Lowered.Status != VerifyStatus::Lowered) {
             AllOk = false;
             AnyFailed = true;
-            std::string Message =
-                std::string(Opts.Backend == BackendKind::Z3 ||
-                                    Opts.Backend == BackendKind::BMC
-                                ? "Z3"
-                                : "backend") +
-                " lowering failed: " + Fn->Name;
+            std::string Message = lowerFailure(Opts.Backend) + Fn->Name;
             Message += backendSuffix(Lowered);
             if (!Lowered.Message.empty())
               Message += " (" + Lowered.Message + ")";
@@ -2833,11 +2894,7 @@ class Verifier {
         if (Opts.LowerOnly) {
           VerifyResult Result;
           Result.Status = VerifyStatus::Lowered;
-          Result.BackendName = Opts.Backend == BackendKind::CVC5 ? "cvc5"
-                               : Opts.Backend == BackendKind::Portfolio
-                                   ? "portfolio"
-                               : Opts.Backend == BackendKind::Race ? "race"
-                                                                   : "z3";
+          Result.BackendName = backendName(Opts.Backend);
           Diags.push_back({VerifyDiagnostic::Lowered, Fn->Name,
                            SourceLocation(), Fn->Name, std::move(Result)});
           continue;
@@ -2852,7 +2909,8 @@ class Verifier {
           Passivizer Again;
           Again.setFunctionMap(InterfaceMap);
           Again.setUnfoldingDepth(Depth, WithFuel);
-          auto Built = buildObligationModule(Again.run(*WorkFn));
+          auto Built =
+              buildObligationModule(Again.run(*WorkFn), Opts.MaxQueryNodes);
           if (!Built) {
             llvm::consumeError(Built.takeError());
             return false;
@@ -3527,6 +3585,7 @@ class Verifier {
       std::vector<std::optional<VerifyResult>> Outcomes(Confirmations.size());
       std::vector<char> CutShort(Confirmations.size());
       auto confirm = [&](size_t I) {
+        NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes);
         const FunctionRun::Confirmation &Pending = Confirmations[I];
         const VerifyDiagnostic &Verdict = Diags[Pending.Index];
         if (Verdict.K != VerifyDiagnostic::Unresolved ||
diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h
index 7983a7055a..e321091a02 100644
--- a/clang/lib/Verify/Driver/Verifier.h
+++ b/clang/lib/Verify/Driver/Verifier.h
@@ -18,6 +18,13 @@ inline constexpr unsigned DefaultCollectionTimeoutMs =
 /// and their retries, so it legitimately takes several query timeouts.
 inline constexpr unsigned DefaultFunctionTimeoutMs =
     10 * DefaultSolverTimeoutMs;
+/// The expression nodes the proof obligations of one function may take, as
+/// built: building a module takes up to about 450 bytes a node at once, and
+/// the largest of the test suite (the ULEB128 case study's) has 22.6
+/// million.
+inline constexpr uint64_t DefaultMaxQueryNodes = 32000000;
+/// The megabytes Z3's queries may allocate together, and each cvc5 process.
+inline constexpr uint64_t DefaultMemoryLimitMB = 8192;
 
 enum class DiagnosticFormat { Text, Json };
 
@@ -55,8 +62,12 @@ struct VerifyOptions {
   unsigned SolverResourceLimit = 0;
   /// Number of isolated solver jobs. 0 selects available physical cores.
   unsigned Jobs = 1;
-  /// Maximum canonical expression nodes per backend module; 0 disables it.
-  uint64_t MaxQueryNodes = 0;
+  /// Maximum canonical expression nodes per module, checked as it is built
+  /// and before a backend runs it; 0 disables it.
+  uint64_t MaxQueryNodes = DefaultMaxQueryNodes;
+  /// The megabytes Z3's queries may allocate together, and each cvc5
+  /// process; 0 disables the limit.
+  uint64_t MemoryLimitMB = DefaultMemoryLimitMB;
   /// Solver representation of machine integers (Z3, cvc5, portfolio, BMC).
   MachineIntegerEncoding IntegerEncoding = MachineIntegerEncoding::Auto;
   /// Optional cvc5 executable for cvc5 and strict portfolio verification.
diff --git a/clang/lib/Verify/IR/NodeBudget.cpp b/clang/lib/Verify/IR/NodeBudget.cpp
new file mode 100644
index 0000000000..dee0280c01
--- /dev/null
+++ b/clang/lib/Verify/IR/NodeBudget.cpp
@@ -0,0 +1,23 @@
+//===--- NodeBudget.cpp ---------------------------------------------------===//
+#include "NodeBudget.h"
+
+using namespace clang;
+using namespace verify;
+
+thread_local NodeBudget *NodeBudget::Active = nullptr;
+
+static thread_local uint64_t ThreadLimit = 0;
+
+NodeBudget::Limit::Limit(uint64_t Nodes) : Saved(ThreadLimit) {
+  ThreadLimit = Nodes;
+}
+
+NodeBudget::Limit::~Limit() { ThreadLimit = Saved; }
+
+NodeBudget::NodeBudget() : Outer(Active), Max(ThreadLimit) { Active = this; }
+
+NodeBudget::~NodeBudget() {
+  Active = Outer;
+  if (Outer)
+    Outer->Built += Built;
+}
diff --git a/clang/lib/Verify/IR/NodeBudget.h b/clang/lib/Verify/IR/NodeBudget.h
new file mode 100644
index 0000000000..cc6f484d14
--- /dev/null
+++ b/clang/lib/Verify/IR/NodeBudget.h
@@ -0,0 +1,61 @@
+//===--- NodeBudget.h - Bounds on the expression trees built ----*- C++ -*-===//
+#ifndef LLVM_CLANG_VERIFY_IR_NODEBUDGET_H
+#define LLVM_CLANG_VERIFY_IR_NODEBUDGET_H
+
+#include <cstdint>
+
+namespace clang {
+namespace verify {
+
+/// Counts the expression nodes (VExpr and LogicExpr) built on this thread
+/// while it lives, against the limit the driver sets for the function being
+/// verified (--max-query-nodes). A construction whose size can outgrow the
+/// program, such as a spec unfolded as deep as its fuel, runs in a budget
+/// and stops where it can once the limit is passed; its owner then reports
+/// the function as too large and never uses the partial result.
+class NodeBudget {
+public:
+  /// The limit for the budgets of this thread while it lives; 0: none.
+  class Limit {
+  public:
+    explicit Limit(uint64_t Nodes);
+    ~Limit();
+    Limit(const Limit &) = delete;
+    Limit &operator=(const Limit &) = delete;
+
+  private:
+    uint64_t Saved;
+  };
+
+  /// A budget inside another counts toward it too.
+  NodeBudget();
+  ~NodeBudget();
+  NodeBudget(const NodeBudget &) = delete;
+  NodeBudget &operator=(const NodeBudget &) = delete;
+
+  /// The nodes built in this budget and those enclosing it.
+  uint64_t built() const { return Built + (Outer ? Outer->built() : 0); }
+  /// The thread's limit when the budget began, 0 when there is none.
+  uint64_t limit() const { return Max; }
+  bool exceeded() const { return Max != 0 && built() > Max; }
+
+  /// Whether the innermost budget of this thread is exceeded: where a
+  /// construction can stop, it checks this.
+  static bool exhausted() { return Active && Active->exceeded(); }
+  /// Counts one node; the constructors of expression nodes call it.
+  static void count() {
+    if (Active)
+      ++Active->Built;
+  }
+
+private:
+  static thread_local NodeBudget *Active;
+  NodeBudget *Outer;
+  uint64_t Built = 0;
+  uint64_t Max;
+};
+
+} // namespace verify
+} // namespace clang
+
+#endif
diff --git a/clang/lib/Verify/IR/VExpr.h b/clang/lib/Verify/IR/VExpr.h
index e0ace8e494..97de4e4705 100644
--- a/clang/lib/Verify/IR/VExpr.h
+++ b/clang/lib/Verify/IR/VExpr.h
@@ -2,6 +2,7 @@
 #ifndef LLVM_CLANG_VERIFY_IR_VEXPR_H
 #define LLVM_CLANG_VERIFY_IR_VEXPR_H
 
+#include "NodeBudget.h"
 #include "VType.h"
 #include "clang/Basic/SourceLocation.h"
 #include "llvm/ADT/STLFunctionalExtras.h"
@@ -88,7 +89,9 @@ class VExpr {
 
 protected:
   VExpr(Kind K, VType Ty, SourceLocation Loc)
-      : K(K), Ty(Ty), Loc(Loc), EndLoc(Loc) {}
+      : K(K), Ty(Ty), Loc(Loc), EndLoc(Loc) {
+    NodeBudget::count();
+  }
 };
 
 class VLiteralExpr : public VExpr {
diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp
index fcfabb5a96..d983a7b038 100644
--- a/clang/lib/Verify/Transform/Passivize.cpp
+++ b/clang/lib/Verify/Transform/Passivize.cpp
@@ -3073,6 +3073,15 @@ static void addFrameInstances(PassiveProgram &P, const FunctionMap &FnMap) {
   P.Stmts = std::move(Stmts);
 }
 
+PassiveOversize verify::specFactsOversize(const NodeBudget &Budget) {
+  return {"the facts about the specs it applies (at each application, their "
+          "definitions unfolded as deep as their fuel, and their "
+          "postconditions)",
+          Budget.built(), Budget.limit(),
+          "lower the fuel cppverify::reveal_with_fuel gives, or raise the "
+          "limit"};
+}
+
 /// A spec's proved postcondition, and an inductive predicate's unfolding,
 /// hold at every application of it. An inductive predicate is unfolded
 /// \p Depth levels deep, or as deep as reveal_with_fuel asks when \p WithFuel:
@@ -4602,8 +4611,11 @@ class PassivizerImpl {
       for (const auto &Decrease : Fn.Decreases)
         EntryMeasure.push_back(cloneExpr(Decrease.get(), MeasureCtx));
     }
+    NodeBudget Facts;
     addSpecPostInstances(P, FnMap, Fn, UnfoldingDepth, UnfoldingFuel,
                          EntryMeasure);
+    if (Facts.exceeded())
+      P.TooLarge = specFactsOversize(Facts);
     return P;
   }
 
diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h
index b4dcea5c87..10c59f71e8 100644
--- a/clang/lib/Verify/Transform/Passivize.h
+++ b/clang/lib/Verify/Transform/Passivize.h
@@ -73,11 +73,27 @@ struct PassiveModelVariable {
   SourceLocation EndLoc;
 };
 
+/// What a construction for a program built past its function's limit
+/// (NodeBudget), where it stopped: the program is incomplete, and building
+/// its module is an ObligationSizeError with this instead.
+struct PassiveOversize {
+  std::string What;
+  uint64_t Nodes = 0;
+  uint64_t Limit = 0;
+  std::string Advice;
+};
+
+/// The facts about the specs a program applies, each spec's postconditions
+/// and definitions at its applications, passed \p Budget.
+PassiveOversize specFactsOversize(const NodeBudget &Budget);
+
 struct PassiveProgram {
   std::string FunctionName;
   std::string FunctionIdentity;
   std::vector<std::unique_ptr<PassiveStmt>> Stmts;
   std::vector<std::unique_ptr<VExpr>> EntryAssumes;
+  /// Set when a construction for the program passed the node limit.
+  std::optional<PassiveOversize> TooLarge;
   /// How many leading EntryAssumes are the function's own preconditions.
   size_t PreconditionCount = 0;
   /// Each behavior's assumption in the entry state.
diff --git a/clang/lib/Verify/Transform/SpecInline.cpp b/clang/lib/Verify/Transform/SpecInline.cpp
index 9873c6f760..8c7c4b33f1 100644
--- a/clang/lib/Verify/Transform/SpecInline.cpp
+++ b/clang/lib/Verify/Transform/SpecInline.cpp
@@ -193,6 +193,10 @@ class SpecInlinerImpl {
   }
 
   std::unique_ptr<VExpr> inlineSpecCall(const VSpecCallExpr &C) {
+    // Past the function's node limit nothing more is unfolded; the
+    // construction that unfolds reports it.
+    if (NodeBudget::exhausted())
+      return opaqueCall(C);
     if (InlineDepth++ >= MaxInlineDepth)
       return opaqueCall(C);
     struct DepthGuard {
@@ -2804,7 +2808,12 @@ static void addSpecPostChecks(PassiveProgram &P, const VFunction &Fn,
     PS->Cond = cloneAtEntryState(Obligation.get());
     P.Stmts.push_back(std::move(PS));
   }
-  addPostApplicationFacts(P, Fn, FnMap);
+  {
+    NodeBudget Facts;
+    addPostApplicationFacts(P, Fn, FnMap);
+    if (Facts.exceeded())
+      P.TooLarge = specFactsOversize(Facts);
+  }
   if (Collector.Unsupported) {
     auto PS = std::make_unique<PassiveStmt>();
     PS->K = PassiveStmt::Assert;
@@ -3032,6 +3041,8 @@ verify::withClauseProofs(PassiveProgram Check, const VFunction &Spec,
   Passivizer Lowering;
   Lowering.setFunctionMap(FnMap);
   PassiveProgram P = Lowering.run(Proof);
+  if (!P.TooLarge)
+    P.TooLarge = std::move(Check.TooLarge);
   P.AssumedPosts.insert(Check.AssumedPosts.begin(), Check.AssumedPosts.end());
   P.AssumedUnfoldings.insert(Check.AssumedUnfoldings.begin(),
                              Check.AssumedUnfoldings.end());
diff --git a/clang/test/Verify/suite/Inputs/many_checks.py b/clang/test/Verify/suite/Inputs/many_checks.py
new file mode 100644
index 0000000000..b7e54ca0bf
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/many_checks.py
@@ -0,0 +1,13 @@
+# usage: many_checks.py N OUT: a function of N increments, each followed by a
+# check. Each check repeats every assumption before it, so its obligations
+# grow with N squared.
+import sys
+
+n = int(sys.argv[1])
+steps = "".join("  y = y + 1;\n  cppverify::check(y == x + %d);\n" % (i + 1)
+                for i in range(n))
+with open(sys.argv[2], "w") as out:
+    out.write("int many_checks(int x)\n"
+              "  cppverify::pre(0 <= x && x <= 100)\n"
+              "  cppverify::post(cppverify::result == x + %d)\n"
+              "{\n  int y = x;\n%s  return y;\n}\n" % (n, steps))
diff --git a/clang/test/Verify/suite/backend_execution.test b/clang/test/Verify/suite/backend_execution.test
index 8e3e04a054..c851f7330b 100644
--- a/clang/test/Verify/suite/backend_execution.test
+++ b/clang/test/Verify/suite/backend_execution.test
@@ -96,14 +96,12 @@
 # PRUNE-ONCE-SAME: [reason=cache.corrupt]
 
 # NODES: Unresolved: cached_identity [backend=z3] [reason=query.size-limit]
-# NODES-SAME: exceeds query node budget 1
-# NODES-LOWER: error: Z3 lowering failed: cached_identity
-# NODES-LOWER-SAME: [reason=query.size-limit]
-# NODES-LOWER-SAME: exceeds query node budget 1
-# NODES-DUMP: error: Z3 lowering failed: cached_identity
-# NODES-DUMP-SAME: [reason=query.size-limit]
-# NODES-DUMP-SAME: exceeds query node budget 1
-# NODES-REPLAY: Unresolved: cached_identity (canonical obligation module exceeds query node budget 1)
+# NODES-SAME: (the proof obligations would take at least {{[0-9]+}} expression nodes, more than the limit of 1 (--max-query-nodes)
+# NODES-LOWER: error: Z3 lowering failed: cached_identity [backend=z3] [reason=query.size-limit]
+# NODES-LOWER-SAME: more than the limit of 1 (--max-query-nodes)
+# NODES-DUMP: Unresolved: cached_identity [backend=z3] [reason=query.size-limit]
+# NODES-DUMP-SAME: more than the limit of 1 (--max-query-nodes)
+# NODES-REPLAY: Unresolved: cached_identity (the obligation module has {{[0-9]+}} expression nodes, more than the limit of 1 (--max-query-nodes))
 # NODES-REPLAY-SAME: [reason=query.size-limit]
 
 # RLIMIT: Unresolved: cached_identity
diff --git a/clang/test/Verify/suite/backend_options.cpp b/clang/test/Verify/suite/backend_options.cpp
index 7ed4bccc33..f11436609c 100644
--- a/clang/test/Verify/suite/backend_options.cpp
+++ b/clang/test/Verify/suite/backend_options.cpp
@@ -21,8 +21,9 @@
 // RUN: not %cpp-verify --backend=lean --collection-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=COLLECTION
 // RUN: not %cpp-verify --lean-out=%t/budget.lean --certify-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFY
 // RUN: not %cpp-verify --lean-out=%t/budget.lean --solver-rlimit=100000 %s -- 2>&1 | FileCheck %s --check-prefix=RLIMIT
-// RUN: not %cpp-verify --lean-out=%t/budget.lean --max-query-nodes=100000 %s -- 2>&1 | FileCheck %s --check-prefix=NODES
+// RUN: not %cpp-verify --lean-out=%t/budget.lean --memory-limit=4096 %s -- 2>&1 | FileCheck %s --check-prefix=MEMORY
 // RUN: not test -e %t/budget.lean
+// RUN: %cpp-verify --lean-out=%t/nodes.lean --max-query-nodes=100000 %s -- 2>&1 | FileCheck %s --check-prefix=NODES
 // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --lean-out=%t/budget.lean --timeout=1000 2>&1 | FileCheck %s --check-prefix=TIMEOUT
 // RUN: %cpp-verify --timeout=20000 --function-timeout=200000 --solver-rlimit=50000000 --max-query-nodes=1000000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER
 // RUN: %cpp-verify --lean-fallback=%t/fallback --timeout=20000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER
@@ -62,5 +63,6 @@ int count(int n)
 // COLLECTION: error: --collection-timeout requires a backend that runs an SMT solver
 // CERTIFY: error: --certify-timeout requires a backend that runs an SMT solver
 // RLIMIT: error: --solver-rlimit requires a backend that runs an SMT solver
-// NODES: error: --max-query-nodes requires a backend that runs an SMT solver
+// MEMORY: error: --memory-limit requires a backend that runs an SMT solver
+// NODES: Exported: lean obligation: count
 // SOLVER: Verified: count [backend=z3]
diff --git a/clang/test/Verify/suite/cvc5_memory_limit.cpp b/clang/test/Verify/suite/cvc5_memory_limit.cpp
new file mode 100644
index 0000000000..eba3e165cc
--- /dev/null
+++ b/clang/test/Verify/suite/cvc5_memory_limit.cpp
@@ -0,0 +1,16 @@
+// REQUIRES: cvc5, system-linux
+// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=5 %s -- 2>&1 \
+// RUN:   | FileCheck %s
+//
+// Each cvc5 process may allocate --memory-limit megabytes; on Linux that is
+// its data (RLIMIT_DATA). cvc5 needs more than 5 to start solving, so every
+// query runs out, which cvc5 reports as std::bad_alloc or as its SAT solver's
+// OutOfMemoryException.
+
+int small(int x)
+  cppverify::pre(x < 100)
+  cppverify::post(cppverify::result == x + 1)
+{
+  return x + 1;
+}
+// CHECK: Unresolved: small [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 5 MB (--memory-limit))
diff --git a/clang/test/Verify/suite/memory_bounded.test b/clang/test/Verify/suite/memory_bounded.test
new file mode 100644
index 0000000000..a7bf787ca8
--- /dev/null
+++ b/clang/test/Verify/suite/memory_bounded.test
@@ -0,0 +1,18 @@
+# REQUIRES: system-linux
+# UNSUPPORTED: msan, asan, hwasan
+#
+# Within a 3 GB address space, functions whose obligations, or whose specs
+# unfolded as deep as their fuel, would take far more end with a verdict
+# instead of failing an allocation: what is built is counted as it is built
+# (or before, for the obligations) and stops at --max-query-nodes.
+# RUN: rm -rf %t && mkdir -p %t
+# RUN: %python %S/Inputs/many_checks.py 400 %t/many.cpp
+# RUN: ulimit -v 3000000
+# RUN: not %cpp-verify --jobs=1 --max-query-nodes=2000000 %t/many.cpp -- 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=MANY
+# RUN: not %cpp-verify --jobs=1 --max-query-nodes=2000000 \
+# RUN:   %S/obligation_size_limit.cpp -- -DFUEL 2>&1 | FileCheck %s --check-prefix=FUEL
+
+MANY: Unresolved: many_checks [backend=z3] [reason=query.size-limit] (the proof obligations would take at least {{[0-9]+}} expression nodes, more than the limit of 2000000 (--max-query-nodes)
+FUEL: Verified: small [backend=z3]
+FUEL: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies
diff --git a/clang/test/Verify/suite/obligation_size_limit.cpp b/clang/test/Verify/suite/obligation_size_limit.cpp
new file mode 100644
index 0000000000..d35f245c21
--- /dev/null
+++ b/clang/test/Verify/suite/obligation_size_limit.cpp
@@ -0,0 +1,133 @@
+// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 %s -- 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=LIMIT
+// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 \
+// RUN:   --diagnostics-format=json %s -- 2>&1 | FileCheck %s --check-prefix=JSON
+// RUN: not %cpp-verify --lower-only --max-query-nodes=3000 %s -- 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=LOWER
+//
+// The size is exact: at it the obligations are built, one below they are not.
+// RUN: %cpp-verify --jobs=1 --max-query-nodes=24417 %s -- 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=AT
+// RUN: not %cpp-verify --jobs=1 --max-query-nodes=24416 %s -- 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=BELOW
+//
+// A spec unfolded as deep as its fuel stops at the limit: at fuel 40, fibo's
+// unfolding would have about 2^40 copies of its body.
+// RUN: not %cpp-verify --jobs=1 --max-query-nodes=200000 %s -- -DFUEL 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=FUEL
+//
+// The definitions of the specs a module applies count with its obligations:
+// 26167 nodes here, fib's definitions at fuel 4 included.
+// RUN: %cpp-verify --jobs=1 --max-query-nodes=26167 %s -- -DDEFINITIONS 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=DEFINITIONS-AT
+// RUN: not %cpp-verify --jobs=1 --max-query-nodes=26166 %s -- -DDEFINITIONS \
+// RUN:   2>&1 | FileCheck %s --check-prefix=DEFINITIONS
+
+// Each check repeats every assumption before it, so the obligations of a
+// function grow with its checks times the statements before them.
+int steps(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x + 8)
+{
+  int y = x + 1;
+  cppverify::check(y == x + 1);
+  y = y + 1;
+  cppverify::check(y == x + 2);
+  y = y + 1;
+  cppverify::check(y == x + 3);
+  y = y + 1;
+  cppverify::check(y == x + 4);
+  y = y + 1;
+  cppverify::check(y == x + 5);
+  y = y + 1;
+  cppverify::check(y == x + 6);
+  y = y + 1;
+  cppverify::check(y == x + 7);
+  y = y + 1;
+  cppverify::check(y == x + 8);
+  return y;
+}
+// LIMIT: obligation_size_limit.cpp:[[@LINE-22]]:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)
+// JSON: {"backend":"z3","function":"steps","message":"steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)","reason":"query.size-limit","schema":"cppverify.diagnostic/1","severity":"error","source":{"column":5,"end_column":5,"end_line":[[@LINE-23]],"file":"{{.*}}obligation_size_limit.cpp","line":[[@LINE-23]]},"status":"unresolved"}
+// LOWER: obligation_size_limit.cpp:[[@LINE-24]]:5: error: Z3 lowering failed: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000
+// AT: Verified: steps [backend=z3]
+// BELOW: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 24416 (--max-query-nodes)
+
+// Its verdict relies on the contract of steps, which nothing establishes.
+int caller(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x + 9)
+{
+  int y = steps(x);
+  return y + 1;
+}
+// LIMIT: Unresolved: caller [backend=z3] [reason=callee.contract] (relies on the contract of steps, which is not established)
+// JSON: {"backend":"z3","function":"caller","message":"caller [backend=z3] [reason=callee.contract] (relies on the contract of steps, which is not established)","reason":"callee.contract",
+// LOWER: Lowered: caller
+// AT: Verified: caller [backend=z3]
+// BELOW: Unresolved: caller [backend=z3] [reason=callee.contract]
+
+int small(int x)
+  cppverify::pre(x < 100)
+  cppverify::post(cppverify::result == x + 1)
+{
+  return x + 1;
+}
+// LIMIT: Verified: small [backend=z3]
+// LOWER: Lowered: small
+// AT: Verified: small [backend=z3]
+// BELOW: Verified: small [backend=z3]
+
+#ifdef FUEL
+cppverify::spec int fibo(int n)
+  cppverify::decreases(n)
+{
+  return n <= 1 ? n : fibo(n - 1) + fibo(n - 2);
+}
+
+int unfolds(int n)
+  cppverify::pre(n == 3)
+  cppverify::post(cppverify::result == fibo(3))
+{
+  cppverify::ghost { cppverify::reveal_with_fuel(fibo, 40); }
+  return 2;
+}
+#endif
+// FUEL: Verified: steps [backend=z3]
+// FUEL: Verified: spec decreases: fibo
+// FUEL: obligation_size_limit.cpp:[[@LINE-10]]:5: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies (at each application, their definitions unfolded as deep as their fuel, and their postconditions) would take at least {{[0-9]+}} expression nodes, more than the limit of 200000 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, or raise the limit)
+
+#ifdef DEFINITIONS
+cppverify::spec int fib(int n)
+  cppverify::decreases(n)
+{
+  return n <= 1 ? n : fib(n - 1) + fib(n - 2);
+}
+
+int defined(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x + 8 && fib(6) == 8)
+{
+  cppverify::ghost { cppverify::reveal_with_fuel(fib, 4); }
+  int y = x;
+  y = y + 1;
+  cppverify::check(y == x + 1);
+  y = y + 1;
+  cppverify::check(y == x + 2);
+  y = y + 1;
+  cppverify::check(y == x + 3);
+  y = y + 1;
+  cppverify::check(y == x + 4);
+  y = y + 1;
+  cppverify::check(y == x + 5);
+  y = y + 1;
+  cppverify::check(y == x + 6);
+  y = y + 1;
+  cppverify::check(y == x + 7);
+  y = y + 1;
+  cppverify::check(y == x + 8);
+  return y;
+}
+#endif
+// DEFINITIONS-AT: Verified: defined [backend=z3]
+// DEFINITIONS: Unresolved: defined [backend=z3] [reason=query.size-limit] (the proof obligations with the definitions of the specs they apply would take at least 26167 expression nodes, more than the limit of 26166 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, split the function, or raise the limit)
diff --git a/clang/test/Verify/suite/solver_memory_limit.cpp b/clang/test/Verify/suite/solver_memory_limit.cpp
new file mode 100644
index 0000000000..7a52b5ad3a
--- /dev/null
+++ b/clang/test/Verify/suite/solver_memory_limit.cpp
@@ -0,0 +1,36 @@
+// RUN: not %cpp-verify --jobs=1 --timeout=60000 --memory-limit=100 %s -- 2>&1 \
+// RUN:   | FileCheck %s
+// RUN: not %cpp-verify --jobs=1 --timeout=60000 --memory-limit=100 \
+// RUN:   --diagnostics-format=json %s -- 2>&1 | FileCheck %s --check-prefix=JSON
+// RUN: not %cpp-verify --backend=lean --memory-limit=100 %s -- 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=LEAN
+
+// A matching loop: each instance of the quantifier makes a term that matches
+// it again, so Z3's memory grows until something stops the query. Without a
+// memory limit that is the timeout, at 2 GB after 20 s.
+cppverify::spec int g(int n)
+  cppverify::decreases(n)
+{
+  return n <= 0 ? 0 : g(n - 1);
+}
+
+void matching_loop(int a)
+  cppverify::pre(cppverify::forall(k, cppverify::trigger(g(k)) == g(k + 1) + 1))
+{
+  cppverify::ghost { cppverify::hide(g); }
+  cppverify::check(g(a) > 100);
+}
+// CHECK: solver_memory_limit.cpp:[[@LINE-2]]:3: Unresolved: matching_loop [backend=z3] [reason=solver.memory-limit] ({{.*}}: Z3 reached the memory limit: its queries share 100 MB (--memory-limit))
+// JSON: "function":"matching_loop"{{.*}}"reason":"solver.memory-limit"
+
+// The memory of a stopped query is freed, and the next one runs within the
+// limit.
+int small(int x)
+  cppverify::pre(x < 100)
+  cppverify::post(cppverify::result == x + 1)
+{
+  return x + 1;
+}
+// CHECK: Verified: small [backend=z3]
+
+// LEAN: error: --memory-limit requires a backend that runs an SMT solver
diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
index 56e3ebfa58..075ee1425b 100644
--- a/clang/tools/cpp-verify/Main.cpp
+++ b/clang/tools/cpp-verify/Main.cpp
@@ -173,11 +173,17 @@ static unsigned jobs() {
   return 0;
 }
 
-static cl::opt<uint64_t>
-    MaxQueryNodes("max-query-nodes",
-                  cl::desc("Maximum canonical expression nodes per solver "
-                           "module (0 = no limit)"),
-                  cl::init(0), cl::cat(CppVerifyCategory));
+static cl::opt<uint64_t> MaxQueryNodes(
+    "max-query-nodes",
+    cl::desc("Maximum expression nodes of one function's proof obligations, "
+             "checked as they are built (default 32000000; 0 = no limit)"),
+    cl::init(verify::DefaultMaxQueryNodes), cl::cat(CppVerifyCategory));
+
+static cl::opt<uint64_t> MemoryLimit(
+    "memory-limit",
+    cl::desc("Megabytes Z3's queries may allocate together, and each cvc5 "
+             "process (default 8192; 0 = no limit)"),
+    cl::init(verify::DefaultMemoryLimitMB), cl::cat(CppVerifyCategory));
 
 static cl::opt<verify::MachineIntegerEncoding> IntEncoding(
     "int-encoding",
@@ -263,6 +269,7 @@ static verify::BackendExecutionOptions backendExecutionOptions() {
   Options.SolverResourceLimit = SolverResourceLimit;
   Options.Jobs = jobs();
   Options.MaxQueryNodes = MaxQueryNodes;
+  Options.MemoryLimitMB = MemoryLimit;
   Options.IntegerEncoding = IntEncoding;
   Options.CVC5Path = CVC5Path;
   Options.ProofCachePath = ProofCache;
@@ -341,6 +348,7 @@ class VerifyConsumer : public ASTConsumer {
       VOpts.SolverResourceLimit = SolverResourceLimit.getValue();
       VOpts.Jobs = jobs();
       VOpts.MaxQueryNodes = MaxQueryNodes.getValue();
+      VOpts.MemoryLimitMB = MemoryLimit.getValue();
       VOpts.IntegerEncoding = IntEncoding.getValue();
       VOpts.CVC5Path = CVC5Path.getValue();
       VOpts.ProofCachePath = ProofCache.getValue();
@@ -561,7 +569,7 @@ static bool resolveOptions(bool Replay) {
   const cl::Option *SolverOption = nullptr;
   for (const cl::Option *Option : std::initializer_list<const cl::Option *>{
            &SolverTimeout, &CollectionTimeout, &CertifyTimeout,
-           &FunctionTimeout, &SolverResourceLimit, &MaxQueryNodes,
+           &FunctionTimeout, &SolverResourceLimit, &MemoryLimit,
            &IntEncoding})
     if (!SolverOption && given(*Option))
       SolverOption = Option;
@@ -629,6 +637,7 @@ static int replayObligationArchive() {
     return 1;
   }
 
+  verify::setZ3MemoryLimit(MemoryLimit);
   auto Buffer = llvm::MemoryBuffer::getFile(ObligationIn);
   if (!Buffer) {
     llvm::errs() << "error: cannot read obligation archive: "
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index acf48ef64e..927d7d88d8 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -487,6 +487,25 @@ Construction returns `llvm::Expected`. A null, unhandled, malformed, or
 untyped term prevents publication of the module and is reported as `unknown`;
 it is never replaced by `true`.
 
+**Size.** Each obligation's goal is its condition under a negated copy of
+every assumption before it, so a module grows with its obligations times
+the assumptions before them. Its node count, as `obligationModuleNodeCount`
+counts it, is computed from the lowered statements before any goal is built
+(four times the goals' nodes, for the goals, their queries, the complete
+goal, and its query, plus three per obligation less one; an assertion
+checks the count against the built module); over `--max-query-nodes` the
+build returns `ObligationSizeError`. Constructions whose size the program
+does not bound are counted as they go: `NodeBudget` (`IR/NodeBudget.h`)
+counts the `VExpr` and `LogicExpr` nodes built on its thread against the
+limit the driver sets for the function, and the spec inliner unfolds
+nothing more once it is spent. The definitions `SpecAxioms` materializes,
+each spec unfolded as deep as its fuel, are counted level by level into the
+module's count; the facts the passivizer adds at each spec application are
+counted in a budget, and a spent one leaves `PassiveProgram::TooLarge`, which
+makes the build an `ObligationSizeError`; so does a spent budget while specs
+are inlined for BMC. The driver reports the error as the function's verdict,
+`Unresolved` with `query.size-limit`, and never uses the partial result.
+
 Every source-built or replayed module then passes through one fail-closed
 canonicalization step before hashing or backend dispatch. The pass folds only
 sort-preserving Boolean constants, double negation, constant conditionals, and
@@ -1540,7 +1559,19 @@ split; `Certified` still means Lean checked every obligation. SAT
 counterexamples are never fallback successes.
 
 Z3-backed execution accepts explicit timeout, deterministic solver-resource,
-canonical query-node, job-count, and proof-cache budgets. A module that
+canonical query-node, memory, job-count, and proof-cache budgets. Z3 runs in
+the process, so its memory limit is for its queries together: the watchdog
+of every check, which already interrupts it at its time, polls Z3's
+allocation every 10 ms while a limit is set and interrupts the check past
+it, and the encoder's result is then `solver.memory-limit`. Z3's own limits
+are not used: `memory_max_size` fails whichever allocation passes it in any
+context, `Z3_mk_context`'s included, which then returns no context, and the
+high watermark stops a search reporting only `canceled` and frees what it
+took before the check returns. Each cvc5 process gets the limit as its
+`RLIMIT_DATA`, set with `prlimit` once it is spawned (on Windows, the job
+object of `ExecuteNoWait`): a limit makes `ExecuteNoWait` fork rather than
+spawn on POSIX hosts, and fork runs Z3's fork handlers, which wait for the
+timers of every check in the process. A module that
 requires the `sequences` or `collections` feature gets the collection
 timeout (`--collection-timeout`, by default twice `--timeout`) on every
 solver backend. The driver verifies each function as a task (its own backend,
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 249d5bde2a..8798996e7c 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -1708,8 +1708,9 @@ parameter and result signature.
 
 Backend results carry stable machine-readable reason codes independently of
 their human message: `counterexample`, `solver.timeout`, `solver.unknown`,
-`solver.resource-limit`, `solver.unavailable`, `solver.invocation-failed`,
-`solver.malformed-output`, `query.size-limit`, `encoding.failed`,
+`solver.resource-limit`, `solver.memory-limit`, `solver.unavailable`,
+`solver.invocation-failed`, `solver.malformed-output`, `query.size-limit`,
+`encoding.failed`,
 `obligation.invalid`, `logic.unsupported`, `query.missing`,
 `backend.invalid-result`, `backend.inconsistent-results`,
 `bmc.incomplete-bound`, `lean.export-failed`, `cache.corrupt`,
@@ -1734,10 +1735,18 @@ canonical source order, so concurrency cannot choose which failure is public.
 `--function-timeout` (by default ten times `--timeout`) bounds all queries
 of one function together, in wall-clock time; once it is spent no further
 query starts and the function is `Unresolved` (`solver.timeout`). AST/VCR lowering and Lean emission remain serial.
-`--solver-rlimit` adds a deterministic per-query Z3 budget, while
-`--max-query-nodes` rejects an oversized canonical module before
-verification, lower-only encoding, or a requested Z3 dump; neither limit can
-become success.
+`--solver-rlimit` adds a deterministic per-query Z3 budget.
+`--max-query-nodes` (default 32,000,000) bounds the expression nodes built
+for one function: the size of its obligations, each of which repeats every
+assumption before it, is known exactly before they are built, so a function
+over the limit is refused before it takes the memory, and the facts about
+the specs it applies (definitions unfolded as deep as their fuel,
+postconditions at each application) are counted as they are built and stop
+at the limit. `--memory-limit` (default 8192 MB) bounds Z3's queries
+together, which a check's watchdog stops once Z3's allocations pass it, and
+each cvc5 process, whose allocations past it fail. Neither limit can become
+success: a function over the first is `Unresolved` with `query.size-limit`,
+a query stopped by the second with `solver.memory-limit`.
 
 `--proof-cache=DIR` stores only successful individual proofs. The key binds an
 obligation's dependency-scoped semantic hash to hash format v4, the backend
diff --git a/website/scripts/check-doc-examples.py b/website/scripts/check-doc-examples.py
index 2c48ef57d4..39fb855b77 100644
--- a/website/scripts/check-doc-examples.py
+++ b/website/scripts/check-doc-examples.py
@@ -17,7 +17,9 @@
     .. cppverify-example: fails NAME ...   these functions fail with a
                                            counterexample
     .. cppverify-example: unresolved NAME ...
-                                           these stay unresolved
+                                           these stay unresolved; one too
+                                           large to build (query.size-limit)
+                                           fails to lower too
     .. cppverify-example: rejects          the example is an error: cpp-verify
                                            reports one and exits non-zero
 
@@ -47,6 +49,8 @@
     r" (.+?)(?=\s+\[|\s+\(|$)")
 FAILED = re.compile(r"error: (verification failed|spec [\w ]+? failed): "
                     r"(.+?)(?=\s+\[|\s+\(|$)")
+TOO_LARGE = re.compile(r"error: \w+ lowering failed: (\S+) .*"
+                       r"\[reason=query\.size-limit\]")
 LOCATION = re.compile(r"^\S+\.(?:cpp|h):\d+:\d+: ")
 DIAGNOSTIC = re.compile(r"^(?:error|warning): ")
 
@@ -206,7 +210,15 @@ def check(cpp_verify, job):
                     f"\nactual output:\n{output.strip()[:2500]}"), False
         return None
     code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300)
-    if code is None or code != 0 or "error:" in output:
+    # A function refused for its size builds no obligations to lower.
+    refused, errors = set(), []
+    for line in output.splitlines():
+        match = TOO_LARGE.search(line)
+        if match and match.group(1) in unresolved:
+            refused.add(match.group(1))
+        elif "error:" in line:
+            errors.append(line)
+    if code is None or errors or (code != 0 and not refused):
         return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False
     code, output = run(cpp_verify, source,
                        [f"--jobs={SOLVER_JOBS}", *arguments], 900)
diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
index 0b2992dabb..cd0b8e4f95 100644
--- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst
+++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
@@ -66,8 +66,12 @@ Other flags
   others
 - ``cpp-verify --solver-rlimit=N`` — deterministic per-query resource budget
   for Z3 and cvc5 (``0`` disables)
-- ``cpp-verify --max-query-nodes=N`` — refuse a query larger than ``N``
-  expression nodes (``query.size-limit``)
+- ``cpp-verify --max-query-nodes=N`` — the expression nodes the verifier may
+  build for one function: its proof obligations, and the facts about the
+  specs they apply (default 32000000; ``0`` disables; ``query.size-limit``)
+- ``cpp-verify --memory-limit=MB`` — the megabytes the solvers may use, Z3's
+  queries together and each cvc5 process (default 8192; ``0`` disables;
+  ``solver.memory-limit``)
 - ``cpp-verify --jobs=N`` — solver workers shared by all functions (default
   the available physical cores, or ``CPPVERIFY_JOBS``; 1 for ``--backend=lean``)
 - ``cpp-verify --proof-cache=DIR`` — keep proofs of single obligations between
diff --git a/website/source/book/part-ii/ch16-when-verification-fails.rst b/website/source/book/part-ii/ch16-when-verification-fails.rst
index 7db5d0f911..419e1cd4dc 100644
--- a/website/source/book/part-ii/ch16-when-verification-fails.rst
+++ b/website/source/book/part-ii/ch16-when-verification-fails.rst
@@ -30,10 +30,11 @@ are replaced with the Unicode replacement character, so JSON output remains
 valid UTF-8.
 
 An undecided query is different from a counterexample. ``Unresolved`` with
-reason ``solver.timeout``, ``solver.resource-limit``, or ``solver.unknown``
-means Z3 timed out, exhausted an explicit resource/query budget, or entered a
-fragment it could not decide, often because the VC combines quantifiers with
-heap arrays. CppVerify may retry smaller ordered obligations, but if those also
+reason ``solver.timeout``, ``solver.resource-limit``, ``solver.memory-limit``,
+or ``solver.unknown`` means Z3 timed out, exhausted an explicit resource/query
+budget, reached the memory ``--memory-limit`` gives it, or entered a fragment
+it could not decide, often because the VC combines quantifiers with heap
+arrays. CppVerify may retry smaller ordered obligations, but if those also
 remain undecided it reports the function ``Unresolved``. It never treats solver
 uncertainty as success.
 
@@ -156,6 +157,10 @@ Every result that is not a proof carries one stable reason code (text
        other solver of ``--backend=race`` settled the function.
    * - ``solver.resource-limit``
      - ``--solver-rlimit`` was reached.
+   * - ``solver.memory-limit``
+     - A solver reached ``--memory-limit``: Z3's queries, which share it, or
+       a cvc5 process. Raise the limit, run fewer ``--jobs``, or help the
+       proof (a matching loop takes memory until it is stopped).
    * - ``solver.unavailable``
      - The solver (cvc5) is not installed; pass ``--cvc5-path``.
    * - ``solver.invocation-failed``, ``solver.malformed-output``
@@ -170,7 +175,10 @@ Every result that is not a proof carries one stable reason code (text
      - ``BoundedSafe``: safe within ``--unroll`` iterations, but a loop can
        run longer. Raise the bound, or prove the loop with an invariant.
    * - ``query.size-limit``
-     - The query is larger than ``--max-query-nodes``.
+     - The function's proof obligations, or the facts about the specs they
+       apply, would be larger than ``--max-query-nodes``. Split the function
+       into functions with contracts, lower ``cppverify::reveal_with_fuel``,
+       or raise the limit.
    * - ``logic.unsupported``
      - The backend does not support a feature the query needs (Lean and
        collections, for example).
diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst
index 2f5057c7d0..80a0d9586a 100644
--- a/website/source/language/limitations.rst
+++ b/website/source/language/limitations.rst
@@ -135,7 +135,11 @@ C++ feature boundaries
        instantiate, and are ignored with a warning, and one with contract
        statements is reported), variadics, indirect calls, recursion through a
        function that allocates or frees storage, and general link-time
-       summaries.
+       summaries. A function whose proof obligations would take more than
+       ``--max-query-nodes`` expression nodes (32 million by default) is
+       ``Unresolved`` with reason ``query.size-limit``: each check repeats
+       every assumption before it, so a long function with many checks grows
+       fastest. See the memory limits of :doc:`tooling`.
    * - Storage
      - Supported locals, constrained scalar dynamic storage, and inferred
        acyclic fresh-owned scalar factory results.
diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index c0ad318cfc..5c69782e3d 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -23,6 +23,7 @@ Standalone verifier
    cpp-verify --timeout=20000 file.cpp
    cpp-verify --jobs=4 --proof-cache=.cppverify-cache file.cpp
    cpp-verify --solver-rlimit=500000 --max-query-nodes=50000 file.cpp
+   cpp-verify --memory-limit=4096 file.cpp
    cpp-verify --diagnostics-format=json file.cpp
    cpp-verify --dump-ir=1,2,3,4 file.cpp
    cpp-verify --lower-only --dump-ir=1,2,3,4 file.cpp
@@ -173,7 +174,8 @@ Lean export runs no solver, so every solver option is an error with
 ``--backend=lean``, ``--lean-out``, or ``--lean-project``, the same way as
 ``--timeout`` above: ``--timeout``, ``--collection-timeout``,
 ``--certify-timeout``, ``--function-timeout``, ``--solver-rlimit``,
-``--max-query-nodes``, and ``--int-encoding``. ``--lean-fallback`` runs Z3
+``--memory-limit``, and ``--int-encoding``. ``--max-query-nodes`` bounds what
+is built for every backend, Lean's included. ``--lean-fallback`` runs Z3
 first, and accepts all of them.
 
 The same rules hold when replaying an archive: ``--check-ub`` and
@@ -300,11 +302,16 @@ Backends
        cvc5 may report the conservative ``solver.unknown``.
        Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--max-query-nodes=N``
-     - Reject a solver-backed canonical obligation module larger than ``N``
-       expression nodes before verification, lower-only encoding, or a requested
-       Z3 dump (default ``0``, disabled). Exhaustion is fail-closed with reason
-       ``query.size-limit``.
-       Not accepted with ``--backend=lean``, which runs no solver.
+     - The expression nodes the verifier may build for one function (default
+       32000000; ``0`` disables): its proof obligations, counted before they
+       are built, and the facts about the specs they apply, counted as they
+       are built. A function over it is ``Unresolved`` with reason
+       ``query.size-limit``, under every backend. See `Memory limits`_.
+   * - ``--memory-limit=MB``
+     - The megabytes the solvers may use (default 8192; ``0`` disables): Z3's
+       queries together, and each cvc5 process. A query that reaches it is
+       ``Unresolved`` with reason ``solver.memory-limit``. Not accepted with
+       ``--backend=lean``, which runs no solver. See `Memory limits`_.
    * - ``--int-encoding=MODE``
      - Solver representation of machine integers for Z3, cvc5, portfolio, and
        BMC: ``auto`` (default; integers reduced modulo ``2^N`` unless a query
@@ -429,6 +436,159 @@ and the final check. A step that takes longer leaves every result
 ``Unresolved`` with reason ``lean.export-failed``, and its message gives the
 command's error.
 
+Memory limits
+-------------
+
+Two limits bound the memory verification takes:
+
+- ``--max-query-nodes`` bounds what the verifier builds for **one** function
+  (default 32,000,000 expression nodes): its proof obligations, and the facts
+  about the specs they apply. The obligations are counted before they are
+  built, so a function over the limit is refused before it takes the memory;
+  the facts are counted as they are built and stop at the limit.
+- ``--memory-limit`` bounds the solvers (default 8192 MB): Z3's queries
+  together, since Z3 runs inside cpp-verify, and each cvc5 process on its
+  own.
+
+A function that reaches either is ``Unresolved``, never a proof or a
+counterexample, and every function whose proof relies on its contract is
+``Unresolved`` with reason ``callee.contract``. Nothing else changes.
+
+The proof obligations of a function grow faster than its code. Each check is
+proved from everything before it (the preconditions, the statements, and the
+earlier checks), and its obligation repeats all of it, so a function whose
+checks follow many statements takes about their product. With two, four, and
+eight checks like the four below, the obligations take 3,405, 8,505, and
+25,425 nodes. With a limit of 2,000:
+
+.. cppverify-example: flags --max-query-nodes=2000
+.. cppverify-example: unresolved steps
+.. code-block:: cpp
+
+   int steps(int x)
+     cppverify::pre(0 <= x && x <= 100)
+     cppverify::post(cppverify::result == x + 4)
+   {
+     int y = x;
+     y = y + 1;
+     cppverify::check(y == x + 1);
+     y = y + 1;
+     cppverify::check(y == x + 2);
+     y = y + 1;
+     cppverify::check(y == x + 3);
+     y = y + 1;
+     cppverify::check(y == x + 4);
+     return y;
+   }
+
+.. code-block:: text
+
+   steps.cpp:1:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 8505 expression nodes, more than the limit of 2000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)
+
+The count is exact: with ``--max-query-nodes=8505`` the function verifies.
+Under ``--lower-only`` the same is an error, ``Z3 lowering failed: steps``,
+since no obligations were built. A function split into functions with
+contracts keeps each one's obligations small: a call repeats the callee's
+contract, not its body.
+
+The default admits the largest function of the test suite, in the ULEB128
+case study (:doc:`../case-studies/llvm-uleb128`), whose obligations have 22.6
+million nodes. While obligations are built and checked, a node takes about
+400 bytes, so the default lets one function take up to about 13 GB; with more
+than one job, each job builds the obligations of its own function at once.
+
+The facts about the specs a function applies include each spec's definition,
+unfolded as deep as its fuel. A spec that applies itself twice doubles with
+every level: at fuel 40, ``fibo``'s unfolding would have about 2^40 copies of
+its body. Its unfolding stops where it passes the limit, which, at the
+default, takes a few seconds:
+
+.. cppverify-example: flags --max-query-nodes=200000
+.. cppverify-example: unresolved unfolds
+.. code-block:: cpp
+
+   cppverify::spec int fibo(int n)
+     cppverify::decreases(n)
+   {
+     return n <= 1 ? n : fibo(n - 1) + fibo(n - 2);
+   }
+
+   int unfolds(int n)
+     cppverify::pre(n == 3)
+     cppverify::post(cppverify::result == fibo(3))
+   {
+     cppverify::ghost { cppverify::reveal_with_fuel(fibo, 40); }
+     return 2;
+   }
+
+.. code-block:: text
+
+   Verified: spec decreases: fibo
+   fibo.cpp:7:5: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies (at each application, their definitions unfolded as deep as their fuel, and their postconditions) would take at least 228066 expression nodes, more than the limit of 200000 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, or raise the limit)
+
+cpp-verify enforces ``--memory-limit`` while Z3 checks a query: every 10 ms
+it compares what Z3 has allocated, all its queries together, with the limit,
+and stops the query once it is past it. A matching loop, in which every
+instance of a quantifier makes a term that matches it again, takes memory
+until something stops it; without the limit that is the timeout, at 2 GB
+after 20 s:
+
+.. cppverify-example: flags --memory-limit=100 --timeout=60000
+.. cppverify-example: unresolved matching_loop
+.. code-block:: cpp
+
+   cppverify::spec int g(int n)
+     cppverify::decreases(n)
+   {
+     return n <= 0 ? 0 : g(n - 1);
+   }
+
+   void matching_loop(int a)
+     cppverify::pre(cppverify::forall(k, cppverify::trigger(g(k)) == g(k + 1) + 1))
+   {
+     cppverify::ghost { cppverify::hide(g); }
+     cppverify::check(g(a) > 100);
+   }
+
+   int small(int x)
+     cppverify::pre(x < 100)
+     cppverify::post(cppverify::result == x + 1)
+   {
+     return x + 1;
+   }
+
+.. code-block:: text
+
+   Verified: spec decreases: g
+   loop.cpp:11:3: Unresolved: matching_loop [backend=z3] [reason=solver.memory-limit] (proof obligation fn_5f5a31336d61746368696e675f6c6f6f7069::assertion@11:3: Z3 reached the memory limit: its queries share 100 MB (--memory-limit))
+   Verified: small [backend=z3]
+
+The memory of a stopped query is freed, so the next one runs within the
+limit. Since Z3's queries share it, one that passes it stops every query
+running beside it, which, like the time limits on a loaded machine, can leave
+a function ``Unresolved`` that would verify alone; with ``--jobs=1`` a query
+has the limit to itself. Under ``--int-encoding=bitvector`` a query stopped
+for memory is retried in the integer encoding, as after a timeout.
+
+cvc5 runs as a process of its own, which may allocate up to the limit. Past
+it an allocation fails and cvc5 stops (``std::bad_alloc``, or its SAT
+solver's ``OutOfMemoryException``), and the query is ``Unresolved`` with
+reason ``solver.memory-limit``: ``cvc5 ran out of memory: each cvc5 process
+may use N MB (--memory-limit)``. The limit is applied on Linux, to the data
+the process may allocate, and on Windows, to its committed memory; on macOS,
+which applies no such limit to the memory a process maps, cvc5 is not
+bounded. With several jobs, as many cvc5 processes may run at once.
+
+Choosing the limits:
+
+- Interactive use: the defaults. A function over ``--max-query-nodes`` is
+  usually one to split into functions with contracts.
+- A machine with little memory: lower ``--jobs`` first, since each job
+  builds one function's obligations at once, then the two limits.
+- Continuous integration with a memory allowance: give ``--memory-limit``
+  the solvers' share, and ``--max-query-nodes`` the rest divided by
+  ``--jobs`` and by 400 bytes.
+
 Parallel solving and proof caching
 ----------------------------------
 
@@ -516,7 +676,7 @@ the same names, ranges, IDs, and trace data during replay.
 
 Each non-success verification result also carries a stable reason code. Current
 codes include ``counterexample``, ``solver.timeout``, ``solver.unknown``,
-``solver.resource-limit``, ``solver.unavailable``,
+``solver.resource-limit``, ``solver.memory-limit``, ``solver.unavailable``,
 ``solver.invocation-failed``, ``solver.malformed-output``,
 ``query.size-limit``, ``encoding.failed`` (the obligations could not be
 encoded for the solver; when Z3 rejected a call, the message quotes it:
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index d9695f3f7d..4138e9d6c2 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -158,6 +158,17 @@ expression nested more than 256 operations deep is reported where it is
 report something unrelated. The query now ends ``Unresolved`` with reason
 ``encoding.failed`` and Z3's message (:doc:`language/tooling`).
 
+**Memory limits.** Nothing bounded the memory a run took: a function whose
+proof obligations, which repeat every assumption before each check, came to
+hundreds of millions of nodes, or ``cppverify::reveal_with_fuel(fibo, 24)``,
+took tens of gigabytes until the system stopped the run. ``--max-query-nodes``
+now has a default, 32 million expression nodes, and bounds what is built for
+one function before it is built; a function over it is ``Unresolved`` with
+reason ``query.size-limit``, which names what was too large. The new
+``--memory-limit`` (default 8192 MB) bounds Z3's queries together and each
+cvc5 process; a query that reaches it is ``Unresolved`` with reason
+``solver.memory-limit`` (:doc:`language/tooling`).
+
 **Parallel runs.** With more than one job, a function waiting for its own
 queries could run another function's long query, delaying its result and
 spending its ``--function-timeout``. A waiting function now runs only its own
@@ -175,8 +186,8 @@ Data formats
 
 Archives stay ``cppverify.obligation/2`` and JSON diagnostics
 ``cppverify.diagnostic/1``. JSON records may carry the status
-``proved-obligations`` (archive replay) and the reason ``interrupted``
-(Ctrl-C).
+``proved-obligations`` (archive replay) and the reasons ``interrupted``
+(Ctrl-C) and ``solver.memory-limit`` (``--memory-limit``).
 
 0.1.1
 -----