diff --git a/regression/snapshot-harness/dynamic-array-int-ordering/test.desc b/regression/snapshot-harness/dynamic-array-int-ordering/test.desc
index cc65ba43d83..7164950c762 100644
--- a/regression/snapshot-harness/dynamic-array-int-ordering/test.desc
+++ b/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
diff --git a/regression/snapshot-harness/dynamic-array-int/test.desc b/regression/snapshot-harness/dynamic-array-int/test.desc
index 3178475a0ba..0395cff2ea1 100644
--- a/regression/snapshot-harness/dynamic-array-int/test.desc
+++ b/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
diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h
index 52a51fc2560..aa60431263f 100644
--- a/src/goto-harness/memory_snapshot_harness_generator.h
+++ b/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>