diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp
index c0142054db..ce5eab7a47 100644
--- a/clang/lib/Verify/Backend/VerifyBackend.cpp
+++ b/clang/lib/Verify/Backend/VerifyBackend.cpp
@@ -614,6 +614,9 @@ VerifyResult VerifyBackend::verifyDirect(const ObligationModule &Module) {
   VerifyResult Result = verifyModule(Module);
   if (Result.BackendName.empty())
     Result.BackendName = getName().str();
+  for (VerifyResult &More : Result.MoreFailures)
+    if (More.BackendName.empty())
+      More.BackendName = Result.BackendName;
   if (!Capabilities.ProducesVerificationVerdict &&
       Result.Status != VerifyStatus::Exported &&
       Result.Status != VerifyStatus::Unresolved) {
diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h
index 3a891f5f6e..0dfe816511 100644
--- a/clang/lib/Verify/Backend/VerifyBackend.h
+++ b/clang/lib/Verify/Backend/VerifyBackend.h
@@ -146,6 +146,9 @@ struct VerifyResult {
   std::string Message;
   std::vector<VerifyModelValue> Model;
   std::vector<VerifyTraceEvent> Trace;
+  /// The failing obligations after this one, in order, each with its own
+  /// counterexample, as many as the run's MaxFailures allows.
+  std::vector<VerifyResult> MoreFailures;
   std::string ObligationId;
   std::optional<ObligationKind> ObligationType;
   /// For a certified counterexample: the value of every free variable of the
@@ -287,6 +290,9 @@ struct BackendExecutionOptions {
   /// unresolved. Interactive fallback backends can consume those unresolved
   /// obligations without spending a second whole-module timeout budget.
   bool SkipWholeModuleRetry = false;
+  /// How many failing obligations of a module are reported, each with its
+  /// own counterexample; 0 reports every one.
+  unsigned MaxFailures = 1;
   /// Solve the whole-module query once, at the full budget, and report it:
   /// no per-obligation queries, refinement fallback, or induction. For small
   /// auxiliary questions such as the vacuity checks.
diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp
index e7774fa955..4d1f81fbe7 100644
--- a/clang/lib/Verify/Backend/Z3Encode.cpp
+++ b/clang/lib/Verify/Backend/Z3Encode.cpp
@@ -3595,8 +3595,8 @@ static VerifyResult finishZ3Result(VerifyResult Result) {
 
 std::vector<VerifyResult>
 Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
-                                   bool StopAtFailure, Race *Racing,
-                                   unsigned TimeoutCapMs) {
+                                   std::optional<unsigned> ReportedFailures,
+                                   Race *Racing, unsigned TimeoutCapMs) {
   TimeoutMs =
       budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs));
   if (TimeoutCapMs != 0)
@@ -3626,13 +3626,31 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
   auto IsReused = [&](size_t I) {
     return ReuseVerifiedQueries && VerifiedQueries.count(QueryHashes[I]) != 0;
   };
+  // When failures are reported, each obligation after the first failure is
+  // solved in the executions that pass every earlier one that fails, as
+  // Boogie assumes an assertion after checking it: alone, its counterexample
+  // could start where an earlier check already fails, and fixing that one
+  // would remove it. A check not settled is not assumed, so a proof past
+  // the failures rests on no check that may not hold.
+  const unsigned StopAfterFailures = ReportedFailures.value_or(0);
+  std::vector<size_t> Failing;
+  std::vector<bool> PastEarlier(Module.Obligations.size());
   if (Jobs == 1 || Module.Obligations.size() < 2) {
+    unsigned Failures = 0;
     for (size_t I = 0; I != Module.Obligations.size(); ++I) {
-      Results.push_back(verifyObligation(
-          Module, Module.Obligations[I],
-          Cache ? llvm::StringRef(CacheHashes[I]) : llvm::StringRef(),
-          Cache ? &CacheLookups[I] : nullptr, IsReused(I), Racing));
-      if (StopAtFailure && Results.back().Status == VerifyStatus::Failed)
+      PastEarlier[I] = ReportedFailures && Failures != 0;
+      Results.push_back(
+          PastEarlier[I]
+              ? verifyPastEarlier(Module, I, Failing, Racing)
+              : verifyObligation(Module, Module.Obligations[I],
+                                 Cache ? llvm::StringRef(CacheHashes[I])
+                                       : llvm::StringRef(),
+                                 Cache ? &CacheLookups[I] : nullptr,
+                                 IsReused(I), Racing));
+      if (Results.back().Status != VerifyStatus::Failed)
+        continue;
+      Failing.push_back(I);
+      if (++Failures == StopAfterFailures)
         break;
     }
   } else {
@@ -3656,10 +3674,26 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
     Group.wait();
     for (std::shared_future<VerifyResult> &Future : Futures)
       Results.push_back(Future.get());
+    // A failure after the first is solved again past the earlier checks; a
+    // proof or an unresolved result stays one there.
+    unsigned Failures = 0;
+    for (size_t I = 0;
+         ReportedFailures && I != Results.size() &&
+         (StopAfterFailures == 0 || Failures < StopAfterFailures);
+         ++I) {
+      if (Failures != 0 && Results[I].Status == VerifyStatus::Failed) {
+        PastEarlier[I] = true;
+        Results[I] = verifyPastEarlier(Module, I, Failing, Racing);
+      }
+      if (Results[I].Status == VerifyStatus::Failed) {
+        Failing.push_back(I);
+        ++Failures;
+      }
+    }
   }
   if (ReuseVerifiedQueries)
     for (size_t I = 0; I != Results.size(); ++I)
-      if (Results[I].Status == VerifyStatus::Verified)
+      if (Results[I].Status == VerifyStatus::Verified && !PastEarlier[I])
         VerifiedQueries.insert(QueryHashes[I]);
   return Results;
 }
@@ -3671,7 +3705,8 @@ Z3VerifyBackend::Z3VerifyBackend(const BackendExecutionOptions &Execution,
       SolverTimeoutMs(Execution.SolverTimeoutMs),
       CollectionTimeoutMs(Execution.CollectionTimeoutMs),
       ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs),
-      Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes),
+      MaxFailures(Execution.MaxFailures), Pool(Execution.Pool),
+      MaxQueryNodes(Execution.MaxQueryNodes),
       IntegerEncoding(Execution.IntegerEncoding),
       SkipWholeModuleRetry(Execution.SkipWholeModuleRetry),
       SingleQuery(Execution.SingleQuery),
@@ -3789,6 +3824,18 @@ VerifyResult Z3VerifyBackend::solveQuery(
   return WithFacts;
 }
 
+/// \p Result as the result of obligation \p Item.
+static VerifyResult attributed(VerifyResult Result, const Obligation &Item) {
+  Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
+  Result.ObligationType = Item.Kind;
+  Result.Location = Item.Loc;
+  Result.Source = Item.Source;
+  if (Result.Status == VerifyStatus::Unresolved)
+    Result.Message = "proof obligation " + Result.ObligationId +
+                     (Result.Message.empty() ? "" : ": " + Result.Message);
+  return finishZ3Result(std::move(Result));
+}
+
 VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module,
                                                const Obligation &Item,
                                                llvm::StringRef SemanticHash,
@@ -3836,14 +3883,31 @@ VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module,
     }
   }
 
-  Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
-  Result.ObligationType = Item.Kind;
-  Result.Location = Item.Loc;
-  Result.Source = Item.Source;
-  if (Result.Status == VerifyStatus::Unresolved)
-    Result.Message = "proof obligation " + Result.ObligationId +
-                     (Result.Message.empty() ? "" : ": " + Result.Message);
-  return finishZ3Result(std::move(Result));
+  return attributed(std::move(Result), Item);
+}
+
+VerifyResult
+Z3VerifyBackend::verifyPastEarlier(const ObligationModule &Module, size_t I,
+                                   const std::vector<size_t> &Earlier,
+                                   Race *Racing) {
+  const Obligation &Item = Module.Obligations[I];
+  auto Query = cloneLogicExpr(Item.CounterexampleQuery.get());
+  for (size_t J : Earlier) {
+    auto Conjunction = std::make_unique<LogicExpr>(LogicExpr::And);
+    Conjunction->Sort = LogicSort::boolSort();
+    Conjunction->Loc = Query->Loc;
+    Conjunction->EndLoc = Query->EndLoc;
+    Conjunction->Source = Query->Source;
+    Conjunction->Children.push_back(std::move(Query));
+    Conjunction->Children.push_back(
+        cloneLogicExpr(Module.Obligations[J].Goal.get()));
+    Query = std::move(Conjunction);
+  }
+  return attributed(spent() ? timeSpent()
+                            : solveQuery(Module, Query.get(),
+                                         Item.TraceEventCount,
+                                         budget(TimeoutMs), Racing),
+                    Item);
 }
 
 /// Internal IDs of the obligations that one-to-one Results did not prove.
@@ -3859,6 +3923,17 @@ unprovedObligations(const ObligationModule &Module,
   return Unproved;
 }
 
+VerifyResult
+Z3VerifyBackend::withMoreFailures(std::vector<VerifyResult> &Results,
+                                  size_t First) {
+  VerifyResult Reported = std::move(Results[First]);
+  for (size_t I = First + 1; I != Results.size(); ++I)
+    if (Results[I].Status == VerifyStatus::Failed &&
+        (MaxFailures == 0 || Reported.MoreFailures.size() + 1 < MaxFailures))
+      Reported.MoreFailures.push_back(std::move(Results[I]));
+  return Reported;
+}
+
 VerifyResult Z3VerifyBackend::verifyModule(const ObligationModule &Module) {
   TimeoutMs =
       budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs));
@@ -4014,7 +4089,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
     Group.emplace(*Pool);
     Ordered = Group->async([this, &Module, &Rivals, &WholeRace] {
       std::vector<VerifyResult> Results =
-          verifyObligations(Module, /*StopAtFailure=*/true, &Rivals);
+          verifyObligations(Module, MaxFailures, &Rivals);
       // The obligations settle the module when they prove all of it or one
       // fails, and the whole query, or its retry, is then stopped.
       if (llvm::any_of(Results,
@@ -4070,8 +4145,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
   if (Whole.Status == VerifyStatus::Verified)
     return finishZ3Result(std::move(Whole));
   auto orderedResults = [&] {
-    return Racing ? Ordered.get()
-                  : verifyObligations(Module, /*StopAtFailure=*/true);
+    return Racing ? Ordered.get() : verifyObligations(Module, MaxFailures);
   };
 
   if (Whole.Status == VerifyStatus::Failed) {
@@ -4084,18 +4158,18 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
       TimeoutMs = FullTimeout;
       UnitsCap = 0;
     });
-    std::vector<VerifyResult> Results = verifyObligations(
-        Module, /*StopAtFailure=*/true, nullptr, WholeTimeout);
+    std::vector<VerifyResult> Results =
+        verifyObligations(Module, MaxFailures, nullptr, WholeTimeout);
     bool SawUnresolved = false;
-    for (VerifyResult &Result : Results) {
-      if (Result.Status == VerifyStatus::Verified)
+    for (size_t I = 0; I != Results.size(); ++I) {
+      if (Results[I].Status == VerifyStatus::Verified)
         continue;
-      if (Result.Status == VerifyStatus::Unresolved) {
+      if (Results[I].Status == VerifyStatus::Unresolved) {
         SawUnresolved = true;
         continue;
       }
-      if (Result.Status == VerifyStatus::Failed)
-        return std::move(Result);
+      if (Results[I].Status == VerifyStatus::Failed)
+        return withMoreFailures(Results, I);
     }
     if (SawUnresolved)
       return finishZ3Result(std::move(Whole));
@@ -4122,13 +4196,16 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
   std::optional<std::vector<std::string>> Unproved =
       unprovedObligations(Module, Results);
   std::optional<VerifyResult> FirstUnresolved;
-  for (VerifyResult &Result : Results) {
+  for (size_t I = 0; I != Results.size(); ++I) {
+    VerifyResult &Result = Results[I];
     if (Result.Status != VerifyStatus::Verified) {
       if (Result.Status == VerifyStatus::Unresolved) {
         if (!FirstUnresolved)
           FirstUnresolved = std::move(Result);
         continue;
       }
+      if (Result.Status == VerifyStatus::Failed)
+        return withMoreFailures(Results, I);
       return std::move(Result);
     }
   }
diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h
index 4cdbac49bb..cfc3bdb5a5 100644
--- a/clang/lib/Verify/Backend/Z3Encode.h
+++ b/clang/lib/Verify/Backend/Z3Encode.h
@@ -333,6 +333,8 @@ class Z3VerifyBackend : public VerifyBackend {
   /// of their queries may do: the work the complete query's probe had, or 0.
   unsigned UnitsCap = 0;
   unsigned Jobs;
+  /// How many failing obligations a module reports; 0: every one.
+  unsigned MaxFailures;
   llvm::StdThreadPool *Pool;
   uint64_t MaxQueryNodes;
   MachineIntegerEncoding IntegerEncoding;
@@ -345,6 +347,10 @@ class Z3VerifyBackend : public VerifyBackend {
 
   std::optional<std::chrono::steady_clock::time_point> Deadline;
   unsigned budget(unsigned Ms) const { return withinDeadline(Ms, Deadline); }
+  /// The failure at First of the results of verifyObligations, carrying the
+  /// failures after it, as many as MaxFailures allows.
+  VerifyResult withMoreFailures(std::vector<VerifyResult> &Results,
+                                size_t First);
   /// The function's time is spent, so no further query starts.
   bool spent() const {
     return Cancellation.Cancelled ||
@@ -381,6 +387,12 @@ class Z3VerifyBackend : public VerifyBackend {
                                 llvm::StringRef SemanticHash = {},
                                 const ProofCacheLookup *Lookup = nullptr,
                                 bool Reused = false, Race *Racing = nullptr);
+  /// Obligation \p I of \p Module in the executions that pass every one of
+  /// \p Earlier, failing obligations before it. No cache holds it, since it
+  /// asks less than the obligation.
+  VerifyResult verifyPastEarlier(const ObligationModule &Module, size_t I,
+                                 const std::vector<size_t> &Earlier,
+                                 Race *Racing);
 
 public:
   explicit Z3VerifyBackend(const BackendExecutionOptions &Execution = {},
@@ -390,13 +402,15 @@ class Z3VerifyBackend : public VerifyBackend {
   BackendCapabilities getCapabilities() const override {
     return {allLogicFeatures(), true};
   }
-  /// One result per obligation in order. With StopAtFailure a serial run ends
-  /// after the first failure, since later results cannot change it. A nonzero
-  /// TimeoutCapMs bounds every query's timeout.
-  std::vector<VerifyResult> verifyObligations(const ObligationModule &Module,
-                                              bool StopAtFailure = false,
-                                              Race *Racing = nullptr,
-                                              unsigned TimeoutCapMs = 0);
+  /// One result per obligation in order, each solved alone. With
+  /// ReportedFailures, a serial run ends after that many failures (0: never),
+  /// since later results are not reported, and each obligation after the
+  /// first failure is solved in the executions that pass every earlier one
+  /// that fails. A nonzero TimeoutCapMs bounds every query's timeout.
+  std::vector<VerifyResult>
+  verifyObligations(const ObligationModule &Module,
+                    std::optional<unsigned> ReportedFailures = std::nullopt,
+                    Race *Racing = nullptr, unsigned TimeoutCapMs = 0);
   void cancel() override { Cancellation.cancel(); }
   void resume() override { Cancellation.reset(); }
   std::optional<unsigned>
diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index 8967072384..20d81c54db 100644
--- a/clang/lib/Verify/Driver/Verifier.cpp
+++ b/clang/lib/Verify/Driver/Verifier.cpp
@@ -13,6 +13,7 @@
 #include "../Backend/ProofCache.h"
 #include "../Backend/SpecAxioms.h"
 #include "../Backend/TaskGroup.h"
+#include "../Backend/Z3Encode.h"
 #include "../Frontend/ASTConverter.h"
 #include "../IR/VStmt.h"
 #include "../Transform/LoopUnroll.h"
@@ -37,6 +38,7 @@
 #include "llvm/Support/Error.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/FormatVariadic.h"
+#include "llvm/Support/GlobPattern.h"
 #include "llvm/Support/JSON.h"
 #include "llvm/Support/MD5.h"
 #include "llvm/Support/MathExtras.h"
@@ -1101,6 +1103,11 @@ struct VerifyDiagnostic {
   SourceRange Span;
   /// A spec function that needs no check, listed with --verbose: no verdict.
   bool Axiom = false;
+  /// What else the verifier found about the verdict, each printed as a note.
+  std::vector<std::string> Notes;
+  /// A failing obligation after the one a function's verdict reports: no
+  /// verdict of its own.
+  bool Additional = false;
 };
 
 /// The backend a lowering reports, as lower-only names it.
@@ -3133,6 +3140,24 @@ class Verifier {
     // the function is Unresolved, its first error carrying the verdict, and
     // the rest of the translation unit is verified. An error outside every
     // function stops the run.
+    // --function: the functions the run reports, by their names.
+    std::vector<llvm::GlobPattern> Patterns;
+    for (const std::string &Text : Opts.FunctionPatterns) {
+      auto Pattern = llvm::GlobPattern::create(Text);
+      if (!Pattern) {
+        Diags.push_back(
+            {VerifyDiagnostic::Error, "--function=" + Text + ": " +
+                                          llvm::toString(Pattern.takeError())});
+        return false;
+      }
+      Patterns.push_back(std::move(*Pattern));
+    }
+    auto selects = [&](llvm::StringRef Name) {
+      return Patterns.empty() ||
+             llvm::any_of(Patterns, [&](const llvm::GlobPattern &Pattern) {
+               return Pattern.match(Name);
+             });
+    };
     bool OutsideFunctions = false;
     std::map<std::string, std::string> UnsupportedConstructs;
     for (const ConversionError &Err : Converter.getErrors()) {
@@ -3143,6 +3168,7 @@ class Verifier {
         OutsideFunctions = true;
       else
         D.FunctionName = Err.FunctionName;
+      D.Hidden = !Err.Function.empty() && !selects(Err.FunctionName);
       if (!Err.Function.empty() &&
           UnsupportedConstructs.emplace(Err.Function, Err.Message).second) {
         VerifyResult R;
@@ -3168,10 +3194,37 @@ class Verifier {
           {VerifyDiagnostic::Warning, "no verifiable functions found"});
       return true;
     }
+    // A function is selected by the name its verdicts print, which for an
+    // inductive predicate's step is the predicate's; the predicate's rule
+    // proofs are reported with it.
+    std::vector<bool> Selected(Functions.size());
+    for (size_t I = 0; I != Functions.size(); ++I) {
+      const VFunction &Fn = *Functions[I];
+      Selected[I] =
+          selects(Fn.InductiveStepOf.empty() ? Fn.Name : Fn.InductiveStepOf);
+    }
+    std::set<std::string> SelectedIdentities;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      if (Selected[I])
+        SelectedIdentities.insert(Functions[I]->Identity);
+    for (size_t I = 0; I != Functions.size(); ++I)
+      Selected[I] = Selected[I] ||
+                    SelectedIdentities.count(Functions[I]->InductiveRuleOf);
+    if (!Patterns.empty() &&
+        llvm::none_of(Selected, [](bool S) { return S; }) &&
+        llvm::none_of(Converter.getErrors(), [&](const ConversionError &Err) {
+          return !Err.Function.empty() && selects(Err.FunctionName);
+        })) {
+      Diags.push_back({VerifyDiagnostic::Error,
+                       "no function matches --function=" +
+                           llvm::join(Opts.FunctionPatterns, ", --function=")});
+      return false;
+    }
     if (Opts.ListFunctions) {
-      for (const auto &Fn : Functions) {
+      for (size_t I = 0; I != Functions.size(); ++I) {
+        const auto &Fn = Functions[I];
         if (Fn->IsBuiltin || Fn->IsChoice || !Fn->InductiveStepOf.empty() ||
-            !Fn->InductiveRuleOf.empty())
+            !Fn->InductiveRuleOf.empty() || !Selected[I])
           continue;
         const char *Kind = Fn->IsConstexprSpec ? "constexpr spec"
                            : Fn->IsSpec        ? "spec"
@@ -3250,6 +3303,7 @@ class Verifier {
     Execution.MemoryLimitMB = Opts.MemoryLimitMB;
     Execution.IntegerEncoding = Opts.IntegerEncoding;
     Execution.SkipWholeModuleRetry = !Opts.LeanFallbackProjectPath.empty();
+    Execution.MaxFailures = Opts.MaxFailures;
     Execution.CVC5Path = Opts.CVC5Path;
     Execution.ProfileQuantifiers = Opts.ProfileQuantifiers;
     Execution.ProofCachePath = Opts.ProofCachePath;
@@ -3502,6 +3556,166 @@ class Verifier {
       }
       auto SmokeBackend = createVerifyBackend(BackendKind::Z3, nullptr, 0,
                                               SmokeExecution, nullptr);
+      // What else a failure shows. A counterexample that passes through a
+      // loop starts from any state the loop's invariants allow, which no
+      // execution need reach; unrolling the loops looks for an execution
+      // that fails, or proves that none does.
+      auto failureNotes = [&](const VFunction &F, const VerifyResult &Failure) {
+        std::vector<std::string> Notes;
+        auto at = [&](SourceLocation Loc) {
+          const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc(Loc);
+          return Where.isValid() ? std::to_string(Where.getLine()) + ":" +
+                                       std::to_string(Where.getColumn())
+                                 : std::string("?");
+        };
+        if (F.UnmeasuredLoop.isValid())
+          Notes.push_back("the loop at " + at(F.UnmeasuredLoop) +
+                          " has no cppverify::decreases: a proof would be "
+                          "Unresolved (decreases.missing) until it has one");
+        const auto Loop = llvm::find_if(Failure.Trace, [](const auto &Event) {
+          return Event.Kind == DiagnosticTraceKind::Loop &&
+                 Event.Active.value_or(false);
+        });
+        if (Loop == Failure.Trace.end() || !isDeductiveBackend(Opts.Backend) ||
+            Failure.Reason != VerifyReason::Counterexample)
+          return Notes;
+        Notes.push_back(
+            "the counterexample's state at the loop at " +
+            (Loop->Source.isValid() ? std::to_string(Loop->Source.Line) + ":" +
+                                          std::to_string(Loop->Source.Column)
+                                    : std::string("?")) +
+            " is any state its invariants allow, not necessarily one an "
+            "execution reaches");
+        if (Opts.ConfirmBound == 0 || !Failure.ObligationType)
+          return Notes;
+        VFunction Bounded = cloneVFunction(F);
+        annotatePointerOrigins(Bounded);
+        if (Opts.CheckUB && !F.TotalExpressions && instrumentUBChecks(Bounded))
+          return Notes;
+        SpecInliner(FnMap, Bounded.SpecFuel).prepareFunction(Bounded);
+        // The search after a failure takes at most one query's time.
+        Z3VerifyBackend Unroller(Execution, "bmc");
+        std::optional<std::chrono::steady_clock::time_point> Until = Deadline;
+        if (Opts.SolverTimeoutMs != 0) {
+          const auto Slice = std::chrono::steady_clock::now() +
+                             std::chrono::milliseconds(Opts.SolverTimeoutMs);
+          if (!Until || Slice < *Until)
+            Until = Slice;
+        }
+        Unroller.setDeadline(Until);
+        auto iterations = [](unsigned Bound) {
+          return std::to_string(Bound) +
+                 (Bound == 1 ? " iteration" : " iterations");
+        };
+        // Unrolling keeps the function's checks, each copied into every
+        // iteration it is in, but not the loops' invariants and measures:
+        // the copies of the failed check are those of its kind at its place.
+        auto copyOfFailure = [&](const VerifyResult &Result) {
+          return Result.ObligationType == Failure.ObligationType &&
+                 Result.Source.Line == Failure.Source.Line &&
+                 Result.Source.Column == Failure.Source.Column &&
+                 Result.Source.File == Failure.Source.File;
+        };
+        bool Unrolled = false;
+        std::string Earlier;
+        for (unsigned Bound = 0; Bound <= Opts.ConfirmBound; ++Bound) {
+          VFunction Copy = LoopUnroller::unroll(Bounded, Bound);
+          Passivizer Unrolling;
+          Unrolling.setFunctionMap(InterfaceMap);
+          auto Lowered = buildObligationModule(Unrolling.run(Copy));
+          if (!Lowered) {
+            llvm::consumeError(Lowered.takeError());
+            return Notes;
+          }
+          auto Simplified = simplifyObligationModule(std::move(*Lowered));
+          if (!Simplified) {
+            llvm::consumeError(Simplified.takeError());
+            return Notes;
+          }
+          ObligationModule Module = std::move(*Simplified);
+          Module.BMCTransform = BMCTransformProvenance{Bound};
+          annotateObligationSources(Module);
+          bool Copies = false;
+          bool CopiesHold = true;
+          bool Unwound = true;
+          // Every failure is reported, so a copy, or a loop's unwinding, is
+          // solved in the executions that pass the failing checks before it:
+          // one that fails an earlier check never reaches it. What holds
+          // past another check that fails says so.
+          std::vector<VerifyResult> Results =
+              Unroller.verifyObligations(Module, /*ReportedFailures=*/0);
+          size_t Last = 0;
+          for (size_t I = 0; I != Results.size(); ++I)
+            if (Results[I].ObligationType == ObligationKind::Unwinding ||
+                copyOfFailure(Results[I]))
+              Last = I;
+          Earlier.clear();
+          for (size_t I = 0; I != Last && Earlier.empty(); ++I)
+            if (Results[I].Status == VerifyStatus::Failed &&
+                Results[I].ObligationType &&
+                Results[I].ObligationType != ObligationKind::Unwinding &&
+                !copyOfFailure(Results[I]))
+              Earlier = std::string(" (the ") +
+                        obligationKindName(*Results[I].ObligationType) +
+                        " check at " + std::to_string(Results[I].Source.Line) +
+                        ":" + std::to_string(Results[I].Source.Column) +
+                        " fails)";
+          for (VerifyResult &Result : Results) {
+            if (Result.ObligationType == ObligationKind::Unwinding) {
+              Unwound &= Result.Status == VerifyStatus::Verified;
+              continue;
+            }
+            if (!copyOfFailure(Result))
+              continue;
+            Copies = true;
+            if (Result.Status == VerifyStatus::Failed &&
+                Result.Reason == VerifyReason::Counterexample) {
+              Notes.push_back(
+                  "an execution fails this check " +
+                  (Bound == 0
+                       ? std::string("with no iteration of any loop")
+                       : "within " + iterations(Bound) + " of each loop") +
+                  (Result.Message.empty()
+                       ? std::string()
+                       : " (counterexample: " + Result.Message + ")"));
+              return Notes;
+            }
+            CopiesHold &= Result.Status == VerifyStatus::Verified;
+          }
+          Unrolled |= Copies;
+          // Unrolled once, every loop body holds a copy of each of its
+          // checks, and a check after a loop has one from no iteration on;
+          // a failure without a copy by then is of an invariant or a
+          // measure, which unrolling drops at every bound.
+          if (Bound >= 1 && !Unrolled)
+            return Notes;
+          if (!CopiesHold)
+            return Notes;
+          if (Copies && Unwound) {
+            Notes.push_back(
+                Earlier.empty()
+                    ? "no execution fails this check: every loop ends within " +
+                          iterations(Bound) +
+                          ", and unrolling proves it there; the loops' "
+                          "invariants are too weak for an unbounded proof"
+                    : "no execution fails this check without failing an "
+                      "earlier one first" +
+                          Earlier +
+                          ": those that pass the checks before it end every "
+                          "loop within " +
+                          iterations(Bound) + ", and unrolling proves it there");
+            return Notes;
+          }
+        }
+        if (Unrolled)
+          Notes.push_back("no execution fails this check within " +
+                          iterations(Opts.ConfirmBound) + " of each loop" +
+                          (Earlier.empty()
+                               ? std::string()
+                               : " without failing an earlier one first" +
+                                     Earlier));
+        return Notes;
+      };
       Passivizer P;
       P.setFunctionMap(InterfaceMap);
       auto proves = [&](PassiveProgram Smoke) {
@@ -4712,14 +4926,24 @@ class Verifier {
                   Module, *Item, *R.Assignment, LeanModules.Specs, Pending.Why);
             Run.Refutations.push_back(std::move(Pending));
           }
-          std::string Msg = "verification failed: " + Fn->Name;
-          if (!R.ObligationId.empty())
-            Msg += " [" + R.ObligationId + "]";
-          if (!R.Message.empty())
-            Msg += " (counterexample: " + R.Message + ")";
-          Msg += backendSuffix(R);
-          Diags.push_back(
-              {VerifyDiagnostic::Error, Msg, R.Location, Fn->Name, R});
+          // The failure, and those after it --max-failures reports, each
+          // with its counterexample and notes.
+          auto failure = [&](const VerifyResult &Failure) {
+            std::string Msg = "verification failed: " + Fn->Name;
+            if (!Failure.ObligationId.empty())
+              Msg += " [" + Failure.ObligationId + "]";
+            if (!Failure.Message.empty())
+              Msg += " (counterexample: " + Failure.Message + ")";
+            Msg += backendSuffix(Failure);
+            Diags.push_back({VerifyDiagnostic::Error, Msg, Failure.Location,
+                             Fn->Name, Failure});
+            Diags.back().Notes = failureNotes(*Fn, Failure);
+          };
+          failure(R);
+          for (const VerifyResult &More : R.MoreFailures) {
+            failure(More);
+            Diags.back().Additional = true;
+          }
         } else {
           const bool FallbackExported = R.Status == VerifyStatus::Unresolved &&
                                         exportLeanFallback(Module, Fn->Name, R);
@@ -4740,14 +4964,51 @@ class Verifier {
       }
       DumpStream.flush();
     };
-    if (Parallel) {
-      TaskGroup Group(*Pool);
-      for (size_t I = 0; I != Functions.size(); ++I)
-        Group.async([&verifyFunction, I] { verifyFunction(I); });
-      Group.wait();
-    } else {
+    // With --function, the executable functions run are the selected ones
+    // and, round by round, those whose contracts a verdict of the run relies
+    // on; specs, proof functions, and generated checks always run, since any
+    // verdict may rest on their facts. Every verdict reported is then the
+    // one a run of the whole file gives.
+    std::vector<bool> Scheduled(Functions.size(), true);
+    if (!Opts.FunctionPatterns.empty())
       for (size_t I = 0; I != Functions.size(); ++I)
-        verifyFunction(I);
+        Scheduled[I] =
+            Selected[I] || Functions[I]->IsSpec || Functions[I]->IsProof;
+    std::map<std::string, size_t> IndexOf;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      IndexOf.emplace(Functions[I]->Identity, I);
+    std::vector<size_t> Batch;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      if (Scheduled[I])
+        Batch.push_back(I);
+    while (!Batch.empty()) {
+      if (Parallel) {
+        TaskGroup Group(*Pool);
+        for (size_t I : Batch)
+          Group.async([&verifyFunction, I] { verifyFunction(I); });
+        Group.wait();
+      } else {
+        for (size_t I : Batch)
+          verifyFunction(I);
+      }
+      std::vector<size_t> Next;
+      auto need = [&](const std::string &Identity) {
+        auto It = IndexOf.find(Identity);
+        if (It != IndexOf.end() && !Scheduled[It->second]) {
+          Scheduled[It->second] = true;
+          Next.push_back(It->second);
+        }
+      };
+      for (size_t I : Batch) {
+        for (const auto &[Index, Identity, Callees] : Runs[I].CallDependencies)
+          for (const std::string &Callee : Callees)
+            need(Callee);
+        for (const SpecReliance &Reliance : Runs[I].ProofDependencies)
+          for (const std::string &Callee : Reliance.Callees)
+            need(Callee);
+      }
+      llvm::sort(Next);
+      Batch = std::move(Next);
     }
     // A function whose verification Ctrl-C cut short is reported by one
     // line. Its verdicts stay, hidden, for what they establish: a query the
@@ -4778,6 +5039,9 @@ class Verifier {
       for (VerifyDiagnostic &D : Run.Diags) {
         if (D.FindingOf)
           *D.FindingOf += Base;
+        // What a function --function leaves out reports stays, hidden, for
+        // what it establishes.
+        D.Hidden |= !Selected[I];
         Diags.push_back(std::move(D));
       }
       AllOk &= Run.AllOk;
@@ -5636,6 +5900,14 @@ class Verifier {
       }
     }
 
+    // A run --function narrows succeeds when what it reports does.
+    if (!Opts.FunctionPatterns.empty())
+      return llvm::none_of(Diags, [](const VerifyDiagnostic &D) {
+        return !D.Hidden && (D.K == VerifyDiagnostic::Error ||
+                             D.K == VerifyDiagnostic::Unresolved ||
+                             D.K == VerifyDiagnostic::Interrupted ||
+                             D.K == VerifyDiagnostic::BoundedSafe);
+      });
     return AllOk;
   }
 
@@ -5654,6 +5926,12 @@ class Verifier {
             ? "error"
             : "note";
     Record["message"] = jsonText(D.Message);
+    if (!D.Notes.empty()) {
+      llvm::json::Array Notes;
+      for (const std::string &Note : D.Notes)
+        Notes.push_back(jsonText(Note));
+      Record["notes"] = std::move(Notes);
+    }
     if (!D.FunctionName.empty())
       Record["function"] = jsonText(D.FunctionName);
 
@@ -5853,7 +6131,7 @@ class Verifier {
   /// verdict only when it carries one, as the first error of a function the
   /// verifier does not represent does.
   static void count(const VerifyDiagnostic &D, VerifySummary &Summary) {
-    if (D.Axiom)
+    if (D.Axiom || D.Additional)
       return;
     switch (D.K) {
     case VerifyDiagnostic::Verified:
@@ -6000,6 +6278,8 @@ class Verifier {
              << PLoc.getColumn() << ": ";
         OS << "note: " << InstantiationNote << "\n";
       }
+      for (const std::string &Note : D.Notes)
+        OS << "note: " << Note << "\n";
     }
   }
 };
diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h
index 258d13892b..ddba569f37 100644
--- a/clang/lib/Verify/Driver/Verifier.h
+++ b/clang/lib/Verify/Driver/Verifier.h
@@ -120,6 +120,16 @@ struct VerifyOptions {
   bool Verbose = false;
   /// List the functions the run would verify, and verify none.
   bool ListFunctions = false;
+  /// How many failing obligations of a function are reported, each with its
+  /// own counterexample (Z3 only); 0 reports every one.
+  unsigned MaxFailures = 1;
+  /// Glob patterns over function names: only the functions they match are
+  /// reported. Empty: every function.
+  std::vector<std::string> FunctionPatterns;
+  /// For a failure whose counterexample passes through a loop, the most
+  /// iterations of each loop that unrolling may try to find an execution
+  /// that fails (0: do not try).
+  unsigned ConfirmBound = 10;
   /// Where the run counts the verdicts it prints, if anywhere.
   VerifySummary *Summary = nullptr;
 };
diff --git a/clang/test/Verify/suite/function_filter.cpp b/clang/test/Verify/suite/function_filter.cpp
new file mode 100644
index 0000000000..91da544d7e
--- /dev/null
+++ b/clang/test/Verify/suite/function_filter.cpp
@@ -0,0 +1,150 @@
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefix=ALL
+// RUN: not %cpp-verify --jobs=1 --function=uses_wrong %s -- 2>&1 | FileCheck %s --check-prefix=ONE --implicit-check-not=Verified --implicit-check-not=error:
+// RUN: %cpp-verify --jobs=1 --function='add_*' %s -- 2>&1 | FileCheck %s --check-prefix=GLOB --implicit-check-not=uses_ --implicit-check-not=error:
+// RUN: rm -f %t.cpv
+// RUN: not %cpp-verify --jobs=1 --function=uses_wrong --obligation-out=%t.cpv %s -- > /dev/null 2>&1
+// RUN: not %cpp-verify --obligation-in=%t.cpv 2>&1 | FileCheck %s --check-prefix=RAN --implicit-check-not=add_two
+// RUN: %cpp-verify --jobs=1 --function=uses_add %s -- 2>&1 | FileCheck %s --check-prefix=CALLEE --implicit-check-not=Verified
+// RUN: not %cpp-verify --jobs=1 --function=uses_bad %s -- 2>&1 | FileCheck %s --check-prefix=SPEC --implicit-check-not=error:
+// RUN: %cpp-verify --jobs=1 --function=reach %s -- 2>&1 | FileCheck %s --check-prefix=PREDICATE --implicit-check-not=Verified
+// RUN: not %cpp-verify --jobs=1 --function=climbs %s -- 2>&1 | FileCheck %s --check-prefix=STEP
+// RUN: not %cpp-verify --jobs=1 --solver-rlimit=1 --function=reach %s -- 2>&1 | FileCheck %s --check-prefix=RULES
+// RUN: not %cpp-verify --jobs=1 --function=nothing %s -- 2>&1 | FileCheck %s --check-prefix=NONE
+// RUN: %cpp-verify --list-functions --function='add_*' %s -- 2>&1 | FileCheck %s --check-prefix=LIST --implicit-check-not=uses_
+//
+// --function reports only the functions whose names match: a glob pattern,
+// repeatable. What their verdicts rely on is verified too, so each verdict
+// is the one a run of the whole file gives; what they do not rely on is not
+// verified at all.
+
+namespace cv = cppverify;
+
+int add_one(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 1)
+{
+  return x + 1;
+}
+
+int add_two(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 2)
+{
+  return x + 2;
+}
+
+int wrong(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
+
+int uses_wrong(int x)
+  cv::pre(x < 50)
+  cv::post(cv::result == x + 1)
+{
+  int y = wrong(x);
+  return y + 1;
+}
+
+int uses_add(int x)
+  cv::pre(x < 50)
+  cv::post(cv::result == x + 2)
+{
+  int y = add_one(x);
+  return y + 1;
+}
+
+// A spec whose termination fails has no definition, whoever is selected.
+cv::spec int bad(int n)
+  cv::decreases(n)
+{
+  return n > 100 ? 0 : bad(n + 1);
+}
+
+int uses_bad(int x)
+  cv::post(bad(x) == bad(x) + 0)
+{
+  return x;
+}
+
+int jumps(int x)
+  cv::post(true)
+{
+  goto done;
+done:
+  return x;
+}
+
+cv::spec bool edge(int a, int b) { return b == a + 1; }
+
+cv::spec bool reach(int a, int b)
+  cv::inductive
+{
+  return a == b || cv::exists(c, edge(a, c) && reach(c, b));
+}
+
+// Its postcondition is false at a == b; the induction that refutes it is
+// a generated function.
+cv::spec bool climbs(int a, int b)
+  cv::inductive
+  cv::post(!cv::result || a < b)
+{
+  return a == b || cv::exists(c, edge(a, c) && climbs(c, b));
+}
+
+// ALL: Verified: add_one [backend=z3]
+// ALL: Verified: add_two [backend=z3]
+// ALL: error: verification failed: wrong
+// ALL: Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established)
+// ALL: Verified: uses_add [backend=z3]
+// ALL: error: spec decreases failed: bad
+// ALL: Unresolved: uses_bad [backend=z3] [reason=spec.termination]
+// ALL: Verified: inductive predicate: reach
+// ALL: Verified: inductive predicate: climbs
+// ALL: Unresolved: spec post: climbs [reason=spec.post]
+// ALL: error: spec post by induction failed: climbs
+// ALL: Summary: 5 verified, 3 failed, 4 unresolved (callee.contract 1, construct.unsupported 1, spec.post 1, spec.termination 1)
+
+// The same verdict, alone: wrong is verified, and its failure demotes it.
+// ONE: Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established)
+// ONE-NEXT: Summary: 1 unresolved (callee.contract 1)
+
+// GLOB: Verified: add_one [backend=z3]
+// GLOB-NEXT: Verified: add_two [backend=z3]
+// GLOB-NEXT: Summary: 2 verified
+
+// Only uses_wrong and what it relies on were verified.
+// RAN-DAG: wrong
+// RAN-DAG: uses_wrong
+
+// A callee that verifies is verified, so its caller is.
+// CALLEE: Verified: uses_add [backend=z3]
+// CALLEE-NEXT: Summary: 1 verified
+
+// SPEC: Unresolved: uses_bad [backend=z3] [reason=spec.termination] (relies on the definition of bad, whose termination is not established)
+// SPEC-NEXT: Summary: 1 unresolved (spec.termination 1)
+
+// An inductive predicate is reported with its rules.
+// PREDICATE: Verified: inductive predicate: reach
+// PREDICATE-NEXT: Summary: 1 verified
+
+// Its step and rule proofs are reported with it when they do not hold.
+// RULES: Unresolved: inductive predicate: reach [reason=spec.inductive] (its rules are not established: monotonicity, case analysis, introduction)
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: spec decreases unresolved: reach
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (monotonicity)
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (case analysis)
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (introduction)
+// RULES-NEXT: Summary: 5 unresolved ({{.*}}spec.inductive 1)
+
+// The induction of a generated function is reported with its predicate.
+// STEP: Verified: inductive predicate: climbs
+// STEP-NEXT: Unresolved: spec post: climbs [reason=spec.post] (relies on the postcondition of climbs.step, which is not established)
+// STEP-NEXT: function_filter.cpp:92:24: error: spec post by induction failed: climbs
+// STEP-NEXT: Summary: 1 verified, 1 failed, 1 unresolved (spec.post 1)
+
+// NONE: error: no function matches --function=nothing
+
+// LIST: function_filter.cpp:22:5: function add_one
+// LIST-NEXT: function_filter.cpp:29:5: function add_two
diff --git a/clang/test/Verify/suite/inductive_counterexamples.cpp b/clang/test/Verify/suite/inductive_counterexamples.cpp
index 4fb3d8c718..7ce2f26981 100644
--- a/clang/test/Verify/suite/inductive_counterexamples.cpp
+++ b/clang/test/Verify/suite/inductive_counterexamples.cpp
@@ -1,76 +1,241 @@
-// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --jobs=1 --confirm-bound=0 %s -- 2>&1 | FileCheck %s --check-prefix=NONE
+// RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON
+// RUN: not %cpp-verify --backend=bmc --confirm-bound=3 %s -- 2>&1 | FileCheck %s --check-prefix=OPTION
 //
-// A counterexample may need an inductive predicate to be false somewhere,
-// which no derivation height shows. Its check decides that by the least
-// fixpoint over the arguments the predicate's derivations reach, when they
-// are finitely many, or by a proved postcondition; otherwise the message
-// names the application it could not decide.
+// A counterexample that passes through a loop starts the loop's next steps
+// from any state its invariants allow, which no execution need reach. Its
+// failure says so, and unrolling each loop looks for an execution that
+// fails: one within the bound, none within it, or a proof that none fails at
+// all. A loop without a measure is named beside a failure too.
 
-#include <cppverify.h>
-using cppverify::valid;
+namespace cv = cppverify;
 
-cppverify::spec bool edge(int a, int b) { return b == a + 2 || b == 2 * a; }
-
-// Finitely many arguments: every step goes up, and none above b counts.
-cppverify::spec bool climb(int a, int b) cppverify::inductive {
-  return a == b || (a < b && cppverify::exists(c, edge(a, c) && climb(c, b)));
+int count_up(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n)
+{
+  int c = 0;
+  while (c < n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
 
-cppverify::proof void climb_three_four() cppverify::post(climb(3, 4)) {}
-// CHECK-DAG: error: verification failed: climb_three_four {{.*}}[reason=counterexample]
+int sum_wrong(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n)
+{
+  int s = 0;
+  for (int i = 0; i < n; i = i + 1)
+    cv::invariant(0 <= i && i <= n && s == 2 * i)
+    cv::decreases(n - i)
+  {
+    s = s + 2;
+  }
+  return s;
+}
 
-cppverify::proof void climb_one_four() cppverify::post(climb(1, 4)) {
-  cppverify::check(climb(4, 4));
-  cppverify::check(climb(2, 4));
+int far_wrong(int n)
+  cv::pre(n >= 0 && n <= 1000)
+  cv::post(cv::result < 100)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
-// CHECK-DAG: Verified: climb_one_four
 
-// Defined together, with finitely many arguments.
-cppverify::spec bool ev(int n);
-cppverify::spec bool od(int n) cppverify::inductive { return n == 1 || (n > 1 && ev(n - 1)); }
-cppverify::spec bool ev(int n) cppverify::inductive { return n == 0 || (n > 0 && od(n - 1)); }
+int no_loop(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
 
-cppverify::proof void four_is_odd() cppverify::post(od(4)) {}
-// CHECK-DAG: error: verification failed: four_is_odd {{.*}}[reason=counterexample]
+int unmeasured(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n + 1)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+  {
+    c = c + 1;
+  }
+  return c;
+}
 
-// Reading memory: a cycle that never reaches 5.
-cppverify::spec bool linked(const int *next, int n, int i, int j)
-  cppverify::inductive
-  cppverify::reads(next, n)
+// Unrolling checks the copies of the failed check, here the division in
+// each iteration, and finds the execution that divides by zero.
+int divides(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result >= -5)
 {
-  return i == j || (0 <= i && i < n && linked(next, n, next[i], j));
+  int c = 0;
+  int q = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    q = 10 / (3 - c);
+    c = c + 1;
+  }
+  return q - 5;
 }
 
-void around(const int *next)
-  cppverify::pre(valid(next, 2) && next[0] == 1 && next[1] == 0)
+// Unrolling keeps no invariant, so it cannot confirm a failed one.
+int grows(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
 {
-  cppverify::check(linked(next, 2, 0, 5));
+  int c = 0;
+  while (c < n)
+    cv::invariant(c <= 2)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
-// CHECK-DAG: error: verification failed: around {{.*}}[reason=counterexample]
 
-// Infinitely many arguments, but a proved postcondition decides it.
-cppverify::spec bool even(int n) cppverify::inductive cppverify::post(!cppverify::result || (n >= 0 && n % 2 == 0)) {
-  return n == 0 || even(n - 2);
+// The copies of the failed check are those at its place: the check after
+// the loop fails sooner, with n == 2, but it is another check.
+int two_checks(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    cv::check(c != 4);
+    c = c + 1;
+  }
+  cv::check(c != 2);
+  return c;
 }
 
-cppverify::proof void three_is_even() cppverify::post(even(3)) {}
-// CHECK-DAG: error: verification failed: three_is_even {{.*}}[reason=counterexample]
+// And those of its kind: the failed check is the overflow of INT_MIN / -1,
+// and the division by zero at the same place fails one iteration sooner, in
+// every execution that would reach it. A copy is solved in the executions
+// that pass the failing checks before it, so none fails the overflow.
+int two_kinds(int a, int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
+{
+  int c = 0;
+  int q = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    q = a / (1 - c);
+    c = c + 1;
+  }
+  return q;
+}
 
-// Neither: the message names the application.
-cppverify::spec bool odd(int n) cppverify::inductive { return n == 1 || odd(n - 2); }
+// The first division fails at c == k, and the second one iteration sooner
+// when m == k - 1: the execution that fails the first within 2 iterations
+// divides by zero in the second first. The one shown passes it.
+int past_failure(int k, int m, int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::pre((k == 1 && m == 0) || (k == 3 && m == 100))
+  cv::post(true)
+{
+  int c = 0;
+  int q = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    q = 100 / (k - c);
+    q = q + 100 / (m - c);
+    c = c + 1;
+  }
+  return q;
+}
 
-cppverify::proof void four_is_odd_too() cppverify::post(odd(4)) {}
-// CHECK-DAG: four_is_odd_too {{.*}}whether odd(4) holds: no derivation was found among the heights tried
+// A failure on a path that skips the loop has no loop to note.
+int skipped(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result >= 0)
+{
+  int c = 0;
+  if (n > 3) {
+    while (c < n)
+      cv::invariant(0 <= c && c <= n)
+      cv::decreases(n - c)
+    {
+      c = c + 1;
+    }
+  }
+  return c - 1;
+}
 
-// A postcondition that is not established is no evidence: the
-// counterexample that used it is not reported as one. ge(-5000) holds, by a
-// derivation too tall to find, while the false postcondition says it
-// cannot.
-cppverify::spec bool ge(int n);
-cppverify::spec bool ge(int n) cppverify::inductive cppverify::post(!cppverify::result || n > -1000) {
-  return n == 20 || ge(n + 1);
+// A proof gets no notes.
+int count_up_proved(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
-// CHECK-DAG: error: spec post by induction failed: ge
 
-cppverify::proof void far() cppverify::post(ge(-5000)) {}
-// CHECK-DAG: Unresolved: verification unresolved: far {{.*}}[reason=spec.post] (its counterexample is checked with the postcondition of ge, which is not established)
+// CHECK:      inductive_counterexamples.cpp:16:23: error: verification failed: count_up [{{.*}}::postcondition@16:23] {{.*}}trace: loop.entry@19:3 -> loop.exit@19:3
+// CHECK-NEXT: note: the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// CHECK-NEXT: inductive_counterexamples.cpp:29:23: error: verification failed: sum_wrong [{{.*}}::postcondition@29:23]
+// CHECK-NEXT: note: the counterexample's state at the loop at 32:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 1 iteration of each loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 1{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:43:23: error: verification failed: far_wrong [{{.*}}::postcondition@43:23]
+// CHECK-NEXT: note: the counterexample's state at the loop at 46:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: no execution fails this check within 10 iterations of each loop
+// CHECK-NEXT: inductive_counterexamples.cpp:57:23: error: verification failed: no_loop [{{.*}}::postcondition@57:23]
+// CHECK-NEXT: inductive_counterexamples.cpp:64:23: error: verification failed: unmeasured [{{.*}}::postcondition@64:23]
+// CHECK-NEXT: note: the loop at 67:3 has no cppverify::decreases: a proof would be Unresolved (decreases.missing) until it has one
+// CHECK-NEXT: note: the counterexample's state at the loop at 67:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:87:7: error: verification failed: divides [{{.*}}::division-by-zero@87:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 83:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 4 iterations of each loop (counterexample: {{.*}}c [ssa=c_4] [type=i32] = 3{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:100:21: error: verification failed: grows [{{.*}}::invariant-preserved@100:21]
+// CHECK-NEXT: note: the counterexample's state at the loop at 99:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: inductive_counterexamples.cpp:119:5: error: verification failed: two_checks [{{.*}}::assertion@119:5]
+// CHECK-NEXT: note: the counterexample's state at the loop at 115:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 5 iterations of each loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 5{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:140:7: error: verification failed: two_kinds [{{.*}}::overflow@140:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 136:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: no execution fails this check without failing an earlier one first (the division-by-zero check at 140:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there
+// CHECK-NEXT: inductive_counterexamples.cpp:160:7: error: verification failed: past_failure [{{.*}}::division-by-zero@160:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 156:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 4 iterations of each loop (counterexample: {{.*}}k [ssa=k_0] [type=i32] = 3, m [ssa=m_0] [type=i32] = 100{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:170:23: error: verification failed: skipped [{{.*}}::postcondition@170:23]
+// CHECK-NEXT: Verified: count_up_proved [backend=z3]
+// CHECK-NEXT: Summary: 1 verified, 11 failed
+
+// Without unrolling, a failure still says where its state comes from.
+// NONE:      error: verification failed: count_up
+// NONE-NEXT: note: the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches
+// NONE-NEXT: error: verification failed: sum_wrong
+
+// JSON: "function":"count_up",{{.*}}"notes":["the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches","no execution fails this check: every loop ends within 5 iterations{{.*}}"]
+// JSON: "function":"no_loop"
+// JSON-NOT: "notes"
+// JSON: "function":"unmeasured"
+
+// OPTION: error: --confirm-bound requires source verification with --backend=z3, cvc5, portfolio, or race
diff --git a/clang/test/Verify/suite/max_failures.cpp b/clang/test/Verify/suite/max_failures.cpp
new file mode 100644
index 0000000000..ee169ceb8d
--- /dev/null
+++ b/clang/test/Verify/suite/max_failures.cpp
@@ -0,0 +1,103 @@
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefix=ONE
+// RUN: not %cpp-verify --jobs=1 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=TWO
+// RUN: not %cpp-verify --jobs=4 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=TWO
+// RUN: not %cpp-verify --jobs=1 --max-failures=0 %s -- 2>&1 | FileCheck %s --check-prefix=ALL
+// RUN: not %cpp-verify --jobs=4 --max-failures=0 %s -- 2>&1 | FileCheck %s --check-prefix=ALL
+// RUN: not %cpp-verify --jobs=1 --max-failures=0 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON
+// RUN: not %cpp-verify --backend=cvc5 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=OPTION
+//
+// A function reports the first check that fails, in the order an execution
+// meets them; --max-failures=N reports the first N, and 0 every one, each
+// with its own counterexample. A check after the first failure is solved in
+// the executions that pass the failing checks before it, so its
+// counterexample reaches it, and a check that fails only where an earlier
+// one does is not reported. The summary still counts functions.
+
+namespace cv = cppverify;
+
+int three_bugs(int x, int y)
+  cv::pre(x < 1000 && y < 1000)
+  cv::post(cv::result > 0)
+  cv::post(cv::result < 100)
+{
+  int q = 10 / y;
+  int r = x + q;
+  return r;
+}
+
+int one_bug(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
+
+// The assertion fails only where the division divides by zero.
+int dependent(int x)
+  cv::pre(x < 100)
+  cv::post(true)
+{
+  int q = 100 / x;
+  cv::check(x != 0);
+  return q;
+}
+
+// Each failure has its notes: the first holds in every execution, which its
+// loop's missing invariant hides, and the second fails at once.
+int counted(int n)
+  cv::pre(n >= 0 && n <= 3)
+  cv::post(cv::result == n)
+  cv::post(cv::result == n + 1)
+{
+  int c = 0;
+  while (c < n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
+}
+
+// ONE:      max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = 0{{.*}}) [backend=z3] [reason=counterexample]
+// ONE-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23]
+// ONE-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3]
+// ONE-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23]
+// ONE-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// ONE-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// ONE-NEXT: Summary: 4 failed
+
+// The overflow's counterexample divides by y, which is not zero.
+// TWO:      max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3]
+// TWO-NEXT: max_failures.cpp:24:3: error: verification failed: three_bugs [{{.*}}::overflow@24:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}}) [backend=z3] [reason=counterexample]
+// TWO-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23]
+// TWO-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3]
+// TWO-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23]
+// TWO-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// TWO-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// TWO-NEXT: max_failures.cpp:50:23: error: verification failed: counted [{{.*}}::postcondition@50:23]
+// TWO-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// TWO-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}})
+// TWO-NEXT: Summary: 4 failed
+
+// ALL:      max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3]
+// ALL-NEXT: max_failures.cpp:24:3: error: verification failed: three_bugs [{{.*}}::overflow@24:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}})
+// ALL-NEXT: max_failures.cpp:20:23: error: verification failed: three_bugs [{{.*}}::postcondition@20:23] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}};
+// ALL-NEXT: max_failures.cpp:21:23: error: verification failed: three_bugs [{{.*}}::postcondition@21:23] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}};
+// ALL-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23]
+// ALL-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3]
+// ALL-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23]
+// ALL-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// ALL-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// ALL-NEXT: max_failures.cpp:50:23: error: verification failed: counted [{{.*}}::postcondition@50:23]
+// ALL-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// ALL-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}})
+// ALL-NEXT: Summary: 4 failed
+
+// JSON-COUNT-4: "function":"three_bugs"
+// JSON-NOT: "function":"three_bugs"
+// JSON: "function":"one_bug"
+// JSON-NEXT: "function":"dependent"
+// JSON-COUNT-2: "function":"counted"{{.*}}"notes":[
+// JSON-NOT: "function"
+
+// OPTION: error: --max-failures requires source verification with --backend=z3
diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
index 040acc1148..b6bdd052b9 100644
--- a/clang/tools/cpp-verify/Main.cpp
+++ b/clang/tools/cpp-verify/Main.cpp
@@ -287,6 +287,25 @@ static cl::opt<bool>
                      "(spec axiom)"),
             cl::cat(CppVerifyCategory));
 
+static cl::opt<unsigned> ConfirmBound(
+    "confirm-bound",
+    cl::desc("For a failure whose counterexample passes through a loop, "
+             "unroll each loop up to this many iterations to look for an "
+             "execution that fails (default 10, 0 = do not look)"),
+    cl::init(10), cl::cat(CppVerifyCategory));
+
+static cl::opt<unsigned> MaxFailures(
+    "max-failures",
+    cl::desc("Report up to this many failing checks of a function, each with "
+             "its own counterexample (default 1, 0 = all; --backend=z3)"),
+    cl::init(1), cl::cat(CppVerifyCategory));
+
+static cl::list<std::string> FunctionPatterns(
+    "function",
+    cl::desc("Report only the functions whose names match this glob pattern "
+             "(repeatable); what their verdicts rely on is verified too"),
+    cl::value_desc("pattern"), cl::cat(CppVerifyCategory));
+
 static cl::opt<bool> ListFunctions(
     "list-functions",
     cl::desc("List the functions a run would verify, with their kinds and "
@@ -448,6 +467,10 @@ class VerifyConsumer : public ASTConsumer {
       VOpts.Quiet = Quiet.getValue();
       VOpts.Verbose = Verbose.getValue();
       VOpts.ListFunctions = ListFunctions.getValue();
+      VOpts.MaxFailures = MaxFailures.getValue();
+      VOpts.FunctionPatterns.assign(FunctionPatterns.begin(),
+                                    FunctionPatterns.end());
+      VOpts.ConfirmBound = ConfirmBound.getValue();
       VOpts.Summary = &gSummary;
       if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts))
         ++gVerifyFailures;
@@ -678,6 +701,12 @@ static bool resolveOptions(bool Replay) {
             "--backend=race";
   else if (given(BMCUnroll) && !Replay && Backend != "bmc")
     Error = "--unroll requires --backend=bmc";
+  else if (given(ConfirmBound) &&
+           (Replay || Backend == "bmc" || Backend == "lean"))
+    Error = "--confirm-bound requires source verification with --backend=z3, "
+            "cvc5, portfolio, or race";
+  else if (given(MaxFailures) && (Replay || Backend != "z3"))
+    Error = "--max-failures requires source verification with --backend=z3";
   else if (given(LeanFallbackScope) && LeanFallback.empty())
     Error = "--lean-fallback-scope requires --lean-fallback";
   else if (given(LeanAutoTimeout) && LeanProject.empty() &&
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 0927560a31..23c2700e7a 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -752,6 +752,31 @@ function as possibly divergent: its proof, and the proof of every caller, is
 reported `[partial]`. Calls within an executable or proof recursion cycle
 assert the decrease of the shared measure at the call site.
 
+**Counterexamples after a loop.** A certified failure (on Z3, cvc5, the
+portfolio, or the race) whose trace has an active loop event passed through
+the loop's havoc, so its state there is any the invariants allow. The driver
+notes that (`VerifyDiagnostic::Notes`, printed as `note:` lines and JSON
+`notes`) and confirms it the way BMC verifies: a copy of the function
+prepared for unrolling (`SpecInliner::prepareFunction`, the UB checks), each
+bound from 0 to `--confirm-bound` unrolled (`LoopUnroller`), passivized
+against the interface map, and solved obligation by obligation
+(`Z3VerifyBackend::verifyObligations`) with one query timeout for all
+bounds. The copies of the failed check are the obligations of its kind at
+its source location: one per iteration for a check in a loop's body, none
+for a loop's invariant or measure, which unrolling does not keep (then
+nothing is noted). A copy that fails at bound `b` is an execution within `b`
+iterations of each loop (callees still by their contracts), and its
+counterexample is noted; copies that all hold where every loop's unwinding
+is proved hold for every execution; copies that hold short of that go on to
+the next bound; anything unresolved ends the search without a note. Every
+failure of the unrolled module is reported, so each copy, and each loop's
+unwinding, is solved past the failing obligations before it (see
+`--max-failures` below): the execution noted fails no earlier check, and a
+copy that holds there, when another check fails before it, is noted as
+holding in every execution that does not fail that check first, named by its
+kind and place. A function with an unmeasured loop (`UnmeasuredLoop`) also
+gets a note naming it on any failure.
+
 **Loop exits.** A `break` or `return` inside the body leaves from the
 inductive iteration: its path guard is recorded and the path ends. After the
 loop the continuation assumes `(¬choice ∧ ¬cond) ∨ break₁ ∨ … ∨ return₁ ∨ …`.
@@ -2447,7 +2472,17 @@ expression being converted (`ASTConverter::CurrentRange`), unless the site
 names a place of its own, such as a function for the checks made after every
 function is converted. It is printed with Clang's `TextDiagnostic`, line and
 caret included, as a compiler error is, and its JSON record carries the range.
-A text run ends with a summary line: `printDiagnostics` counts each verdict
+`--function` filters what a run reports, not what its verdicts mean. A
+function is selected by the name its verdicts print, which for an inductive
+predicate's step (`InductiveStepOf`) is the predicate's, and a selected
+predicate's rule proofs (`InductiveRuleOf`) with it. `Verifier::run`
+schedules the selected functions, every spec and proof
+function (any verdict may rest on their facts, and a confirmation by proof
+on any established lemma), and then, round by round, each executable
+function whose contract a run's verdicts call (`CallDependencies`, proof
+blocks' `Callees`), until none is new. The fixpoints then run as for the
+whole file over the verdicts there are; the diagnostics of functions not
+selected stay, hidden, for what they establish. A text run ends with a summary line: `printDiagnostics` counts each verdict
 it prints into the run's `VerifySummary` (a first error that carries a
 verdict counts, a `--verbose` spec axiom line does not), and the driver
 prints the counts of every file of the run with its time.
@@ -2658,6 +2693,24 @@ the whole query had refuted the function in milliseconds: model search over
 quantified heap queries depends on the solver's search order, and 16 of 40
 random seeds took the full 30 s.
 
+With `--max-failures=N` (`BackendExecutionOptions::MaxFailures`, Z3 only)
+the obligations report up to `N` failures (0: all), and the result of the
+first carries the others (`VerifyResult::MoreFailures`), which the driver
+prints after it, each with its notes, as diagnostics marked `Additional` that
+the summary does not count. `verifyObligations` given a number of failures to
+report solves each obligation after the first failure in the executions that
+pass every earlier failing one, as Boogie's subsumption assumes an assertion
+after checking it (`verifyPastEarlier`: the obligation's counterexample query
+conjoined with those obligations' goals, never cached): alone, its
+counterexample could start where an earlier check already fails, and a check
+that fails only there would be reported though fixing the earlier one fixes
+it. Checks not settled are not assumed, so nothing proved past the failures
+rests on a check that may not hold. A serial run stops after the `N`th
+failure; a parallel one solves every obligation alone and then solves each
+failure after the first again, in order. Without a number, every obligation
+is solved alone, as the portfolio's comparison of Z3's and cvc5's results
+needs.
+
 The whole query of a module without logic functions is a probe of a fixed
 amount of work, `WholeProbeUnits` (6 million) Z3 resource units, with the
 module's timeout as its bound in time, so where it stops depends neither on
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index dcff8d2b56..8bf47bdbca 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -1894,7 +1894,24 @@ int safe_fib(int n) cppverify::pre(...) cppverify::post(cppverify::result == fib
 - `Failed`: a counterexample that holds when every logical function is
   evaluated at its true definition. It is relative to the declared
   abstractions only: callee contracts, loop invariants, and `cppverify::modifies`
-  frames.
+  frames. A counterexample that passes through a loop starts from any state
+  the loop's invariants allow, so such a failure says so in a note, and the
+  verifier unrolls each loop up to `--confirm-bound` iterations (default 10)
+  to look for an execution that fails the same check, as G5 proposed with
+  CBMC's and Kani's unrolling: it reports that execution, or that unrolling
+  proves the check, or that none fails it within the bound. The execution
+  passes every failing check before this one, and a check that holds in the
+  executions that pass them says so and names one that fails. Unrolling keeps
+  no loop invariant and no measure, so their failures are not confirmed. The verdict stays `Failed`
+  (decision Q12 of the 0.2 plan): the claim is not proved, and the note
+  carries the difference. A failure of a function whose loop has no
+  `cppverify::decreases` names that loop too.
+- Several failures of one function (`--max-failures`): after the first,
+  a check is a failure only when an execution that passes the failing checks
+  before it fails it, as Boogie assumes an assertion once checked and Dafny
+  then reports each failing assertion. Each such failure is a bug of its
+  own: one that fails only after an earlier failure disappears with its fix,
+  and is not reported. Checks not settled are not assumed.
 - Anything else is `Unresolved` with a reason. `spec.fuel`: every
   counterexample found relies on a recursive spec beyond what refinement could
   unfold, the automatic inductions did not prove it, and no counterexample
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 fe476e306d..f396d3f0ec 100644
--- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst
+++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
@@ -44,6 +44,17 @@ Other flags
   check (``Verified: spec axiom: twice``), which the default leaves out
 - ``cpp-verify --list-functions`` — list the functions a run would verify,
   with their locations and kinds, and verify none
+- ``cpp-verify --function=PATTERN`` — report only the functions whose names
+  match a glob pattern (repeatable), with the same verdicts as a whole run:
+  what they rely on is verified too, and nothing else that is executable
+- ``cpp-verify --confirm-bound=N`` — for a failure whose counterexample passes
+  through a loop, unroll each loop up to ``N`` iterations (default 10, ``0``
+  skips it) to find an execution that fails or prove that none does (see
+  :doc:`ch16-when-verification-fails`)
+- ``cpp-verify --max-failures=N`` — report the first ``N`` checks of a
+  function that fail (``0``: every one), each with its own counterexample,
+  instead of the first only; a check after a failure counts only when an
+  execution that passes the failing checks before it fails it
 - ``cpp-verify --backend={z3,cvc5,portfolio,race,bmc,lean}`` — verification
   engine: Z3 (the default), cvc5, both with agreement required
   (``portfolio``), both at once with the first proof or certified
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 6bd6aa9d8a..4a056a2812 100644
--- a/website/source/book/part-ii/ch16-when-verification-fails.rst
+++ b/website/source/book/part-ii/ch16-when-verification-fails.rst
@@ -29,6 +29,47 @@ text, and IR dumps intentionally make the stream mixed. Malformed display bytes
 are replaced with the Unicode replacement character, so JSON output remains
 valid UTF-8.
 
+A counterexample after a loop is only as real as the loop's invariants. At
+the loop, the verifier knows what the invariants say and nothing else, so a
+loop with too weak an invariant fails a correct function:
+
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int count_up(int n)
+     cv::pre(n >= 0 && n <= 5)
+     cv::post(cv::result == n)
+   {
+     int c = 0;
+     while (c < n)
+       cv::decreases(n - c)
+     {
+       c = c + 1;
+     }
+     return c;
+   }
+
+.. code-block:: text
+
+   count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample]
+   note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches
+   note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+
+The first note says where the counterexample's state comes from; the second
+is what unrolling the loop found about the same check (``--confirm-bound``,
+10 iterations by default): here, that every execution passes it, so the
+invariant is what is missing (``cv::invariant(0 <= c && c <= n)``). When
+unrolling finds an execution that fails the check, the note gives that
+execution and the number of iterations, and the bug is in the code or the
+contract, not in the invariant. When the check fails only in executions that
+fail an earlier check first, the note names that check: fix it first.
+
+A function reports its first failing check. To see every one, each with its
+own counterexample, run ``cpp-verify --max-failures=0``: a check after a
+failure is reported only when some execution that passes the earlier failing
+checks fails it, so each line is a bug of its own.
+
 An undecided query is different from a counterexample. ``Unresolved`` with
 reason ``solver.timeout``, ``solver.resource-limit``, ``solver.memory-limit``,
 or ``solver.unknown`` means Z3 timed out, exhausted an explicit resource/query
diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst
index 4c69734279..2aabca3f6f 100644
--- a/website/source/language/functions-loops.rst
+++ b/website/source/language/functions-loops.rst
@@ -638,6 +638,83 @@ rest of the loop, and a ``continue`` goes to the condition, where the
 invariant must first hold. ``cppverify::ghost`` code cannot leave an
 executable loop.
 
+A failure is relative to the loop's invariants: after the loop, and at the
+start of an iteration, the verifier knows only what they say, so a
+counterexample there may start from a state no execution reaches. Such a
+failure says so in a note, and the verifier then unrolls each loop, up to
+``--confirm-bound`` iterations (10 by default, ``0`` to skip), to look for an
+execution that fails the same check, with callees still by their contracts:
+
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int count_up(int n)
+     cv::pre(n >= 0 && n <= 5)
+     cv::post(cv::result == n)
+   {
+     int c = 0;
+     while (c < n)
+       cv::decreases(n - c)
+     {
+       c = c + 1;
+     }
+     return c;
+   }
+
+.. code-block:: text
+
+   count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample]
+   note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches
+   note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+
+Here the loop has no invariant, so after it ``c`` may be anything; the fix is
+``cv::invariant(0 <= c && c <= n)``. When unrolling finds an execution that
+fails the check (in any iteration's copy of it, for a check in the loop's
+body), the note says within how many iterations and gives that execution;
+when it finds neither a failure nor a proof within the bound, the note says
+that no execution fails the check within that many iterations. The execution
+a note gives passes the checks before this one that fail, since one that
+fails an earlier check never reaches it. When the check holds in every
+execution that passes them, the note says so and names an earlier check that
+fails, the one to fix first (``--max-failures=0`` reports it with its own
+counterexample, see :doc:`tooling`):
+
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int divide(int a, int n)
+     cv::pre(n >= 0 && n <= 5)
+     cv::post(true)
+   {
+     int c = 0;
+     int q = 0;
+     while (c < n)
+       cv::invariant(0 <= c && c <= n)
+       cv::decreases(n - c)
+     {
+       q = a / (1 - c);
+       c = c + 1;
+     }
+     return q;
+   }
+
+.. code-block:: text
+
+   divide.cpp:13:7: error: verification failed: divide [fn_...::overflow@13:7] (counterexample: a [ssa=a_0] [type=i32] = -2147483648, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 2, n [ssa=n_0] [type=i32] = 3, q [ssa=q_1] [type=i32] = 0; trace: loop.entry@9:3 -> loop.inductive iteration@9:3 condition=true) [backend=z3] [reason=counterexample]
+   note: the counterexample's state at the loop at 9:3 is any state its invariants allow, not necessarily one an execution reaches
+   note: no execution fails this check without failing an earlier one first (the division-by-zero check at 13:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there
+
+``INT_MIN / -1`` needs ``c == 2``, and every execution that gets there
+divides by ``1 - 1`` one iteration sooner.
+
+Unrolling keeps no invariant and no measure, so a failed invariant or
+measure gets the first note only. The verdict stays ``verification failed`` either way, since
+the claim is not proved. A failure of a function
+whose loop has no ``cppverify::decreases`` also notes that loop: with a
+proof, the function would still be ``Unresolved`` (``decreases.missing``).
+
 A range-based ``for`` loop over an array (a local array, an array member,
 a constant table) visits its elements in order. Its contract names the
 position, ``cppverify::index``, the number of elements before the current
diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index 12094a6595..5e2f798c66 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -11,6 +11,7 @@ Standalone verifier
    cpp-verify --quiet file.cpp
    cpp-verify --verbose file.cpp
    cpp-verify --list-functions file.cpp
+   cpp-verify --function='parse_*' --function=encode file.cpp
    cpp-verify file.cpp -- -I include -DNDEBUG
    cpp-verify --backend=z3 file.cpp
    cpp-verify --backend=cvc5 file.cpp
@@ -24,6 +25,8 @@ Standalone verifier
    cpp-verify --no-check-ub file.cpp
    cpp-verify --profile-quantifiers file.cpp
    cpp-verify --timeout=20000 file.cpp
+   cpp-verify --confirm-bound=4 file.cpp
+   cpp-verify --max-failures=0 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
@@ -213,6 +216,22 @@ whole output, of ``--list-functions``, and of archive replay
    summary.cpp:5:5: function add_one
    summary.cpp:12:5: function add_two
 
+``--function=PATTERN`` reports only the functions whose names match the glob
+pattern (``*``, ``?``, ``[...]``; repeatable, a function matching any is
+reported), as ``Verified`` and the other lines print the name: ``Ring::push``,
+``total<short>``; an inductive predicate is reported with the checks generated
+for it (its step's termination and induction, its rule proofs). Every verdict
+it reports is the one a run of the whole file gives: the functions whose
+contracts those verdicts rely on are verified too, round by round, and so
+are all spec and proof functions, whose facts any
+proof may use; their results are not printed, and a selected function that
+relies on a callee whose verification fails is ``Unresolved`` with
+``callee.contract`` exactly as in a whole run. An executable function no
+reported verdict relies on is not verified at all. The exit status follows
+what is reported: 0 when every reported verdict is a proof. A pattern that
+matches no function is an error. With ``--list-functions`` it narrows the
+listing.
+
 ``cpp-verify --help`` shows each time limit's default (``--timeout``,
 30000 ms).
 
@@ -955,6 +974,55 @@ False guards are omitted; a guard the model does not determine is retained with
 JSON ``"active": null`` rather than an invented path choice. Archives preserve
 the same names, ranges, IDs, and trace data during replay.
 
+A failure may carry notes, printed after it as ``note:`` lines and in JSON as
+``notes``: a counterexample that passes through a loop starts from any state
+the loop's invariants allow, and what unrolling each loop then finds about
+the same check, within ``--confirm-bound`` iterations (default 10; ``0``
+skips it; only with the solver backends, since BMC unrolls already and Lean
+runs no solver): an execution that fails it, a proof that none does, or no
+failure within the bound. The search takes at most one query timeout. Unrolling
+drops the loops' invariants and measures, so a failure of one gets no
+search: it would find no copy of the check at any bound. A loop without
+``cppverify::decreases`` is noted too (see :doc:`functions-loops`).
+
+A function reports one failure: the first check that fails, in the order an
+execution meets them. ``--max-failures=N`` reports the first ``N``, and
+``--max-failures=0`` every one, each with its own counterexample and notes,
+as Dafny reports every failing assertion of a method (only with
+``--backend=z3``). A check after the first failure is solved in the
+executions that pass the failing checks before it, as Boogie assumes an
+assertion once it has checked it: its counterexample reaches it without
+failing an earlier check, and a check that fails only where an earlier one
+fails is not reported, since fixing that one fixes it. The summary still
+counts each function once:
+
+.. cppverify-example: flags --max-failures=0
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int three_bugs(int x, int y)
+     cv::pre(x < 1000 && y < 1000)
+     cv::post(cv::result > 0)
+   {
+     int q = 10 / y;
+     int r = x + q;
+     return r;
+   }
+
+.. code-block:: text
+
+   $ cpp-verify --max-failures=0 three_bugs.cpp
+   three_bugs.cpp:7:3: error: verification failed: three_bugs [fn_...::division-by-zero@7:3] (counterexample: x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 0) [backend=z3] [reason=counterexample]
+   three_bugs.cpp:8:3: error: verification failed: three_bugs [fn_...::overflow@8:3] (counterexample: q [ssa=q_1] [type=i32] = -1, x [ssa=x_0] [type=i32] = -2147483648, y [ssa=y_0] [type=i32] = -9) [backend=z3] [reason=counterexample]
+   three_bugs.cpp:5:23: error: verification failed: three_bugs [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 0, q [ssa=q_1] [type=i32] = 0, r [ssa=r_1] [type=i32] = 0, x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 11; trace: return.return@9:3 value=0) [backend=z3] [reason=counterexample]
+   Summary: 1 failed in 0.0 s
+
+Without the option only the first line is printed. The overflow's
+counterexample divides by ``y = -9``, not by zero, and the postcondition's
+returns from an execution with no undefined operation. In JSON each failure
+is a record of its own.
+
 Each non-success verification result also carries a stable reason code. Current
 codes include ``counterexample``, ``solver.timeout``, ``solver.unknown``,
 ``solver.resource-limit``, ``solver.memory-limit``, ``solver.unavailable``,
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index 58d1cfe2aa..77b62d388c 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -483,11 +483,33 @@ are errors at the statement (:doc:`language/functions-loops`).
 Running cpp-verify
 ~~~~~~~~~~~~~~~~~~
 
+**Counterexamples after a loop.** A failure whose counterexample passed
+through a loop looked like any other, though its state there came from the
+loop's invariants and no execution need reach it: the first loop most users
+write, without an invariant, failed with ``c = 0`` after ``while (c < n)``.
+Such a failure now says so in a note, and unrolling each loop then looks for
+an execution that fails the same check within ``--confirm-bound`` iterations
+(default 10): it gives that execution, or says that no execution fails the
+check (when unrolling proves it) or that none fails it within the bound. The
+execution it gives passes the failing checks before this one, and a check
+that holds in every execution that passes them is noted with an earlier
+check that fails. A failure of a function whose loop has no
+``cppverify::decreases`` names that loop too
+(:doc:`language/functions-loops`).
+
+**Every failure of a function.** A function reported only its first failing
+check. ``--max-failures=N`` reports the first ``N`` (``0``: every one), each
+with its own counterexample and notes; a check after a failure is reported
+only when an execution that passes the earlier failing checks fails it, as
+Dafny reports every failing assertion (:doc:`language/tooling`).
+
 **A summary, and what to print.** A run now ends with one line that counts
 its verdicts by kind, with the reasons of the unresolved ones and the time it
 took (``Summary: 12 verified, 1 failed, 2 unresolved (spec.fuel 1,
 solver.timeout 1) in 3.2 s``). ``--quiet`` prints only what needs attention,
-``--list-functions`` lists what a run would verify without verifying it, and
+``--list-functions`` lists what a run would verify without verifying it,
+``--function=PATTERN`` reports only the functions a glob pattern matches,
+with the verdicts a whole run gives, and
 the ``Verified: spec axiom: f`` line of a spec that needs no check is printed
 only with ``--verbose``. ``--help`` shows the default of ``--timeout``
 (:doc:`language/tooling`).