Clarify logic

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

src/crab/fwd_analyzer.cpp

@@ -125,7 +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()) {
-            // Skip non-deterministic blocks. Only deterministic blocks have loop counters.
+            // 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.
             if (label.to != -1) {
                 continue;
             }