Retrieve info for recursion tracker reliably

Fixes #3035

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

@@ -37,6 +37,23 @@ impl<'tcx> GotocCtx<'tcx> {
         let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract);
         let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap();
 
+        let recursion_tracker = items
+            .iter()
+            .filter_map(|i| match i {
+                MonoItem::Static(recursion_tracker)
+                    if (*recursion_tracker).name().contains("REENTRY") =>
+                {
+                    Some(*recursion_tracker)
+                }
+                _ => None,
+            })
+            .next();
+        assert!(
+            recursion_tracker.is_some(),
+            "There should exist a recursion tracker called REENTRY"
+        );
+        let instance_recursion_tracker = recursion_tracker.unwrap();
+
         let mut instance_under_contract = items.iter().filter_map(|i| match i {
             MonoItem::Fn(instance @ Instance { def, .. })
                 if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) =>
@@ -65,11 +82,11 @@ impl<'tcx> GotocCtx<'tcx> {
         let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper);
 
         let full_name = format!(
-            "{}:{}::REENTRY",
+            "{}:{}",
             location_of_recursion_wrapper
                 .filename()
                 .expect("recursion location wrapper should have a file name"),
-            tcx.item_name(recursion_wrapper_id),
+            instance_recursion_tracker.name(),
         );
 
         AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name }