diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp
index cc0d13e1a0b..a2a863af064 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp
@@ -457,14 +457,6 @@ exprt dfcc_utilst::make_sizeof_expr(const exprt &expr)
   return size.value();
 }
 
-exprt dfcc_utilst::make_map_start_address(const exprt &expr)
-{
-  return typecast_exprt::conditional_cast(
-    address_of_exprt(index_exprt(
-      expr, from_integer(0, to_array_type(expr.type()).index_type()))),
-    pointer_type(bool_typet()));
-}
-
 void dfcc_utilst::inline_function(const irep_idt &function_id)
 {
   auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
index 7524d1845ea..5d9f5319d9e 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
@@ -195,9 +195,6 @@ class dfcc_utilst
   /// \brief Returns the expression `sizeof(expr)`.
   exprt make_sizeof_expr(const exprt &expr);
 
-  /// \brief Returns the expression `&expr[0]`
-  exprt make_map_start_address(const exprt &expr);
-
   /// \brief Inlines the given function, aborts on recursive calls during
   /// inlining.
   void inline_function(const irep_idt &function_id);