PR feedback

Signed-off-by: Alan Jowett <[email protected]>

src/asm_syntax.hpp

@@ -397,6 +397,9 @@ struct Assert {
 struct IncrementLoopCounter {
     label_t name;
     bool operator==(const IncrementLoopCounter&) const = default;
+    // Maximum number of loop iterations allowed during verification.
+    // This prevents infinite loops while allowing reasonable bounded loops.
+    // When exceeded, the verifier will report that it cannot prove termination.
     static constexpr int limit = 100000;
 };
 

src/crab_verifier.cpp

@@ -95,9 +95,8 @@ static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_
     }
 
     if (thread_local_options.check_termination) {
-        const auto last_inv = post_invariants.at(cfg.exit_label());
-
-        // Find the max loop count from any post-invariant.
+        // Calculate the maximum loop count across all post-invariants to detect potential
+        // infinite loops or excessive iterations in any part of the program.
         for (auto [label, inv] : post_invariants) {
             if (inv.is_bottom()) {
                 continue;