fix(detect): never prove post-loop conditions from a bounded unroll

The dead-branch, always-condition and unreachable walkers unroll loops
loop_unroll times, following only the path on which the guard holds.
When the guard could also be false (any symbolic bound), that early
exit was dropped, and the loop's assigned variables were havocked only
for loops containing calls. The state after the loop was therefore
"the loop ran exactly loop_unroll times", and conditions on it were
reported as Proved:

  int s = 0; for (unsigned i = 0; i < n; ++i) s += 1;
  if (s == 0) ...   // "dead" proved/exact, "always false" proved

The same held for `s > 100`, while loops, and a `break` out of a
constant loop. On the audit probes this was 7 Proved findings, all
false.

LoopUnrollExits now records whether the unroll saw every way out of
the loop: no iteration could exit early (the guard's false branch was
infeasible), the unroll stopped because the guard became infeasible
rather than because loop_unroll ran out, and the body has no break or
goto that escapes. When any of that fails, the walker havocs the loop's
assigned variables and restores the entry path, as it already did for
opaque loops. A loop the unroll exits exactly (constant bound within
budget) keeps its precise state, so a genuinely dead branch after it
is still Proved.

Loop-bound provenance (--suppress-loop-bound-always-conditions) stays
off by default: it existed to downgrade proofs that leaned on the
unroll bound, and an inexact loop exit now havocs instead of producing
such a proof in the first place.

The duplicated helpers (containsCallExpr, collectAssignedVars,
appendAssignedVars, havocAssignedVars) move from dead_branch.cpp and
always_condition.cpp into detect/loop_havoc so all three walkers share
them; dead_branch.cpp drops under the 800-line soft cap.

Tests: test_loop_exit_soundness covers the symbolic-bound cases for all
three detectors (4 Proved each for dead and always-condition before),
the break escape, the exact-loop negative control, and the extracted
helpers (containsLoopEscape, LoopUnrollExits). Full suite 136/136.

include/fold/detect/loop_havoc.hpp

@@ -0,0 +1,66 @@
+#pragma once
+
+#include <vector>
+
+#include "fold/symbolic/encoder.hpp"
+
+namespace clang {
+class Stmt;
+class VarDecl;
+} // namespace clang
+
+namespace fold::detect {
+
+// Shared by the control-flow walkers (dead-branch, always-condition,
+// unreachable) that unroll loops a bounded number of times.
+
+[[nodiscard]] bool containsCallExpr(const clang::Stmt* stmt);
+
+// Variables assigned (=, op=, ++, --) anywhere in `stmt`, canonical decls, in
+// first-seen order.
+[[nodiscard]] std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt);
+void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
+                        const std::vector<const clang::VarDecl*>& extra);
+
+// Replace each assigned bitvector variable with a fresh unknown and drop
+// access-path facts: after this, nothing about their post-loop values is known.
+void havocAssignedVars(SymbolicEnv& env, const std::vector<const clang::VarDecl*>& vars);
+
+// A `break` or `goto` in `body` that leaves the loop (a `break` inside a nested
+// loop or switch does not). Such an exit carries state the unroll never
+// follows.
+[[nodiscard]] bool containsLoopEscape(const clang::Stmt* body);
+
+// Whether a bounded unroll saw every way out of a loop.
+//
+// The walkers follow only the path on which the loop guard holds. The state
+// they reach after the loop is exact only if no iteration could have exited
+// early, the unroll stopped because the guard became infeasible (not because
+// loop_unroll ran out), and the body has no escaping break/goto. Otherwise the
+// caller must havoc the loop's assigned variables and restore the entry path,
+// or a condition after the loop is "proved" from the loop having run exactly
+// loop_unroll times.
+class LoopUnrollExits {
+  public:
+    explicit LoopUnrollExits(const clang::Stmt* body);
+
+    // The guard could not be encoded, or it was not assumed (tracked
+    // loop-bound assumptions are active): the exits were not modeled.
+    void guardNotModeled() { exact_ = false; }
+
+    // Record one guard evaluation. Returns false when the loop certainly exits
+    // here (the guard cannot hold), so the unroll should stop.
+    bool guard(bool may_continue, bool may_exit);
+
+    // The body walk stopped early (return/abort inside the body).
+    void bodyStopped() { exact_ = false; }
+
+    // The unroll left the loop along its only exit.
+    [[nodiscard]] bool exact() const { return exact_ && exited_; }
+
+  private:
+    bool exact_ = true;
+    bool exited_ = false;
+};
+
+} // namespace fold::detect

src/detect/always_condition.cpp

@@ -22,6 +22,7 @@
 #include <vector>
 
 #include "fold/detect/incremental_cache.hpp"
+#include "fold/detect/loop_havoc.hpp"
 #include "fold/symbolic/assumption_provenance.hpp"
 #include "fold/symbolic/cfg_helpers.hpp"
 #include "fold/symbolic/encoder.hpp"
@@ -87,80 +88,10 @@ bool isMacroBodyStatement(const clang::Stmt* stmt, const clang::ASTContext& ctx)
     return loc.isValid() && sm.isMacroBodyExpansion(loc);
 }
 
-bool containsCallExpr(const clang::Stmt* stmt) {
-    if (!stmt)
-        return false;
-    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
-        bool found = false;
-        bool VisitCallExpr(clang::CallExpr*) {
-            found = true;
-            return false;
-        }
-    } visitor;
-    visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
-    return visitor.found;
-}
-
-std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt) {
-    if (!stmt)
-        return {};
-    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
-        std::vector<const clang::VarDecl*> vars;
-        std::unordered_set<const clang::VarDecl*> seen;
-
-        void add(const clang::VarDecl* vd) {
-            if (!vd)
-                return;
-            vd = vd->getCanonicalDecl();
-            if (seen.insert(vd).second)
-                vars.push_back(vd);
-        }
-
-        bool VisitBinaryOperator(clang::BinaryOperator* op) {
-            if (!op || !op->isAssignmentOp())
-                return true;
-            const auto* lhs = op->getLHS()->IgnoreParenImpCasts();
-            if (const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(lhs))
-                add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
-            return true;
-        }
-
-        bool VisitUnaryOperator(clang::UnaryOperator* op) {
-            if (!op || !op->isIncrementDecrementOp())
-                return true;
-            const auto* sub = op->getSubExpr()->IgnoreParenImpCasts();
-            if (const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(sub))
-                add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
-            return true;
-        }
-    } visitor;
-    visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
-    return visitor.vars;
-}
-
-void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
-                        const std::vector<const clang::VarDecl*>& extra) {
-    if (vars.empty()) {
-        vars = extra;
-        return;
-    }
-    std::unordered_set<const clang::VarDecl*> seen(vars.begin(), vars.end());
-    for (const auto* vd : extra) {
-        if (vd && seen.insert(vd).second)
-            vars.push_back(vd);
-    }
-}
-
-void havocAssignedVars(SymbolicEnv& env, const std::vector<const clang::VarDecl*>& vars) {
-    for (const clang::VarDecl* vd : vars) {
-        auto current = env.tryGet(vd);
-        if (!current || !current->is_bv())
-            continue;
-        env.replace(vd, env.freshUnknown(current->get_sort().bv_size()));
-    }
-    env.clearAccessPathFacts();
-    env.markLoopHavoc();
-}
+using detect::appendAssignedVars;
+using detect::collectAssignedVars;
+using detect::containsCallExpr;
+using detect::havocAssignedVars;
 
 class AlwaysConditionWalker {
   public:
@@ -351,43 +282,54 @@ class AlwaysConditionWalker {
                     SymbolicEnv& env) {
         const bool opaque_loop =
             containsCallExpr(cond) || containsCallExpr(body) || containsCallExpr(inc);
-        std::vector<const clang::VarDecl*> assigned;
-        if (opaque_loop) {
-            assigned = collectAssignedVars(cond);
-            appendAssignedVars(assigned, collectAssignedVars(body));
-            appendAssignedVars(assigned, collectAssignedVars(inc));
-        }
+        std::vector<const clang::VarDecl*> assigned = collectAssignedVars(cond);
+        appendAssignedVars(assigned, collectAssignedVars(body));
+        appendAssignedVars(assigned, collectAssignedVars(inc));
         const z3::expr entry_path = env.currentPath();
+        detect::LoopUnrollExits exits(body);
         for (int iter = 0; iter < budget_.loop_unroll; ++iter) {
             if (cond) {
                 const EncodingPrecisionContext precision_before = env.tag();
                 z3::expr guard = encodeCondition(cond, ctx_, env);
-                if (precisionWorsened(precision_before, env))
+                if (precisionWorsened(precision_before, env)) {
+                    exits.guardNotModeled();
                     break;
+                }
                 if (env.trackedAssumptions().empty()) {
                     SourcePathAssumeOptions options{
                         .prune_infeasible = true,
                         .timeout_ms = static_cast<unsigned>(budget_.per_query.count())};
                     auto assumed = SourcePathState{env}.assume(guard, options);
-                    if (!assumed.truthy.has_value())
+                    if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value()))
                         break;
                     env = std::move(assumed.truthy->env());
+                } else {
+                    exits.guardNotModeled();
                 }
+            } else {
+                exits.guardNotModeled();
             }
-            if (!body)
+            if (!body) {
+                exits.bodyStopped();
                 break;
+            }
             {
                 ++loop_depth_;
                 bool ok = walk(body, env);
                 --loop_depth_;
-                if (!ok)
+                if (!ok) {
+                    exits.bodyStopped();
                     break;
+                }
             }
             if (inc) {
                 (void)encodeExpr(inc, ctx_, env);
             }
         }
-        if (opaque_loop) {
+        // Unless the unroll left the loop along its only exit, the state here
+        // is "the loop ran some prefix of iterations": keeping it would prove
+        // post-loop conditions from a trip count the program need not take.
+        if (opaque_loop || !exits.exact()) {
             havocAssignedVars(env, assigned);
             env.restorePath(entry_path);
         }

src/detect/dead_branch.cpp

@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "fold/detect/incremental_cache.hpp"
+#include "fold/detect/loop_havoc.hpp"
 #include "fold/frontend/stable_identity.hpp"
 #include "fold/symbolic/assumption_provenance.hpp"
 #include "fold/symbolic/cfg_helpers.hpp"
@@ -198,76 +199,10 @@ bool isMacroBodyStatement(const clang::Stmt* stmt, const clang::ASTContext& ctx)
     return loc.isValid() && sm.isMacroBodyExpansion(loc);
 }
 
-bool containsCallExpr(const clang::Stmt* stmt) {
-    if (!stmt)
-        return false;
-    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
-        bool found = false;
-        bool VisitCallExpr(clang::CallExpr*) {
-            found = true;
-            return false;
-        }
-    } visitor;
-    visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
-    return visitor.found;
-}
-
-std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt) {
-    if (!stmt)
-        return {};
-    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
-        std::vector<const clang::VarDecl*> vars;
-        std::unordered_set<const clang::VarDecl*> seen;
-
-        void add(const clang::VarDecl* vd) {
-            if (!vd)
-                return;
-            vd = vd->getCanonicalDecl();
-            if (seen.insert(vd).second)
-                vars.push_back(vd);
-        }
-
-        bool VisitBinaryOperator(clang::BinaryOperator* op) {
-            if (!op || !op->isAssignmentOp())
-                return true;
-            const auto* lhs = op->getLHS()->IgnoreParenImpCasts();
-            if (const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(lhs))
-                add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
-            return true;
-        }
-
-        bool VisitUnaryOperator(clang::UnaryOperator* op) {
-            if (!op || !op->isIncrementDecrementOp())
-                return true;
-            const auto* sub = op->getSubExpr()->IgnoreParenImpCasts();
-            if (const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(sub))
-                add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
-            return true;
-        }
-    } visitor;
-    visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
-    return visitor.vars;
-}
-
-void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
-                        const std::vector<const clang::VarDecl*>& extra) {
-    std::unordered_set<const clang::VarDecl*> seen(vars.begin(), vars.end());
-    for (const auto* vd : extra) {
-        if (vd && seen.insert(vd).second)
-            vars.push_back(vd);
-    }
-}
-
-void havocAssignedVars(SymbolicEnv& env, const std::vector<const clang::VarDecl*>& vars) {
-    for (const clang::VarDecl* vd : vars) {
-        auto current = env.tryGet(vd);
-        if (!current || !current->is_bv())
-            continue;
-        env.replace(vd, env.freshUnknown(current->get_sort().bv_size()));
-    }
-    env.clearAccessPathFacts();
-    env.markLoopHavoc();
-}
+using detect::appendAssignedVars;
+using detect::collectAssignedVars;
+using detect::containsCallExpr;
+using detect::havocAssignedVars;
 
 // Recursively walk the body, threading (env, path_predicate). At each IfStmt,
 // SAT-check each arm before descending. Branch state is forked so an
@@ -373,38 +308,52 @@ class BodyWalker {
         appendAssignedVars(assigned, collectAssignedVars(body));
         appendAssignedVars(assigned, collectAssignedVars(inc));
         const z3::expr entry_path = path;
+        detect::LoopUnrollExits exits(body);
         for (int iter = 0; iter < budget_.loop_unroll; ++iter) {
             z3::expr body_path = path;
             if (cond) {
                 const EncodingPrecisionContext precision_before = env.tag();
                 z3::expr guard = encodeCondition(cond, ctx_, env);
-                if (precisionWorsened(precision_before, env))
+                if (precisionWorsened(precision_before, env)) {
+                    exits.guardNotModeled();
                     break;
+                }
                 if (env.trackedAssumptions().empty()) {
                     SourcePathAssumeOptions options{
                         .prune_infeasible = true,
                         .timeout_ms = static_cast<unsigned>(budget_.per_query.count())};
                     auto assumed = SourcePathState{env}.withPath(path).assume(guard, options);
-                    if (!assumed.truthy.has_value())
+                    if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value()))
                         break;
                     env = std::move(assumed.truthy->env());
                     body_path = env.currentPath();
+                } else {
+                    exits.guardNotModeled();
                 }
+            } else {
+                exits.guardNotModeled();
             }
-            if (!body)
+            if (!body) {
+                exits.bodyStopped();
                 break;
+            }
             {
                 ++loop_depth_;
                 bool ok = walk(body, env, body_path);
                 --loop_depth_;
-                if (!ok)
+                if (!ok) {
+                    exits.bodyStopped();
                     break;
+                }
             }
             if (inc) {
                 (void)encodeExpr(inc, ctx_, env);
             }
         }
-        if (opaque_loop) {
+        // Unless the unroll left the loop along its only exit, the state here
+        // is "the loop ran some prefix of iterations": keeping it would prove
+        // post-loop conditions from a trip count the program need not take.
+        if (opaque_loop || !exits.exact()) {
             havocAssignedVars(env, assigned);
             path = entry_path;
         }

src/detect/loop_havoc.cpp

@@ -0,0 +1,125 @@
+#include "fold/detect/loop_havoc.hpp"
+
+#include <clang/AST/RecursiveASTVisitor.h>
+#include <clang/AST/Stmt.h>
+#include <clang/AST/StmtCXX.h>
+
+#include <unordered_set>
+
+namespace fold::detect {
+
+bool containsCallExpr(const clang::Stmt* stmt) {
+    if (!stmt)
+        return false;
+    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
+        bool found = false;
+        bool VisitCallExpr(clang::CallExpr*) {
+            found = true;
+            return false;
+        }
+    } visitor;
+    visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
+    return visitor.found;
+}
+
+std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt) {
+    if (!stmt)
+        return {};
+    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
+        std::vector<const clang::VarDecl*> vars;
+        std::unordered_set<const clang::VarDecl*> seen;
+
+        void add(const clang::VarDecl* vd) {
+            if (!vd)
+                return;
+            vd = vd->getCanonicalDecl();
+            if (seen.insert(vd).second)
+                vars.push_back(vd);
+        }
+
+        bool VisitBinaryOperator(clang::BinaryOperator* op) {
+            if (!op || !op->isAssignmentOp())
+                return true;
+            const auto* lhs = op->getLHS()->IgnoreParenImpCasts();
+            if (const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(lhs))
+                add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
+            return true;
+        }
+
+        bool VisitUnaryOperator(clang::UnaryOperator* op) {
+            if (!op || !op->isIncrementDecrementOp())
+                return true;
+            const auto* sub = op->getSubExpr()->IgnoreParenImpCasts();
+            if (const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(sub))
+                add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
+            return true;
+        }
+    } visitor;
+    visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
+    return visitor.vars;
+}
+
+void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
+                        const std::vector<const clang::VarDecl*>& extra) {
+    std::unordered_set<const clang::VarDecl*> seen(vars.begin(), vars.end());
+    for (const auto* vd : extra) {
+        if (vd && seen.insert(vd).second)
+            vars.push_back(vd);
+    }
+}
+
+void havocAssignedVars(SymbolicEnv& env, const std::vector<const clang::VarDecl*>& vars) {
+    for (const clang::VarDecl* vd : vars) {
+        auto current = env.tryGet(vd);
+        if (!current || !current->is_bv())
+            continue;
+        env.replace(vd, env.freshUnknown(current->get_sort().bv_size()));
+    }
+    env.clearAccessPathFacts();
+    env.markLoopHavoc();
+}
+
+namespace {
+
+// Walks a loop body tracking how many loops/switches enclose each statement,
+// so only a break that targets the loop being unrolled counts.
+bool escapes(const clang::Stmt* stmt, int breakable_depth) {
+    if (!stmt)
+        return false;
+    if (clang::isa<clang::GotoStmt>(stmt) || clang::isa<clang::IndirectGotoStmt>(stmt))
+        return true;
+    if (clang::isa<clang::BreakStmt>(stmt))
+        return breakable_depth == 0;
+    const bool breakable = clang::isa<clang::ForStmt>(stmt) || clang::isa<clang::WhileStmt>(stmt) ||
+                           clang::isa<clang::DoStmt>(stmt) ||
+                           clang::isa<clang::CXXForRangeStmt>(stmt) ||
+                           clang::isa<clang::SwitchStmt>(stmt);
+    for (const clang::Stmt* child : stmt->children()) {
+        if (escapes(child, breakable_depth + (breakable ? 1 : 0)))
+            return true;
+    }
+    return false;
+}
+
+} // namespace
+
+bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0); }
+
+LoopUnrollExits::LoopUnrollExits(const clang::Stmt* body) {
+    if (containsLoopEscape(body))
+        exact_ = false;
+}
+
+bool LoopUnrollExits::guard(bool may_continue, bool may_exit) {
+    if (!may_continue) {
+        exited_ = true;
+        return false;
+    }
+    // Both branches feasible: the loop may exit at this iteration, and that
+    // exit's state is not the one the unroll carries forward.
+    if (may_exit)
+        exact_ = false;
+    return true;
+}
+
+} // namespace fold::detect

src/detect/meson.build

@@ -12,6 +12,7 @@ fold_core_sources += files(
   'clone.cpp',
   'clone_hash_cache.cpp',
   'dead_branch.cpp',
+  'loop_havoc.cpp',
   'dead_statement.cpp',
   'complexity.cpp',
   'equiv.cpp',

src/detect/unreachable.cpp

@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "fold/detect/incremental_cache.hpp"
+#include "fold/detect/loop_havoc.hpp"
 #include "fold/symbolic/cfg_helpers.hpp"
 #include "fold/symbolic/encoder.hpp"
 #include "fold/symbolic/loop_bound_pin.hpp"
@@ -230,32 +231,52 @@ class UnreachableBodyWalker {
 
     bool unrollLoop(const clang::Expr* cond, const clang::Stmt* body, const clang::Expr* inc,
                     SymbolicEnv& env, z3::expr& path) {
+        std::vector<const clang::VarDecl*> assigned = detect::collectAssignedVars(cond);
+        detect::appendAssignedVars(assigned, detect::collectAssignedVars(body));
+        detect::appendAssignedVars(assigned, detect::collectAssignedVars(inc));
+        const z3::expr entry_path = path;
+        detect::LoopUnrollExits exits(body);
         for (int iter = 0; iter < budget_.loop_unroll; ++iter) {
             z3::expr body_path = path;
             if (cond) {
                 const EncodingPrecisionContext precision_before = env.tag();
                 z3::expr guard = encodeCondition(cond, ctx_, env);
-                if (precisionWorsened(precision_before, env))
+                if (precisionWorsened(precision_before, env)) {
+                    exits.guardNotModeled();
                     break;
+                }
                 if (env.trackedAssumptions().empty()) {
                     SourcePathAssumeOptions options{
                         .prune_infeasible = true,
                         .timeout_ms = static_cast<unsigned>(budget_.per_query.count())};
                     auto assumed = SourcePathState{env}.withPath(path).assume(guard, options);
-                    if (!assumed.truthy.has_value())
+                    if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value()))
                         break;
                     env = std::move(assumed.truthy->env());
                     body_path = env.currentPath();
+                } else {
+                    exits.guardNotModeled();
                 }
+            } else {
+                exits.guardNotModeled();
             }
-            if (!body)
+            if (!body) {
+                exits.bodyStopped();
                 break;
-            if (!walk(body, env, body_path))
+            }
+            if (!walk(body, env, body_path)) {
+                exits.bodyStopped();
                 break;
+            }
             if (inc) {
                 (void)encodeExpr(inc, ctx_, env);
             }
         }
+        // The same loop-exit soundness rule as dead-branch / always-condition.
+        if (!exits.exact()) {
+            detect::havocAssignedVars(env, assigned);
+            path = entry_path;
+        }
         return true;
     }
 

tests/unit/meson.build

@@ -186,6 +186,15 @@ test_always_condition_freestanding = executable(
 )
 test('always_condition_freestanding', test_always_condition_freestanding)
 
+test_loop_exit_soundness = executable(
+  'test_loop_exit_soundness',
+  'test_loop_exit_soundness.cpp',
+  dependencies: [fold_core_dep, catch2_dep],
+  install: false,
+  build_by_default: false,
+)
+test('loop_exit_soundness', test_loop_exit_soundness)
+
 test_batch_safety_observer = executable(
   'test_batch_safety_observer',
   'test_batch_safety_observer.cpp',

tests/unit/test_loop_exit_soundness.cpp

@@ -0,0 +1,179 @@
+#include <clang/AST/RecursiveASTVisitor.h>
+#include <clang/Frontend/ASTUnit.h>
+#include <clang/Tooling/Tooling.h>
+
+#include <catch2/catch_test_macros.hpp>
+#include <memory>
+#include <string>
+#include <vector>
+
+#include "fold/detect/always_condition.hpp"
+#include "fold/detect/dead_branch.hpp"
+#include "fold/detect/loop_havoc.hpp"
+#include "fold/detect/unreachable.hpp"
+#include "fold/report/finding.hpp"
+#include "fold/symbolic/budget.hpp"
+#include "fold/symbolic/modeling_options.hpp"
+
+// Bounded loop unrolling followed only the path on which the loop guard stays
+// true. When the guard could also be false (a symbolic bound), that early exit
+// was dropped, so the state after the loop was "the loop ran loop_unroll
+// times" and conditions on it were reported as Proved dead / always-true or
+// always-false. These cases were all Proved before the fix.
+
+namespace {
+
+std::unique_ptr<clang::ASTUnit> parse(const std::string& code) {
+    return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
+}
+
+std::vector<fold::Finding> runDead(const std::string& code) {
+    auto unit = parse(code);
+    REQUIRE(unit);
+    fold::SolverBudget b;
+    fold::SolverStats s;
+    return fold::detectDeadBranchesInContext(unit->getASTContext(), b, s);
+}
+
+std::vector<fold::Finding> runAlways(const std::string& code) {
+    auto unit = parse(code);
+    REQUIRE(unit);
+    fold::SolverBudget b;
+    fold::SolverStats s;
+    return fold::detectAlwaysConditionsInContext(unit->getASTContext(), b, s);
+}
+
+std::vector<fold::Finding> runUnreachable(const std::string& code) {
+    auto unit = parse(code);
+    REQUIRE(unit);
+    fold::SolverBudget b;
+    fold::SolverStats s;
+    return fold::detectUnreachableCodeInContext(unit->getASTContext(), b, s);
+}
+
+std::size_t proved(const std::vector<fold::Finding>& findings) {
+    std::size_t n = 0;
+    for (const auto& f : findings)
+        if (f.confidence == fold::Confidence::Proved)
+            ++n;
+    return n;
+}
+
+// Symbolic bound: the loop may run zero times, or more than loop_unroll times.
+const std::string kSymbolicLoops =
+    "int a0(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }"
+    "  if (s == 0) return 7; return 0; }\n"
+    "int a1(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }"
+    "  if (s > 100) return 7; return 0; }\n"
+    "int a2(unsigned n) { int s = 0; while (n > 0) { s += 1; n--; }"
+    "  if (s == 0) return 7; return 0; }\n"
+    "int a3(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }"
+    "  if (s > 5) return 1; return 0; }\n";
+
+// Constant bound within the unroll budget: the unroll sees the loop's only
+// exit, so the post-loop state is exact and a genuinely dead branch stays
+// provable.
+const std::string kExactLoop = "int e(int x) { int s = 0; for (int i = 0; i < 3; ++i) { s += 1; }"
+                               "  if (s == 7) return -1; return s + x; }\n";
+
+// Constant bound, but a `break` offers a second way out whose state the
+// unroll does not follow.
+const std::string kBreakLoop =
+    "int b(int x) { int s = 0; for (int i = 0; i < 3; ++i) { if (x == i) break; s += 1; }"
+    "  if (s == 0) return -1; return s; }\n";
+
+} // namespace
+
+TEST_CASE("dead: a branch after a symbolic-bound loop is not proven dead", "[dead][loop]") {
+    CHECK(proved(runDead(kSymbolicLoops)) == 0);
+}
+
+TEST_CASE("always-condition: a condition after a symbolic-bound loop is not proven constant",
+          "[always][loop]") {
+    CHECK(proved(runAlways(kSymbolicLoops)) == 0);
+}
+
+TEST_CASE("unreachable: code after a symbolic-bound loop is not proven unreachable",
+          "[unreachable][loop]") {
+    CHECK(proved(runUnreachable(kSymbolicLoops)) == 0);
+}
+
+TEST_CASE("dead: a loop the unroll exits exactly keeps its precision", "[dead][loop]") {
+    // Negative control for the fix: havocking every loop would silence this too.
+    CHECK(proved(runDead(kExactLoop)) == 1);
+}
+
+TEST_CASE("dead: a break out of a constant loop is an exit the unroll did not follow",
+          "[dead][loop]") {
+    CHECK(proved(runDead(kBreakLoop)) == 0);
+}
+
+namespace {
+
+// The body of the first loop statement in the translation unit.
+const clang::Stmt* firstLoopBody(clang::ASTUnit& unit) {
+    struct Finder : clang::RecursiveASTVisitor<Finder> {
+        const clang::Stmt* body = nullptr;
+        bool VisitForStmt(clang::ForStmt* s) {
+            if (!body)
+                body = s->getBody();
+            return true;
+        }
+        bool VisitWhileStmt(clang::WhileStmt* s) {
+            if (!body)
+                body = s->getBody();
+            return true;
+        }
+    } finder;
+    finder.TraverseDecl(unit.getASTContext().getTranslationUnitDecl());
+    return finder.body;
+}
+
+bool escapesIn(const std::string& code) {
+    auto unit = parse(code);
+    REQUIRE(unit);
+    const auto* body = firstLoopBody(*unit);
+    REQUIRE(body);
+    return fold::detect::containsLoopEscape(body);
+}
+
+} // namespace
+
+TEST_CASE("loop escape: a break out of the loop escapes; a nested one does not", "[loop_havoc]") {
+    CHECK(escapesIn("void f(int x){ for(int i=0;i<3;++i){ if(x) break; } }"));
+    CHECK(escapesIn("void f(int x){ while(x){ goto out; } out:; }"));
+    CHECK_FALSE(escapesIn("void f(int x){ for(int i=0;i<3;++i){ for(;;){ break; } } }"));
+    CHECK_FALSE(escapesIn(
+        "void f(int x){ for(int i=0;i<3;++i){ switch(x){ case 1: break; default: break; } } }"));
+    CHECK_FALSE(escapesIn("void f(int x){ for(int i=0;i<3;++i){ x += i; } }"));
+}
+
+TEST_CASE("loop exits: exact only when the unroll leaves along the only exit", "[loop_havoc]") {
+    SECTION("guard falsified after iterations that could not exit") {
+        fold::detect::LoopUnrollExits exits(nullptr);
+        CHECK(exits.guard(/*may_continue=*/true, /*may_exit=*/false));
+        CHECK_FALSE(exits.guard(/*may_continue=*/false, /*may_exit=*/true));
+        CHECK(exits.exact());
+    }
+    SECTION("an iteration that could also exit makes the state inexact") {
+        fold::detect::LoopUnrollExits exits(nullptr);
+        CHECK(exits.guard(true, true));
+        CHECK_FALSE(exits.guard(false, true));
+        CHECK_FALSE(exits.exact());
+    }
+    SECTION("the unroll budget running out is not an exit") {
+        fold::detect::LoopUnrollExits exits(nullptr);
+        CHECK(exits.guard(true, false));
+        CHECK_FALSE(exits.exact());
+    }
+    SECTION("an unmodeled guard or a stopped body is never exact") {
+        fold::detect::LoopUnrollExits unmodeled(nullptr);
+        unmodeled.guardNotModeled();
+        CHECK_FALSE(unmodeled.guard(false, true));
+        CHECK_FALSE(unmodeled.exact());
+        fold::detect::LoopUnrollExits stopped(nullptr);
+        stopped.bodyStopped();
+        CHECK_FALSE(stopped.guard(false, true));
+        CHECK_FALSE(stopped.exact());
+    }
+}