Fix segfault in k-induction step case with nested loops

The original code assumed `loop_head->condition()` always contained the
loop guard, but in nested loop scenarios, the loop structure can vary.
The backedge might contain the condition instead, or the loop might be
unconditional.

Also, when processing nested loops, modifying the outer loop's
goto-program could invalidate iterators pointing to the inner loop,
causing memory access violations.

Co-authored-by: Kiro autonomous agent

Fixes: #5357

Author: tautschnig

regression/k-induction/nested-loops/main.c

@@ -0,0 +1,21 @@
+// Test case for nested loops in k-induction instrumentation
+// This used to cause segmentation faults in CBMC versions 5.6 and 5.12
+// when using --step-case because the code incorrectly assumed loop heads
+// always have conditions and didn't handle nested loop iterator invalidation
+int nondet_condition();
+int main()
+{
+  int i = 0;
+  int j = 0;
+  while(i < 10)
+  {
+    while(nondet_condition() == 0)
+    {
+      j++;
+      if(j == 10)
+        j = 0;
+    }
+    __CPROVER_assert(j < 11, "should hold");
+    i++;
+  }
+}

regression/k-induction/nested-loops/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+2
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting k-induction for k=2, base case$
+^Instrumenting k-induction for k=2, step case$
+--
+^warning: ignoring

src/goto-instrument/k_induction.cpp

@@ -11,11 +11,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "k_induction.h"
 
-#include <analyses/natural_loops.h>
-#include <analyses/local_may_alias.h>
+#include <util/expr_util.h>
+#include <util/std_expr.h>
 
 #include <goto-programs/remove_skip.h>
 
+#include <analyses/local_may_alias.h>
+#include <analyses/natural_loops.h>
+
 #include "havoc_utils.h"
 #include "loop_utils.h"
 #include "unwind.h"
@@ -66,13 +69,44 @@ void k_inductiont::process_loop(
 {
   PRECONDITION(!loop.empty());
 
-  // save the loop guard
-  const exprt loop_guard = loop_head->condition();
-
   // compute the loop exit
   goto_programt::targett loop_exit=
     get_loop_exit(loop);
 
+  // Find the loop guard. The loop condition can be in one of two places:
+  // 1. In the backwards goto at the end of the loop (the backedge)
+  // 2. In a forward goto at the loop head that targets the loop exit
+
+  // Find the backwards goto (backedge) for this loop
+  goto_programt::targett backedge = loop_exit;
+  for(loopt::const_iterator it = loop.begin(); it != loop.end(); ++it)
+  {
+    if((*it)->is_backwards_goto() && (*it)->get_target() == loop_head)
+    {
+      backedge = *it;
+      break;
+    }
+  }
+
+  exprt loop_guard;
+
+  if(backedge != loop_exit && !backedge->condition().is_true())
+  {
+    // condition in backedge
+    loop_guard = backedge->condition();
+  }
+  else if(loop_head->is_goto())
+  {
+    if(loop_head->get_target() == loop_exit) // condition in forward edge
+      loop_guard = boolean_negate(loop_head->condition());
+    else
+      loop_guard = true_exprt(); // unconditional loop
+  }
+  else
+  {
+    loop_guard = true_exprt(); // unconditional loop
+  }
+
   if(base_case)
   {
     // now unwind k times
@@ -157,12 +191,52 @@ void k_inductiont::process_loop(
 void k_inductiont::k_induction()
 {
   // iterate over the (natural) loops in the function
+  // We need to be careful with nested loops, as processing the outer loop
+  // might invalidate iterators for the inner loop. So we collect all loops
+  // first, then process only outermost loops.
+
+  std::vector<std::pair<goto_programt::targett, loopt>> loops_to_process;
 
   for(natural_loops_mutablet::loop_mapt::const_iterator
       l_it=natural_loops.loop_map.begin();
       l_it!=natural_loops.loop_map.end();
       l_it++)
-    process_loop(l_it->first, l_it->second);
+  {
+    // Check if this loop is nested within another loop
+    bool is_nested = false;
+    goto_programt::targett loop_head = l_it->first;
+
+    for(natural_loops_mutablet::loop_mapt::const_iterator other_it =
+          natural_loops.loop_map.begin();
+        other_it != natural_loops.loop_map.end();
+        other_it++)
+    {
+      if(other_it == l_it)
+        continue; // skip self
+
+      // Check if loop_head is contained within other_it's loop
+      const loopt &other_loop = other_it->second;
+      if(
+        std::find(other_loop.begin(), other_loop.end(), loop_head) !=
+        other_loop.end())
+      {
+        is_nested = true;
+        break;
+      }
+    }
+
+    // Only process outermost loops to avoid iterator invalidation
+    if(!is_nested)
+    {
+      loops_to_process.push_back(std::make_pair(l_it->first, l_it->second));
+    }
+  }
+
+  // Now process the outermost loops
+  for(auto &loop_pair : loops_to_process)
+  {
+    process_loop(loop_pair.first, loop_pair.second);
+  }
 }
 
 void k_induction(