diff --git a/regression/cbmc/library1/main.c b/regression/cbmc/library1/main.c
new file mode 100644
index 00000000000..a719833c455
--- /dev/null
+++ b/regression/cbmc/library1/main.c
@@ -0,0 +1,16 @@
+struct _IO_FILE;
+typedef struct _IO_FILE FILE;
+struct _IO_FILE
+{
+  char dummy;
+};
+
+extern FILE *fopen(char const *fname, char const *mode);
+
+int main()
+{
+  FILE *f;
+  f = fopen("some_file", "r");
+  __CPROVER_assert(f == 0, "");
+  return 0;
+}
diff --git a/regression/cbmc/library1/test.desc b/regression/cbmc/library1/test.desc
new file mode 100644
index 00000000000..e41d42cf59f
--- /dev/null
+++ b/regression/cbmc/library1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+implicit function declaration
+syntax error
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index bbb1236e9e7..f3e61b8e161 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/find_symbols.h>
 
 #include <linking/linking.h>
 #include <linking/remove_internal_symbols.h>
@@ -52,6 +53,15 @@ bool ansi_c_languaget::preprocess(
 bool ansi_c_languaget::parse(
   std::istream &instream,
   const std::string &path)
+{
+  symbol_tablet st;
+  return parse(instream, path, st);
+}
+
+bool ansi_c_languaget::parse(
+  std::istream &instream,
+  const std::string &path,
+  const symbol_tablet &symbol_table)
 {
   // store the path
   parse_path=path;
@@ -78,6 +88,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.set_symbol_table(symbol_table);
 
   ansi_c_scanner_init();
 
@@ -95,6 +106,27 @@ bool ansi_c_languaget::parse(
   // save result
   parse_tree.swap(ansi_c_parser.parse_tree);
 
+  // copy depended-on symbols from the existing symbol table
+  std::list<irep_idt> needed_syms;
+  for(const auto &scope_syms : ansi_c_parser.root_scope().name_map)
+  {
+    if(scope_syms.second.from_symbol_table)
+      needed_syms.push_back(scope_syms.second.prefixed_name);
+  }
+  while(!needed_syms.empty())
+  {
+    const irep_idt id = needed_syms.front();
+    needed_syms.pop_front();
+    const symbolt &symbol = symbol_table.lookup_ref(id);
+
+    if(symbol.is_type && !new_symbol_table.add(symbol))
+    {
+      find_symbols_sett deps;
+      find_type_symbols(symbol.type, deps);
+      needed_syms.insert(needed_syms.end(), deps.begin(), deps.end());
+    }
+  }
+
   // save some memory
   ansi_c_parser.clear();
 
@@ -105,8 +137,6 @@ bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  symbol_tablet new_symbol_table;
-
   if(ansi_c_typecheck(
     parse_tree,
     new_symbol_table,
@@ -118,10 +148,10 @@ bool ansi_c_languaget::typecheck(
 
   remove_internal_symbols(new_symbol_table);
 
-  if(linking(symbol_table, new_symbol_table, get_message_handler()))
-    return true;
+  bool retval = linking(symbol_table, new_symbol_table, get_message_handler());
+  new_symbol_table.clear();
 
-  return false;
+  return retval;
 }
 
 bool ansi_c_languaget::generate_support_functions(
@@ -196,6 +226,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.in=&i_preprocessed;
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.set_symbol_table(ns.get_symbol_table());
   ansi_c_scanner_init();
 
   bool result=ansi_c_parser.parse();
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index b23bdad6469..d9a420a95cb 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/make_unique.h>
+#include <util/symbol_table.h>
 
 #include <langapi/language.h>
 
@@ -30,6 +31,9 @@ class ansi_c_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool
+  parse(std::istream &instream, const std::string &path, const symbol_tablet &);
+
   bool generate_support_functions(
     symbol_tablet &symbol_table) override;
 
@@ -75,6 +79,7 @@ class ansi_c_languaget:public languaget
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
+  symbol_tablet new_symbol_table;
 };
 
 std::unique_ptr<languaget> new_ansi_c_language();
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
index 46d9f51d1b4..80b0f96c6f8 100644
--- a/src/ansi-c/ansi_c_parser.cpp
+++ b/src/ansi-c/ansi_c_parser.cpp
@@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ansi_c_parser.h"
 
-#include <iostream>
+#include <util/symbol_table.h>
 
 #include "c_storage_spec.h"
 
@@ -42,6 +42,24 @@ ansi_c_id_classt ansi_c_parsert::lookup(
     }
   }
 
+  // if a symbol table has been provided, try to resolve global-scoped symbols
+  if(!tag && !label && symbol_table)
+  {
+    const symbolt *symbol = symbol_table->lookup(scope_name);
+    if(symbol)
+    {
+      ansi_c_identifiert &i = root_scope().name_map[scope_name];
+      i.from_symbol_table = true;
+      i.id_class = symbol->is_type && symbol->is_macro
+                     ? ansi_c_id_classt::ANSI_C_TYPEDEF
+                     : ansi_c_id_classt::ANSI_C_SYMBOL;
+      i.prefixed_name = symbol->name;
+      i.base_name = symbol->base_name;
+      identifier = i.prefixed_name;
+      return i.id_class;
+    }
+  }
+
   // Not found.
   // If it's a tag, we will add to current scope.
   if(tag)
@@ -150,6 +168,10 @@ void ansi_c_parsert::add_declarator(
     ansi_c_identifiert &identifier=scope.name_map[base_name];
     identifier.id_class=id_class;
     identifier.prefixed_name=prefixed_name;
+    // it may already have been put in the scope from an existing symbol table
+    // via lookup; now that we know it's being declared here we don't need or
+    // want the entry from the symbol table
+    identifier.from_symbol_table = false;
   }
 
   ansi_c_declaration.declarators().push_back(new_declarator);
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
index b5dad0a515f..78931277d3a 100644
--- a/src/ansi-c/ansi_c_parser.h
+++ b/src/ansi-c/ansi_c_parser.h
@@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert
     mode(modet::NONE),
     cpp98(false),
     cpp11(false),
-    for_has_scope(false)
+    for_has_scope(false),
+    symbol_table(nullptr)
   {
   }
 
@@ -59,6 +60,8 @@ class ansi_c_parsert:public parsert
     // set up global scope
     scopes.clear();
     scopes.push_back(scopet());
+
+    symbol_table = nullptr;
   }
 
   // internal state of the scanner
@@ -139,6 +142,14 @@ class ansi_c_parsert:public parsert
     lookup(base_name, identifier, false, true);
     return identifier;
   }
+
+  void set_symbol_table(const symbol_tablet &st)
+  {
+    symbol_table = &st;
+  }
+
+private:
+  const symbol_tablet *symbol_table;
 };
 
 extern ansi_c_parsert ansi_c_parser;
diff --git a/src/ansi-c/ansi_c_scope.h b/src/ansi-c/ansi_c_scope.h
index 4095c58ec63..a5ef0afe13e 100644
--- a/src/ansi-c/ansi_c_scope.h
+++ b/src/ansi-c/ansi_c_scope.h
@@ -29,9 +29,11 @@ class ansi_c_identifiert
 {
 public:
   ansi_c_id_classt id_class;
+  bool from_symbol_table;
   irep_idt base_name, prefixed_name;
 
-  ansi_c_identifiert():id_class(ansi_c_id_classt::ANSI_C_UNKNOWN)
+  ansi_c_identifiert()
+    : id_class(ansi_c_id_classt::ANSI_C_UNKNOWN), from_symbol_table(false)
   {
   }
 };
diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp
index f13e321d752..efecfcb123e 100644
--- a/src/ansi-c/cprover_library.cpp
+++ b/src/ansi-c/cprover_library.cpp
@@ -14,6 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ansi_c_language.h"
 
+static void
+add_library(const std::string &src, symbol_tablet &, message_handlert &);
+
 struct cprover_library_entryt
 {
   const char *function;
@@ -78,7 +81,7 @@ void add_cprover_library(
   add_library(library_text, symbol_table, message_handler);
 }
 
-void add_library(
+static void add_library(
   const std::string &src,
   symbol_tablet &symbol_table,
   message_handlert &message_handler)
@@ -90,7 +93,7 @@ void add_library(
 
   ansi_c_languaget ansi_c_language;
   ansi_c_language.set_message_handler(message_handler);
-  ansi_c_language.parse(in, "");
+  ansi_c_language.parse(in, "", symbol_table);
 
   ansi_c_language.typecheck(symbol_table, "<built-in-library>");
 }
diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h
index 6f36eb5abca..babcfea7778 100644
--- a/src/ansi-c/cprover_library.h
+++ b/src/ansi-c/cprover_library.h
@@ -19,11 +19,6 @@ std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_tablet &);
 
-void add_library(
-  const std::string &src,
-  symbol_tablet &,
-  message_handlert &);
-
 void add_cprover_library(
   const std::set<irep_idt> &functions,
   symbol_tablet &,
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 7fce070860a..a16feef74c7 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -38,6 +38,7 @@ void __CPROVER_cover(__CPROVER_bool condition);
 
 void __CPROVER_input(const char *id, ...);
 void __CPROVER_output(const char *id, ...);
+int __CPROVER_printf(const char *fmt, ...);
 
 // concurrency-related
 void __CPROVER_atomic_begin();
diff --git a/src/ansi-c/library/err.c b/src/ansi-c/library/err.c
index bbf9f133427..d21f1260fa8 100644
--- a/src/ansi-c/library/err.c
+++ b/src/ansi-c/library/err.c
@@ -1,14 +1,6 @@
 /* FUNCTION: err */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
+void abort(void);
 
 void err(int eval, const char *fmt, ...)
 {
@@ -19,15 +11,7 @@ void err(int eval, const char *fmt, ...)
 
 /* FUNCTION: err */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
+void abort(void);
 
 void errx(int eval, const char *fmt, ...)
 {
@@ -38,11 +22,6 @@ void errx(int eval, const char *fmt, ...)
 
 /* FUNCTION: warn */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
 void warn(const char *fmt, ...)
 {
   (void)*fmt;
@@ -50,11 +29,6 @@ void warn(const char *fmt, ...)
 
 /* FUNCTION: warnx */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
 void warnx(const char *fmt, ...)
 {
   (void)*fmt;
diff --git a/src/ansi-c/library/fcntl.c b/src/ansi-c/library/fcntl.c
index 7001724c9bf..9153a37ed8e 100644
--- a/src/ansi-c/library/fcntl.c
+++ b/src/ansi-c/library/fcntl.c
@@ -1,10 +1,5 @@
 /* FUNCTION: fcntl */
 
-#ifndef __CPROVER_FCNTL_H_INCLUDED
-#include <fcntl.h>
-#define __CPROVER_FCNTL_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 int fcntl(int fd, int cmd, ...)
diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c
index 0045cbd105d..7f261ad5b7f 100644
--- a/src/ansi-c/library/getopt.c
+++ b/src/ansi-c/library/getopt.c
@@ -1,15 +1,16 @@
+#ifdef LIBRARY_CHECK
+#include <getopt.h>
+#endif
+
 /* FUNCTION: getopt */
 
 extern char *optarg;
 extern int optind;
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
+__CPROVER_size_t strlen(const char *s);
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-size_t __VERIFIER_nondet_size_t();
+__CPROVER_size_t __VERIFIER_nondet_size_t();
 
 inline int getopt(
   int argc, char * const argv[], const char *optstring)
@@ -23,7 +24,7 @@ inline int getopt(
   if(optind>=argc || argv[optind][0]!='-')
     return -1;
 
-  size_t result_index=__VERIFIER_nondet_size_t();
+  __CPROVER_size_t result_index = __VERIFIER_nondet_size_t();
   __CPROVER_assume(
     result_index<strlen(optstring) && optstring[result_index]!=':');
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -49,7 +50,7 @@ inline int getopt(
       ++optind;
     }
     else
-      optarg=NULL;
+      optarg = 0;
   }
 
   return result;
@@ -57,10 +58,7 @@ inline int getopt(
 
 /* FUNCTION: getopt_long */
 
-#ifndef __CPROVER_GETOPT_H_INCLUDED
-#include <getopt.h>
-#define __CPROVER_GETOPT_H_INCLUDED
-#endif
+int getopt(int argc, char *const argv[], const char *optstring);
 
 inline int getopt_long(
   int argc,
diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c
index 54623bffb5a..f8db5ab47c1 100644
--- a/src/ansi-c/library/inet.c
+++ b/src/ansi-c/library/inet.c
@@ -1,12 +1,17 @@
-/* FUNCTION: inet_addr */
-
 #ifndef _WIN32
-
-#ifndef __CPROVER_INET_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <arpa/inet.h>
-#define __CPROVER_INET_H_INCLUDED
+#undef htonl
+#undef htons
+#undef ntohl
+#undef ntohs
+#endif
 #endif
 
+/* FUNCTION: inet_addr */
+
+#ifndef _WIN32
+
 in_addr_t __VERIFIER_nondet_in_addr_t();
 
 in_addr_t inet_addr(const char *cp)
@@ -28,11 +33,6 @@ in_addr_t inet_addr(const char *cp)
 
 #ifndef _WIN32
 
-#ifndef __CPROVER_INET_H_INCLUDED
-#include <arpa/inet.h>
-#define __CPROVER_INET_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 int inet_aton(const char *cp, struct in_addr *pin)
@@ -55,11 +55,6 @@ int inet_aton(const char *cp, struct in_addr *pin)
 
 #ifndef _WIN32
 
-#ifndef __CPROVER_INET_H_INCLUDED
-#include <arpa/inet.h>
-#define __CPROVER_INET_H_INCLUDED
-#endif
-
 in_addr_t __VERIFIER_nondet_in_addr_t();
 
 in_addr_t inet_network(const char *cp)
@@ -79,16 +74,9 @@ in_addr_t inet_network(const char *cp)
 
 /* FUNCTION: htonl */
 
-#ifndef __CPROVER_STDINT_H_INCLUDED
-#include <stdint.h>
-#define __CPROVER_STDINT_H_INCLUDED
-#endif
-
-#undef htonl
-
-uint32_t __builtin_bswap32(uint32_t);
+unsigned int __builtin_bswap32(unsigned int);
 
-uint32_t htonl(uint32_t hostlong)
+unsigned int htonl(unsigned int hostlong)
 {
 #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   return __builtin_bswap32(hostlong);
@@ -99,16 +87,9 @@ uint32_t htonl(uint32_t hostlong)
 
 /* FUNCTION: htons */
 
-#ifndef __CPROVER_STDINT_H_INCLUDED
-#include <stdint.h>
-#define __CPROVER_STDINT_H_INCLUDED
-#endif
-
-#undef htons
-
-uint16_t __builtin_bswap16(uint16_t);
+unsigned short __builtin_bswap16(unsigned short);
 
-uint16_t htons(uint16_t hostshort)
+unsigned short htons(unsigned short hostshort)
 {
 #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   return __builtin_bswap16(hostshort);
@@ -120,16 +101,9 @@ uint16_t htons(uint16_t hostshort)
 
 /* FUNCTION: ntohl */
 
-#ifndef __CPROVER_STDINT_H_INCLUDED
-#include <stdint.h>
-#define __CPROVER_STDINT_H_INCLUDED
-#endif
-
-#undef ntohl
-
-uint32_t __builtin_bswap32(uint32_t);
+unsigned int __builtin_bswap32(unsigned int);
 
-uint32_t ntohl(uint32_t netlong)
+unsigned int ntohl(unsigned int netlong)
 {
 #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   return __builtin_bswap32(netlong);
@@ -141,16 +115,9 @@ uint32_t ntohl(uint32_t netlong)
 
 /* FUNCTION: ntohs */
 
-#ifndef __CPROVER_STDINT_H_INCLUDED
-#include <stdint.h>
-#define __CPROVER_STDINT_H_INCLUDED
-#endif
-
-#undef ntohs
-
-uint16_t __builtin_bswap16(uint16_t);
+unsigned short __builtin_bswap16(unsigned short);
 
-uint16_t ntohs(uint16_t netshort)
+unsigned short ntohs(unsigned short netshort)
 {
 #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   return __builtin_bswap16(netshort);
diff --git a/src/ansi-c/library/locale.c b/src/ansi-c/library/locale.c
index 61d5353457e..8a60844bb02 100644
--- a/src/ansi-c/library/locale.c
+++ b/src/ansi-c/library/locale.c
@@ -1,11 +1,9 @@
-
-/* FUNCTION: setlocale */
-
-#ifndef __CPROVER_LOCALE_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <locale.h>
-#define __CPROVER_LOCALE_H_INCLUDED
 #endif
 
+/* FUNCTION: setlocale */
+
 inline char *setlocale(int category, const char *locale)
 {
   __CPROVER_HIDE:;
@@ -24,11 +22,6 @@ inline char *setlocale(int category, const char *locale)
 
 /* FUNCTION: localeconv */
 
-#ifndef __CPROVER_LOCALE_H_INCLUDED
-#include <locale.h>
-#define __CPROVER_LOCALE_H_INCLUDED
-#endif
-
 inline struct lconv *localeconv(void)
 {
   __CPROVER_HIDE:;
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index c9f52dc8f76..573758089c3 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -714,11 +714,6 @@ __CPROVER_hide:;
  *      square root (i.e. the real value of the square root rounded).
  */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -801,11 +796,6 @@ float sqrtf(float f)
 
 /* The same caveats as sqrtf apply */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -872,11 +862,6 @@ double sqrt(double d)
 
 /* The same caveats as sqrtf apply */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -962,34 +947,28 @@ long double sqrtl(long double d)
 
 /* FUNCTION: fmax */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
-double fmax(double f, double g) { return ((f >= g) || isnan(g)) ? f : g; }
+double fmax(double f, double g)
+{
+  return ((f >= g) || __CPROVER_isnand(g)) ? f : g;
+}
 
 /* FUNCTION : fmaxf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
-float fmaxf(float f, float g) { return ((f >= g) || isnan(g)) ? f : g; }
+float fmaxf(float f, float g)
+{
+  return ((f >= g) || __CPROVER_isnanf(g)) ? f : g;
+}
 
 
 /* FUNCTION : fmaxl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
-long double fmaxl(long double f, long double g) { return ((f >= g) || isnan(g)) ? f : g; }
+long double fmaxl(long double f, long double g)
+{
+  return ((f >= g) || __CPROVER_isnanld(g)) ? f : g;
+}
 
 
 /* ISO 9899:2011
@@ -1006,33 +985,27 @@ long double fmaxl(long double f, long double g) { return ((f >= g) || isnan(g))
 
 /* FUNCTION: fmin */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
- 
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
-double fmin(double f, double g) { return ((f <= g) || isnan(g)) ? f : g; }
+double fmin(double f, double g)
+{
+  return ((f <= g) || __CPROVER_isnand(g)) ? f : g;
+}
 
 /* FUNCTION: fminf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB 
-float fminf(float f, float g) { return ((f <= g) || isnan(g)) ? f : g; }
+float fminf(float f, float g)
+{
+  return ((f <= g) || __CPROVER_isnanf(g)) ? f : g;
+}
 
 /* FUNCTION: fminl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB 
-long double fminl(long double f, long double g) { return ((f <= g) || isnan(g)) ? f : g; }
+long double fminl(long double f, long double g)
+{
+  return ((f <= g) || __CPROVER_isnanld(g)) ? f : g;
+}
 
 
 /* ISO 9899:2011
@@ -1045,31 +1018,16 @@ long double fminl(long double f, long double g) { return ((f <= g) || isnan(g))
 
 /* FUNCTION: fdim */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 double fdim(double f, double g) { return ((f > g) ? f - g : +0.0); }
 
 
 /* FUNCTION: fdimf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 float fdimf(float f, float g) { return ((f > g) ? f - g : +0.0f); }
 
 
 /* FUNCTION: fdiml */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0); }
 
 
@@ -1077,15 +1035,8 @@ long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0
 /* FUNCTION: __sort_of_CPROVER_round_to_integral */
 // TODO : Should be a real __CPROVER function to convert to SMT-LIB
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
+int fegetround();
+int fesetround(int);
 
 double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d)
 {
@@ -1116,15 +1067,8 @@ double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d)
 /* FUNCTION: __sort_of_CPROVER_round_to_integralf */
 // TODO : Should be a real __CPROVER function to convert to SMT-LIB
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
+int fegetround();
+int fesetround(int);
 
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d)
 {
@@ -1156,15 +1100,8 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d)
 /* FUNCTION: __sort_of_CPROVER_round_to_integrall */
 // TODO : Should be a real __CPROVER function to convert to SMT-LIB
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
+int fegetround();
+int fesetround(int);
 
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d)
 {
@@ -1200,11 +1137,6 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double
 
 /* FUNCTION: ceil */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1219,11 +1151,6 @@ double ceil(double x)
 
 /* FUNCTION: ceilf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1239,11 +1166,6 @@ float ceilf(float x)
 
 /* FUNCTION: ceill */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1264,11 +1186,6 @@ long double ceill(long double x)
 
 /* FUNCTION: floor */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1283,11 +1200,6 @@ double floor(double x)
 
 /* FUNCTION: floorf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1303,11 +1215,6 @@ float floorf(float x)
 
 /* FUNCTION: floorl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1329,11 +1236,6 @@ long double floorl(long double x)
 
 /* FUNCTION: trunc */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1348,11 +1250,6 @@ double trunc(double x)
 
 /* FUNCTION: truncf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1368,11 +1265,6 @@ float truncf(float x)
 
 /* FUNCTION: truncl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1394,11 +1286,6 @@ long double truncl(long double x)
 
 /* FUNCTION: round */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1430,11 +1317,6 @@ double round(double x)
 
 /* FUNCTION: roundf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1467,11 +1349,6 @@ float roundf(float x)
 
 /* FUNCTION: roundl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1512,17 +1389,8 @@ long double roundl(long double x)
 
 /* FUNCTION: nearbyint */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+int fegetround();
 
 double nearbyint(double x)
 {
@@ -1531,17 +1399,8 @@ double nearbyint(double x)
 
 /* FUNCTION: nearbyintf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+int fegetround();
 
 float nearbyintf(float x)
 {
@@ -1551,17 +1410,8 @@ float nearbyintf(float x)
 
 /* FUNCTION: nearbyintl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+int fegetround();
 
 long double nearbyintl(long double x)
 {
@@ -1579,17 +1429,8 @@ long double nearbyintl(long double x)
 
 /* FUNCTION: rint */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+int fegetround();
 
 double rint(double x)
 {
@@ -1598,17 +1439,8 @@ double rint(double x)
 
 /* FUNCTION: rintf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+int fegetround();
 
 float rintf(float x)
 {
@@ -1617,17 +1449,8 @@ float rintf(float x)
 
 /* FUNCTION: rintl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+int fegetround();
 
 long double rintl(long double x)
 {
@@ -1647,17 +1470,8 @@ long double rintl(long double x)
 
 /* FUNCTION: lrint */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+int fegetround();
 
 long int lrint(double x)
 {
@@ -1669,17 +1483,8 @@ long int lrint(double x)
 
 /* FUNCTION: lrintf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+int fegetround();
 
 long int lrintf(float x)
 {
@@ -1692,17 +1497,8 @@ long int lrintf(float x)
 
 /* FUNCTION: lrintl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+int fegetround();
 
 long int lrintl(long double x)
 {
@@ -1715,17 +1511,8 @@ long int lrintl(long double x)
 
 /* FUNCTION: llrint */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
+int fegetround();
 
 long long int llrint(double x)
 {
@@ -1737,17 +1524,8 @@ long long int llrint(double x)
 
 /* FUNCTION: llrintf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
+int fegetround();
 
 long long int llrintf(float x)
 {
@@ -1760,17 +1538,8 @@ long long int llrintf(float x)
 
 /* FUNCTION: llrintl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_FENV_H_INCLUDED
-#include <fenv.h>
-#define __CPROVER_FENV_H_INCLUDED
-#endif
-
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
+int fegetround();
 
 long long int llrintl(long double x)
 {
@@ -1792,11 +1561,6 @@ long long int llrintl(long double x)
 
 /* FUNCTION: lround */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1829,11 +1593,6 @@ long int lround(double x)
 
 /* FUNCTION: lroundf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1866,11 +1625,6 @@ long int lroundf(float x)
 
 /* FUNCTION: lroundl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1903,11 +1657,6 @@ long int lroundl(long double x)
 
 /* FUNCTION: llround */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1939,11 +1688,6 @@ long long int llround(double x)
 
 /* FUNCTION: llroundf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -1976,11 +1720,6 @@ long long int llroundf(float x)
 
 /* FUNCTION: llroundl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2021,11 +1760,6 @@ long long int llroundl(long double x)
 
 /* FUNCTION: modf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2041,11 +1775,6 @@ double modf(double x, double *iptr)
 
 /* FUNCTION: modff */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2062,11 +1791,6 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
 
 /* FUNCTION: modfl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2145,11 +1869,6 @@ long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long
 
 /* FUNCTION: fmod */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2162,11 +1881,6 @@ double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZE
 
 /* FUNCTION: fmodf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2179,11 +1893,6 @@ float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZER
 
 /* FUNCTION: fmodl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2210,11 +1919,6 @@ long double fmodl(long double x, long double y) { return __sort_of_CPROVER_remai
 
 /* FUNCTION: remainder */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2227,11 +1931,6 @@ double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TON
 
 /* FUNCTION: remainderf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2244,11 +1943,6 @@ float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONE
 
 /* FUNCTION: remainderl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_FENV_H_INCLUDED
 #include <fenv.h>
 #define __CPROVER_FENV_H_INCLUDED
@@ -2271,47 +1965,26 @@ long double remainderl(long double x, long double y) { return __sort_of_CPROVER_
 
 /* FUNCTION: copysign */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-double fabs (double d);
-
 double copysign(double x, double y)
 {
-  double abs = fabs(x);
-  return (signbit(y)) ? -abs : abs;
+  double abs = __CPROVER_fabs(x);
+  return (__CPROVER_signd(y)) ? -abs : abs;
 }
 
 /* FUNCTION: copysignf */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-float fabsf (float d);
-
 float copysignf(float x, float y)
 {
-  float abs = fabs(x);
-  return (signbit(y)) ? -abs : abs;
+  float abs = __CPROVER_fabs(x);
+  return (__CPROVER_signf(y)) ? -abs : abs;
 }
 
 /* FUNCTION: copysignl */
 
-#ifndef __CPROVER_MATH_H_INCLUDED
-#include <math.h>
-#define __CPROVER_MATH_H_INCLUDED
-#endif
-
-long double fabsl (long double d);
-
 long double copysignl(long double x, long double y)
 {
-  long double abs = fabsl(x);
-  return (signbit(y)) ? -abs : abs;
+  long double abs = __CPROVER_fabsl(x);
+  return (__CPROVER_signld(y)) ? -abs : abs;
 }
 
 
diff --git a/src/ansi-c/library/netdb.c b/src/ansi-c/library/netdb.c
index 289e7945202..1869f350c52 100644
--- a/src/ansi-c/library/netdb.c
+++ b/src/ansi-c/library/netdb.c
@@ -1,6 +1,8 @@
-/* FUNCTION: gethostbyname */
-
+#ifdef LIBRARY_CHECK
 #include <netdb.h>
+#endif
+
+/* FUNCTION: gethostbyname */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index 97194052a54..dc556485f23 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -1,10 +1,9 @@
-/* FUNCTION: pthread_mutexattr_settype */
-
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
+/* FUNCTION: pthread_mutexattr_settype */
+
 int __VERIFIER_nondet_int();
 
 inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
@@ -25,11 +24,6 @@ inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 
 /* FUNCTION: pthread_cancel */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int pthread_cancel(pthread_t thread)
@@ -48,11 +42,6 @@ inline int pthread_cancel(pthread_t thread)
 
 /* FUNCTION: pthread_mutex_init */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_mutex_t_defined
 #define __CPROVER_mutex_t_defined
 #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32
@@ -93,11 +82,6 @@ inline int pthread_mutex_init(
 
 /* FUNCTION: pthread_mutex_lock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_mutex_t_defined
 #define __CPROVER_mutex_t_defined
 #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32
@@ -142,11 +126,6 @@ inline int pthread_mutex_lock(pthread_mutex_t *mutex)
 
 /* FUNCTION: pthread_mutex_trylock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_mutex_t_defined
 #define __CPROVER_mutex_t_defined
 #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32
@@ -193,11 +172,6 @@ inline int pthread_mutex_trylock(pthread_mutex_t *mutex)
 
 /* FUNCTION: pthread_mutex_unlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_mutex_t_defined
 #define __CPROVER_mutex_t_defined
 #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32
@@ -241,11 +215,6 @@ inline int pthread_mutex_unlock(pthread_mutex_t *mutex)
 
 /* FUNCTION: pthread_mutex_destroy */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_mutex_t_defined
 #define __CPROVER_mutex_t_defined
 #if defined __CYGWIN__ || defined __MINGW32__ || defined _WIN32
@@ -285,11 +254,6 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex)
 
 /* FUNCTION: pthread_exit */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 
@@ -303,11 +267,6 @@ inline void pthread_exit(void *value_ptr)
 
 /* FUNCTION: pthread_join */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_ERRNO_H_INCLUDED
 #include <errno.h>
 #define __CPROVER_ERRNO_H_INCLUDED
@@ -338,11 +297,6 @@ inline int pthread_join(pthread_t thread, void **value_ptr)
 
 // This is for Apple
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_ERRNO_H_INCLUDED
 #include <errno.h>
 #define __CPROVER_ERRNO_H_INCLUDED
@@ -373,11 +327,6 @@ inline int _pthread_join(pthread_t thread, void **value_ptr)
 
 /* FUNCTION: pthread_rwlock_destroy */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_rwlock_destroy(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
@@ -394,11 +343,6 @@ inline int pthread_rwlock_destroy(pthread_rwlock_t *lock)
 
 /* FUNCTION: pthread_rwlock_init */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
 inline void pthread_rwlock_cleanup(void *p)
 {
@@ -424,11 +368,6 @@ inline int pthread_rwlock_init(pthread_rwlock_t *lock,
 
 /* FUNCTION: pthread_rwlock_rdlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
@@ -443,11 +382,6 @@ inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: pthread_rwlock_tryrdlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
@@ -460,11 +394,6 @@ inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: pthread_rwlock_trywrlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
@@ -477,11 +406,6 @@ inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: pthread_rwlock_unlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_rwlock_unlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
@@ -494,11 +418,6 @@ inline int pthread_rwlock_unlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: pthread_rwlock_wrlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
 {
   __CPROVER_HIDE:;
@@ -513,11 +432,6 @@ inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: pthread_create */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 extern unsigned long __CPROVER_next_thread_id;
@@ -560,11 +474,6 @@ inline int pthread_create(
 
 /* FUNCTION: pthread_cond_init */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_cond_init(
     pthread_cond_t *cond,
     const pthread_condattr_t *attr)
@@ -576,11 +485,6 @@ inline int pthread_cond_init(
 
 /* FUNCTION: pthread_cond_signal */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_cond_signal(
   pthread_cond_t *cond)
 { __CPROVER_HIDE:
@@ -592,11 +496,6 @@ inline int pthread_cond_signal(
 
 /* FUNCTION: pthread_cond_broadcast */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_cond_broadcast(
     pthread_cond_t *cond)
 { __CPROVER_HIDE:
@@ -608,11 +507,6 @@ inline int pthread_cond_broadcast(
 
 /* FUNCTION: pthread_cond_wait */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 inline int pthread_cond_wait(
     pthread_cond_t *cond,
     pthread_mutex_t *mutex)
@@ -643,11 +537,6 @@ inline int pthread_cond_wait(
 
 /* FUNCTION: pthread_spin_lock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 // no pthread_spinlock_t on the Mac
 #ifndef __APPLE__
 int pthread_spin_lock(pthread_spinlock_t *lock)
@@ -666,11 +555,6 @@ int pthread_spin_lock(pthread_spinlock_t *lock)
 
 /* FUNCTION: pthread_spin_unlock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 // no pthread_spinlock_t on the Mac
 #ifndef __APPLE__
 int pthread_spin_unlock(pthread_spinlock_t *lock)
@@ -687,11 +571,6 @@ int pthread_spin_unlock(pthread_spinlock_t *lock)
 
 /* FUNCTION: pthread_spin_trylock */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 #ifndef __CPROVER_ERRNO_H_INCLUDED
 #include <errno.h>
 #define __CPROVER_ERRNO_H_INCLUDED
@@ -721,11 +600,6 @@ int pthread_spin_trylock(pthread_spinlock_t *lock)
 
 /* FUNCTION: pthread_barrier_init */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 // no pthread_barrier_t on the Mac
@@ -751,11 +625,6 @@ inline int pthread_barrier_init(
 
 /* FUNCTION: pthread_barrier_destroy */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 // no pthread_barrier_t on the Mac
@@ -781,11 +650,6 @@ inline int pthread_barrier_destroy(pthread_barrier_t *barrier)
 
 /* FUNCTION: pthread_barrier_wait */
 
-#ifndef __CPROVER_PTHREAD_H_INCLUDED
-#include <pthread.h>
-#define __CPROVER_PTHREAD_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 // no pthread_barrier_t on the Mac
diff --git a/src/ansi-c/library/semaphore.c b/src/ansi-c/library/semaphore.c
index 5499a8ca72f..e2c458a7085 100644
--- a/src/ansi-c/library/semaphore.c
+++ b/src/ansi-c/library/semaphore.c
@@ -1,6 +1,8 @@
-/* FUNCTION: sem_init */
-
+#ifdef LIBRARY_CHECK
 #include <semaphore.h>
+#endif
+
+/* FUNCTION: sem_init */
 
 inline int sem_init(sem_t *sem, int pshared, unsigned int value)
 {
@@ -19,8 +21,6 @@ inline int sem_init(sem_t *sem, int pshared, unsigned int value)
 
 /* FUNCTION: sem_wait */
 
-#include <semaphore.h>
-
 inline int sem_wait(sem_t *sem)
 {
   __CPROVER_HIDE:;
@@ -38,8 +38,6 @@ inline int sem_wait(sem_t *sem)
 
 /* FUNCTION: sem_timedwait */
 
-#include <semaphore.h>
-
 inline int sem_timedwait(sem_t *sem, const struct timespec *abstime)
 {
   __CPROVER_HIDE:;
@@ -58,8 +56,6 @@ inline int sem_timedwait(sem_t *sem, const struct timespec *abstime)
 
 /* FUNCTION: sem_trywait */
 
-#include <semaphore.h>
-
 inline int sem_trywait(sem_t *sem)
 {
   __CPROVER_HIDE:;
@@ -77,8 +73,6 @@ inline int sem_trywait(sem_t *sem)
 
 /* FUNCTION: sem_post */
 
-#include <semaphore.h>
-
 inline int sem_post(sem_t *sem)
 {
   __CPROVER_HIDE:;
@@ -96,8 +90,6 @@ inline int sem_post(sem_t *sem)
 
 /* FUNCTION: sem_post_multiple */
 
-#include <semaphore.h>
-
 inline int sem_post_multiple(sem_t *sem, int number)
 {
   __CPROVER_HIDE:;
@@ -116,8 +108,6 @@ inline int sem_post_multiple(sem_t *sem, int number)
 
 /* FUNCTION: sem_getvalue */
 
-#include <semaphore.h>
-
 inline int sem_getvalue(sem_t *sem, int *sval)
 {
   __CPROVER_HIDE:;
@@ -136,8 +126,6 @@ inline int sem_getvalue(sem_t *sem, int *sval)
 
 /* FUNCTION: sem_destroy */
 
-#include <semaphore.h>
-
 inline int sem_destroy(sem_t *sem)
 {
   __CPROVER_HIDE:;
diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c
index 57c14998bb3..d56d06ca4f2 100644
--- a/src/ansi-c/library/setjmp.c
+++ b/src/ansi-c/library/setjmp.c
@@ -1,11 +1,9 @@
-
-/* FUNCTION: longjmp */
-
-#ifndef __CPROVER_SETJMP_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <setjmp.h>
-#define __CPROVER_SETJMP_H_INCLUDED
 #endif
 
+/* FUNCTION: longjmp */
+
 inline void longjmp(jmp_buf env, int val)
 {
   // does not return
@@ -16,11 +14,6 @@ inline void longjmp(jmp_buf env, int val)
 
 /* FUNCTION: _longjmp */
 
-#ifndef __CPROVER_SETJMP_H_INCLUDED
-#include <setjmp.h>
-#define __CPROVER_SETJMP_H_INCLUDED
-#endif
-
 inline void _longjmp(jmp_buf env, int val)
 {
   // does not return
@@ -31,11 +24,6 @@ inline void _longjmp(jmp_buf env, int val)
 
 /* FUNCTION: siglongjmp */
 
-#ifndef __CPROVER_SETJMP_H_INCLUDED
-#include <setjmp.h>
-#define __CPROVER_SETJMP_H_INCLUDED
-#endif
-
 inline void siglongjmp(sigjmp_buf env, int val)
 {
   // does not return
@@ -46,11 +34,6 @@ inline void siglongjmp(sigjmp_buf env, int val)
 
 /* FUNCTION: setjmp */
 
-#ifndef __CPROVER_SETJMP_H_INCLUDED
-#include <setjmp.h>
-#define __CPROVER_SETJMP_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int setjmp(jmp_buf env)
diff --git a/src/ansi-c/library/signal.c b/src/ansi-c/library/signal.c
index 45fb723a7a4..a4f7d8a32f5 100644
--- a/src/ansi-c/library/signal.c
+++ b/src/ansi-c/library/signal.c
@@ -1,14 +1,8 @@
-/* FUNCTION: kill */
-
-#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <sys/types.h>
-#define __CPROVER_SYS_TYPES_H_INCLUDED
 #endif
 
-#ifndef __CPROVER_SIGNAL_H_INCLUDED
-#include <signal.h>
-#define __CPROVER_SIGNAL_H_INCLUDED
-#endif
+/* FUNCTION: kill */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index d0ef51db92b..106f3832776 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -1,28 +1,22 @@
-
-/* FUNCTION: putchar */
-
-#ifndef __CPROVER_STDIO_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
+#include <stdarg.h>
 #endif
 
+/* FUNCTION: putchar */
+
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline int putchar(int c)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
-  printf("%c", c);
+  __CPROVER_printf("%c", c);
   return (error?-1:c);
 }
 
 /* FUNCTION: puts */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 int __VERIFIER_nondet_int();
 
@@ -31,23 +25,13 @@ inline int puts(const char *s)
   __CPROVER_HIDE:;
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
   int ret=__VERIFIER_nondet_int();
-  printf("%s\n", s);
+  __CPROVER_printf("%s\n", s);
   if(error) ret=-1; else __CPROVER_assume(ret>=0);
   return ret;
 }
 
 /* FUNCTION: fopen */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
-
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
 inline void fclose_cleanup(void *stream)
 {
@@ -59,6 +43,7 @@ inline void fclose_cleanup(void *stream)
 #endif
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+void *malloc(__CPROVER_size_t malloc_size);
 
 inline FILE *fopen(const char *filename, const char *mode)
 {
@@ -75,11 +60,11 @@ inline FILE *fopen(const char *filename, const char *mode)
   __CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool();
 
   #if !defined(__linux__) || defined(__GLIBC__)
-  fopen_result=fopen_error?NULL:malloc(sizeof(FILE));
+  fopen_result = fopen_error ? 0 : malloc(sizeof(FILE));
   #else
   // libraries need to expose the definition of FILE; this is the
   // case for musl
-  fopen_result=fopen_error?NULL:malloc(sizeof(int));
+  fopen_result = fopen_error ? 0 : malloc(sizeof(int));
   #endif
 
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
@@ -92,11 +77,6 @@ inline FILE *fopen(const char *filename, const char *mode)
 
 /* FUNCTION: freopen */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 inline FILE* freopen(const char *filename, const char *mode, FILE *f)
 {
   __CPROVER_HIDE:;
@@ -113,17 +93,8 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
 
 /* FUNCTION: fclose */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
+void free(void *ptr);
 
 inline int fclose(FILE *stream)
 {
@@ -141,15 +112,7 @@ inline int fclose(FILE *stream)
 
 /* FUNCTION: fdopen */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
+void *malloc(__CPROVER_size_t malloc_size);
 
 inline FILE *fdopen(int handle, const char *mode)
 {
@@ -179,17 +142,9 @@ inline FILE *fdopen(int handle, const char *mode)
 // header files rename fdopen to _fdopen and would thus yield
 // unbounded recursion.
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
-
 #ifdef __APPLE__
+void *malloc(__CPROVER_size_t malloc_size);
+
 inline FILE *_fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
@@ -208,11 +163,6 @@ inline FILE *_fdopen(int handle, const char *mode)
 
 /* FUNCTION: fgets */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 int __VERIFIER_nondet_int();
 
@@ -262,22 +212,14 @@ char *fgets(char *str, int size, FILE *stream)
 
 /* FUNCTION: fread */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+__CPROVER_size_t __VERIFIER_nondet_size_t();
 
-size_t __VERIFIER_nondet_size_t();
-
-inline size_t fread(
-  void *ptr,
-  size_t size,
-  size_t nitems,
-  FILE *stream)
+inline __CPROVER_size_t
+fread(void *ptr, __CPROVER_size_t size, __CPROVER_size_t nitems, FILE *stream)
 {
   __CPROVER_HIDE:;
-  size_t nread=__VERIFIER_nondet_size_t();
-  size_t bytes=nread*size;
+  __CPROVER_size_t nread = __VERIFIER_nondet_size_t();
+  __CPROVER_size_t bytes = nread * size;
   __CPROVER_assume(nread<=nitems);
 
   #if !defined(__linux__) || defined(__GLIBC__)
@@ -291,7 +233,7 @@ inline size_t fread(
                    "fread file must be open");
   #endif
 
-  for(size_t i=0; i<bytes; i++)
+  for(__CPROVER_size_t i = 0; i < bytes; i++)
   {
     char nondet_char;
     ((char *)ptr)[i]=nondet_char;
@@ -302,11 +244,6 @@ inline size_t fread(
 
 /* FUNCTION: feof */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int feof(FILE *stream)
@@ -331,11 +268,6 @@ inline int feof(FILE *stream)
 
 /* FUNCTION: ferror */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int ferror(FILE *stream)
@@ -360,11 +292,6 @@ inline int ferror(FILE *stream)
 
 /* FUNCTION: fileno */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int fileno(FILE *stream)
@@ -389,11 +316,6 @@ inline int fileno(FILE *stream)
 
 /* FUNCTION: fputs */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int fputs(const char *s, FILE *stream)
@@ -422,11 +344,6 @@ inline int fputs(const char *s, FILE *stream)
 
 /* FUNCTION: fflush */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int fflush(FILE *stream)
@@ -447,11 +364,6 @@ inline int fflush(FILE *stream)
 
 /* FUNCTION: fpurge */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int fpurge(FILE *stream)
@@ -476,11 +388,6 @@ inline int fpurge(FILE *stream)
 
 /* FUNCTION: fgetc */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int fgetc(FILE *stream)
@@ -507,11 +414,6 @@ inline int fgetc(FILE *stream)
 
 /* FUNCTION: getc */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int getc(FILE *stream)
@@ -540,11 +442,6 @@ inline int getc(FILE *stream)
 
 /* FUNCTION: getchar */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int getchar()
@@ -559,11 +456,6 @@ inline int getchar()
 
 /* FUNCTION: getw */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int getw(FILE *stream)
@@ -590,11 +482,6 @@ inline int getw(FILE *stream)
 
 /* FUNCTION: fseek */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int fseek(FILE *stream, long offset, int whence)
@@ -620,11 +507,6 @@ inline int fseek(FILE *stream, long offset, int whence)
 
 /* FUNCTION: ftell */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 long __VERIFIER_nondet_long();
 
 inline long ftell(FILE *stream)
@@ -648,11 +530,6 @@ inline long ftell(FILE *stream)
 
 /* FUNCTION: rewind */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 void rewind(FILE *stream)
 {
   __CPROVER_HIDE:
@@ -671,17 +548,12 @@ void rewind(FILE *stream)
 
 /* FUNCTION: fwrite */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-size_t __VERIFIER_nondet_size_t();
+__CPROVER_size_t __VERIFIER_nondet_size_t();
 
-size_t fwrite(
+__CPROVER_size_t fwrite(
   const void *ptr,
-  size_t size,
-  size_t nitems,
+  __CPROVER_size_t size,
+  __CPROVER_size_t nitems,
   FILE *stream)
 {
   __CPROVER_HIDE:;
@@ -699,18 +571,13 @@ size_t fwrite(
                    "fwrite file must be open");
   #endif
 
-  size_t nwrite=__VERIFIER_nondet_size_t();
+  __CPROVER_size_t nwrite = __VERIFIER_nondet_size_t();
   __CPROVER_assume(nwrite<=nitems);
   return nwrite;
 }
 
 /* FUNCTION: perror */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
 void perror(const char *s)
 {
   __CPROVER_HIDE:;
@@ -721,7 +588,7 @@ void perror(const char *s)
     #endif
     // should go to stderr
     if(s[0]!=0)
-      printf("%s: ", s);
+      __CPROVER_printf("%s: ", s);
   }
 
   // TODO: print errno error
@@ -729,15 +596,7 @@ void perror(const char *s)
 
 /* FUNCTION: fscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg);
 
 inline int fscanf(FILE *restrict stream, const char *restrict format, ...)
 {
@@ -751,15 +610,7 @@ inline int fscanf(FILE *restrict stream, const char *restrict format, ...)
 
 /* FUNCTION: scanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg);
 
 inline int scanf(const char *restrict format, ...)
 {
@@ -773,15 +624,7 @@ inline int scanf(const char *restrict format, ...)
 
 /* FUNCTION: sscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+int vsscanf(const char *restrict s, const char *restrict format, va_list arg);
 
 inline int sscanf(const char *restrict s, const char *restrict format, ...)
 {
@@ -795,16 +638,6 @@ inline int sscanf(const char *restrict s, const char *restrict format, ...)
 
 /* FUNCTION: vfscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
@@ -829,15 +662,7 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a
 
 /* FUNCTION: vscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg);
 
 inline int vscanf(const char *restrict format, va_list arg)
 {
@@ -847,16 +672,6 @@ inline int vscanf(const char *restrict format, va_list arg)
 
 /* FUNCTION: vsscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
@@ -871,15 +686,7 @@ inline int vsscanf(const char *restrict s, const char *restrict format, va_list
 
 /* FUNCTION: fprintf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+int vfprintf(FILE *stream, const char *restrict format, va_list arg);
 
 inline int fprintf(FILE *stream, const char *restrict format, ...)
 {
@@ -893,16 +700,6 @@ inline int fprintf(FILE *stream, const char *restrict format, ...)
 
 /* FUNCTION: vfprintf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
@@ -929,23 +726,9 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 
 /* FUNCTION: vasprintf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
-
 char __VERIFIER_nondet_char();
 int __VERIFIER_nondet_int();
+void *malloc(__CPROVER_size_t malloc_size);
 
 inline int vasprintf(char **ptr, const char *fmt, va_list ap)
 {
diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
index 8781b77c35d..21b59222222 100644
--- a/src/ansi-c/library/string.c
+++ b/src/ansi-c/library/string.c
@@ -47,7 +47,7 @@ __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size
   __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,
                    "strcat buffer overflow");
   __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst);
-  //"  for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
+  //"  for(__CPROVER_size_t i=0; i<__CPROVER_zero_string_length(src); i++)
   //"    dst[old_size+i];
   dst[new_size]=0;
   __CPROVER_is_zero_string(dst)=1;
@@ -120,13 +120,6 @@ __inline char *__builtin___strncat_chk(
 
 /* FUNCTION: strcpy */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strcpy
-
 inline char *strcpy(char *dst, const char *src)
 {
   __CPROVER_HIDE:;
@@ -158,14 +151,7 @@ inline char *strcpy(char *dst, const char *src)
 
 /* FUNCTION: strncpy */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strncpy
-
-inline char *strncpy(char *dst, const char *src, size_t n)
+inline char *strncpy(char *dst, const char *src, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -197,12 +183,11 @@ inline char *strncpy(char *dst, const char *src, size_t n)
 
 /* FUNCTION: __builtin___strncpy_chk */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size)
+inline char *__builtin___strncpy_chk(
+  char *dst,
+  const char *src,
+  __CPROVER_size_t n,
+  __CPROVER_size_t object_size)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -237,13 +222,6 @@ inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_
 
 /* FUNCTION: strcat */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strcat
-
 inline char *strcat(char *dst, const char *src)
 {
   __CPROVER_HIDE:;
@@ -257,7 +235,7 @@ inline char *strcat(char *dst, const char *src)
   __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,
                    "strcat buffer overflow");
   __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst);
-  //"  for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
+  //"  for(__CPROVER_size_t i=0; i<__CPROVER_zero_string_length(src); i++)
   //"    dst[old_size+i];
   dst[new_size]=0;
   __CPROVER_is_zero_string(dst)=1;
@@ -283,14 +261,7 @@ inline char *strcat(char *dst, const char *src)
 
 /* FUNCTION: strncat */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strncat
-
-inline char *strncat(char *dst, const char *src, size_t n)
+inline char *strncat(char *dst, const char *src, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -334,13 +305,6 @@ inline char *strncat(char *dst, const char *src, size_t n)
 
 /* FUNCTION: strcmp */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strcmp
-
 inline int strcmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
@@ -380,13 +344,6 @@ inline int strcmp(const char *s1, const char *s2)
 
 /* FUNCTION: strcasecmp */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strcasecmp
-
 inline int strcasecmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
@@ -429,14 +386,7 @@ inline int strcasecmp(const char *s1, const char *s2)
 
 /* FUNCTION: strncmp */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strncmp
-
-inline int strncmp(const char *s1, const char *s2, size_t n)
+inline int strncmp(const char *s1, const char *s2, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -471,14 +421,7 @@ inline int strncmp(const char *s1, const char *s2, size_t n)
 
 /* FUNCTION: strncasecmp */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strncasecmp
-
-inline int strncasecmp(const char *s1, const char *s2, size_t n)
+inline int strncasecmp(const char *s1, const char *s2, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -516,14 +459,7 @@ inline int strncasecmp(const char *s1, const char *s2, size_t n)
 
 /* FUNCTION: strlen */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strlen
-
-inline size_t strlen(const char *s)
+inline __CPROVER_size_t strlen(const char *s)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -539,18 +475,8 @@ inline size_t strlen(const char *s)
 
 /* FUNCTION: strdup */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
-
-#undef strdup
-#undef strcpy
+void *malloc(__CPROVER_size_t malloc_size);
+char *strcpy(char *dst, const char *src);
 
 inline char *strdup(const char *str)
 {
@@ -568,14 +494,7 @@ inline char *strdup(const char *str)
 
 /* FUNCTION: memcpy */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef memcpy
-
-void *memcpy(void *dst, const void *src, size_t n)
+void *memcpy(void *dst, const void *src, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -583,7 +502,7 @@ void *memcpy(void *dst, const void *src, size_t n)
                          "memcpy buffer overflow");
   __CPROVER_precondition(__CPROVER_buffer_size(dst)>=n,
                          "memcpy buffer overflow");
-  //  for(size_t i=0; i<n ; i++) dst[i]=src[i];
+  //  for(__CPROVER_size_t i=0; i<n ; i++) dst[i]=src[i];
   if(__CPROVER_is_zero_string(src) &&
      n > __CPROVER_zero_string_length(src))
   {
@@ -625,7 +544,7 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
                          "memcpy buffer overflow");
   __CPROVER_precondition(__CPROVER_buffer_size(dst)==s,
                          "builtin object size");
-  //  for(size_t i=0; i<n ; i++) dst[i]=src[i];
+  //  for(__CPROVER_size_t i=0; i<n ; i++) dst[i]=src[i];
   if(__CPROVER_is_zero_string(src) &&
      n > __CPROVER_zero_string_length(src))
   {
@@ -658,20 +577,13 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
 
 /* FUNCTION: memset */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef memset
-
-void *memset(void *s, int c, size_t n)
+void *memset(void *s, int c, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
                          "memset buffer overflow");
-  //  for(size_t i=0; i<n ; i++) s[i]=c;
+  //  for(__CPROVER_size_t i=0; i<n ; i++) s[i]=c;
   if(__CPROVER_is_zero_string(s) &&
      n > __CPROVER_zero_string_length(s))
   {
@@ -708,7 +620,7 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
                          "memset buffer overflow");
-  //  for(size_t i=0; i<n ; i++) s[i]=c;
+  //  for(__CPROVER_size_t i=0; i<n ; i++) s[i]=c;
   if(__CPROVER_is_zero_string(s) &&
      n > __CPROVER_zero_string_length(s))
   {
@@ -749,7 +661,7 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
                          "memset buffer overflow");
   __CPROVER_precondition(__CPROVER_buffer_size(s)==size,
                          "builtin object size");
-  //  for(size_t i=0; i<n ; i++) s[i]=c;
+  //  for(__CPROVER_size_t i=0; i<n ; i++) s[i]=c;
   if(__CPROVER_is_zero_string(s) &&
      n > __CPROVER_zero_string_length(s))
   {
@@ -781,14 +693,7 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
 
 /* FUNCTION: memmove */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef memmove
-
-void *memmove(void *dest, const void *src, size_t n)
+void *memmove(void *dest, const void *src, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -821,14 +726,11 @@ void *memmove(void *dest, const void *src, size_t n)
 
 /* FUNCTION: __builtin___memmove_chk */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef memmove
-
-void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
+void *__builtin___memmove_chk(
+  void *dest,
+  const void *src,
+  __CPROVER_size_t n,
+  __CPROVER_size_t size)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
@@ -866,14 +768,7 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
 
 /* FUNCTION: memcmp */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef memcmp
-
-inline int memcmp(const void *s1, const void *s2, size_t n)
+inline int memcmp(const void *s1, const void *s2, __CPROVER_size_t n)
 {
   __CPROVER_HIDE:;
   int res=0;
@@ -896,13 +791,6 @@ inline int memcmp(const void *s1, const void *s2, size_t n)
 
 /* FUNCTION: strchr */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strchr
-
 inline char *strchr(const char *src, int c)
 {
   __CPROVER_HIDE:;
@@ -925,13 +813,6 @@ inline char *strchr(const char *src, int c)
 
 /* FUNCTION: strrchr */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
-#undef strchr
-
 inline char *strrchr(const char *src, int c)
 {
   __CPROVER_HIDE:;
@@ -954,11 +835,6 @@ inline char *strrchr(const char *src, int c)
 
 /* FUNCTION: strerror */
 
-#ifndef __CPROVER_STRING_H_INCLUDED
-#include <string.h>
-#define __CPROVER_STRING_H_INCLUDED
-#endif
-
 char *strerror(int errnum)
 {
   __CPROVER_HIDE:;
diff --git a/src/ansi-c/library/syslog.c b/src/ansi-c/library/syslog.c
index 4acd52ca16c..c72f9c45dd0 100644
--- a/src/ansi-c/library/syslog.c
+++ b/src/ansi-c/library/syslog.c
@@ -1,10 +1,5 @@
 /* FUNCTION: openlog */
 
-#ifndef __CPROVER_SYSLOG_H_INCLUDED
-#include <syslog.h>
-#define __CPROVER_SYSLOG_H_INCLUDED
-#endif
-
 void openlog(const char *ident, int option, int facility)
 {
   (void)*ident;
@@ -14,22 +9,12 @@ void openlog(const char *ident, int option, int facility)
 
 /* FUNCTION: closelog */
 
-#ifndef __CPROVER_SYSLOG_H_INCLUDED
-#include <syslog.h>
-#define __CPROVER_SYSLOG_H_INCLUDED
-#endif
-
 void closelog(void)
 {
 }
 
 /* FUNCTION: syslog */
 
-#ifndef __CPROVER_SYSLOG_H_INCLUDED
-#include <syslog.h>
-#define __CPROVER_SYSLOG_H_INCLUDED
-#endif
-
 void syslog(int priority, const char *format, ...)
 {
   (void)priority;
diff --git a/src/ansi-c/library/threads.c b/src/ansi-c/library/threads.c
index d0c10ac03e0..bd63208ac7d 100644
--- a/src/ansi-c/library/threads.c
+++ b/src/ansi-c/library/threads.c
@@ -1,45 +1,29 @@
+#ifdef LIBRARY_CHECK
+#include <threads.h>
+#endif
+
 /* FUNCTION: thrd_create */
 
 // following http://en.cppreference.com/w/c/thread
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int thrd_create(thrd_t *thr, thrd_start_t func, void *arg)
 {
 }
 
 /* FUNCTION: thrd_equal */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int thrd_equal( thrd_t lhs, thrd_t rhs )
 {
 }
 
 /* FUNCTION: thrd_current */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 thrd_t thrd_current()
 {
 }
 
 /* FUNCTION: thrd_sleep */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int thrd_sleep(const struct timespec* time_point,
                struct timespec* remaining)
 {
@@ -60,33 +44,18 @@ void thrd_exit(int res)
 
 /* FUNCTION: mtx_init */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int mtx_init( mtx_t* mutex, int type )
 {
 }
 
 /* FUNCTION: mtx_lock */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int mtx_lock(mtx_t* mutex)
 {
 }
 
 /* FUNCTION: mtx_timedlock */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int mtx_timedlock(mtx_t *restrict mutex,
                   const struct timespec *restrict time_point)
 {
@@ -95,22 +64,12 @@ int mtx_timedlock(mtx_t *restrict mutex,
 
 /* FUNCTION: mtx_trylock */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int mtx_trylock(mtx_t *mutex)
 {
 }
 
 /* FUNCTION: mtx_unlock */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int mtx_unlock(mtx_t *mutex)
 {
 
@@ -118,44 +77,24 @@ int mtx_unlock(mtx_t *mutex)
 
 /* FUNCTION: mtx_destroy */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 void mtx_destroy(mtx_t *mutex)
 {
 }
 
 /* FUNCTION: call_once */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 void call_once(once_flag* flag, void (*func)(void))
 {
 }
 
 /* FUNCTION: cnd_init */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int cnd_init(cnd_t* cond)
 {
 }
 
 /* FUNCTION: cnd_signal */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int cnd_signal(cnd_t *cond)
 {
 
@@ -163,33 +102,18 @@ int cnd_signal(cnd_t *cond)
 
 /* FUNCTION: cnd_broadcast */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int cnd_broadcast(cnd_t *cond)
 {
 }
 
 /* FUNCTION: cnd_wait */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int cnd_wait(cnd_t* cond, mtx_t* mutex)
 {
 }
 
 /* FUNCTION: cnd_timedwait */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 int cnd_timedwait(cnd_t* restrict cond, mtx_t* restrict mutex,
                   const struct timespec* restrict time_point)
 {
@@ -197,11 +121,6 @@ int cnd_timedwait(cnd_t* restrict cond, mtx_t* restrict mutex,
 
 /* FUNCTION: cnd_destroy */
 
-#ifndef __CPROVER_THREADS_H_INCLUDED
-#include <threads.h>
-#define __CPROVER_THREADS_H_INCLUDED
-#endif
-
 void cnd_destroy(cnd_t* cond)
 {
 }
diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c
index 71606de0012..d92098e6584 100644
--- a/src/ansi-c/library/time.c
+++ b/src/ansi-c/library/time.c
@@ -1,11 +1,8 @@
-/* FUNCTION: time */
-
-#ifndef __CPROVER_TIME_H_INCLUDED
+#ifdef LIBRARY_CHECK
 #include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
 #endif
 
-#undef time
+/* FUNCTION: time */
 
 time_t __VERIFIER_nondet_time_t();
 
@@ -18,13 +15,6 @@ time_t time(time_t *tloc)
 
 /* FUNCTION: gmtime */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
-#undef gmtime
-
 struct tm *gmtime(const time_t *clock)
 {
   // not very general, may be too restrictive
@@ -43,13 +33,6 @@ struct tm *gmtime(const time_t *clock)
 
 /* FUNCTION: gmtime_r */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
-#undef gmtime
-
 struct tm *gmtime_r(const time_t *clock, struct tm *result)
 {
   // need to set the fields to something meaningful
@@ -59,13 +42,6 @@ struct tm *gmtime_r(const time_t *clock, struct tm *result)
 
 /* FUNCTION: localtime */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
-#undef localtime
-
 struct tm *localtime(const time_t *clock)
 {
   // not very general, may be too restrictive
@@ -84,13 +60,6 @@ struct tm *localtime(const time_t *clock)
 
 /* FUNCTION: localtime_r */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
-#undef localtime
-
 struct tm *localtime_r(const time_t *clock, struct tm *result)
 {
   // need to set the fields to something meaningful
@@ -100,13 +69,6 @@ struct tm *localtime_r(const time_t *clock, struct tm *result)
 
 /* FUNCTION: mktime */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
-#undef mktime
-
 time_t __VERIFIER_nondet_time_t();
 
 time_t mktime(struct tm *timeptr)
@@ -118,13 +80,6 @@ time_t mktime(struct tm *timeptr)
 
 /* FUNCTION: timegm */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
-#undef timegm
-
 time_t __VERIFIER_nondet_time_t();
 
 time_t timegm(struct tm *timeptr)
@@ -136,11 +91,6 @@ time_t timegm(struct tm *timeptr)
 
 /* FUNCTION: asctime */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
 char *asctime(const struct tm *timeptr)
 {
   (void)*timeptr;
@@ -157,11 +107,6 @@ char *asctime(const struct tm *timeptr)
 
 /* FUNCTION: ctime */
 
-#ifndef __CPROVER_TIME_H_INCLUDED
-#include <time.h>
-#define __CPROVER_TIME_H_INCLUDED
-#endif
-
 char *ctime(const time_t *clock)
 {
   (void)*clock;
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c
index 7f57c5a5d45..806bfae7302 100644
--- a/src/ansi-c/library/unistd.c
+++ b/src/ansi-c/library/unistd.c
@@ -126,12 +126,8 @@ inline int _close(int fildes)
 #define ret_type int
 #define size_type unsigned
 #else
-#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
-#include <sys/types.h>
-#define __CPROVER_SYS_TYPES_H_INCLUDED
-#endif
-#define ret_type ssize_t
-#define size_type size_t
+#define ret_type long int
+#define size_type __CPROVER_size_t
 #endif
 
 extern struct __CPROVER_pipet __CPROVER_pipes[];
@@ -175,12 +171,8 @@ ret_type write(int fildes, const void *buf, size_type nbyte)
 #define ret_type int
 #define size_type unsigned
 #else
-#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
-#include <sys/types.h>
-#define __CPROVER_SYS_TYPES_H_INCLUDED
-#endif
-#define ret_type ssize_t
-#define size_type size_t
+#define ret_type long int
+#define size_type __CPROVER_size_t
 #endif
 
 ret_type write(int fildes, const void *buf, size_type nbyte);
@@ -200,12 +192,8 @@ inline ret_type _write(int fildes, const void *buf, size_type nbyte)
 #define ret_type int
 #define size_type unsigned
 #else
-#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
-#include <sys/types.h>
-#define __CPROVER_SYS_TYPES_H_INCLUDED
-#endif
-#define ret_type ssize_t
-#define size_type size_t
+#define ret_type long int
+#define size_type __CPROVER_size_t
 #endif
 
 extern struct __CPROVER_pipet __CPROVER_pipes[];
@@ -279,12 +267,8 @@ ret_type read(int fildes, void *buf, size_type nbyte)
 #define ret_type int
 #define size_type unsigned
 #else
-#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
-#include <sys/types.h>
-#define __CPROVER_SYS_TYPES_H_INCLUDED
-#endif
-#define ret_type ssize_t
-#define size_type size_t
+#define ret_type long int
+#define size_type __CPROVER_size_t
 #endif
 
 ret_type read(int fildes, void *buf, size_type nbyte);
diff --git a/src/ansi-c/library/windows.c b/src/ansi-c/library/windows.c
index 1c6b5e758bf..d50065dc2a2 100644
--- a/src/ansi-c/library/windows.c
+++ b/src/ansi-c/library/windows.c
@@ -1,7 +1,12 @@
+#ifdef _WIN32
+#ifdef LIBRARY_CHECK
+#include <windows.h>
+#endif
+#endif
+
 /* FUNCTION: QueryPerformanceFrequency */
 
 #ifdef _WIN32
-#include <windows.h>
 
 BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency)
 {
@@ -18,7 +23,6 @@ BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency)
 /* FUNCTION: ExitThread */
 
 #ifdef _WIN32
-#include <windows.h>
 
 inline VOID ExitThread(DWORD dwExitCode)
 {
@@ -30,7 +34,6 @@ inline VOID ExitThread(DWORD dwExitCode)
 /* FUNCTION: CreateThread */
 
 #ifdef _WIN32
-#include <windows.h>
 
 inline HANDLE CreateThread(
   LPSECURITY_ATTRIBUTES lpThreadAttributes,