diff --git a/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc
index 897a3670bfb..022e6e3d98c 100644
--- a/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc
+++ b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc
@@ -19,5 +19,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 --
+no body for function '__CPROVER
 --
 This test shows that __CPROVER_object_upto is supported in loop contracts.
diff --git a/regression/contracts/variant_multidimensional_ackermann/loop.desc b/regression/contracts/variant_multidimensional_ackermann/loop.desc
index 82af4451f1a..eb904a6431d 100644
--- a/regression/contracts/variant_multidimensional_ackermann/loop.desc
+++ b/regression/contracts/variant_multidimensional_ackermann/loop.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-loop-contracts
 ^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 8cb69c96ed8..da25c01f569 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -848,12 +848,9 @@ void code_contractst::apply_loop_contract(
     return;
 
   inlining_decoratort decorated(log.get_message_handler());
-  goto_function_inline(
-    goto_functions, function_name, ns, log.get_message_handler());
+  goto_function_inline(goto_functions, function_name, ns, decorated);
 
-  INVARIANT(
-    decorated.get_recursive_call_set().size() == 0,
-    "Recursive functions found during inlining");
+  decorated.throw_on_recursive_calls(log, 0);
 
   // restore internal invariants
   goto_functions.update();
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
index 072e20b8efe..6c1d6d23fd0 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
@@ -265,6 +265,8 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
   std::set<irep_idt> recursive_call;
   std::set<irep_idt> not_enough_arguments;
 
+  // we inspect all warnings ourselves, no need to surface them
+  null_message_handlert null_message_handler;
   dfcc_utilst::inline_program(
     goto_model,
     goto_program,
@@ -272,7 +274,7 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
     recursive_call,
     missing_function,
     not_enough_arguments,
-    message_handler);
+    null_message_handler);
 
   // check that the only no body / missing functions are the cprover builtins
   for(const auto &id : no_body)
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
index 36c724498e2..c83a378d65e 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
@@ -339,9 +339,11 @@ void dfcc_infer_loop_assigns_for_function(
   auto malloc_body = goto_functions.function_map.extract(irep_idt("malloc"));
   auto free_body = goto_functions.function_map.extract(irep_idt("free"));
 
-  // Inline all function calls in goto_function_copy.
+  // Inline all function calls in goto_function_copy; this is best-effort
+  // inlining, we can safely ignore warnings here.
+  null_message_handlert null_message_handler;
   goto_program_inline(
-    goto_functions, goto_function_copy.body, ns, log.get_message_handler());
+    goto_functions, goto_function_copy.body, ns, null_message_handler);
   // Update the body to make sure all goto correctly jump to valid targets.
   goto_function_copy.body.update();
   // Build the loop graph after inlining.