Fix variable initialization order in snapshot-harness aliasing pointers

The root cause was in the topological sort implementation. The `dfs()`
method enforced that seen and inserted sets must be empty on entry (via
`PRECONDITION`) and would clear them on exit. However,
`topological_sort()` calls `dfs()` multiple times in a loop for each
item in the input collection. This meant only the first item was sorted
correctly; subsequent items would fail the precondition or produce
incorrect results.

The fix moves the set clearing logic to the beginning of
`topological_sort()`, ensuring a fresh DFS traversal for the entire
collection while allowing the DFS to maintain state across recursive
calls within a single item's dependency graph.

Co-authored-by: Kiro autonomous agent

Fixes: #4978

Author: tautschnig

regression/snapshot-harness/dynamic-array-int-ordering/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -14,5 +14,3 @@ a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type in
 VERIFICATION FAILED
 --
 unwinding assertion loop \d+: FAILURE
---
-For more information take a look at github#5351

regression/snapshot-harness/dynamic-array-int/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 array,iterator1,iterator2,iterator3 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -14,6 +14,3 @@ array,iterator1,iterator2,iterator3 --harness-type initialize-with-memory-snapsh
 VERIFICATION FAILED
 --
 unwinding assertion loop \d+: FAILURE
---
-Broken by https://github.com/diffblue/cbmc/issues/4978
-For more information take a look at github#5351

src/goto-harness/memory_snapshot_harness_generator.h

@@ -324,6 +324,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
       auto push_to_output = [&output](const valuet &value) {
         output.push_back(value);
       };
+      // Clear the sets before starting the sort to ensure a fresh traversal
+      seen.clear();
+      inserted.clear();
       for(const auto &item : input)
       {
         dfs(item, associate_key_with_t, push_to_output);
@@ -339,10 +342,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
     template <typename Value, typename Map, typename Handler>
     void dfs(Value &&node, Map &&key_to_t, Handler &&handle)
     {
-      PRECONDITION(seen.empty() && inserted.empty());
       dfs_inner(node, key_to_t, handle);
-      seen.clear();
-      inserted.clear();
     }
 
     template <typename Value, typename Map, typename Handler>