diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh
index c388dc26c914..54829580e44f 100755
--- a/regression/contracts-dfcc/chain.sh
+++ b/regression/contracts-dfcc/chain.sh
@@ -58,5 +58,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}${dfcc_suffix}-mod.c"
 fi
+if ! echo "${args_cbmc}" | grep -q -- --function ; then
+  $goto_instrument --drop-unused-functions "${name}${dfcc_suffix}-mod.gb" "${name}${dfcc_suffix}-mod.gb"
+fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
 $cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
diff --git a/regression/contracts/assigns_enforce_03/main.c b/regression/contracts/assigns_enforce_03/main.c
index 433eab010498..295b23fbd5fa 100644
--- a/regression/contracts/assigns_enforce_03/main.c
+++ b/regression/contracts/assigns_enforce_03/main.c
@@ -1,3 +1,6 @@
+void f2(int *, int *, int *);
+void f3(int *, int *, int *);
+
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
 {
   f2(x1, y1, z1);
@@ -22,6 +25,8 @@ int main()
   int q = 2;
   int r = 3;
   f1(&p, &q, &r);
+  f2(&p, &q, &r);
+  f3(&p, &q, &r);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc
index 4b342024cc93..1a2be3f0e630 100644
--- a/regression/contracts/assigns_enforce_03/test.desc
+++ b/regression/contracts/assigns_enforce_03/test.desc
@@ -1,18 +1,18 @@
 CORE
 main.c
 --enforce-contract f1 --enforce-contract f2 --enforce-contract f3
-^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
-^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
-^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
-^\[f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$
-^\[f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$
-^\[f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$
-^\[f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$
-^\[f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$
+^\[f1.assigns.\d+\] line 4 Check that \*x1 is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 4 Check that \*y1 is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 4 Check that \*z1 is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 9 Check that \*x2 is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 9 Check that \*y2 is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 9 Check that \*z2 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 14 Check that \*x3 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 14 Check that \*y3 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 15 Check that \*z3 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 17 Check that \*x3 is assignable: SUCCESS$
+^\[f3.assigns.\d+\] line 18 Check that \*y3 is assignable: SUCCESS$
+^\[f3.assigns.\d+\] line 19 Check that \*z3 is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh
index 37aa18a35b53..0cfcbb3fe20d 100755
--- a/regression/contracts/chain.sh
+++ b/regression/contracts/chain.sh
@@ -41,5 +41,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}-mod.c"
 fi
+if ! echo "${args_cbmc}" | grep -q -- --function ; then
+  $goto_instrument --drop-unused-functions "${name}-mod.gb" "${name}-mod.gb"
+fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
 $cbmc "${name}-mod.gb" ${args_cbmc}
diff --git a/regression/contracts/variant_multidimensional_ackermann/loop.desc b/regression/contracts/variant_multidimensional_ackermann/loop.desc
new file mode 100644
index 000000000000..82af4451f1af
--- /dev/null
+++ b/regression/contracts/variant_multidimensional_ackermann/loop.desc
@@ -0,0 +1,27 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
+^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
+^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
+^\[ackermann.assigns.\d+\] line 29 Check that m is assignable: SUCCESS$
+^\[ackermann.assigns.\d+\] line 30 Check that n is assignable: SUCCESS$
+^\[ackermann.assigns.\d+\] line 35 Check that m is assignable: SUCCESS$
+^\[ackermann.overflow.\d+] line 39 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+It tests whether we can prove (only partially) the termination of the Ackermann
+function using a multidimensional decreases clause. 
+
+Note that this particular implementation of the Ackermann function contains
+both a while-loop and recursion. Therefore, to fully prove the termination of 
+the Ackermann function, we must prove both 
+(i) the termination of the while-loop and
+(ii) the termination of the recursion. 
+Because CBMC does not support termination proofs of recursions (yet), we cannot
+prove the latter, but the former. Hence, the termination proof in the code is
+only "partial."
diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc
index 213f347ed885..aa9cf7ddedca 100644
--- a/regression/contracts/variant_multidimensional_ackermann/test.desc
+++ b/regression/contracts/variant_multidimensional_ackermann/test.desc
@@ -1,38 +1,18 @@
 CORE
 main.c
---apply-loop-contracts --replace-call-with-contract ackermann
+--replace-call-with-contract ackermann
 ^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in main: SUCCESS$
-^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in ackermann: SUCCESS$
-^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
-^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
-^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
-^\[ackermann.assigns.\d+\] line 29 Check that m is assignable: SUCCESS$
-^\[ackermann.assigns.\d+\] line 30 Check that n is assignable: SUCCESS$
-^\[ackermann.assigns.\d+\] line 34 Check that n is assignable: SUCCESS$
-^\[ackermann.assigns.\d+\] line 35 Check that m is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-It tests whether we can prove (only partially) the termination of the Ackermann
-function using a multidimensional decreases clause. 
-
-Note that this particular implementation of the Ackermann function contains
-both a while-loop and recursion. Therefore, to fully prove the termination of 
-the Ackermann function, we must prove both 
-(i) the termination of the while-loop and
-(ii) the termination of the recursion. 
-Because CBMC does not support termination proofs of recursions (yet), we cannot
-prove the latter, but the former. Hence, the termination proof in the code is
-only "partial."
-
-Furthermore, the Ackermann function has a function contract that the result
+The Ackermann function has a function contract that the result
 is always non-negative. This post-condition is necessary for establishing
 the loop invariant. However, in this test, we do not enforce the function
 contract. Instead, we assume that the function contract is correct and use it
-(i.e. replace a recursive call of the Ackermann function with its contract). 
+(i.e. replace a recursive call of the Ackermann function with its contract).
 
 We cannot verify/enforce the function contract of the Ackermann function, since
 CBMC does not support function contracts for recursively defined functions.
-As of now, CBMC only supports function contracts for non-recursive functions. 
+As of now, CBMC only supports function contracts for non-recursive functions.
diff --git a/src/ansi-c/goto-conversion/link_to_library.cpp b/src/ansi-c/goto-conversion/link_to_library.cpp
index cc814e1965ad..8cdd5dcfd36e 100644
--- a/src/ansi-c/goto-conversion/link_to_library.cpp
+++ b/src/ansi-c/goto-conversion/link_to_library.cpp
@@ -41,26 +41,32 @@ add_one_function(
   // convert to CFG
   if(
     library_model.symbol_table.symbols.find(missing_function) !=
-    library_model.symbol_table.symbols.end())
+      library_model.symbol_table.symbols.end() &&
+    library_model.symbol_table.lookup_ref(missing_function).value.is_not_nil())
   {
     goto_convert(
       missing_function,
       library_model.symbol_table,
       library_model.goto_functions,
       message_handler);
+    library_model.symbol_table.get_writeable_ref(missing_function)
+      .set_compiled();
   }
   // We might need a function that's outside our own library, but brought in via
   // some header file included by the library. Those functions already exist in
   // goto_model.symbol_table, but haven't been converted just yet.
   else if(
     goto_model.symbol_table.symbols.find(missing_function) !=
-    goto_model.symbol_table.symbols.end())
+      goto_model.symbol_table.symbols.end() &&
+    goto_model.symbol_table.lookup_ref(missing_function).value.is_not_nil() &&
+    !goto_model.symbol_table.lookup_ref(missing_function).is_compiled())
   {
     goto_convert(
       missing_function,
       goto_model.symbol_table,
       library_model.goto_functions,
       message_handler);
+    goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled();
   }
 
   // check whether additional initialization may be required
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
index 63c4d8046008..242b330b4d30 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -326,6 +326,7 @@ void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
   {
     goto_convert(
       id, goto_model.symbol_table, goto_model.goto_functions, message_handler);
+    goto_model.symbol_table.get_writeable_ref(id).set_compiled();
   }
 
   // check that all symbols have a goto_implementation
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index 8d5a8ef282c9..dd32b5eec57d 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -546,12 +546,8 @@ cext cegis_verifiert::build_cex(
 
 void cegis_verifiert::restore_functions()
 {
-  for(const auto &fun_entry : goto_model.goto_functions.function_map)
-  {
-    irep_idt fun_name = fun_entry.first;
-    goto_model.goto_functions.function_map[fun_name].body.swap(
-      original_functions[fun_name]);
-  }
+  for(auto &[fun_name, orig_fun_body] : original_functions)
+    goto_model.goto_functions.function_map[fun_name].body.swap(orig_fun_body);
 }
 
 std::optional<cext> cegis_verifiert::verify()
@@ -569,10 +565,12 @@ std::optional<cext> cegis_verifiert::verify()
   // 3. construct the formatted counterexample from the violated property and
   //    its trace.
 
-  // Store the original functions. We will restore them after the verification.
+  // Store the original functions when they have a body (library functions might
+  // not yet have one). We will restore them after the verification.
   for(const auto &fun_entry : goto_model.goto_functions.function_map)
   {
-    original_functions[fun_entry.first].copy_from(fun_entry.second.body);
+    if(fun_entry.second.body_available())
+      original_functions[fun_entry.first].copy_from(fun_entry.second.body);
   }
 
   // Annotate the candidates to the goto_model for checking.