diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index f1befc993b3..d12604562ff 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -19,6 +19,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/contracts.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
+      contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
       contracts/dynamic-frames/dfcc_pointer_in_range.cpp \
       contracts/dynamic-frames/dfcc_is_freeable.cpp \
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
new file mode 100644
index 00000000000..210aec5746c
--- /dev/null
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, delmasrd@amazon.com
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_is_cprover_symbol.h"
+
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
+#include <util/suffix.h>
+
+bool dfcc_is_cprover_symbol(const irep_idt &id)
+{
+  std::string str = id2string(id);
+  return has_prefix(str, CPROVER_PREFIX) || has_prefix(str, "__VERIFIER") ||
+         has_prefix(str, "nondet") || has_suffix(str, "$object");
+}
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h
new file mode 100644
index 00000000000..9b3d3699002
--- /dev/null
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h
@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, delmasrd@amazon.com
+
+Date: March 2023
+
+\*******************************************************************/
+
+/// \file
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_CPROVER_SYMBOL_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_CPROVER_SYMBOL_H
+
+#include <util/irep.h>
+
+/// \return True iff the id starts with CPROVER_PREFIX, `__VERIFIER`, `nondet`
+/// or ends with `$object`.
+bool dfcc_is_cprover_symbol(const irep_idt &id);
+
+#endif