diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/main.c b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
index e022d770c6e..39c49fd3e5f 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-1/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/main.c b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
index 84ef19235fe..7fc257fc51e 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-2/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/main.c b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
index d49b7ec72b7..77bd433bb93 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-3/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/main.c b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
index 7870ce77aa5..92297746fed 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-4/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-nondet-5/main.c b/regression/goto-analyzer/heap-allocation-nondet-5/main.c
index faa8283feff..fb3bd9c97e2 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-5/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-5/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-nondet-6/main.c b/regression/goto-analyzer/heap-allocation-nondet-6/main.c
index 8dabb4a1132..9f7dda347ef 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-6/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-6/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-write-2/main.c b/regression/goto-analyzer/heap-allocation-write-2/main.c
index 020067294d8..2d63500ffd5 100644
--- a/regression/goto-analyzer/heap-allocation-write-2/main.c
+++ b/regression/goto-analyzer/heap-allocation-write-2/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation-write/main.c b/regression/goto-analyzer/heap-allocation-write/main.c
index 6019ab2f1d7..1e666f099e2 100644
--- a/regression/goto-analyzer/heap-allocation-write/main.c
+++ b/regression/goto-analyzer/heap-allocation-write/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/heap-allocation/main.c b/regression/goto-analyzer/heap-allocation/main.c
index c09abc337b8..6c50b5d00f9 100644
--- a/regression/goto-analyzer/heap-allocation/main.c
+++ b/regression/goto-analyzer/heap-allocation/main.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {
diff --git a/src/ansi-c/library/ctype.c b/src/ansi-c/library/ctype.c
index ac13bd9c07a..e7bfb4461ad 100644
--- a/src/ansi-c/library/ctype.c
+++ b/src/ansi-c/library/ctype.c
@@ -1,47 +1,47 @@
 
 /* FUNCTION: isalnum */
 
-inline int isalnum(int c)
+int isalnum(int c)
 { return (c>='a' && c<='z') || (c>='A' && c<='Z') || (c>='0' && c<='9'); }
 
 /* FUNCTION: isalpha */
 
-inline int isalpha(int c)
+int isalpha(int c)
 { return (c>='a' && c<='z') || (c>='A' && c<='Z'); }
 
 /* FUNCTION: isblank */
 
-inline int isblank(int c)
+int isblank(int c)
 { return c==' ' || c=='\t'; }
 
 /* FUNCTION: iscntrl */
 
-inline int iscntrl(int c)
+int iscntrl(int c)
 { return (c>=0 && c<='\037') || c=='\177'; }
 
 /* FUNCTION: isdigit */
 
-inline int isdigit(int c)
+int isdigit(int c)
 { return c>='0' && c<='9'; }
 
 /* FUNCTION: isgraph */
 
-inline int isgraph(int c)
+int isgraph(int c)
 { return c>='!' && c<='~'; }
 
 /* FUNCTION: islower */
 
-inline int islower(int c)
+int islower(int c)
 { return c>='a' && c<='z'; }
 
 /* FUNCTION: isprint */
 
-inline int isprint(int c)
+int isprint(int c)
 { return c>=' ' && c<='~'; }
 
 /* FUNCTION: ispunct */
 
-inline int ispunct(int c)
+int ispunct(int c)
 { return c=='!' ||
          c=='"' ||
          c=='#' ||
@@ -77,7 +77,7 @@ inline int ispunct(int c)
 
 /* FUNCTION: isspace */
 
-inline int isspace(int c)
+int isspace(int c)
 { return c=='\t' ||
          c=='\n' ||
          c=='\v' ||
@@ -87,20 +87,20 @@ inline int isspace(int c)
 
 /* FUNCTION: isupper */
 
-inline int isupper(int c)
+int isupper(int c)
 { return c>='A' && c<='Z'; }
 
 /* FUNCTION: isxdigit */
 
-inline int isxdigit(int c)
+int isxdigit(int c)
 { return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); }
 
 /* FUNCTION: tolower */
 
-inline int tolower(int c)
+int tolower(int c)
 { return (c>='A' && c<='Z')?c+('a'-'A'):c; }
 
 /* FUNCTION: toupper */
 
-inline int toupper(int c)
+int toupper(int c)
 { return (c>='a' && c<='z')?c-('a'-'A'):c; }
diff --git a/src/ansi-c/library/errno.c b/src/ansi-c/library/errno.c
index e19ac3a6d1b..edb46ccaabe 100644
--- a/src/ansi-c/library/errno.c
+++ b/src/ansi-c/library/errno.c
@@ -5,7 +5,7 @@
 
 __CPROVER_thread_local int __CPROVER_errno;
 
-inline int * __error(void)
+int *__error(void)
 {
   return &__CPROVER_errno;
 }
@@ -17,7 +17,7 @@ inline int * __error(void)
 
 __CPROVER_thread_local int __CPROVER_errno;
 
-inline int *__errno_location(void)
+int *__errno_location(void)
 {
   return &__CPROVER_errno;
 }
@@ -29,7 +29,7 @@ inline int *__errno_location(void)
 
 __CPROVER_thread_local int __CPROVER_errno;
 
-inline int *_errno(void)
+int *_errno(void)
 {
   return &__CPROVER_errno;
 }
diff --git a/src/ansi-c/library/fenv.c b/src/ansi-c/library/fenv.c
index 6c9eb388653..31e17d615d2 100644
--- a/src/ansi-c/library/fenv.c
+++ b/src/ansi-c/library/fenv.c
@@ -4,7 +4,7 @@
 
 extern int __CPROVER_rounding_mode;
 
-inline int fegetround(void)
+int fegetround(void)
 {
 __CPROVER_HIDE:;
   // CPROVER uses the x86 numbering of the rounding modes
@@ -24,7 +24,7 @@ __CPROVER_HIDE:;
 
 #include <fenv.h>
 
-inline int fesetround(int rounding_mode)
+int fesetround(int rounding_mode)
 {
 __CPROVER_HIDE:;
   // CPROVER uses the x86 numbering of the rounding modes
diff --git a/src/ansi-c/library/float.c b/src/ansi-c/library/float.c
index a2ba36e4daa..a3b14577159 100644
--- a/src/ansi-c/library/float.c
+++ b/src/ansi-c/library/float.c
@@ -26,7 +26,7 @@ unsigned int _controlfp(
 
 __CPROVER_thread_local unsigned __CPROVER_fpu_control_word;
 
-inline unsigned int _status87(void)
+unsigned int _status87(void)
 {
   return __CPROVER_fpu_control_word;
 }
@@ -39,7 +39,7 @@ inline unsigned int _status87(void)
 
 __CPROVER_thread_local unsigned __CPROVER_fpu_control_word;
 
-inline unsigned int _statusfp(void)
+unsigned int _statusfp(void)
 {
   return __CPROVER_fpu_control_word;
 }
@@ -52,7 +52,7 @@ inline unsigned int _statusfp(void)
 
 __CPROVER_thread_local unsigned __CPROVER_fpu_control_word;
 
-inline void _statusfp2(unsigned int *px86, unsigned int *pSSE2)
+void _statusfp2(unsigned int *px86, unsigned int *pSSE2)
 {
   unsigned SSE2_status;
   *px86=__CPROVER_fpu_control_word;
@@ -63,7 +63,7 @@ inline void _statusfp2(unsigned int *px86, unsigned int *pSSE2)
 
 /* FUNCTION: _isnan */
 
-inline int _isnan(double x)
+int _isnan(double x)
 {
   return __CPROVER_isnand(x);
 }
@@ -72,7 +72,7 @@ inline int _isnan(double x)
 
 extern int __CPROVER_rounding_mode;
 
-inline int __builtin_flt_rounds(void)
+int __builtin_flt_rounds(void)
 {
   // This is a clang builtin for FLT_ROUNDS
   // The magic numbers are C99 and different from the
@@ -88,7 +88,7 @@ inline int __builtin_flt_rounds(void)
 
 int __builtin_flt_rounds(void);
 
-inline int __flt_rounds(void)
+int __flt_rounds(void)
 {
   // Spotted on FreeBSD
   return __builtin_flt_rounds();
diff --git a/src/ansi-c/library/gcc.c b/src/ansi-c/library/gcc.c
index ee5f8b17d93..79ac7fda79e 100644
--- a/src/ansi-c/library/gcc.c
+++ b/src/ansi-c/library/gcc.c
@@ -1,27 +1,27 @@
 /* FUNCTION: __builtin_ia32_sfence */
 
-inline void __builtin_ia32_sfence(void)
+void __builtin_ia32_sfence(void)
 {
   __asm("sfence");
 }
 
 /* FUNCTION: __builtin_ia32_lfence */
 
-inline void __builtin_ia32_lfence(void)
+void __builtin_ia32_lfence(void)
 {
   __asm("lfence");
 }
 
 /* FUNCTION: __builtin_ia32_mfence */
 
-inline void __builtin_ia32_mfence(void)
+void __builtin_ia32_mfence(void)
 {
   __asm("mfence");
 }
 
 /* FUNCTION: __sync_synchronize */
 
-inline void __sync_synchronize(void)
+void __sync_synchronize(void)
 {
   // WARNING: this was a NOP before gcc 4.3.1,
   // but is now believed to be the strongest possible barrier.
@@ -37,7 +37,7 @@ inline void __sync_synchronize(void)
 
 int __builtin_clz(unsigned int x);
 
-inline int __builtin_ffs(int x)
+int __builtin_ffs(int x)
 {
   if(x == 0)
     return 0;
@@ -54,7 +54,7 @@ inline int __builtin_ffs(int x)
 
 int __builtin_clzl(unsigned long x);
 
-inline int __builtin_ffsl(long x)
+int __builtin_ffsl(long x)
 {
   if(x == 0)
     return 0;
@@ -71,7 +71,7 @@ inline int __builtin_ffsl(long x)
 
 int __builtin_clzll(unsigned long long x);
 
-inline int __builtin_ffsll(long long x)
+int __builtin_ffsll(long long x)
 {
   if(x == 0)
     return 0;
@@ -88,7 +88,7 @@ inline int __builtin_ffsll(long long x)
 
 void __atomic_thread_fence(int memorder);
 
-inline _Bool __atomic_test_and_set(void *ptr, int memorder)
+_Bool __atomic_test_and_set(void *ptr, int memorder)
 {
 __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -103,7 +103,7 @@ __CPROVER_HIDE:;
 
 void __atomic_thread_fence(int memorder);
 
-inline void __atomic_clear(_Bool *ptr, int memorder)
+void __atomic_clear(_Bool *ptr, int memorder)
 {
 __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -145,7 +145,7 @@ __CPROVER_HIDE:;
 #  define __ATOMIC_SEQ_CST 5
 #endif
 
-inline void __atomic_thread_fence(int memorder)
+void __atomic_thread_fence(int memorder)
 {
 __CPROVER_HIDE:;
   if(memorder == __ATOMIC_CONSUME || memorder == __ATOMIC_ACQUIRE)
@@ -168,7 +168,7 @@ __CPROVER_HIDE:;
 
 void __atomic_thread_fence(int memorder);
 
-inline void __atomic_signal_fence(int memorder)
+void __atomic_signal_fence(int memorder)
 {
 __CPROVER_HIDE:;
   __atomic_thread_fence(memorder);
@@ -176,7 +176,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: __atomic_always_lock_free */
 
-inline _Bool __atomic_always_lock_free(__CPROVER_size_t size, void *ptr)
+_Bool __atomic_always_lock_free(__CPROVER_size_t size, void *ptr)
 {
 __CPROVER_HIDE:;
   (void)ptr;
@@ -185,7 +185,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: __atomic_is_lock_free */
 
-inline _Bool __atomic_is_lock_free(__CPROVER_size_t size, void *ptr)
+_Bool __atomic_is_lock_free(__CPROVER_size_t size, void *ptr)
 {
 __CPROVER_HIDE:;
   (void)ptr;
diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c
index 0045cbd105d..9acc33a3f63 100644
--- a/src/ansi-c/library/getopt.c
+++ b/src/ansi-c/library/getopt.c
@@ -11,8 +11,7 @@ extern int optind;
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 size_t __VERIFIER_nondet_size_t();
 
-inline int getopt(
-  int argc, char * const argv[], const char *optstring)
+int getopt(int argc, char *const argv[], const char *optstring)
 {
   __CPROVER_HIDE:;
   int result=-1;
@@ -62,9 +61,9 @@ inline int getopt(
 #define __CPROVER_GETOPT_H_INCLUDED
 #endif
 
-inline int getopt_long(
+int getopt_long(
   int argc,
-  char * const argv[],
+  char *const argv[],
   const char *optstring,
   const struct option *longopts,
   int *longindex)
diff --git a/src/ansi-c/library/intrin.c b/src/ansi-c/library/intrin.c
index fed5b57ed2c..1ea076b7f72 100644
--- a/src/ansi-c/library/intrin.c
+++ b/src/ansi-c/library/intrin.c
@@ -2,7 +2,7 @@
 
 /* FUNCTION: _InterlockedDecrement */
 
-inline long _InterlockedDecrement(long volatile *p)
+long _InterlockedDecrement(long volatile *p)
 {
   __CPROVER_HIDE:;
   // This function generates a full memory barrier (or fence) to ensure that
@@ -16,7 +16,7 @@ inline long _InterlockedDecrement(long volatile *p)
 
 /* FUNCTION: _InterlockedExchange */
 
-inline long _InterlockedExchange(long volatile *p, long v)
+long _InterlockedExchange(long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -28,7 +28,7 @@ inline long _InterlockedExchange(long volatile *p, long v)
 
 /* FUNCTION: _InterlockedExchange16 */
 
-inline short _InterlockedExchange16(short volatile *p, short v)
+short _InterlockedExchange16(short volatile *p, short v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -40,7 +40,7 @@ inline short _InterlockedExchange16(short volatile *p, short v)
 
 /* FUNCTION: _InterlockedExchange8 */
 
-inline char _InterlockedExchange8(char volatile *p, char v)
+char _InterlockedExchange8(char volatile *p, char v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -52,7 +52,7 @@ inline char _InterlockedExchange8(char volatile *p, char v)
 
 /* FUNCTION: _InterlockedExchangeAdd */
 
-inline long _InterlockedExchangeAdd(long volatile *p, long v)
+long _InterlockedExchangeAdd(long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -64,7 +64,7 @@ inline long _InterlockedExchangeAdd(long volatile *p, long v)
 
 /* FUNCTION: _InterlockedExchangeAdd16 */
 
-inline short _InterlockedExchangeAdd16(short volatile *p, short v)
+short _InterlockedExchangeAdd16(short volatile *p, short v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -76,7 +76,7 @@ inline short _InterlockedExchangeAdd16(short volatile *p, short v)
 
 /* FUNCTION: _InterlockedExchangeAdd8 */
 
-inline char _InterlockedExchangeAdd8(char volatile *p, char v)
+char _InterlockedExchangeAdd8(char volatile *p, char v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -88,7 +88,7 @@ inline char _InterlockedExchangeAdd8(char volatile *p, char v)
 
 /* FUNCTION: _InterlockedCompareExchange */
 
-inline long _InterlockedCompareExchange(long volatile *p, long v1, long v2)
+long _InterlockedCompareExchange(long volatile *p, long v1, long v2)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -101,7 +101,8 @@ inline long _InterlockedCompareExchange(long volatile *p, long v1, long v2)
 
 /* FUNCTION: _InterlockedCompareExchange64 */
 
-inline long long _InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2)
+long long
+_InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -114,7 +115,7 @@ inline long long _InterlockedCompareExchange64(long long volatile *p, long long
 
 /* FUNCTION: __InterlockedIncrement */
 
-inline long _InterlockedIncrement(long volatile *p)
+long _InterlockedIncrement(long volatile *p)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -126,7 +127,7 @@ inline long _InterlockedIncrement(long volatile *p)
 
 /* FUNCTION: _InterlockedOr */
 
-inline long _InterlockedOr(long volatile *p, long v)
+long _InterlockedOr(long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -138,7 +139,7 @@ inline long _InterlockedOr(long volatile *p, long v)
 
 /* FUNCTION: _InterlockedOr8 */
 
-inline char _InterlockedOr8(char volatile *p, char v)
+char _InterlockedOr8(char volatile *p, char v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -150,7 +151,7 @@ inline char _InterlockedOr8(char volatile *p, char v)
 
 /* FUNCTION: _InterlockedOr16 */
 
-inline short _InterlockedOr16(short volatile *p, short v)
+short _InterlockedOr16(short volatile *p, short v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -162,7 +163,7 @@ inline short _InterlockedOr16(short volatile *p, short v)
 
 /* FUNCTION: _InterlockedXor */
 
-inline long _InterlockedXor(long volatile *p, long v)
+long _InterlockedXor(long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -174,7 +175,7 @@ inline long _InterlockedXor(long volatile *p, long v)
 
 /* FUNCTION: _InterlockedXor8 */
 
-inline char _InterlockedXor8(char volatile *p, char v)
+char _InterlockedXor8(char volatile *p, char v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -186,7 +187,7 @@ inline char _InterlockedXor8(char volatile *p, char v)
 
 /* FUNCTION: _InterlockedXor16 */
 
-inline short _InterlockedXor16(short volatile *p, short v)
+short _InterlockedXor16(short volatile *p, short v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -198,7 +199,7 @@ inline short _InterlockedXor16(short volatile *p, short v)
 
 /* FUNCTION: _InterlockedAnd */
 
-inline long _InterlockedAnd(long volatile *p, long v)
+long _InterlockedAnd(long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -210,7 +211,7 @@ inline long _InterlockedAnd(long volatile *p, long v)
 
 /* FUNCTION: _InterlockedAnd8 */
 
-inline char _InterlockedAnd8(char volatile *p, char v)
+char _InterlockedAnd8(char volatile *p, char v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -222,7 +223,7 @@ inline char _InterlockedAnd8(char volatile *p, char v)
 
 /* FUNCTION: _InterlockedAnd16 */
 
-inline short _InterlockedAnd16(short volatile *p, short v)
+short _InterlockedAnd16(short volatile *p, short v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -234,7 +235,7 @@ inline short _InterlockedAnd16(short volatile *p, short v)
 
 /* FUNCTION: _InterlockedAdd */
 
-inline long _InterlockedAdd(long volatile *p, long v)
+long _InterlockedAdd(long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -246,7 +247,7 @@ inline long _InterlockedAdd(long volatile *p, long v)
 
 /* FUNCTION: _InterlockedAddLargeStatistic */
 
-inline long _InterlockedAddLargeStatistic(long long volatile *p, long v)
+long _InterlockedAddLargeStatistic(long long volatile *p, long v)
 {
   __CPROVER_HIDE:;
   // not atomic:
@@ -258,14 +259,14 @@ inline long _InterlockedAddLargeStatistic(long long volatile *p, long v)
 
 /* FUNCTION: _mm_lfence */
 
-inline void _mm_lfence(void)
+void _mm_lfence(void)
 {
   __CPROVER_HIDE:;
 }
 
 /* FUNCTION: _mm_mfence */
 
-inline void _mm_mfence(void)
+void _mm_mfence(void)
 {
   __CPROVER_HIDE:;
   __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
@@ -273,14 +274,14 @@ inline void _mm_mfence(void)
 
 /* FUNCTION: _WriteBarrier */
 
-inline void _WriteBarrier(void)
+void _WriteBarrier(void)
 {
   __CPROVER_HIDE:;
 }
 
 /* FUNCTION: _ReadWriteBarrier */
 
-inline void _ReadWriteBarrier(void)
+void _ReadWriteBarrier(void)
 {
   __CPROVER_HIDE:;
   __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
@@ -288,14 +289,14 @@ inline void _ReadWriteBarrier(void)
 
 /* FUNCTION: _ReadBarrier */
 
-inline void _ReadBarrier(void)
+void _ReadBarrier(void)
 {
   __CPROVER_HIDE:;
 }
 
 /* FUNCTION: _InterlockedIncrement16 */
 
-inline short _InterlockedIncrement16(short volatile *p)
+short _InterlockedIncrement16(short volatile *p)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -307,7 +308,7 @@ inline short _InterlockedIncrement16(short volatile *p)
 
 /* FUNCTION: _InterlockedDecrement16 */
 
-inline short _InterlockedDecrement16(short volatile *p)
+short _InterlockedDecrement16(short volatile *p)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -319,7 +320,7 @@ inline short _InterlockedDecrement16(short volatile *p)
 
 /* FUNCTION: _InterlockedCompareExchange16 */
 
-inline short _InterlockedCompareExchange16(short volatile *p, short v1, short v2)
+short _InterlockedCompareExchange16(short volatile *p, short v1, short v2)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -332,7 +333,7 @@ inline short _InterlockedCompareExchange16(short volatile *p, short v1, short v2
 
 /* FUNCTION: _InterlockedCompareExchange8 */
 
-inline char _InterlockedCompareExchange8(char volatile *p, char v1, char v2)
+char _InterlockedCompareExchange8(char volatile *p, char v1, char v2)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -351,7 +352,7 @@ inline char _InterlockedCompareExchange8(char volatile *p, char v1, char v2)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_set_epi32(int e3, int e2, int e1, int e0)
+__m128i _mm_set_epi32(int e3, int e2, int e1, int e0)
 {
   return (__m128i){.m128i_i32 = {e0, e1, e2, e3}};
 }
@@ -365,7 +366,7 @@ inline __m128i _mm_set_epi32(int e3, int e2, int e1, int e0)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0)
+__m128i _mm_setr_epi32(int e3, int e2, int e1, int e0)
 {
   return (__m128i){.m128i_i32 = {e3, e2, e1, e0}};
 }
@@ -379,7 +380,7 @@ inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_set_epi16(
+__m128i _mm_set_epi16(
   short e7,
   short e6,
   short e5,
@@ -401,7 +402,7 @@ inline __m128i _mm_set_epi16(
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_setr_epi16(
+__m128i _mm_setr_epi16(
   short e7,
   short e6,
   short e5,
@@ -423,7 +424,7 @@ inline __m128i _mm_setr_epi16(
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m64 _mm_set_pi16(short e3, short e2, short e1, short e0)
+__m64 _mm_set_pi16(short e3, short e2, short e1, short e0)
 {
   return (__m64){.m64_i16 = {e0, e1, e2, e3}};
 }
@@ -437,7 +438,7 @@ inline __m64 _mm_set_pi16(short e3, short e2, short e1, short e0)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0)
+__m64 _mm_setr_pi16(short e3, short e2, short e1, short e0)
 {
   return (__m64){.m64_i16 = {e3, e2, e1, e0}};
 }
@@ -451,7 +452,7 @@ inline __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline int _mm_extract_epi32(__m128i a, const int imm8)
+int _mm_extract_epi32(__m128i a, const int imm8)
 {
   return a.m128i_i32[imm8];
 }
@@ -465,7 +466,7 @@ inline int _mm_extract_epi32(__m128i a, const int imm8)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline int _mm_extract_epi16(__m128i a, const int imm8)
+int _mm_extract_epi16(__m128i a, const int imm8)
 {
   return a.m128i_i16[imm8];
 }
@@ -479,7 +480,7 @@ inline int _mm_extract_epi16(__m128i a, const int imm8)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline int _mm_extract_pi16(__m64 a, const int imm8)
+int _mm_extract_pi16(__m64 a, const int imm8)
 {
   return a.m64_i16[imm8];
 }
@@ -493,7 +494,7 @@ inline int _mm_extract_pi16(__m64 a, const int imm8)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_adds_epi16(__m128i a, __m128i b)
+__m128i _mm_adds_epi16(__m128i a, __m128i b)
 {
   return (__m128i){
     .m128i_i16 = {
@@ -517,7 +518,7 @@ inline __m128i _mm_adds_epi16(__m128i a, __m128i b)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_subs_epi16(__m128i a, __m128i b)
+__m128i _mm_subs_epi16(__m128i a, __m128i b)
 {
   return (__m128i){
     .m128i_i16 = {
@@ -533,7 +534,7 @@ inline __m128i _mm_subs_epi16(__m128i a, __m128i b)
 }
 #endif
 
-/* FUNCTION: _mm_subs_epi16 */
+/* FUNCTION: _mm_adds_epu16 */
 
 #ifdef _MSC_VER
 #  ifndef __CPROVER_INTRIN_H_INCLUDED
@@ -541,18 +542,18 @@ inline __m128i _mm_subs_epi16(__m128i a, __m128i b)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_subs_epi16(__m128i a, __m128i b)
+__m128i _mm_adds_epu16(__m128i a, __m128i b)
 {
   return (__m128i){
     .m128i_i16 = {
-      __CPROVER_saturating_minus(a.m128i_i16[0], b.m128i_i16[0]),
-      __CPROVER_saturating_minus(a.m128i_i16[1], b.m128i_i16[1]),
-      __CPROVER_saturating_minus(a.m128i_i16[2], b.m128i_i16[2]),
-      __CPROVER_saturating_minus(a.m128i_i16[3], b.m128i_i16[3]),
-      __CPROVER_saturating_minus(a.m128i_i16[4], b.m128i_i16[4]),
-      __CPROVER_saturating_minus(a.m128i_i16[5], b.m128i_i16[5]),
-      __CPROVER_saturating_minus(a.m128i_i16[6], b.m128i_i16[6]),
-      __CPROVER_saturating_minus(a.m128i_i16[7], b.m128i_i16[7]),
+      __CPROVER_saturating_plus(a.m128i_u16[0], b.m128i_u16[0]),
+      __CPROVER_saturating_plus(a.m128i_u16[1], b.m128i_u16[1]),
+      __CPROVER_saturating_plus(a.m128i_u16[2], b.m128i_u16[2]),
+      __CPROVER_saturating_plus(a.m128i_u16[3], b.m128i_u16[3]),
+      __CPROVER_saturating_plus(a.m128i_u16[4], b.m128i_u16[4]),
+      __CPROVER_saturating_plus(a.m128i_u16[5], b.m128i_u16[5]),
+      __CPROVER_saturating_plus(a.m128i_u16[6], b.m128i_u16[6]),
+      __CPROVER_saturating_plus(a.m128i_u16[7], b.m128i_u16[7]),
     }};
 }
 #endif
@@ -565,7 +566,7 @@ inline __m128i _mm_subs_epi16(__m128i a, __m128i b)
 #    define __CPROVER_INTRIN_H_INCLUDED
 #  endif
 
-inline __m128i _mm_subs_epu16(__m128i a, __m128i b)
+__m128i _mm_subs_epu16(__m128i a, __m128i b)
 {
   return (__m128i){
     .m128i_u16 = {
diff --git a/src/ansi-c/library/locale.c b/src/ansi-c/library/locale.c
index 61d5353457e..1250fd93d0c 100644
--- a/src/ansi-c/library/locale.c
+++ b/src/ansi-c/library/locale.c
@@ -6,7 +6,7 @@
 #define __CPROVER_LOCALE_H_INCLUDED
 #endif
 
-inline char *setlocale(int category, const char *locale)
+char *setlocale(int category, const char *locale)
 {
   __CPROVER_HIDE:;
   (void)category;
@@ -29,7 +29,7 @@ inline char *setlocale(int category, const char *locale)
 #define __CPROVER_LOCALE_H_INCLUDED
 #endif
 
-inline struct lconv *localeconv(void)
+struct lconv *localeconv(void)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 34da9f51cb1..9814d428cf5 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -1,26 +1,44 @@
 /* FUNCTION: fabs */
 
-inline double fabs(double d) { return __CPROVER_fabs(d); }
+double fabs(double d)
+{
+  return __CPROVER_fabs(d);
+}
 
 /* FUNCTION: fabsl */
 
-inline long double fabsl(long double d) { return __CPROVER_fabsl(d); }
+long double fabsl(long double d)
+{
+  return __CPROVER_fabsl(d);
+}
 
 /* FUNCTION: fabsf */
 
-inline float fabsf(float f) { return __CPROVER_fabsf(f); }
+float fabsf(float f)
+{
+  return __CPROVER_fabsf(f);
+}
 
 /* FUNCTION: __builtin_fabs */
 
-inline double __builtin_fabs(double d) { return __CPROVER_fabs(d); }
+double __builtin_fabs(double d)
+{
+  return __CPROVER_fabs(d);
+}
 
 /* FUNCTION: __builtin_fabsl */
 
-inline long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); }
+long double __builtin_fabsl(long double d)
+{
+  return __CPROVER_fabsl(d);
+}
 
 /* FUNCTION: __builtin_fabsf */
 
-inline float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); }
+float __builtin_fabsf(float f)
+{
+  return __CPROVER_fabsf(f);
+}
 
 /* FUNCTION: __CPROVER_isgreaterf */
 
@@ -98,137 +116,233 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
 
 #undef isinf
 
-inline int isinf(double d) { return __CPROVER_isinfd(d); }
+int isinf(double d)
+{
+  return __CPROVER_isinfd(d);
+}
 
 /* FUNCTION: __isinf */
 
-inline int __isinf(double d) { return __CPROVER_isinfd(d); }
+int __isinf(double d)
+{
+  return __CPROVER_isinfd(d);
+}
 
 /* FUNCTION: isinff */
 
-inline int isinff(float f) { return __CPROVER_isinff(f); }
+int isinff(float f)
+{
+  return __CPROVER_isinff(f);
+}
 
 /* FUNCTION: __isinff */
 
-inline int __isinff(float f) { return __CPROVER_isinff(f); }
+int __isinff(float f)
+{
+  return __CPROVER_isinff(f);
+}
 
 /* FUNCTION: isinfl */
 
-inline int isinfl(long double ld) { return __CPROVER_isinfld(ld); }
+int isinfl(long double ld)
+{
+  return __CPROVER_isinfld(ld);
+}
 
 /* FUNCTION: __isinfl */
 
-inline int __isinfl(long double ld) { return __CPROVER_isinfld(ld); }
+int __isinfl(long double ld)
+{
+  return __CPROVER_isinfld(ld);
+}
 
 /* FUNCTION: isnan */
 
 #undef isnan
 
-inline int isnan(double d) { return __CPROVER_isnand(d); }
+int isnan(double d)
+{
+  return __CPROVER_isnand(d);
+}
 
 /* FUNCTION: __isnan */
 
-inline int __isnan(double d) { return __CPROVER_isnand(d); }
+int __isnan(double d)
+{
+  return __CPROVER_isnand(d);
+}
 
 /* FUNCTION: __isnanf */
 
-inline int __isnanf(float f) { return __CPROVER_isnanf(f); }
+int __isnanf(float f)
+{
+  return __CPROVER_isnanf(f);
+}
 
 /* FUNCTION: isnanf */
 
-inline int isnanf(float f) { return __CPROVER_isnanf(f); }
+int isnanf(float f)
+{
+  return __CPROVER_isnanf(f);
+}
 
 /* FUNCTION: isnanl */
 
-inline int isnanl(long double ld) { return __CPROVER_isnanld(ld); }
+int isnanl(long double ld)
+{
+  return __CPROVER_isnanld(ld);
+}
 
 /* FUNCTION: __isnanl */
 
-inline int __isnanl(long double ld) { return __CPROVER_isnanld(ld); }
+int __isnanl(long double ld)
+{
+  return __CPROVER_isnanld(ld);
+}
 
 /* FUNCTION: isnormal */
 
 #undef isnormal
 
-inline int isnormal(double d) { return __CPROVER_isnormald(d); }
+int isnormal(double d)
+{
+  return __CPROVER_isnormald(d);
+}
 
 /* FUNCTION: __isnormalf */
 
-inline int __isnormalf(float f) { return __CPROVER_isnormalf(f); }
+int __isnormalf(float f)
+{
+  return __CPROVER_isnormalf(f);
+}
 
 /* FUNCTION: __builtin_inff */
 
-inline float __builtin_inff(void) { return 1.0f/0.0f; }
+float __builtin_inff(void)
+{
+  return 1.0f / 0.0f;
+}
 
 /* FUNCTION: __builtin_inf */
 
-inline double __builtin_inf(void) { return 1.0/0.0; }
+double __builtin_inf(void)
+{
+  return 1.0 / 0.0;
+}
 
 /* FUNCTION: __builtin_infl */
 
-inline long double __builtin_infl(void) { return 1.0l/0.0l; }
+long double __builtin_infl(void)
+{
+  return 1.0l / 0.0l;
+}
 
 /* FUNCTION: __builtin_isinf */
 
-inline int __builtin_isinf(double d) { return __CPROVER_isinfd(d); }
+int __builtin_isinf(double d)
+{
+  return __CPROVER_isinfd(d);
+}
 
 /* FUNCTION: __builtin_isinff */
 
-inline int __builtin_isinff(float f) { return __CPROVER_isinff(f); }
+int __builtin_isinff(float f)
+{
+  return __CPROVER_isinff(f);
+}
 
 /* FUNCTION: __builtin_isinf */
 
-inline int __builtin_isinfl(long double ld) { return __CPROVER_isinfld(ld); }
+int __builtin_isinfl(long double ld)
+{
+  return __CPROVER_isinfld(ld);
+}
 
 /* FUNCTION: __builtin_isnan */
 
-inline int __builtin_isnan(double d) { return __CPROVER_isnand(d); }
+int __builtin_isnan(double d)
+{
+  return __CPROVER_isnand(d);
+}
 
 /* FUNCTION: __builtin_isnanf */
 
-inline int __builtin_isnanf(float f) { return __CPROVER_isnanf(f); }
+int __builtin_isnanf(float f)
+{
+  return __CPROVER_isnanf(f);
+}
 
 /* FUNCTION: __builtin_huge_valf */
 
-inline float __builtin_huge_valf(void) { return 1.0f/0.0f; }
+float __builtin_huge_valf(void)
+{
+  return 1.0f / 0.0f;
+}
 
 /* FUNCTION: __builtin_huge_val */
 
-inline double __builtin_huge_val(void) { return 1.0/0.0; }
+double __builtin_huge_val(void)
+{
+  return 1.0 / 0.0;
+}
 
 /* FUNCTION: __builtin_huge_vall */
 
-inline long double __builtin_huge_vall(void) { return 1.0l/0.0l; }
+long double __builtin_huge_vall(void)
+{
+  return 1.0l / 0.0l;
+}
 
 /* FUNCTION: _dsign */
 
-inline int _dsign(double d) { return __CPROVER_signd(d); }
+int _dsign(double d)
+{
+  return __CPROVER_signd(d);
+}
 
 /* FUNCTION: _ldsign */
 
-inline int _ldsign(long double ld) { return __CPROVER_signld(ld); }
+int _ldsign(long double ld)
+{
+  return __CPROVER_signld(ld);
+}
 
 /* FUNCTION: _fdsign */
 
-inline int _fdsign(float f) { return __CPROVER_signf(f); }
+int _fdsign(float f)
+{
+  return __CPROVER_signf(f);
+}
 
 /* FUNCTION: signbit */
 
 #undef signbit
 
-inline int signbit(double d) { return __CPROVER_signd(d); }
+int signbit(double d)
+{
+  return __CPROVER_signd(d);
+}
 
 /* FUNCTION: __signbitd */
 
-inline int __signbitd(double d) { return __CPROVER_signd(d); }
+int __signbitd(double d)
+{
+  return __CPROVER_signd(d);
+}
 
 /* FUNCTION: __signbitf */
 
-inline int __signbitf(float f) { return __CPROVER_signf(f); }
+int __signbitf(float f)
+{
+  return __CPROVER_signf(f);
+}
 
 /* FUNCTION: __signbit */
 
-inline int __signbit(double ld) { return __CPROVER_signld(ld); }
+int __signbit(double ld)
+{
+  return __CPROVER_signld(ld);
+}
 
 /* FUNCTION: _dclass */
 
@@ -237,8 +351,9 @@ inline int __signbit(double ld) { return __CPROVER_signld(ld); }
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-inline short _dclass(double d) {
-  __CPROVER_HIDE:
+short _dclass(double d)
+{
+__CPROVER_HIDE:
   return __CPROVER_isnand(d)?FP_NAN:
          __CPROVER_isinfd(d)?FP_INFINITE:
          d==0?FP_ZERO:
@@ -253,8 +368,9 @@ inline short _dclass(double d) {
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-inline short _ldclass(long double ld) {
-  __CPROVER_HIDE:
+short _ldclass(long double ld)
+{
+__CPROVER_HIDE:
   return __CPROVER_isnanld(ld)?FP_NAN:
          __CPROVER_isinfld(ld)?FP_INFINITE:
          ld==0?FP_ZERO:
@@ -269,8 +385,9 @@ inline short _ldclass(long double ld) {
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-inline short _fdclass(float f) {
-  __CPROVER_HIDE:
+short _fdclass(float f)
+{
+__CPROVER_HIDE:
   return __CPROVER_isnanf(f)?FP_NAN:
          __CPROVER_isinff(f)?FP_INFINITE:
          f==0?FP_ZERO:
@@ -285,10 +402,11 @@ inline short _fdclass(float f) {
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-inline int __fpclassifyd(double d) {
-  __CPROVER_HIDE:
-    return __CPROVER_fpclassify(
-      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
+int __fpclassifyd(double d)
+{
+__CPROVER_HIDE:
+  return __CPROVER_fpclassify(
+    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
 }
 
 /* FUNCTION: __fpclassifyf */
@@ -298,10 +416,11 @@ inline int __fpclassifyd(double d) {
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-inline int __fpclassifyf(float f) {
-  __CPROVER_HIDE:
-    return __CPROVER_fpclassify(
-      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
+int __fpclassifyf(float f)
+{
+__CPROVER_HIDE:
+  return __CPROVER_fpclassify(
+    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
 }
 
 /* FUNCTION: __fpclassifyl */
@@ -311,10 +430,11 @@ inline int __fpclassifyf(float f) {
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-inline int __fpclassifyl(long double f) {
-  __CPROVER_HIDE:
-    return __CPROVER_fpclassify(
-      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
+int __fpclassifyl(long double f)
+{
+__CPROVER_HIDE:
+  return __CPROVER_fpclassify(
+    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
 }
 
 /* FUNCTION: __fpclassify */
@@ -328,16 +448,18 @@ inline int __fpclassifyl(long double f) {
 // only; newer ones use __fpclassifyd.
 
 #ifdef __APPLE__
-inline int __fpclassify(long double d) {
-  __CPROVER_HIDE:
-    return __CPROVER_fpclassify(
-      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
+int __fpclassify(long double d)
+{
+__CPROVER_HIDE:
+  return __CPROVER_fpclassify(
+    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
 }
 #else
-inline int __fpclassify(double d) {
-  __CPROVER_HIDE:
-    return __CPROVER_fpclassify(
-      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
+int __fpclassify(double d)
+{
+__CPROVER_HIDE:
+  return __CPROVER_fpclassify(
+    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
 }
 #endif
 
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index 849f217472f..5155a42e6c3 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -7,7 +7,7 @@
 
 int __VERIFIER_nondet_int();
 
-inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
+int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 {
   __CPROVER_HIDE:;
 
@@ -32,7 +32,7 @@ inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 
 int __VERIFIER_nondet_int();
 
-inline int pthread_cancel(pthread_t thread)
+int pthread_cancel(pthread_t thread)
 {
   __CPROVER_HIDE:;
 
@@ -64,7 +64,7 @@ typedef signed char __CPROVER_mutex_t;
 #endif
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-inline void pthread_mutex_cleanup(void *p)
+void pthread_mutex_cleanup(void *p)
 {
   __CPROVER_HIDE:;
   __CPROVER_assert(
@@ -73,8 +73,9 @@ inline void pthread_mutex_cleanup(void *p)
 }
 #endif
 
-inline int pthread_mutex_init(
-  pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
+int pthread_mutex_init(
+  pthread_mutex_t *mutex,
+  const pthread_mutexattr_t *mutexattr)
 {
   __CPROVER_HIDE:;
   *((__CPROVER_mutex_t *)mutex)=0;
@@ -108,7 +109,7 @@ typedef signed char __CPROVER_mutex_t;
 #endif
 #endif
 
-inline int pthread_mutex_lock(pthread_mutex_t *mutex)
+int pthread_mutex_lock(pthread_mutex_t *mutex)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
@@ -157,7 +158,7 @@ typedef signed char __CPROVER_mutex_t;
 #endif
 #endif
 
-inline int pthread_mutex_trylock(pthread_mutex_t *mutex)
+int pthread_mutex_trylock(pthread_mutex_t *mutex)
 {
   __CPROVER_HIDE:;
   int return_value;
@@ -208,7 +209,7 @@ typedef signed char __CPROVER_mutex_t;
 #endif
 #endif
 
-inline int pthread_mutex_unlock(pthread_mutex_t *mutex)
+int pthread_mutex_unlock(pthread_mutex_t *mutex)
 {
   __CPROVER_HIDE:;
 
@@ -256,7 +257,7 @@ typedef signed char __CPROVER_mutex_t;
 #endif
 #endif
 
-inline int pthread_mutex_destroy(pthread_mutex_t *mutex)
+int pthread_mutex_destroy(pthread_mutex_t *mutex)
 {
   __CPROVER_HIDE:;
 
@@ -297,7 +298,7 @@ extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
 extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
 
-inline void pthread_exit(void *value_ptr)
+void pthread_exit(void *value_ptr)
 {
   __CPROVER_HIDE:;
   if(value_ptr!=0) (void)*(char*)value_ptr;
@@ -335,7 +336,7 @@ extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 extern unsigned long __CPROVER_next_thread_id;
 
-inline int pthread_join(pthread_t thread, void **value_ptr)
+int pthread_join(pthread_t thread, void **value_ptr)
 {
 __CPROVER_HIDE:;
 
@@ -372,7 +373,7 @@ extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 extern unsigned long __CPROVER_next_thread_id;
 
-inline int _pthread_join(pthread_t thread, void **value_ptr)
+int _pthread_join(pthread_t thread, void **value_ptr)
 {
 __CPROVER_HIDE:;
 
@@ -398,7 +399,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_rwlock_destroy(pthread_rwlock_t *lock)
+int pthread_rwlock_destroy(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
   __CPROVER_assert(*((signed char *)lock)==0,
@@ -420,7 +421,7 @@ inline int pthread_rwlock_destroy(pthread_rwlock_t *lock)
 #endif
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-inline void pthread_rwlock_cleanup(void *p)
+void pthread_rwlock_cleanup(void *p)
 {
   __CPROVER_HIDE:;
   __CPROVER_assert(__CPROVER_get_must(p, "rwlock_destroyed"),
@@ -428,7 +429,8 @@ inline void pthread_rwlock_cleanup(void *p)
 }
 #endif
 
-inline int pthread_rwlock_init(pthread_rwlock_t *lock,
+int pthread_rwlock_init(
+  pthread_rwlock_t *lock,
   const pthread_rwlockattr_t *attr)
 {
   __CPROVER_HIDE:;
@@ -449,7 +451,7 @@ inline int pthread_rwlock_init(pthread_rwlock_t *lock,
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock)
+int pthread_rwlock_rdlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -468,7 +470,7 @@ inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock)
+int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -485,7 +487,7 @@ inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock)
+int pthread_rwlock_trywrlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -502,7 +504,7 @@ inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_rwlock_unlock(pthread_rwlock_t *lock)
+int pthread_rwlock_unlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
   __CPROVER_assert(*((signed char *)lock)==1,
@@ -519,7 +521,7 @@ inline int pthread_rwlock_unlock(pthread_rwlock_t *lock)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
+int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
   __CPROVER_atomic_begin();
@@ -540,7 +542,7 @@ extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
 extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
 
-inline void __spawned_thread(
+void __spawned_thread(
   unsigned long this_thread_id,
 #if 0
   // Destructor support is disabled as it is too expensive due to its extensive
@@ -609,11 +611,11 @@ void __spawned_thread(
   void *(*start_routine)(void *),
   void *arg);
 
-inline int pthread_create(
-  pthread_t *thread, // must not be null
-  const pthread_attr_t *attr, // may be null
-  void * (*start_routine)(void *), // must not be null
-  void *arg) // may be null
+int pthread_create(
+  pthread_t *thread,              // must not be null
+  const pthread_attr_t *attr,     // may be null
+  void *(*start_routine)(void *), // must not be null
+  void *arg)                      // may be null
 {
   __CPROVER_HIDE:;
   unsigned long this_thread_id;
@@ -659,9 +661,7 @@ inline int pthread_create(
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_cond_init(
-    pthread_cond_t *cond,
-    const pthread_condattr_t *attr)
+int pthread_cond_init(pthread_cond_t *cond, const pthread_condattr_t *attr)
 { __CPROVER_HIDE:
   *((unsigned *)cond)=0;
   if(attr) (void)*attr;
@@ -675,8 +675,7 @@ inline int pthread_cond_init(
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_cond_signal(
-  pthread_cond_t *cond)
+int pthread_cond_signal(pthread_cond_t *cond)
 { __CPROVER_HIDE:
   __CPROVER_atomic_begin();
   (*((unsigned *)cond))++;
@@ -691,8 +690,7 @@ inline int pthread_cond_signal(
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_cond_broadcast(
-    pthread_cond_t *cond)
+int pthread_cond_broadcast(pthread_cond_t *cond)
 { __CPROVER_HIDE:
   __CPROVER_atomic_begin();
   *((unsigned *)cond)=(unsigned)-1;
@@ -707,9 +705,7 @@ inline int pthread_cond_broadcast(
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-inline int pthread_cond_wait(
-    pthread_cond_t *cond,
-    pthread_mutex_t *mutex)
+int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex)
 { __CPROVER_HIDE:
 
   (void)*mutex;
@@ -825,9 +821,10 @@ int __VERIFIER_nondet_int();
 // no pthread_barrier_t on the Mac
 // slightly different declaration on OpenBSD
 #if !defined(__APPLE__) && !defined(__OpenBSD__)
-inline int pthread_barrier_init(
+int pthread_barrier_init(
   pthread_barrier_t *restrict barrier,
-  const pthread_barrierattr_t *restrict attr, unsigned count)
+  const pthread_barrierattr_t *restrict attr,
+  unsigned count)
 {
   __CPROVER_HIDE:;
   (void)barrier;
@@ -846,7 +843,7 @@ inline int pthread_barrier_init(
 
 // pthread_barrier_init has a slightly different decl on OpenBSD
 #if defined(__OpenBSD__)
-inline int pthread_barrier_init(
+int pthread_barrier_init(
   pthread_barrier_t *restrict barrier,
   pthread_barrierattr_t *restrict attr,
   unsigned count)
@@ -877,7 +874,7 @@ int __VERIFIER_nondet_int();
 
 // no pthread_barrier_t on the Mac
 #ifndef __APPLE__
-inline int pthread_barrier_destroy(pthread_barrier_t *barrier)
+int pthread_barrier_destroy(pthread_barrier_t *barrier)
 {
   __CPROVER_HIDE:;
 
@@ -907,7 +904,7 @@ int __VERIFIER_nondet_int();
 
 // no pthread_barrier_t on the Mac
 #ifndef __APPLE__
-inline int pthread_barrier_wait(pthread_barrier_t *barrier)
+int pthread_barrier_wait(pthread_barrier_t *barrier)
 {
   __CPROVER_HIDE:;
 
@@ -936,7 +933,7 @@ extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
 extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
 
-inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void *))
+int pthread_key_create(pthread_key_t *key, void (*destructor)(void *))
 {
 __CPROVER_HIDE:;
   __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0;
@@ -960,7 +957,7 @@ __CPROVER_HIDE:;
 
 extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 
-inline int pthread_key_delete(pthread_key_t key)
+int pthread_key_delete(pthread_key_t key)
 {
 __CPROVER_HIDE:;
   __CPROVER_thread_keys[key] = 0;
@@ -976,7 +973,7 @@ __CPROVER_HIDE:;
 
 extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 
-inline void *pthread_getspecific(pthread_key_t key)
+void *pthread_getspecific(pthread_key_t key)
 {
 __CPROVER_HIDE:;
   return (void *)__CPROVER_thread_keys[key];
@@ -991,7 +988,7 @@ __CPROVER_HIDE:;
 
 extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
 
-inline int pthread_setspecific(pthread_key_t key, const void *value)
+int pthread_setspecific(pthread_key_t key, const void *value)
 {
 __CPROVER_HIDE:;
   __CPROVER_thread_keys[key] = value;
diff --git a/src/ansi-c/library/semaphore.c b/src/ansi-c/library/semaphore.c
index 5499a8ca72f..c071693cb8a 100644
--- a/src/ansi-c/library/semaphore.c
+++ b/src/ansi-c/library/semaphore.c
@@ -2,7 +2,7 @@
 
 #include <semaphore.h>
 
-inline int sem_init(sem_t *sem, int pshared, unsigned int value)
+int sem_init(sem_t *sem, int pshared, unsigned int value)
 {
   __CPROVER_HIDE:;
   (void)pshared;
@@ -21,7 +21,7 @@ inline int sem_init(sem_t *sem, int pshared, unsigned int value)
 
 #include <semaphore.h>
 
-inline int sem_wait(sem_t *sem)
+int sem_wait(sem_t *sem)
 {
   __CPROVER_HIDE:;
   (void)sem;
@@ -40,7 +40,7 @@ inline int sem_wait(sem_t *sem)
 
 #include <semaphore.h>
 
-inline int sem_timedwait(sem_t *sem, const struct timespec *abstime)
+int sem_timedwait(sem_t *sem, const struct timespec *abstime)
 {
   __CPROVER_HIDE:;
   (void)sem;
@@ -60,7 +60,7 @@ inline int sem_timedwait(sem_t *sem, const struct timespec *abstime)
 
 #include <semaphore.h>
 
-inline int sem_trywait(sem_t *sem)
+int sem_trywait(sem_t *sem)
 {
   __CPROVER_HIDE:;
   (void)sem;
@@ -79,7 +79,7 @@ inline int sem_trywait(sem_t *sem)
 
 #include <semaphore.h>
 
-inline int sem_post(sem_t *sem)
+int sem_post(sem_t *sem)
 {
   __CPROVER_HIDE:;
   (void)sem;
@@ -98,7 +98,7 @@ inline int sem_post(sem_t *sem)
 
 #include <semaphore.h>
 
-inline int sem_post_multiple(sem_t *sem, int number)
+int sem_post_multiple(sem_t *sem, int number)
 {
   __CPROVER_HIDE:;
   (void)sem;
@@ -118,7 +118,7 @@ inline int sem_post_multiple(sem_t *sem, int number)
 
 #include <semaphore.h>
 
-inline int sem_getvalue(sem_t *sem, int *sval)
+int sem_getvalue(sem_t *sem, int *sval)
 {
   __CPROVER_HIDE:;
   (void)sem;
@@ -138,7 +138,7 @@ inline int sem_getvalue(sem_t *sem, int *sval)
 
 #include <semaphore.h>
 
-inline int sem_destroy(sem_t *sem)
+int sem_destroy(sem_t *sem)
 {
   __CPROVER_HIDE:;
   (void)sem;
diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c
index 7ee26630129..625a25cc393 100644
--- a/src/ansi-c/library/setjmp.c
+++ b/src/ansi-c/library/setjmp.c
@@ -6,7 +6,7 @@
 #define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
-inline void longjmp(jmp_buf env, int val)
+void longjmp(jmp_buf env, int val)
 {
   // does not return
   (void)env;
@@ -25,7 +25,7 @@ inline void longjmp(jmp_buf env, int val)
 #define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
-inline void _longjmp(jmp_buf env, int val)
+void _longjmp(jmp_buf env, int val)
 {
   // does not return
   (void)env;
@@ -46,7 +46,7 @@ inline void _longjmp(jmp_buf env, int val)
 #define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
-inline void siglongjmp(sigjmp_buf env, int val)
+void siglongjmp(sigjmp_buf env, int val)
 {
   // does not return
   (void)env;
@@ -69,7 +69,7 @@ inline void siglongjmp(sigjmp_buf env, int val)
 
 #undef setjmp
 
-inline int setjmp(jmp_buf env)
+int setjmp(jmp_buf env)
 {
   (void)env;
   // returns via longjmp require instrumentation; only such returns would
@@ -84,7 +84,7 @@ inline int setjmp(jmp_buf env)
 #define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
-inline int _setjmp(jmp_buf env)
+int _setjmp(jmp_buf env)
 {
   (void)env;
   // returns via longjmp require instrumentation; only such returns would
@@ -103,7 +103,7 @@ inline int _setjmp(jmp_buf env)
 
 #undef sigsetjmp
 
-inline int sigsetjmp(sigjmp_buf env, int savesigs)
+int sigsetjmp(sigjmp_buf env, int savesigs)
 {
   (void)env;
   (void)savesigs;
@@ -123,7 +123,7 @@ inline int sigsetjmp(sigjmp_buf env, int savesigs)
 #  define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
-inline int __sigsetjmp(sigjmp_buf env, int savesigs)
+int __sigsetjmp(sigjmp_buf env, int savesigs)
 {
   (void)env;
   (void)savesigs;
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 59250dacae2..0ae97100176 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -18,7 +18,7 @@
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
-inline int putchar(int c)
+int putchar(int c)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
@@ -36,7 +36,7 @@ inline int putchar(int c)
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 int __VERIFIER_nondet_int();
 
-inline int puts(const char *s)
+int puts(const char *s)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
@@ -49,7 +49,7 @@ inline int puts(const char *s)
 /* FUNCTION: fclose_cleanup */
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-inline void fclose_cleanup(void *stream)
+void fclose_cleanup(void *stream)
 {
 __CPROVER_HIDE:;
   __CPROVER_assert(
@@ -73,7 +73,7 @@ __CPROVER_HIDE:;
 void fclose_cleanup(void *stream);
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
-inline FILE *fopen(const char *filename, const char *mode)
+FILE *fopen(const char *filename, const char *mode)
 {
   __CPROVER_HIDE:;
   (void)*filename;
@@ -124,7 +124,7 @@ void fclose_cleanup(void *stream);
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 #ifdef __APPLE__
-inline FILE *_fopen(const char *filename, const char *mode)
+FILE *_fopen(const char *filename, const char *mode)
 {
 __CPROVER_HIDE:;
   (void)*filename;
@@ -159,7 +159,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-inline FILE* freopen(const char *filename, const char *mode, FILE *f)
+FILE *freopen(const char *filename, const char *mode, FILE *f)
 {
   __CPROVER_HIDE:;
   (void)*filename;
@@ -187,7 +187,7 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
 
 int __VERIFIER_nondet_int();
 
-inline int fclose(FILE *stream)
+int fclose(FILE *stream)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
@@ -213,7 +213,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
-inline FILE *fdopen(int handle, const char *mode)
+FILE *fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
   (void)handle;
@@ -252,7 +252,7 @@ inline FILE *fdopen(int handle, const char *mode)
 #endif
 
 #ifdef __APPLE__
-inline FILE *_fdopen(int handle, const char *mode)
+FILE *_fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
   (void)handle;
@@ -333,11 +333,7 @@ char *fgets(char *str, int size, FILE *stream)
 char __VERIFIER_nondet_char();
 size_t __VERIFIER_nondet_size_t();
 
-inline size_t fread(
-  void *ptr,
-  size_t size,
-  size_t nitems,
-  FILE *stream)
+size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
 {
   __CPROVER_HIDE:;
   size_t nread=__VERIFIER_nondet_size_t();
@@ -375,7 +371,7 @@ inline size_t fread(
 
 int __VERIFIER_nondet_int();
 
-inline int feof(FILE *stream)
+int feof(FILE *stream)
 {
   // just return nondet
   __CPROVER_HIDE:;
@@ -407,7 +403,7 @@ inline int feof(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int ferror(FILE *stream)
+int ferror(FILE *stream)
 {
   // just return nondet
   __CPROVER_HIDE:;
@@ -439,7 +435,7 @@ inline int ferror(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int fileno(FILE *stream)
+int fileno(FILE *stream)
 {
 __CPROVER_HIDE:;
   if(stream == stdin)
@@ -475,7 +471,7 @@ __CPROVER_HIDE:;
 
 int __VERIFIER_nondet_int();
 
-inline int fputs(const char *s, FILE *stream)
+int fputs(const char *s, FILE *stream)
 {
   // just return nondet
   __CPROVER_HIDE:;
@@ -511,7 +507,7 @@ inline int fputs(const char *s, FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int fflush(FILE *stream)
+int fflush(FILE *stream)
 {
   // just return nondet
   __CPROVER_HIDE:;
@@ -536,7 +532,7 @@ inline int fflush(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int fpurge(FILE *stream)
+int fpurge(FILE *stream)
 {
   // just return nondet
   __CPROVER_HIDE:;
@@ -568,7 +564,7 @@ inline int fpurge(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int fgetc(FILE *stream)
+int fgetc(FILE *stream)
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
@@ -604,7 +600,7 @@ inline int fgetc(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int getc(FILE *stream)
+int getc(FILE *stream)
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
@@ -640,7 +636,7 @@ inline int getc(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int getchar()
+int getchar()
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
@@ -659,7 +655,7 @@ inline int getchar()
 
 int __VERIFIER_nondet_int();
 
-inline int getw(FILE *stream)
+int getw(FILE *stream)
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
@@ -693,7 +689,7 @@ inline int getw(FILE *stream)
 
 int __VERIFIER_nondet_int();
 
-inline int fseek(FILE *stream, long offset, int whence)
+int fseek(FILE *stream, long offset, int whence)
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
@@ -723,7 +719,7 @@ inline int fseek(FILE *stream, long offset, int whence)
 
 long __VERIFIER_nondet_long();
 
-inline long ftell(FILE *stream)
+long ftell(FILE *stream)
 {
   __CPROVER_HIDE:;
   long return_value=__VERIFIER_nondet_long();
@@ -838,7 +834,7 @@ void perror(const char *s)
 #define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-inline int fscanf(FILE *restrict stream, const char *restrict format, ...)
+int fscanf(FILE *restrict stream, const char *restrict format, ...)
 {
 __CPROVER_HIDE:;
   va_list list;
@@ -860,7 +856,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-inline int scanf(const char *restrict format, ...)
+int scanf(const char *restrict format, ...)
 {
 __CPROVER_HIDE:;
   va_list list;
@@ -882,7 +878,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-inline int sscanf(const char *restrict s, const char *restrict format, ...)
+int sscanf(const char *restrict s, const char *restrict format, ...)
 {
 __CPROVER_HIDE:;
   va_list list;
@@ -906,7 +902,7 @@ __CPROVER_HIDE:;
 
 int __VERIFIER_nondet_int();
 
-inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
+int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
 {
   __CPROVER_HIDE:;
   int result=__VERIFIER_nondet_int();
@@ -943,7 +939,7 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a
 #define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-inline int vscanf(const char *restrict format, va_list arg)
+int vscanf(const char *restrict format, va_list arg)
 {
   __CPROVER_HIDE:;
   return vfscanf(stdin, format, arg);
@@ -963,7 +959,7 @@ inline int vscanf(const char *restrict format, va_list arg)
 
 int __VERIFIER_nondet_int();
 
-inline int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
+int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
 {
   __CPROVER_HIDE:;
   int result=__VERIFIER_nondet_int();
@@ -987,7 +983,7 @@ inline int vsscanf(const char *restrict s, const char *restrict format, va_list
 
 int __VERIFIER_nondet_int();
 
-inline int printf(const char *format, ...)
+int printf(const char *format, ...)
 {
 __CPROVER_HIDE:;
   int result = __VERIFIER_nondet_int();
@@ -1010,7 +1006,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-inline int fprintf(FILE *stream, const char *restrict format, ...)
+int fprintf(FILE *stream, const char *restrict format, ...)
 {
   __CPROVER_HIDE:;
   va_list list;
@@ -1034,7 +1030,7 @@ inline int fprintf(FILE *stream, const char *restrict format, ...)
 
 int __VERIFIER_nondet_int();
 
-inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
+int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 {
   __CPROVER_HIDE:;
 
@@ -1080,7 +1076,7 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 char __VERIFIER_nondet_char();
 int __VERIFIER_nondet_int();
 
-inline int vasprintf(char **ptr, const char *fmt, va_list ap)
+int vasprintf(char **ptr, const char *fmt, va_list ap)
 {
   (void)*fmt;
   (void)ap;
@@ -1113,7 +1109,7 @@ inline int vasprintf(char **ptr, const char *fmt, va_list ap)
 #    define __CPROVER_STDIO_H_INCLUDED
 #  endif
 
-inline FILE *__acrt_iob_func(unsigned fd)
+FILE *__acrt_iob_func(unsigned fd)
 {
   static FILE stdin_file;
   static FILE stdout_file;
@@ -1148,7 +1144,7 @@ inline FILE *__acrt_iob_func(unsigned fd)
 #    define __CPROVER_STDARG_H_INCLUDED
 #  endif
 
-inline int __stdio_common_vfprintf(
+int __stdio_common_vfprintf(
   unsigned __int64 options,
   FILE *stream,
   char const *format,
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index dbe0fb43f75..1d7e36616dd 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -2,37 +2,55 @@
 
 #undef abs
 
-inline int abs(int i) { return __CPROVER_abs(i); }
+int abs(int i)
+{
+  return __CPROVER_abs(i);
+}
 
 /* FUNCTION: labs */
 
 #undef labs
 
-inline long int labs(long int i) { return __CPROVER_labs(i); }
+long int labs(long int i)
+{
+  return __CPROVER_labs(i);
+}
 
 /* FUNCTION: llabs */
 
 #undef llabs
 
-inline long long int llabs(long long int i) { return __CPROVER_llabs(i); }
+long long int llabs(long long int i)
+{
+  return __CPROVER_llabs(i);
+}
 
 /* FUNCTION: __builtin_abs */
 
-inline int __builtin_abs(int i) { return __CPROVER_abs(i); }
+int __builtin_abs(int i)
+{
+  return __CPROVER_abs(i);
+}
 
 /* FUNCTION: __builtin_labs */
 
-inline long int __builtin_labs(long int i) { return __CPROVER_labs(i); }
+long int __builtin_labs(long int i)
+{
+  return __CPROVER_labs(i);
+}
 
 /* FUNCTION: __builtin_llabs */
 
-inline long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i); }
+long long int __builtin_llabs(long long int i)
+{
+  return __CPROVER_llabs(i);
+}
 
 /* FUNCTION: exit */
 
 #undef exit
 
-inline void exit(int status)
+void exit(int status)
 {
   (void)status;
   __CPROVER_assume(0);
@@ -45,7 +63,7 @@ inline void exit(int status)
 
 #undef _Exit
 
-inline void _Exit(int status)
+void _Exit(int status)
 {
   (void)status;
   __CPROVER_assume(0);
@@ -58,7 +76,7 @@ inline void _Exit(int status)
 
 #undef abort
 
-inline void abort(void)
+void abort(void)
 {
   __CPROVER_assume(0);
 #ifdef LIBRARY_CHECK
@@ -75,7 +93,7 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 _Bool __builtin_mul_overflow();
 #endif
 
-inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
+void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
 __CPROVER_HIDE:;
   __CPROVER_size_t alloc_size;
@@ -140,6 +158,8 @@ __CPROVER_HIDE:;
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
+// malloc is marked "inline" for the benefit of goto-analyzer. Really,
+// goto-analyzer should take care of inlining as needed.
 inline void *malloc(__CPROVER_size_t malloc_size)
 {
 // realistically, malloc may return NULL,
@@ -199,7 +219,7 @@ __CPROVER_HIDE:;
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 extern void *__CPROVER_alloca_object;
 
-inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
+void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
   __CPROVER_HIDE:;
   void *res;
@@ -229,7 +249,7 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 
 void *__builtin_alloca(__CPROVER_size_t alloca_size);
 
-inline void *alloca(__CPROVER_size_t alloca_size)
+void *alloca(__CPROVER_size_t alloca_size)
 {
 __CPROVER_HIDE:;
   return __builtin_alloca(alloca_size);
@@ -242,7 +262,7 @@ __CPROVER_HIDE:;
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 extern void *__CPROVER_alloca_object;
 
-inline void free(void *ptr)
+void free(void *ptr)
 {
   __CPROVER_HIDE:;
   // If ptr is NULL, no operation is performed.
@@ -303,7 +323,7 @@ _Bool __builtin_add_overflow();
 _Bool __builtin_mul_overflow();
 #endif
 
-inline long strtol(const char *nptr, char **endptr, int base)
+long strtol(const char *nptr, char **endptr, int base)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -390,7 +410,7 @@ inline long strtol(const char *nptr, char **endptr, int base)
 
 long strtol(const char *nptr, char **endptr, int base);
 
-inline int atoi(const char *nptr)
+int atoi(const char *nptr)
 {
   __CPROVER_HIDE:;
   return (int)strtol(nptr, (char **)0, 10);
@@ -403,7 +423,7 @@ inline int atoi(const char *nptr)
 
 long strtol(const char *nptr, char **endptr, int base);
 
-inline long atol(const char *nptr)
+long atol(const char *nptr)
 {
   __CPROVER_HIDE:;
   return strtol(nptr, (char **)0, 10);
@@ -421,7 +441,7 @@ inline long atol(const char *nptr)
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 ptrdiff_t __VERIFIER_nondet_ptrdiff_t();
 
-inline char *getenv(const char *name)
+char *getenv(const char *name)
 {
   __CPROVER_HIDE:;
 
@@ -464,10 +484,10 @@ inline char *getenv(const char *name)
 
 /* FUNCTION: realloc */
 
-inline void *malloc(__CPROVER_size_t malloc_size);
-inline void free(void *ptr);
+void *malloc(__CPROVER_size_t malloc_size);
+void free(void *ptr);
 
-inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
+void *realloc(void *ptr, __CPROVER_size_t malloc_size)
 {
   __CPROVER_HIDE:;
 
@@ -500,9 +520,9 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
 
 /* FUNCTION: valloc */
 
-inline void *malloc(__CPROVER_size_t malloc_size);
+void *malloc(__CPROVER_size_t malloc_size);
 
-inline void *valloc(__CPROVER_size_t malloc_size)
+void *valloc(__CPROVER_size_t malloc_size)
 {
   // The allocated memory is aligned on a page
   // boundary, which we don't model.
@@ -520,9 +540,11 @@ inline void *valloc(__CPROVER_size_t malloc_size)
 
 #undef posix_memalign
 
-inline void *malloc(__CPROVER_size_t malloc_size);
-inline int
-posix_memalign(void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size)
+void *malloc(__CPROVER_size_t malloc_size);
+int posix_memalign(
+  void **ptr,
+  __CPROVER_size_t alignment,
+  __CPROVER_size_t size)
 {
 __CPROVER_HIDE:;
 
diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
index 757f54d6422..ce6aa57bff4 100644
--- a/src/ansi-c/library/string.c
+++ b/src/ansi-c/library/string.c
@@ -1,6 +1,6 @@
 /* FUNCTION: __builtin___strcpy_chk */
 
-inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
+char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
 {
 __CPROVER_HIDE:;
 
@@ -136,7 +136,7 @@ __CPROVER_HIDE:;
 
 #undef strcpy
 
-inline char *strcpy(char *dst, const char *src)
+char *strcpy(char *dst, const char *src)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -173,7 +173,7 @@ __CPROVER_HIDE:;
 
 #undef strncpy
 
-inline char *strncpy(char *dst, const char *src, size_t n)
+char *strncpy(char *dst, const char *src, size_t n)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -211,7 +211,11 @@ __CPROVER_HIDE:;
 #define __CPROVER_STRING_H_INCLUDED
 #endif
 
-inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size)
+char *__builtin___strncpy_chk(
+  char *dst,
+  const char *src,
+  size_t n,
+  size_t object_size)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -255,7 +259,7 @@ __CPROVER_HIDE:;
 
 #undef strcat
 
-inline char *strcat(char *dst, const char *src)
+char *strcat(char *dst, const char *src)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -301,7 +305,7 @@ __CPROVER_HIDE:;
 
 #undef strncat
 
-inline char *strncat(char *dst, const char *src, size_t n)
+char *strncat(char *dst, const char *src, size_t n)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -356,7 +360,7 @@ __CPROVER_HIDE:;
 
 #undef strcmp
 
-inline int strcmp(const char *s1, const char *s2)
+int strcmp(const char *s1, const char *s2)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -405,7 +409,7 @@ __CPROVER_HIDE:;
 
 #undef strcasecmp
 
-inline int strcasecmp(const char *s1, const char *s2)
+int strcasecmp(const char *s1, const char *s2)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -457,7 +461,7 @@ __CPROVER_HIDE:;
 
 #undef strncmp
 
-inline int strncmp(const char *s1, const char *s2, size_t n)
+int strncmp(const char *s1, const char *s2, size_t n)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -504,7 +508,7 @@ __CPROVER_HIDE:;
 
 #undef strncasecmp
 
-inline int strncasecmp(const char *s1, const char *s2, size_t n)
+int strncasecmp(const char *s1, const char *s2, size_t n)
 {
 __CPROVER_HIDE:;
 #ifdef __CPROVER_STRING_ABSTRACTION
@@ -554,7 +558,7 @@ __CPROVER_HIDE:;
 
 #undef strlen
 
-inline size_t strlen(const char *s)
+size_t strlen(const char *s)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -583,7 +587,7 @@ inline size_t strlen(const char *s)
 #undef strdup
 #undef strcpy
 
-inline char *strdup(const char *str)
+char *strdup(const char *str)
 {
   __CPROVER_HIDE:;
   __CPROVER_size_t bufsz;
@@ -916,7 +920,7 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
 
 #undef memcmp
 
-inline int memcmp(const void *s1, const void *s2, size_t n)
+int memcmp(const void *s1, const void *s2, size_t n)
 {
   __CPROVER_HIDE:;
   int res=0;
@@ -951,7 +955,7 @@ inline int memcmp(const void *s1, const void *s2, size_t n)
 
 #undef strchr
 
-inline char *strchr(const char *src, int c)
+char *strchr(const char *src, int c)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -980,7 +984,7 @@ inline char *strchr(const char *src, int c)
 
 #undef strchr
 
-inline char *strrchr(const char *src, int c)
+char *strrchr(const char *src, int c)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c
index 096d8f9837d..d4bc309954f 100644
--- a/src/ansi-c/library/unistd.c
+++ b/src/ansi-c/library/unistd.c
@@ -16,7 +16,7 @@ unsigned int sleep(unsigned int seconds)
 
 unsigned int sleep(unsigned int seconds);
 
-inline unsigned int _sleep(unsigned int seconds)
+unsigned int _sleep(unsigned int seconds)
 {
   __CPROVER_HIDE:;
   return sleep(seconds);
@@ -125,7 +125,7 @@ int close(int fildes)
 
 int close(int fildes);
 
-inline int _close(int fildes)
+int _close(int fildes)
 {
   __CPROVER_HIDE:;
   return close(fildes);
@@ -199,7 +199,7 @@ ret_type write(int fildes, const void *buf, size_type nbyte)
 
 ret_type write(int fildes, const void *buf, size_type nbyte);
 
-inline ret_type _write(int fildes, const void *buf, size_type nbyte)
+ret_type _write(int fildes, const void *buf, size_type nbyte)
 {
   __CPROVER_HIDE:;
   return write(fildes, buf, nbyte);
@@ -303,7 +303,7 @@ ret_type read(int fildes, void *buf, size_type nbyte)
 
 ret_type read(int fildes, void *buf, size_type nbyte);
 
-inline ret_type _read(int fildes, void *buf, size_type nbyte)
+ret_type _read(int fildes, void *buf, size_type nbyte)
 {
   __CPROVER_HIDE:;
   return read(fildes, buf, nbyte);
diff --git a/src/ansi-c/library/windows.c b/src/ansi-c/library/windows.c
index 1c6b5e758bf..fdb5864b3f3 100644
--- a/src/ansi-c/library/windows.c
+++ b/src/ansi-c/library/windows.c
@@ -20,7 +20,7 @@ BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency)
 #ifdef _WIN32
 #include <windows.h>
 
-inline VOID ExitThread(DWORD dwExitCode)
+VOID ExitThread(DWORD dwExitCode)
 {
   // never returns
   __CPROVER_assume(0);
@@ -32,14 +32,13 @@ inline VOID ExitThread(DWORD dwExitCode)
 #ifdef _WIN32
 #include <windows.h>
 
-inline HANDLE CreateThread(
+HANDLE CreateThread(
   LPSECURITY_ATTRIBUTES lpThreadAttributes,
   SIZE_T dwStackSize,
   LPTHREAD_START_ROUTINE lpStartAddress,
   LPVOID lpParameter,
   DWORD dwCreationFlags,
-  LPDWORD lpThreadId
-)
+  LPDWORD lpThreadId)
 {
   __CPROVER_HIDE:;
   DWORD thread_id;
diff --git a/src/ansi-c/library/x86_assembler.c b/src/ansi-c/library/x86_assembler.c
index d1e5517ea0d..54f83177cec 100644
--- a/src/ansi-c/library/x86_assembler.c
+++ b/src/ansi-c/library/x86_assembler.c
@@ -3,7 +3,7 @@
 
 extern int __CPROVER_rounding_mode;
 
-inline void __asm_fnstcw(unsigned short *dest)
+void __asm_fnstcw(unsigned short *dest)
 {
   // the rounding mode is bits 10 and 11 in the control word
   *dest=__CPROVER_rounding_mode<<10;
@@ -13,7 +13,7 @@ inline void __asm_fnstcw(unsigned short *dest)
 
 extern int __CPROVER_rounding_mode;
 
-inline void __asm_fstcw(unsigned short *dest)
+void __asm_fstcw(unsigned short *dest)
 {
   // the rounding mode is bits 10 and 11 in the control word
   *dest=__CPROVER_rounding_mode<<10;
@@ -23,7 +23,7 @@ inline void __asm_fstcw(unsigned short *dest)
 
 extern int __CPROVER_rounding_mode;
 
-inline void __asm_fldcw(const unsigned short *src)
+void __asm_fldcw(const unsigned short *src)
 {
   // the rounding mode is bits 10 and 11 in the control word
   __CPROVER_rounding_mode=((*src)>>10)&3;
@@ -31,21 +31,21 @@ inline void __asm_fldcw(const unsigned short *src)
 
 /* FUNCTION: __asm_mfence */
 
-inline void __asm_mfence(void)
+void __asm_mfence(void)
 {
   __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
 }
 
 /* FUNCTION: __asm_sfence */
 
-inline void __asm_sfence(void)
+void __asm_sfence(void)
 {
   __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
 }
 
 /* FUNCTION: __asm_lfence */
 
-inline void __asm_lfence(void)
+void __asm_lfence(void)
 {
   __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
 }