diff --git a/regression/contracts/entry_point/main.c b/regression/contracts/entry_point/main.c
new file mode 100644
index 00000000000..151bc7306c2
--- /dev/null
+++ b/regression/contracts/entry_point/main.c
@@ -0,0 +1,9 @@
+int foo(char *arr, unsigned int size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr &&size > 0: arr[0])
+// clang-format on
+{
+  if(arr && size > 0)
+    arr[0] = 1;
+}
diff --git a/regression/contracts/entry_point/test.desc b/regression/contracts/entry_point/test.desc
new file mode 100644
index 00000000000..ee6f79d660d
--- /dev/null
+++ b/regression/contracts/entry_point/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo _ --function foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can use a function with a contract as entry point
+for the analysis when its contract gets enforced.
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index bdcb1b5a9c0..62afc6c2ca5 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -130,7 +130,7 @@ bool ansi_c_entry_point(
       if(s_it==symbol_table.symbols.end())
         continue;
 
-      if(s_it->second.type.id()==ID_code)
+      if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
         matches.push_back(symbol_name_entry.second);
     }
 
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 287c9f0e13f..a10ae5847e2 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -877,8 +877,8 @@ void c_typecheck_baset::typecheck_declaration(
         // create a contract symbol
         symbolt contract;
         contract.name = "contract::" + id2string(new_symbol.name);
-        contract.base_name = new_symbol.name;
-        contract.pretty_name = new_symbol.name;
+        contract.base_name = new_symbol.base_name;
+        contract.pretty_name = new_symbol.pretty_name;
         contract.is_property = true;
         contract.type = code_type;
         contract.mode = new_symbol.mode;
diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp
index 6e10ec8ee87..acd6a01211c 100644
--- a/src/goto-instrument/interrupt.cpp
+++ b/src/goto-instrument/interrupt.cpp
@@ -165,7 +165,7 @@ get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
     if(s_it==symbol_table.symbols.end())
       continue;
 
-    if(s_it->second.type.id()==ID_code)
+    if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
       matches.push_back(s_it->second.symbol_expr());
   }
 
diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp
index 57456145877..f4278bf9369 100644
--- a/src/jsil/jsil_entry_point.cpp
+++ b/src/jsil/jsil_entry_point.cpp
@@ -74,7 +74,7 @@ bool jsil_entry_point(
       if(s_it==symbol_table.symbols.end())
         continue;
 
-      if(s_it->second.type.id()==ID_code)
+      if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
         matches.push_back(symbol_name_entry.second);
     }