PR feedback

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

src/crab/cfg.hpp

@@ -267,7 +267,6 @@ class cfg_t final {
 
   private:
     basic_block_map_t m_blocks;
-    std::optional<std::vector<label_t>> m_potential_loop_headers;
 
     using visited_t = std::set<label_t>;
 

src/crab/fwd_analyzer.cpp

@@ -125,11 +125,11 @@ std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t
     if (thread_local_options.check_termination) {
         // For every potential loop header, initialize the loop counter to 0.
         for (const auto& label : cfg.potential_loop_headers()) {
-            // The initial path adds labels in the form of (from, to) where
-            // where from is the PC and to is -1. When the CFG is expanded to be non-deterministic
-            // branches with actual to labels are added, but these will not have loop counters as
-            // loop counters are only added to the deterministic cfg.
-            // Ignore labels added by the non-deterministic expansion.
+            // See prepare_cfg() in src/asm_cfg.cpp.
+            // It adds IncrementLoopCounter to blocks that are possible loops, but only
+            // on the first pass, where all labels are in the form from::-1. After the cfg is converted to its
+            // non-deterministic form there will be additional labels in the form of from::to where to will be != -1.
+            // Only initialize the loop counter for the original labels.
             if (label.to != -1) {
                 continue;
             }