diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
index 7b8b8fcf243..52fecd2dfb2 100644
--- a/doc/man/cbmc.1
+++ b/doc/man/cbmc.1
@@ -347,10 +347,6 @@ run full slicer (experimental)
 .TP
 \fB\-\-drop\-unused\-functions\fR
 drop functions trivially unreachable from main function
-.TP
-\fB\-\-havoc\-undefined\-functions\fR
-for any function that has no body, assign non\-deterministic values to
-any parameters passed as non\-const pointers and the return value
 .SS "Semantic transformations:"
 .TP
 \fB\-\-nondet\-static\fR
diff --git a/regression/cbmc-cpp/Overloading_Functions4/main.cpp b/regression/cbmc-cpp/Overloading_Functions4/main.cpp
index c63d368170b..5c3b0e418da 100644
--- a/regression/cbmc-cpp/Overloading_Functions4/main.cpp
+++ b/regression/cbmc-cpp/Overloading_Functions4/main.cpp
@@ -1,7 +1,9 @@
 double pow(double _X, double _Y);
 double pow(double _X, int _Y);
 float pow(float _X, float _Y);
-float pow(float _X, int _Y);
+float pow(float _X, int _Y)
+{
+}
 long double pow(long double _X, long double _Y);
 long double pow(long double _X, int _Y);
 
diff --git a/regression/cbmc-library/fprintf-01/__fprintf_chk.desc b/regression/cbmc-library/fprintf-01/__fprintf_chk.desc
index 63ac2792c69..11b3f8b0ca0 100644
--- a/regression/cbmc-library/fprintf-01/__fprintf_chk.desc
+++ b/regression/cbmc-library/fprintf-01/__fprintf_chk.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=0$
@@ -7,3 +7,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __fprintf_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack
diff --git a/regression/cbmc-library/printf-01/__printf_chk.desc b/regression/cbmc-library/printf-01/__printf_chk.desc
index 4a3f228e98a..c10b585dfec 100644
--- a/regression/cbmc-library/printf-01/__printf_chk.desc
+++ b/regression/cbmc-library/printf-01/__printf_chk.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=10$
@@ -8,3 +8,5 @@ main.c
 --
 ^\*\*\*\* WARNING: no body for function __printf_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack
diff --git a/regression/cbmc-library/syslog-01/__syslog_chk.desc b/regression/cbmc-library/syslog-01/__syslog_chk.desc
index 76dffecea90..db78ca0551a 100644
--- a/regression/cbmc-library/syslog-01/__syslog_chk.desc
+++ b/regression/cbmc-library/syslog-01/__syslog_chk.desc
@@ -1,9 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-^\*\*\*\* WARNING: no body for function __syslog_chk
 ^warning: ignoring
+--
+We are missing __builtin_va_arg_pack
diff --git a/regression/cbmc/Array_UF17/main.c b/regression/cbmc/Array_UF17/main.c
index af0d10ab711..3eb5d444454 100644
--- a/regression/cbmc/Array_UF17/main.c
+++ b/regression/cbmc/Array_UF17/main.c
@@ -31,7 +31,9 @@ int istrchr(const char *s, int c);
 int istrrchr(const char *s, int c);
 int istrncmp(const char *s1, int start, const char *s2, size_t n);
 int istrstr(const char *haystack, const char *needle);
-char *r_strncpy(char *dest, const char *src, size_t n);
+char *r_strncpy(char *dest, const char *src, size_t n)
+{
+}
 char *r_strcpy(char *dest, const char *src);
 char *r_strcat(char *dest, const char *src);
 char *r_strncat(char *dest, const char *src, size_t n);
diff --git a/regression/cbmc/Function_Pointer5/main.c b/regression/cbmc/Function_Pointer5/main.c
index 73c54f158d6..f2435de84ef 100644
--- a/regression/cbmc/Function_Pointer5/main.c
+++ b/regression/cbmc/Function_Pointer5/main.c
@@ -1,7 +1,13 @@
 // this is a pointer to a function that takes a function pointer as argument
 
-void signal1(int, void (*)(int));
-void signal2(int, void (*h)(int));
+void signal1(int, void (*)(int))
+{
+}
+
+void signal2(int, void (*h)(int))
+{
+  h(123);
+}
 
 void handler(int x)
 {
diff --git a/regression/cbmc/Malloc2/main.c b/regression/cbmc/Malloc2/main.c
index d8ca4265b88..cb35e38113b 100644
--- a/regression/cbmc/Malloc2/main.c
+++ b/regression/cbmc/Malloc2/main.c
@@ -1,4 +1,4 @@
-typedef unsigned int size_t;
+typedef __CPROVER_size_t size_t;
 typedef int ssize_t;
 typedef int atomic_t;
 typedef unsigned gfp_t;
diff --git a/regression/cbmc/Pointer28/test.desc b/regression/cbmc/Pointer28/test.desc
index 366f3e536c7..681a4be9eb7 100644
--- a/regression/cbmc/Pointer28/test.desc
+++ b/regression/cbmc/Pointer28/test.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+KNOWNBUG no-new-smt
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Promotion4/main.i b/regression/cbmc/Promotion4/main.i
index 91a61350256..c9fac94caa6 100644
--- a/regression/cbmc/Promotion4/main.i
+++ b/regression/cbmc/Promotion4/main.i
@@ -1,10 +1,12 @@
+unsigned nondet_unsigned();
+
 int main(int argc, char *argv[])
 {
   __CPROVER_assert(sizeof(unsigned int) == 2, "[--16] size of int is 16 bit");
   __CPROVER_assert(
     sizeof(unsigned long) == 4, "[--LP32] size of long is 32 bit");
 
-  unsigned int k = non_det_unsigned();
+  unsigned int k = nondet_unsigned();
   __CPROVER_assume(k < 1);
   __CPROVER_assert(k != 0xffff, "false counter example 16Bit?");
 
diff --git a/regression/cbmc/String_Abstraction11/anon-retval.c b/regression/cbmc/String_Abstraction11/anon-retval.c
index 4d7d26c887b..fccf1e5d55b 100644
--- a/regression/cbmc/String_Abstraction11/anon-retval.c
+++ b/regression/cbmc/String_Abstraction11/anon-retval.c
@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 char *foo()
 {
diff --git a/regression/cbmc/String_Abstraction19/structs.c b/regression/cbmc/String_Abstraction19/structs.c
index 8468ae845cd..0b7701e244c 100644
--- a/regression/cbmc/String_Abstraction19/structs.c
+++ b/regression/cbmc/String_Abstraction19/structs.c
@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
 typedef struct str_struct
 {
diff --git a/regression/cbmc/Undefined_Function1/test.desc b/regression/cbmc/Undefined_Function1/test.desc
index 431b8dc42b1..9e89636fde8 100644
--- a/regression/cbmc/Undefined_Function1/test.desc
+++ b/regression/cbmc/Undefined_Function1/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
 
+^\[main\.no-body\.f\] line 9 no body for callee f: FAILURE$
+^\[main\.assertion\.1] line 10 assertion i==1: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\*\*\* WARNING: no body for function f$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Undefined_Function2/test.desc b/regression/cbmc/Undefined_Function2/test.desc
index bf3843459f5..3ad1a33245e 100644
--- a/regression/cbmc/Undefined_Function2/test.desc
+++ b/regression/cbmc/Undefined_Function2/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
 
+^\[main\.no-body\.asd\] line 7 no body for callee asd: FAILURE$
+^\[main\.assertion\.1\] line 8 assertion v1==v2: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\*\*\* WARNING: no body for function asd$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/havoc_undefined_functions/main.c b/regression/cbmc/havoc_undefined_functions/main.c
deleted file mode 100644
index 69402434a97..00000000000
--- a/regression/cbmc/havoc_undefined_functions/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-void function(int *a);
-
-int main()
-{
-  int a = 0;
-  function(&a);
-  __CPROVER_assert(a == 0, "");
-  return 0;
-}
diff --git a/regression/cbmc/havoc_undefined_functions/test.desc b/regression/cbmc/havoc_undefined_functions/test.desc
deleted file mode 100644
index 9a9f9b98bd0..00000000000
--- a/regression/cbmc/havoc_undefined_functions/test.desc
+++ /dev/null
@@ -1,6 +0,0 @@
-CORE
-main.c
---havoc-undefined-functions
-^EXIT=10$
-^SIGNAL=0$
-^VERIFICATION FAILED$
diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c
index c92fed9cdad..659a55a4a9a 100644
--- a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c
+++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c
@@ -1,9 +1,11 @@
 #include <assert.h>
 #include <stdlib.h>
 
+_Bool nondet_bool();
+
 void main()
 {
   char *data;
-  data = nondet() ? malloc(1) : malloc(2);
+  data = nondet_bool() ? malloc(1) : malloc(2);
   assert(__CPROVER_OBJECT_SIZE(data) <= 2);
 }
diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc
index 49ee6d9f69e..8e342934a7e 100644
--- a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc
+++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc
@@ -4,9 +4,9 @@ short.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS
+^\[main\.assertion\.\d\] line \d+ assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: SUCCESS$
 --
-\[main.assertion.\d\] line \d assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE
+^\[main\.assertion\.\d\] line \d+ assertion __CPROVER_OBJECT_SIZE\(data\) <= 2: FAILURE$
 --
 This is the reduced version of the issue described in
 https://github.com/diffblue/cbmc/issues/5952
diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc
index c008c1b6ed8..9ad4e4fda9b 100644
--- a/regression/cbmc/memory_allocation2/test.desc
+++ b/regression/cbmc/memory_allocation2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc
index e00d2d72ddf..12355731854 100644
--- a/regression/cbmc/pointer-overflow2/test.desc
+++ b/regression/cbmc/pointer-overflow2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-overflow-check
 ^EXIT=0$
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
index 22f5df0f5c1..6fddab85608 100644
--- a/regression/cbmc/union12/test.desc
+++ b/regression/cbmc/union12/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 
 ^EXIT=10$
@@ -15,3 +15,5 @@ possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
 byte_extract to use the root object) the test already is trivial, however.
 
 This test only fails when using SMT solvers as back-end on Windows.
+
+No body for __CPROVER_allocated_memory
diff --git a/regression/contracts/assigns_replace_02/main.c b/regression/contracts/assigns_replace_02/main.c
index 8487c6564c9..f2d44c5983d 100644
--- a/regression/contracts/assigns_replace_02/main.c
+++ b/regression/contracts/assigns_replace_02/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+void bar(int *)
+{
+}
+
 void foo(int *x, int *y) __CPROVER_assigns(*x)
 {
   *x = 7;
diff --git a/regression/contracts/cprover-assignable-pass/test.desc b/regression/contracts/cprover-assignable-pass/test.desc
index 182e8bc3021..4cb809931cf 100644
--- a/regression/contracts/cprover-assignable-pass/test.desc
+++ b/regression/contracts/cprover-assignable-pass/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 CALL __CPROVER_object_whole
diff --git a/regression/goto-instrument-wmm-core/CMakeLists.txt b/regression/goto-instrument-wmm-core/CMakeLists.txt
index f1fbcc356fd..8131a600122 100644
--- a/regression/goto-instrument-wmm-core/CMakeLists.txt
+++ b/regression/goto-instrument-wmm-core/CMakeLists.txt
@@ -4,6 +4,13 @@ else()
     set(is_windows false)
 endif()
 
+# These tests do not run with Visual Studio since they use
+# gcc's asm syntax.
+
+if(NOT WIN32)
+
 add_test_pl_tests(
     "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}" -X glpk
 )
+
+endif()
diff --git a/regression/goto-instrument-wmm-core/Makefile b/regression/goto-instrument-wmm-core/Makefile
index 252caf1602c..531ad7f696d 100644
--- a/regression/goto-instrument-wmm-core/Makefile
+++ b/regression/goto-instrument-wmm-core/Makefile
@@ -1,15 +1,21 @@
+# These tests do not run with Visual Studio since they use
+# gcc's asm syntax.
+
 default: tests.log
 
 include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	exe=../../../src/goto-cc/goto-cl
-	is_windows=true
+
+test:
+
+tests.log: ../test.pl
+
 else
-	exe=../../../src/goto-cc/goto-cc
-	is_windows=false
-endif
+
+exe=../../../src/goto-cc/goto-cc
+is_windows=false
 
 testalpha:
 	@../test.pl -C -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
@@ -29,6 +35,8 @@ test:
 tests.log:
 	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
 
+endif
+
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.gb' -execdir $(RM) '{}' \;
diff --git a/regression/goto-instrument/dump-vararg1/test.desc b/regression/goto-instrument/dump-vararg1/test.desc
index d1a6d2f2d6f..71bb8d51e6d 100644
--- a/regression/goto-instrument/dump-vararg1/test.desc
+++ b/regression/goto-instrument/dump-vararg1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --dump-c
 ^EXIT=0$
@@ -6,3 +6,5 @@ main.c
 va_list
 --
 ^warning: ignoring
+--
+We are missing __CPROVER_va_start
diff --git a/regression/goto-instrument/inline_16/test.desc b/regression/goto-instrument/inline_16/test.desc
index 9c0b7504b3c..4c415ad4cac 100644
--- a/regression/goto-instrument/inline_16/test.desc
+++ b/regression/goto-instrument/inline_16/test.desc
@@ -1,12 +1,12 @@
 CORE
 main.c
 --inline
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 func1\(\)
 ret.*=.*func2\(\)
-no body for function.*func1
-no body for function.*func2
+^\[\.no-body\.func1\] file main.c line 3 no body for callee func1: FAILURE$
+^\[\.no-body\.func2\] file main.c line 3 no body for callee func2: FAILURE$
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_17/test.desc b/regression/goto-instrument/inline_17/test.desc
index 7f43650ebe1..8b95fe35fc6 100644
--- a/regression/goto-instrument/inline_17/test.desc
+++ b/regression/goto-instrument/inline_17/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
 --function-inline func1
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[func1\.no-body\.func2\] line 3 no body for callee func2: FAILURE$
+^VERIFICATION FAILED$
 func1\(\)
 func2\(\)
 --
diff --git a/regression/goto-instrument/remove-function-body1/test.desc b/regression/goto-instrument/remove-function-body1/test.desc
index 45369a31184..b14f36bcb39 100644
--- a/regression/goto-instrument/remove-function-body1/test.desc
+++ b/regression/goto-instrument/remove-function-body1/test.desc
@@ -1,9 +1,11 @@
 CORE
 main.c
 --remove-function-body foo --remove-function-body bar
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[main\.no-body\.foo\] line 19 no body for callee foo: FAILURE$
+^\[main\.no-body\.bar\] line 20 no body for callee bar: FAILURE$
+^VERIFICATION FAILED$
 --
 ^warning: ignoring
 ^bar
diff --git a/src/ansi-c/library/syslog.c b/src/ansi-c/library/syslog.c
index 033029998f9..d5e717d4f89 100644
--- a/src/ansi-c/library/syslog.c
+++ b/src/ansi-c/library/syslog.c
@@ -21,6 +21,14 @@ void syslog(int priority, const char *format, ...)
   (void)*format;
 }
 
+/* FUNCTION: _syslog$DARWIN_EXTSN */
+
+void _syslog$DARWIN_EXTSN(int priority, const char *format, ...)
+{
+  (void)priority;
+  (void)*format;
+}
+
 /* FUNCTION: __syslog_chk */
 
 void __syslog_chk(int priority, int flag, const char *format, ...)
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 7e2fd2fe11f..3748960176e 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -15,6 +15,7 @@ for f in "$@"; do
     $CC -std=gnu11 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
     $CC -S -Wall -Werror -pedantic -Wextra -std=gnu11 __libcheck.i \
       -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas \
+      -Wno-dollar-in-identifier-extension \
       -Wno-gnu-line-marker -Wno-unknown-warning-option -Wno-psabi
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c
@@ -73,6 +74,7 @@ perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc
 perl -p -i -e 's/^__fread_chk\n//' __functions # fread-01/__fread_chk.desc
 perl -p -i -e 's/^__printf_chk\n//' __functions # printf-01/__printf_chk.desc
 perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc
+perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog-01/test.desc
 perl -p -i -e 's/^__time64\n//' __functions # time
 perl -p -i -e 's/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.desc
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 3068eaa3af2..cf3d5e6102e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -285,9 +285,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("drop-unused-functions"))
     options.set_option("drop-unused-functions", true);
 
-  if(cmdline.isset("havoc-undefined-functions"))
-    options.set_option("havoc-undefined-functions", true);
-
   if(cmdline.isset("string-abstraction"))
     options.set_option("string-abstraction", true);
 
@@ -1061,9 +1058,6 @@ void cbmc_parse_optionst::help()
     " {y--full-slice} \t run full slicer (experimental)\n"
     " {y--drop-unused-functions} \t drop functions trivially unreachable from"
     " main function\n"
-    " {y--havoc-undefined-functions} \t for any function that has no body,"
-    " assign non-deterministic values to any parameters passed as non-const"
-    " pointers and the return value\n"
     "\n"
     "Semantic transformations:\n"
     " {y--nondet-static} \t add nondeterministic initialization of variables"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index de50b68b1f0..a5890bfb88d 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -55,7 +55,6 @@ class optionst;
   OPT_SHOW_PROPERTIES \
   "(show-symbol-table)(show-parse-tree)" \
   "(drop-unused-functions)" \
-  "(havoc-undefined-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(verbosity):(no-library)" \
   "(nondet-static)" \
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index 0fdaa6766ea..56bd0c198d6 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -34,8 +34,6 @@ symex_bmct::symex_bmct(
       path_storage,
       guard_manager),
     record_coverage(!options.get_option("symex-coverage-report").empty()),
-    havoc_bodyless_functions(
-      options.get_bool_option("havoc-undefined-functions")),
     unwindset(unwindset),
     symex_coverage(ns)
 {
@@ -209,18 +207,3 @@ bool symex_bmct::get_unwind_recursion(
 
   return abort;
 }
-
-void symex_bmct::no_body(const irep_idt &identifier)
-{
-  if(body_warnings.insert(identifier).second)
-  {
-    log.warning() << "**** WARNING: no body for function " << identifier;
-
-    if(havoc_bodyless_functions)
-    {
-      log.warning()
-        << "; assigning non-deterministic values to any pointer arguments";
-    }
-    log.warning() << log.eom;
-  }
-}
diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h
index 5e0958c7e0f..8f484482cf4 100644
--- a/src/goto-checker/symex_bmc.h
+++ b/src/goto-checker/symex_bmc.h
@@ -80,7 +80,6 @@ class symex_bmct : public goto_symext
   }
 
   const bool record_coverage;
-  const bool havoc_bodyless_functions;
 
   unwindsett &unwindset;
 
@@ -110,10 +109,6 @@ class symex_bmct : public goto_symext
     unsigned thread_nr,
     unsigned unwind) override;
 
-  void no_body(const irep_idt &identifier) override;
-
-  std::unordered_set<irep_idt> body_warnings;
-
   symex_coveraget symex_coverage;
 };
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 85b2622aed8..ae06ad54072 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -444,12 +444,6 @@ class goto_symext
 
   virtual void loop_bound_exceeded(statet &state, const exprt &guard);
 
-  /// Log a warning that a function has no body
-  /// \param identifier: The name of the function with no body
-  virtual void no_body(const irep_idt &identifier)
-  {
-  }
-
   /// Symbolically execute a FUNCTION_CALL instruction.
   /// Only functions that are symbols are supported, see
   /// \ref goto_symext::symex_function_call_symbol.
diff --git a/src/goto-symex/symex_config.h b/src/goto-symex/symex_config.h
index 0680d648fd9..d9f65c46568 100644
--- a/src/goto-symex/symex_config.h
+++ b/src/goto-symex/symex_config.h
@@ -36,8 +36,6 @@ struct symex_configt final
 
   bool partial_loops;
 
-  bool havoc_undefined_functions;
-
   /// \brief Should the additional validation checks be run?
   /// If this flag is set the checks for renaming (both level1 and level2) are
   /// executed in the goto_symex_statet (in the assignment method).
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index bae27d5d560..6fdf9f4ff5e 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -288,7 +288,19 @@ void goto_symext::symex_function_call_post_clean(
 
   if(!goto_function.body_available())
   {
-    no_body(identifier);
+    // create a fatal assertion
+    if(symex_config.unwinding_assertions)
+    {
+      const auto &symbol = ns.lookup(identifier);
+      const std::string property_id =
+        id2string(state.source.pc->source_location().get_function()) +
+        ".no-body." + id2string(identifier);
+      vcc(
+        false_exprt(),
+        property_id,
+        "no body for callee " + id2string(symbol.display_name()),
+        state);
+    }
 
     // record the return
     target.function_return(
@@ -301,26 +313,6 @@ void goto_symext::symex_function_call_post_clean(
       symex_assign(state, cleaned_lhs, rhs);
     }
 
-    if(symex_config.havoc_undefined_functions)
-    {
-      // assign non det to function arguments if pointers
-      // are not const
-      for(const auto &arg : cleaned_arguments)
-      {
-        if(
-          arg.type().id() == ID_pointer &&
-          !to_pointer_type(arg.type()).base_type().get_bool(ID_C_constant) &&
-          to_pointer_type(arg.type()).base_type().id() != ID_code)
-        {
-          exprt object =
-            dereference_exprt(arg, to_pointer_type(arg.type()).base_type());
-          exprt cleaned_object = clean_expr(object, state, true);
-          const guardt guard(true_exprt(), state.guard_manager);
-          havoc_rec(state, guard, cleaned_object);
-        }
-      }
-    }
-
     symex_transition(state);
     return;
   }
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 8c1ec308bda..de1e7f1f388 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -38,8 +38,6 @@ symex_configt::symex_configt(const optionst &options)
     simplify_opt(options.get_bool_option("simplify")),
     unwinding_assertions(options.get_bool_option("unwinding-assertions")),
     partial_loops(options.get_bool_option("partial-loops")),
-    havoc_undefined_functions(
-      options.get_bool_option("havoc-undefined-functions")),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
     show_points_to_sets(options.get_bool_option("show-points-to-sets")),