diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index 8967072384..583ca512af 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"
@@ -1101,6 +1102,8 @@ 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;
 };
 
 /// The backend a lowering reports, as lower-only names it.
@@ -3502,6 +3505,132 @@ 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;
+        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;
+          for (VerifyResult &Result : Unroller.verifyObligations(Module)) {
+            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(
+                "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");
+            return Notes;
+          }
+        }
+        if (Unrolled)
+          Notes.push_back("no execution fails this check within " +
+                          iterations(Opts.ConfirmBound) + " of each loop");
+        return Notes;
+      };
       Passivizer P;
       P.setFunctionMap(InterfaceMap);
       auto proves = [&](PassiveProgram Smoke) {
@@ -4720,6 +4849,7 @@ class Verifier {
           Msg += backendSuffix(R);
           Diags.push_back(
               {VerifyDiagnostic::Error, Msg, R.Location, Fn->Name, R});
+          Diags.back().Notes = failureNotes(*Fn, R);
         } else {
           const bool FallbackExported = R.Status == VerifyStatus::Unresolved &&
                                         exportLeanFallback(Module, Fn->Name, R);
@@ -5654,6 +5784,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);
 
@@ -6000,6 +6136,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..3ddbb110be 100644
--- a/clang/lib/Verify/Driver/Verifier.h
+++ b/clang/lib/Verify/Driver/Verifier.h
@@ -120,6 +120,10 @@ struct VerifyOptions {
   bool Verbose = false;
   /// List the functions the run would verify, and verify none.
   bool ListFunctions = false;
+  /// 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/inductive_counterexamples.cpp b/clang/test/Verify/suite/inductive_counterexamples.cpp
index 4fb3d8c718..42421b805d 100644
--- a/clang/test/Verify/suite/inductive_counterexamples.cpp
+++ b/clang/test/Verify/suite/inductive_counterexamples.cpp
@@ -1,76 +1,215 @@
-// 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; }
+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;
+}
 
-// 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 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_three_four() cppverify::post(climb(3, 4)) {}
-// CHECK-DAG: error: verification failed: climb_three_four {{.*}}[reason=counterexample]
+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;
+}
 
-cppverify::proof void climb_one_four() cppverify::post(climb(1, 4)) {
-  cppverify::check(climb(4, 4));
-  cppverify::check(climb(2, 4));
+int no_loop(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
 }
-// 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 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;
+}
 
-cppverify::proof void four_is_odd() cppverify::post(od(4)) {}
-// CHECK-DAG: error: verification failed: four_is_odd {{.*}}[reason=counterexample]
+// 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)
+{
+  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;
+}
+
+// Unrolling keeps no invariant, so it cannot confirm a failed one.
+int grows(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(c <= 2)
+    cv::decreases(n - c)
+  {
+    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)
+// 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)
 {
-  return i == j || (0 <= i && i < n && linked(next, n, next[i], j));
+  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;
 }
 
-void around(const int *next)
-  cppverify::pre(valid(next, 2) && next[0] == 1 && next[1] == 0)
+// And those of its kind: the division by zero at the same place fails one
+// iteration sooner, but the failed check is the overflow of INT_MIN / -1.
+int two_kinds(int a, int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
 {
-  cppverify::check(linked(next, 2, 0, 5));
+  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;
 }
-// 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);
+// 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;
 }
 
-cppverify::proof void three_is_even() cppverify::post(even(3)) {}
-// CHECK-DAG: error: verification failed: three_is_even {{.*}}[reason=counterexample]
+// 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;
+}
 
-// Neither: the message names the application.
-cppverify::spec bool odd(int n) cppverify::inductive { return n == 1 || odd(n - 2); }
+// 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:138:7: error: verification failed: two_kinds [{{.*}}::overflow@138:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 134:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 3 iterations of each loop (counterexample: {{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:147:23: error: verification failed: skipped [{{.*}}::postcondition@147:23]
+// CHECK-NEXT: Verified: count_up_proved [backend=z3]
+// CHECK-NEXT: Summary: 1 verified, 10 failed
 
-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
+// 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
 
-// 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);
-}
-// CHECK-DAG: error: spec post by induction failed: ge
+// 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"
 
-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)
+// OPTION: error: --confirm-bound requires source verification with --backend=z3, cvc5, portfolio, or race
diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
index 040acc1148..2dd69af19f 100644
--- a/clang/tools/cpp-verify/Main.cpp
+++ b/clang/tools/cpp-verify/Main.cpp
@@ -287,6 +287,13 @@ 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<bool> ListFunctions(
     "list-functions",
     cl::desc("List the functions a run would verify, with their kinds and "
@@ -448,6 +455,7 @@ class VerifyConsumer : public ASTConsumer {
       VOpts.Quiet = Quiet.getValue();
       VOpts.Verbose = Verbose.getValue();
       VOpts.ListFunctions = ListFunctions.getValue();
+      VOpts.ConfirmBound = ConfirmBound.getValue();
       VOpts.Summary = &gSummary;
       if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts))
         ++gVerifyFailures;
@@ -678,6 +686,10 @@ 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(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..826aeddd99 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -752,6 +752,25 @@ 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. 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₁ ∨ …`.
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index dcff8d2b56..cef926c370 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -1894,7 +1894,16 @@ 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. 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.
 - 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..b3e03b481c 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,10 @@ 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 --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 --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..1c34f6f1a2 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,41 @@ 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.
+
 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..783e4e62b3 100644
--- a/website/source/language/functions-loops.rst
+++ b/website/source/language/functions-loops.rst
@@ -638,6 +638,48 @@ 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. 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..0b437a75d7 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -24,6 +24,7 @@ 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 --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
@@ -955,6 +956,17 @@ 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`).
+
 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..a9591207ce 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -483,6 +483,17 @@ 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. A
+failure of a function whose loop has no ``cppverify::decreases`` names that
+loop too (:doc:`language/functions-loops`).
+
 **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,