diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc
new file mode 100644
index 00000000000..81ec9c8ed2d
--- /dev/null
+++ b/regression/cbmc/Bitfields3/paths.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --paths lifo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index 9453c077af4..1cd691e5d74 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@@ -4,6 +4,7 @@ cd regression/cbmc
 rm Anonymous_Struct3/test.desc
 rm Array_operations1/test.desc
 rm Bitfields3/test.desc
+rm Bitfields3/paths.desc
 rm Empty_struct1/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index fef369b07e8..f7831f6d1fc 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -20,10 +20,3 @@ void goto_symext::do_simplify(exprt &expr)
   if(symex_config.simplify_opt)
     simplify(expr, ns);
 }
-
-nondet_symbol_exprt symex_nondet_generatort::operator()(typet &type)
-{
-  irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
-  nondet_symbol_exprt new_expr(identifier, type);
-  return new_expr;
-}
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 1706bfd7eaa..ae8b45792a3 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -38,16 +38,6 @@ class namespacet;
 class side_effect_exprt;
 class typecast_exprt;
 
-/// Functor generating fresh nondet symbols
-class symex_nondet_generatort
-{
-public:
-  nondet_symbol_exprt operator()(typet &type);
-
-private:
-  unsigned nondet_count = 0;
-};
-
 /// Configuration of the symbolic execution
 struct symex_configt final
 {
@@ -418,7 +408,6 @@ class goto_symext
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 
-  symex_nondet_generatort build_symex_nondet;
   static unsigned dynamic_counter;
 
   void rewrite_quantifiers(exprt &, statet &);
diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp
index 55a5149d0f6..39cfeaffd5c 100644
--- a/src/goto-symex/path_storage.cpp
+++ b/src/goto-symex/path_storage.cpp
@@ -13,6 +13,12 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
 
+nondet_symbol_exprt symex_nondet_generatort::operator()(const typet &type)
+{
+  irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
+  return nondet_symbol_exprt(identifier, type);
+}
+
 // _____________________________________________________________________________
 // path_lifot
 
diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h
index 981dac697e6..b22c760ad02 100644
--- a/src/goto-symex/path_storage.h
+++ b/src/goto-symex/path_storage.h
@@ -15,6 +15,16 @@
 
 #include <memory>
 
+/// Functor generating fresh nondet symbols
+class symex_nondet_generatort
+{
+public:
+  nondet_symbol_exprt operator()(const typet &type);
+
+private:
+  std::size_t nondet_count = 0;
+};
+
 /// \brief Storage for symbolic execution paths to be resumed later
 ///
 /// This data structure supports saving partially-executed symbolic
@@ -85,6 +95,9 @@ class path_storaget
     return size() == 0;
   };
 
+  /// Counter for nondet objects, which require unique names
+  symex_nondet_generatort build_symex_nondet;
+
 private:
   // Derived classes should override these methods, allowing the base class to
   // enforce preconditions.
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 3e3f49cdd28..9a54375bdf5 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -178,7 +178,7 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    const exprt nondet = build_symex_nondet(*object_type);
+    const exprt nondet = path_storage.build_symex_nondet(*object_type);
     const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
   }
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 394c3f12d45..ac95c8a9158 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -181,7 +181,7 @@ void goto_symext::clean_expr(
   statet &state,
   const bool write)
 {
-  replace_nondet(expr, build_symex_nondet);
+  replace_nondet(expr, path_storage.build_symex_nondet);
   dereference(expr, state, write);
 
   // make sure all remaining byte extract operations use the root