diff --git a/regression/ansi-c/gcc_builtins_address_of/main.c b/regression/ansi-c/gcc_builtins_address_of/main.c
new file mode 100644
index 00000000000..37af4a19fb5
--- /dev/null
+++ b/regression/ansi-c/gcc_builtins_address_of/main.c
@@ -0,0 +1,22 @@
+#ifdef __GNUC__
+
+int main()
+{
+  void (*f)(int) = __builtin_exit;
+  int (*g)(float) = __builtin_isnanf;
+  int (*h)(int) = __builtin_ffs;
+  void *(*m)(__SIZE_TYPE__) = __builtin_malloc;
+  void *(*c)(void *, const void *, __SIZE_TYPE__) = __builtin_memcpy;
+  (void)g(3.14f);
+  (void)h(42);
+  f(1);
+  return 0;
+}
+
+#else
+
+int main()
+{
+}
+
+#endif
diff --git a/regression/ansi-c/gcc_builtins_address_of/test.desc b/regression/ansi-c/gcc_builtins_address_of/test.desc
new file mode 100644
index 00000000000..0e1ed863bc1
--- /dev/null
+++ b/regression/ansi-c/gcc_builtins_address_of/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/cbmc-library/__builtin_exit/main.c b/regression/cbmc-library/__builtin_exit/main.c
new file mode 100644
index 00000000000..97f30e97806
--- /dev/null
+++ b/regression/cbmc-library/__builtin_exit/main.c
@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  __builtin_exit(0);
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/__builtin_exit/test.desc b/regression/cbmc-library/__builtin_exit/test.desc
new file mode 100644
index 00000000000..28345e3383d
--- /dev/null
+++ b/regression/cbmc-library/__builtin_exit/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/gcc_builtins_address_of/main.c b/regression/cbmc/gcc_builtins_address_of/main.c
new file mode 100644
index 00000000000..df93ed99d43
--- /dev/null
+++ b/regression/cbmc/gcc_builtins_address_of/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  void (*f)(int) = __builtin_exit;
+  int (*g)(float) = __builtin_isnanf;
+  assert(!g(3.14f));
+  f(1);
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc/gcc_builtins_address_of/test.desc b/regression/cbmc/gcc_builtins_address_of/test.desc
new file mode 100644
index 00000000000..f7efa2024df
--- /dev/null
+++ b/regression/cbmc/gcc_builtins_address_of/test.desc
@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 55a8cb69ef6..476611b8378 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -884,9 +884,15 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
   const symbolt *symbol_ptr;
   if(lookup(identifier, symbol_ptr))
   {
-    error().source_location = expr.source_location();
-    error() << "failed to find symbol '" << identifier << "'" << eom;
-    throw 0;
+    // If this is a built-in, try to add it to the symbol table on the fly,
+    // just like we do for function calls (see
+    // typecheck_side_effect_function_call).
+    if(builtin_factory(identifier) || lookup(identifier, symbol_ptr))
+    {
+      error().source_location = expr.source_location();
+      error() << "failed to find symbol '" << identifier << "'" << eom;
+      throw 0;
+    }
   }
 
   const symbolt &symbol=*symbol_ptr;
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index c82b495e256..bcfcd16f743 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -108,6 +108,14 @@ void exit(int status)
 #endif
 }
 
+/* FUNCTION: __builtin_exit */
+
+void __builtin_exit(int status)
+{
+  (void)status;
+  __CPROVER_assume(0);
+}
+
 /* FUNCTION: _Exit */
 
 #undef _Exit