diff --git a/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc b/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc
index d1c7ba53cbc..7b61cb34c49 100644
--- a/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc
+++ b/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc
@@ -1,7 +1,7 @@
 CORE new-smt-backend
 enum_test3.c
 --show-goto-functions
-0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4$
+0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/ansi-c/c_expr.cpp b/src/ansi-c/c_expr.cpp
index beb999f4129..92cec4044f2 100644
--- a/src/ansi-c/c_expr.cpp
+++ b/src/ansi-c/c_expr.cpp
@@ -9,6 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_expr.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/namespace.h>
+#include <util/simplify_expr.h>
 
 shuffle_vector_exprt::shuffle_vector_exprt(
   exprt vector1,
@@ -64,3 +67,19 @@ vector_exprt shuffle_vector_exprt::lower() const
 
   return vector_exprt{std::move(operands), type()};
 }
+
+exprt enum_is_in_range_exprt::lower(const namespacet &ns) const
+{
+  const auto &enum_type = to_c_enum_tag_type(op().type());
+  const c_enum_typet &c_enum_type = ns.follow_tag(enum_type);
+  const c_enum_typet::memberst enum_values = c_enum_type.members();
+
+  exprt::operandst disjuncts;
+  for(const auto &enum_value : enum_values)
+  {
+    constant_exprt val{enum_value.get_value(), enum_type};
+    disjuncts.push_back(equal_exprt(op(), std::move(val)));
+  }
+
+  return simplify_expr(disjunction(disjuncts), ns);
+}
diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h
index c58c4e41716..55b820cc60f 100644
--- a/src/ansi-c/c_expr.h
+++ b/src/ansi-c/c_expr.h
@@ -320,4 +320,54 @@ to_conditional_target_group_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A Boolean expression returning true, iff the value of an enum-typed
+/// symbol equals one of the enum's declared values.
+class enum_is_in_range_exprt : public unary_predicate_exprt
+{
+public:
+  explicit enum_is_in_range_exprt(exprt _op)
+    : unary_predicate_exprt(ID_enum_is_in_range, std::move(_op))
+  {
+    op().add_source_location().add_pragma("disable:enum-range-check");
+  }
+
+  exprt lower(const namespacet &ns) const;
+};
+
+template <>
+inline bool can_cast_expr<enum_is_in_range_exprt>(const exprt &base)
+{
+  return base.id() == ID_enum_is_in_range;
+}
+
+inline void validate_expr(const enum_is_in_range_exprt &expr)
+{
+  validate_operands(
+    expr, 1, "enum_is_in_range expression must have one operand");
+}
+
+/// \brief Cast an exprt to an \ref enum_is_in_range_exprt
+///
+/// \a expr must be known to be \ref enum_is_in_range_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref enum_is_in_range_exprt
+inline const enum_is_in_range_exprt &to_enum_is_in_range_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_enum_is_in_range);
+  const enum_is_in_range_exprt &ret =
+    static_cast<const enum_is_in_range_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_side_effect_expr_overflow(const exprt &)
+inline enum_is_in_range_exprt &to_enum_is_in_range_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_enum_is_in_range);
+  enum_is_in_range_exprt &ret = static_cast<enum_is_in_range_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_ANSI_C_C_EXPR_H
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 9d6efd36a62..c215f44c851 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2118,6 +2118,106 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
         return;
       }
+      else if(identifier == CPROVER_PREFIX "equal")
+      {
+        if(expr.arguments().size() != 2)
+        {
+          error().source_location = f_op.source_location();
+          error() << "equal expects two operands" << eom;
+          throw 0;
+        }
+
+        equal_exprt equality_expr(
+          expr.arguments().front(), expr.arguments().back());
+        equality_expr.add_source_location() = expr.source_location();
+
+        if(equality_expr.lhs().type() != equality_expr.rhs().type())
+        {
+          error().source_location = f_op.source_location();
+          error() << "equal expects two operands of same type" << eom;
+          throw 0;
+        }
+
+        expr.swap(equality_expr);
+        return;
+      }
+      else if(
+        identifier == CPROVER_PREFIX "overflow_minus" ||
+        identifier == CPROVER_PREFIX "overflow_mult" ||
+        identifier == CPROVER_PREFIX "overflow_plus" ||
+        identifier == CPROVER_PREFIX "overflow_shl")
+      {
+        exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
+        overflow.add_source_location() = f_op.source_location();
+
+        if(identifier == CPROVER_PREFIX "overflow_minus")
+        {
+          overflow.id(ID_minus);
+          typecheck_expr_binary_arithmetic(overflow);
+        }
+        else if(identifier == CPROVER_PREFIX "overflow_mult")
+        {
+          overflow.id(ID_mult);
+          typecheck_expr_binary_arithmetic(overflow);
+        }
+        else if(identifier == CPROVER_PREFIX "overflow_plus")
+        {
+          overflow.id(ID_plus);
+          typecheck_expr_binary_arithmetic(overflow);
+        }
+        else if(identifier == CPROVER_PREFIX "overflow_shl")
+        {
+          overflow.id(ID_shl);
+          typecheck_expr_shifts(to_shift_expr(overflow));
+        }
+
+        binary_overflow_exprt of{
+          overflow.operands()[0], overflow.id(), overflow.operands()[1]};
+        of.add_source_location() = overflow.source_location();
+        expr.swap(of);
+        return;
+      }
+      else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
+      {
+        exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
+        tmp.add_source_location() = f_op.source_location();
+
+        typecheck_expr_unary_arithmetic(tmp);
+
+        unary_minus_overflow_exprt overflow{tmp.operands().front()};
+        overflow.add_source_location() = tmp.source_location();
+        expr.swap(overflow);
+        return;
+      }
+      else if(identifier == CPROVER_PREFIX "enum_is_in_range")
+      {
+        // Check correct number of arguments
+        if(expr.arguments().size() != 1)
+        {
+          std::ostringstream error_message;
+          error_message << identifier << " takes exactly 1 argument, but "
+                        << expr.arguments().size() << " were provided";
+          throw invalid_source_file_exceptiont{
+            error_message.str(), expr.source_location()};
+        }
+        const auto &arg1 = expr.arguments()[0];
+        if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
+        {
+          // Can't enum range check a non-enum
+          std::ostringstream error_message;
+          error_message << identifier << " expects enum, but ("
+                        << expr2c(arg1, *this) << ") has type `"
+                        << type2c(arg1.type(), *this) << '`';
+          throw invalid_source_file_exceptiont{
+            error_message.str(), expr.source_location()};
+        }
+
+        enum_is_in_range_exprt in_range{arg1};
+        in_range.add_source_location() = expr.source_location();
+        exprt lowered = in_range.lower(*this);
+        expr.swap(lowered);
+        return;
+      }
       else if(
         auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
           identifier, expr.arguments(), f_op.source_location()))
@@ -2534,11 +2634,15 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
+    exprt::operandst args_no_cast;
+    args_no_cast.reserve(expr.arguments().size());
     for(const auto &argument : expr.arguments())
     {
+      args_no_cast.push_back(skip_typecast(argument));
       if(
-        argument.type().id() != ID_pointer ||
-        to_pointer_type(argument.type()).base_type().id() != ID_struct_tag)
+        args_no_cast.back().type().id() != ID_pointer ||
+        to_pointer_type(args_no_cast.back().type()).base_type().id() !=
+          ID_struct_tag)
       {
         error().source_location = expr.arguments()[0].source_location();
         error() << "is_sentinel_dll_node expects struct-pointer operands"
@@ -2548,7 +2652,7 @@ exprt c_typecheck_baset::do_special_functions(
     }
 
     predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
-    is_sentinel_dll_expr.operands() = expr.arguments();
+    is_sentinel_dll_expr.operands() = args_no_cast;
     is_sentinel_dll_expr.add_source_location() = source_location;
 
     return std::move(is_sentinel_dll_expr);
@@ -3324,30 +3428,6 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(ffs);
   }
-  else if(identifier==CPROVER_PREFIX "equal")
-  {
-    if(expr.arguments().size()!=2)
-    {
-      error().source_location = f_op.source_location();
-      error() << "equal expects two operands" << eom;
-      throw 0;
-    }
-
-    typecheck_function_call_arguments(expr);
-
-    equal_exprt equality_expr(
-      expr.arguments().front(), expr.arguments().back());
-    equality_expr.add_source_location()=source_location;
-
-    if(equality_expr.lhs().type() != equality_expr.rhs().type())
-    {
-      error().source_location = f_op.source_location();
-      error() << "equal expects two operands of same type" << eom;
-      throw 0;
-    }
-
-    return std::move(equality_expr);
-  }
   else if(identifier=="__builtin_expect")
   {
     // This is a gcc extension to provide branch prediction.
@@ -3533,80 +3613,6 @@ exprt c_typecheck_baset::do_special_functions(
 
     return tmp;
   }
-  else if(
-    identifier == CPROVER_PREFIX "overflow_minus" ||
-    identifier == CPROVER_PREFIX "overflow_mult" ||
-    identifier == CPROVER_PREFIX "overflow_plus" ||
-    identifier == CPROVER_PREFIX "overflow_shl")
-  {
-    exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
-    overflow.add_source_location() = f_op.source_location();
-
-    if(identifier == CPROVER_PREFIX "overflow_minus")
-    {
-      overflow.id(ID_minus);
-      typecheck_expr_binary_arithmetic(overflow);
-    }
-    else if(identifier == CPROVER_PREFIX "overflow_mult")
-    {
-      overflow.id(ID_mult);
-      typecheck_expr_binary_arithmetic(overflow);
-    }
-    else if(identifier == CPROVER_PREFIX "overflow_plus")
-    {
-      overflow.id(ID_plus);
-      typecheck_expr_binary_arithmetic(overflow);
-    }
-    else if(identifier == CPROVER_PREFIX "overflow_shl")
-    {
-      overflow.id(ID_shl);
-      typecheck_expr_shifts(to_shift_expr(overflow));
-    }
-
-    binary_overflow_exprt of{
-      overflow.operands()[0], overflow.id(), overflow.operands()[1]};
-    of.add_source_location() = overflow.source_location();
-    return std::move(of);
-  }
-  else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
-  {
-    exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
-    tmp.add_source_location() = f_op.source_location();
-
-    typecheck_expr_unary_arithmetic(tmp);
-
-    unary_minus_overflow_exprt overflow{tmp.operands().front()};
-    overflow.add_source_location() = tmp.source_location();
-    return std::move(overflow);
-  }
-  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
-  {
-    // Check correct number of arguments
-    if(expr.arguments().size() != 1)
-    {
-      std::ostringstream error_message;
-      error_message << identifier << " takes exactly 1 argument, but "
-                    << expr.arguments().size() << " were provided";
-      throw invalid_source_file_exceptiont{
-        error_message.str(), expr.source_location()};
-    }
-    auto arg1 = expr.arguments()[0];
-    typecheck_expr(arg1);
-    if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
-    {
-      // Can't enum range check a non-enum
-      std::ostringstream error_message;
-      error_message << identifier << " expects enum, but ("
-                    << expr2c(arg1, *this) << ") has type `"
-                    << type2c(arg1.type(), *this) << '`';
-      throw invalid_source_file_exceptiont{
-        error_message.str(), expr.source_location()};
-    }
-    else
-    {
-      return expr;
-    }
-  }
   else if(
     identifier == "__builtin_add_overflow" ||
     identifier == "__builtin_sadd_overflow" ||
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
index 2463de8d629..f0ae5e74004 100644
--- a/src/ansi-c/cprover_builtin_headers.h
+++ b/src/ansi-c/cprover_builtin_headers.h
@@ -6,21 +6,17 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description
 void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
 void __CPROVER_havoc_object(void *);
 void __CPROVER_havoc_slice(void *, __CPROVER_size_t);
-__CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 _Bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
-__CPROVER_bool __CPROVER_r_ok();
-__CPROVER_bool __CPROVER_w_ok();
-__CPROVER_bool __CPROVER_rw_ok();
 
 // experimental features for CHC encodings -- do not use
-__CPROVER_bool __CPROVER_is_list(); // a singly-linked null-terminated dynamically-allocated list
-__CPROVER_bool __CPROVER_is_dll();
-__CPROVER_bool __CPROVER_is_cyclic_dll();
-__CPROVER_bool __CPROVER_is_sentinel_dll();
+__CPROVER_bool __CPROVER_is_list(const void *); // a singly-linked null-terminated dynamically-allocated list
+__CPROVER_bool __CPROVER_is_dll(const void *);
+__CPROVER_bool __CPROVER_is_cyclic_dll(const void *);
+__CPROVER_bool __CPROVER_is_sentinel_dll(const void *, ...);
 __CPROVER_bool __CPROVER_is_cstring(const char *);
 __CPROVER_size_t __CPROVER_cstrlen(const char *);
 __CPROVER_bool __CPROVER_separate(const void *, const void *, ...);
@@ -41,8 +37,8 @@ void __CPROVER_output(const char *id, ...);
 void __CPROVER_cover(__CPROVER_bool condition);
 
 // concurrency-related
-void __CPROVER_atomic_begin();
-void __CPROVER_atomic_end();
+void __CPROVER_atomic_begin(void);
+void __CPROVER_atomic_end(void);
 void __CPROVER_fence(const char *kind, ...);
 
 // contract-related functions
@@ -124,22 +120,11 @@ void __CPROVER_array_replace(const void *dest, const void *src);
 void __CPROVER_array_set(const void *dest, ...);
 
 // k-induction
-void __CPROVER_k_induction_hint(unsigned min, unsigned max, 
-  unsigned step, unsigned loop_free);
+void __CPROVER_k_induction_hint(unsigned min, unsigned max, unsigned step, unsigned loop_free);
 
 // format string-related
 int __CPROVER_scanf(const char *, ...);
 
-// detect overflow
-__CPROVER_bool __CPROVER_overflow_minus();
-__CPROVER_bool __CPROVER_overflow_mult();
-__CPROVER_bool __CPROVER_overflow_plus();
-__CPROVER_bool __CPROVER_overflow_shl();
-__CPROVER_bool __CPROVER_overflow_unary_minus();
-
-// enumerations
-__CPROVER_bool __CPROVER_enum_is_in_range();
-
 // contracts
 void __CPROVER_assignable(void *ptr, __CPROVER_size_t size,
   __CPROVER_bool is_ptr_to_ptr);
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index 25f8a32c23c..5c58d8459e1 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/src/ansi-c/goto_check_c.cpp
@@ -41,6 +41,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include "c_expr.h"
+
 #include <algorithm>
 
 class goto_check_ct
@@ -523,19 +525,15 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
   if(!enable_enum_range_check)
     return;
 
-  const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
-  const c_enum_typet &c_enum_type = ns.follow_tag(c_enum_tag_type);
-
-  const c_enum_typet::memberst enum_values = c_enum_type.members();
-
-  std::vector<exprt> disjuncts;
-  for(const auto &enum_value : enum_values)
+  // we might be looking at a lowered enum_is_in_range_exprt, skip over these
+  const auto &pragmas = expr.source_location().get_pragmas();
+  for(const auto &d : pragmas)
   {
-    const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
-    disjuncts.push_back(equal_exprt(expr, val));
+    if(d.first == "disable:enum-range-check")
+      return;
   }
 
-  const exprt check = disjunction(disjuncts);
+  const exprt check = enum_is_in_range_exprt{expr}.lower(ns);
 
   add_guarded_property(
     check,
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 67b70f1bac7..0b0baa23b1b 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -40,6 +40,35 @@ struct __CPROVER_pipet {
   short next_unread;
 };
 
+// __CPROVER_equal expects two arguments of the same type -- any type is
+// permitted, unsigned long long is just used for the benefit of running syntax
+// checks using system compilers
+__CPROVER_bool __CPROVER_equal(unsigned long long, unsigned long long);
+
+// The following built-ins are type checked by our C front-end and do not
+// require declarations. They work with any types as described below. unsigned
+// long long is just used to enable checks using system compilers.
+
+// detect overflow
+// the following expect two numeric arguments
+__CPROVER_bool __CPROVER_overflow_minus(unsigned long long, unsigned long long);
+__CPROVER_bool __CPROVER_overflow_mult(unsigned long long, unsigned long long);
+__CPROVER_bool __CPROVER_overflow_plus(unsigned long long, unsigned long long);
+__CPROVER_bool __CPROVER_overflow_shl(unsigned long long, unsigned long long);
+// expects one numeric argument
+__CPROVER_bool __CPROVER_overflow_unary_minus(unsigned long long);
+
+// enumerations
+// expects one enum-typed argument
+__CPROVER_bool __CPROVER_enum_is_in_range(unsigned long long);
+
+// The following have an optional second parameter (the width), and are
+// polymorphic in the first parameter: if the second argument is omitted, then
+// the width of the subtype of the pointer-typed first argument is used.
+__CPROVER_bool __CPROVER_r_ok(const void *, ...);
+__CPROVER_bool __CPROVER_w_ok(const void *, ...);
+__CPROVER_bool __CPROVER_rw_ok(const void *, ...);
+
 #include "../cprover_builtin_headers.h"
 
 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
index 721d7452863..619b3744c03 100644
--- a/src/ansi-c/library/cprover_contracts.c
+++ b/src/ansi-c/library/cprover_contracts.c
@@ -14,8 +14,8 @@ const void *__CPROVER_new_object = 0;
 extern const void *__CPROVER_memory_leak;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 int __builtin_clzll(unsigned long long);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-__CPROVER_size_t __VERIFIER_nondet_size();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+__CPROVER_size_t __VERIFIER_nondet_size(void);
 
 /// \brief A conditionally writable range of bytes.
 typedef struct
diff --git a/src/ansi-c/library/fcntl.c b/src/ansi-c/library/fcntl.c
index 7001724c9bf..5de5546bf2e 100644
--- a/src/ansi-c/library/fcntl.c
+++ b/src/ansi-c/library/fcntl.c
@@ -5,7 +5,7 @@
 #define __CPROVER_FCNTL_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fcntl(int fd, int cmd, ...)
 {
diff --git a/src/ansi-c/library/gcc.c b/src/ansi-c/library/gcc.c
index e8a0e7f1d33..cf33e06002c 100644
--- a/src/ansi-c/library/gcc.c
+++ b/src/ansi-c/library/gcc.c
@@ -212,7 +212,7 @@ float __builtin_ia32_vec_ext_v4sf(__gcc_v4sf vec, int offset)
 #ifndef LIBRARY_CHECK
 typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
 #else
-__gcc_v8hi __CPROVER_saturating_minus();
+__gcc_v8hi __CPROVER_saturating_minus(__gcc_v8hi, __gcc_v8hi);
 #endif
 
 __gcc_v8hi __builtin_ia32_psubsw128(__gcc_v8hi a, __gcc_v8hi b)
@@ -224,6 +224,10 @@ __gcc_v8hi __builtin_ia32_psubsw128(__gcc_v8hi a, __gcc_v8hi b)
 
 #ifndef LIBRARY_CHECK
 typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
+#else
+typedef unsigned short v8hi_u __attribute__((__vector_size__(16)));
+__gcc_v8hi __CPROVER_saturating_minus_v8hi_u(v8hi_u, v8hi_u);
+#  define __CPROVER_saturating_minus __CPROVER_saturating_minus_v8hi_u
 #endif
 
 __gcc_v8hi __builtin_ia32_psubusw128(__gcc_v8hi a, __gcc_v8hi b)
@@ -237,7 +241,7 @@ __gcc_v8hi __builtin_ia32_psubusw128(__gcc_v8hi a, __gcc_v8hi b)
 #ifndef LIBRARY_CHECK
 typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
 #else
-__gcc_v4hi __CPROVER_saturating_plus();
+__gcc_v4hi __CPROVER_saturating_plus(__gcc_v4hi, __gcc_v4hi);
 #endif
 
 __gcc_v4hi __builtin_ia32_paddsw(__gcc_v4hi a, __gcc_v4hi b)
@@ -251,6 +255,7 @@ __gcc_v4hi __builtin_ia32_paddsw(__gcc_v4hi a, __gcc_v4hi b)
 typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
 #else
 __gcc_v4hi __CPROVER_saturating_minus_v4hi(__gcc_v4hi, __gcc_v4hi);
+#  undef __CPROVER_saturating_minus
 #  define __CPROVER_saturating_minus __CPROVER_saturating_minus_v4hi
 #endif
 
diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c
index 9acc33a3f63..2606d2f3b8e 100644
--- a/src/ansi-c/library/getopt.c
+++ b/src/ansi-c/library/getopt.c
@@ -8,8 +8,8 @@ extern int optind;
 #define __CPROVER_STRING_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-size_t __VERIFIER_nondet_size_t();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+size_t __VERIFIER_nondet_size_t(void);
 
 int getopt(int argc, char *const argv[], const char *optstring)
 {
diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c
index 491eccbdeea..b15532cb6df 100644
--- a/src/ansi-c/library/inet.c
+++ b/src/ansi-c/library/inet.c
@@ -7,7 +7,7 @@
 #define __CPROVER_INET_H_INCLUDED
 #endif
 
-in_addr_t __VERIFIER_nondet_in_addr_t();
+in_addr_t __VERIFIER_nondet_in_addr_t(void);
 
 in_addr_t inet_addr(const char *cp)
 {
@@ -33,7 +33,7 @@ in_addr_t inet_addr(const char *cp)
 #define __CPROVER_INET_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int inet_aton(const char *cp, struct in_addr *pin)
 {
@@ -60,7 +60,7 @@ int inet_aton(const char *cp, struct in_addr *pin)
 #define __CPROVER_INET_H_INCLUDED
 #endif
 
-in_addr_t __VERIFIER_nondet_in_addr_t();
+in_addr_t __VERIFIER_nondet_in_addr_t(void);
 
 in_addr_t inet_network(const char *cp)
 {
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index ebb8eb3b4af..17e7dc3e9bb 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -465,7 +465,7 @@ int __fpclassify(double d)
 
 /* FUNCTION: sin */
 
-double __VERIFIER_nondet_double();
+double __VERIFIER_nondet_double(void);
 
 double sin(double x)
 {
@@ -486,7 +486,7 @@ double sin(double x)
 
 /* FUNCTION: sinl */
 
-long double __VERIFIER_nondet_long_double();
+long double __VERIFIER_nondet_long_double(void);
 
 long double sinl(long double x)
 {
@@ -507,7 +507,7 @@ long double sinl(long double x)
 
 /* FUNCTION: sinf */
 
-float __VERIFIER_nondet_float();
+float __VERIFIER_nondet_float(void);
 
 float sinf(float x)
 {
@@ -528,7 +528,7 @@ float sinf(float x)
 
 /* FUNCTION: cos */
 
-double __VERIFIER_nondet_double();
+double __VERIFIER_nondet_double(void);
 
 double cos(double x)
 {
@@ -549,7 +549,7 @@ double cos(double x)
 
 /* FUNCTION: cosl */
 
-long double __VERIFIER_nondet_long_double();
+long double __VERIFIER_nondet_long_double(void);
 
 long double cosl(long double x)
 {
@@ -570,7 +570,7 @@ long double cosl(long double x)
 
 /* FUNCTION: cosf */
 
-float __VERIFIER_nondet_float();
+float __VERIFIER_nondet_float(void);
 
 float cosf(float x)
 {
@@ -833,7 +833,7 @@ __CPROVER_hide:;
 
 float nextUpf(float f);
 
-float __VERIFIER_nondet_float();
+float __VERIFIER_nondet_float(void);
 
 float sqrtf(float f)
 {
@@ -920,7 +920,7 @@ float sqrtf(float f)
 
 double nextUp(double d);
 
-double __VERIFIER_nondet_double();
+double __VERIFIER_nondet_double(void);
 
 double sqrt(double d)
 {
@@ -991,7 +991,7 @@ double sqrt(double d)
 
 long double nextUpl(long double d);
 
-long double __VERIFIER_nondet_long_double();
+long double __VERIFIER_nondet_long_double(void);
 
 long double sqrtl(long double d)
 {
diff --git a/src/ansi-c/library/mman.c b/src/ansi-c/library/mman.c
index cdb76d24f8c..d751454d802 100644
--- a/src/ansi-c/library/mman.c
+++ b/src/ansi-c/library/mman.c
@@ -19,7 +19,7 @@
 #    define MAP_UNINITIALIZED 0
 #  endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 void *mmap(
   void *addr,
@@ -72,7 +72,7 @@ void *mmap(
 #    define MAP_UNINITIALIZED 0
 #  endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 void *_mmap(
   void *addr,
@@ -106,7 +106,7 @@ void *_mmap(
 
 /* FUNCTION: munmap */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int munmap(void *addr, __CPROVER_size_t length)
 {
@@ -119,7 +119,7 @@ int munmap(void *addr, __CPROVER_size_t length)
 
 /* FUNCTION: _munmap */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int _munmap(void *addr, __CPROVER_size_t length)
 {
diff --git a/src/ansi-c/library/netdb.c b/src/ansi-c/library/netdb.c
index 30a322ded75..4f2f1ecaefc 100644
--- a/src/ansi-c/library/netdb.c
+++ b/src/ansi-c/library/netdb.c
@@ -6,7 +6,7 @@
 #include <netdb.h>
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 struct hostent *gethostbyname(const char *name)
 {
@@ -35,7 +35,7 @@ struct hostent *gethostbyname(const char *name)
 #include <netdb.h>
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
 {
@@ -59,7 +59,7 @@ struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
 // There does not appear to be a Windows variant of gethostent
 #include <netdb.h>
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 struct hostent *gethostent(void)
 {
diff --git a/src/ansi-c/library/process.c b/src/ansi-c/library/process.c
index f1a89b9f7f4..664adb1a80f 100644
--- a/src/ansi-c/library/process.c
+++ b/src/ansi-c/library/process.c
@@ -1,6 +1,6 @@
 /* FUNCTION: _beginthread */
 
-__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
+__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
 
 __CPROVER_size_t _beginthread(
   void (*start_address)(void *),
@@ -16,7 +16,7 @@ __CPROVER_size_t _beginthread(
 
 /* FUNCTION: _beginthreadex */
 
-__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
+__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
 
 __CPROVER_size_t _beginthreadex(
    void *security,
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index d893d6440a0..87a60a463a4 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -5,7 +5,7 @@
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 {
@@ -30,7 +30,7 @@ int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int pthread_cancel(pthread_t thread)
 {
@@ -839,7 +839,7 @@ int pthread_spin_trylock(pthread_spinlock_t *lock)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 // no pthread_barrier_t on the Mac
 // slightly different declaration on OpenBSD
@@ -893,7 +893,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 // no pthread_barrier_t on the Mac
 #ifndef __APPLE__
@@ -923,7 +923,7 @@ int pthread_barrier_destroy(pthread_barrier_t *barrier)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 // no pthread_barrier_t on the Mac
 #ifndef __APPLE__
diff --git a/src/ansi-c/library/random.c b/src/ansi-c/library/random.c
index 65d2ef7947a..b024c66e5ae 100644
--- a/src/ansi-c/library/random.c
+++ b/src/ansi-c/library/random.c
@@ -17,8 +17,8 @@
 #    define GRND_NONBLOCK 0
 #  endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-size_t __VERIFIER_nondet_size_t();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+size_t __VERIFIER_nondet_size_t(void);
 
 ssize_t getrandom(void *buf, size_t buflen, unsigned int flags)
 {
diff --git a/src/ansi-c/library/signal.c b/src/ansi-c/library/signal.c
index 45fb723a7a4..86a19411ae2 100644
--- a/src/ansi-c/library/signal.c
+++ b/src/ansi-c/library/signal.c
@@ -10,7 +10,7 @@
 #define __CPROVER_SIGNAL_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int kill(pid_t pid, int sig)
 {
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index fb8dfa09c82..903d7bcf950 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -16,7 +16,7 @@
 #undef fileno
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int putchar(int c)
 {
@@ -33,8 +33,8 @@ int putchar(int c)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-int __VERIFIER_nondet_int();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+int __VERIFIER_nondet_int(void);
 
 int puts(const char *s)
 {
@@ -71,7 +71,7 @@ __CPROVER_HIDE:;
 #endif
 
 void fclose_cleanup(void *stream);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 FILE *fopen(const char *filename, const char *mode)
 {
@@ -121,7 +121,7 @@ FILE *fopen(const char *filename, const char *mode)
 #endif
 
 void fclose_cleanup(void *stream);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 #ifdef __APPLE__
 FILE *_fopen(const char *filename, const char *mode)
@@ -185,7 +185,7 @@ FILE *freopen(const char *filename, const char *mode, FILE *f)
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fclose(FILE *stream)
 {
@@ -275,8 +275,8 @@ FILE *_fdopen(int handle, const char *mode)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-int __VERIFIER_nondet_int();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+int __VERIFIER_nondet_int(void);
 
 char *fgets(char *str, int size, FILE *stream)
 {
@@ -330,8 +330,8 @@ char *fgets(char *str, int size, FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-char __VERIFIER_nondet_char();
-size_t __VERIFIER_nondet_size_t();
+char __VERIFIER_nondet_char(void);
+size_t __VERIFIER_nondet_size_t(void);
 
 size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
 {
@@ -369,7 +369,7 @@ size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int feof(FILE *stream)
 {
@@ -401,7 +401,7 @@ int feof(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int ferror(FILE *stream)
 {
@@ -433,7 +433,7 @@ int ferror(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fileno(FILE *stream)
 {
@@ -469,7 +469,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fputs(const char *s, FILE *stream)
 {
@@ -505,7 +505,7 @@ int fputs(const char *s, FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fflush(FILE *stream)
 {
@@ -530,7 +530,7 @@ int fflush(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fpurge(FILE *stream)
 {
@@ -562,7 +562,7 @@ int fpurge(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fgetc(FILE *stream)
 {
@@ -598,7 +598,7 @@ int fgetc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int getc(FILE *stream)
 {
@@ -634,9 +634,9 @@ int getc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
-int getchar()
+int getchar(void)
 {
   __CPROVER_HIDE:;
   int return_value=__VERIFIER_nondet_int();
@@ -653,7 +653,7 @@ int getchar()
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int getw(FILE *stream)
 {
@@ -687,7 +687,7 @@ int getw(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fseek(FILE *stream, long offset, int whence)
 {
@@ -717,7 +717,7 @@ int fseek(FILE *stream, long offset, int whence)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-long __VERIFIER_nondet_long();
+long __VERIFIER_nondet_long(void);
 
 long ftell(FILE *stream)
 {
@@ -768,7 +768,7 @@ void rewind(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-size_t __VERIFIER_nondet_size_t();
+size_t __VERIFIER_nondet_size_t(void);
 
 size_t fwrite(
   const void *ptr,
@@ -980,7 +980,7 @@ __CPROVER_HIDE:;
 #    define __CPROVER_STDARG_H_INCLUDED
 #  endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
 {
@@ -1026,7 +1026,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
 #  define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int __isoc99_vfscanf(
   FILE *restrict stream,
@@ -1075,7 +1075,7 @@ __CPROVER_HIDE:;
 #    define __CPROVER_STDARG_H_INCLUDED
 #  endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int __stdio_common_vfscanf(
   unsigned __int64 options,
@@ -1166,7 +1166,7 @@ __CPROVER_HIDE:;
 #    define __CPROVER_STDARG_H_INCLUDED
 #  endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
 {
@@ -1198,7 +1198,7 @@ __CPROVER_HIDE:;
 #  define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int __isoc99_vsscanf(
   const char *restrict s,
@@ -1233,7 +1233,7 @@ __CPROVER_HIDE:;
 #    define __CPROVER_STDARG_H_INCLUDED
 #  endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int __stdio_common_vsscanf(
   unsigned __int64 options,
@@ -1274,7 +1274,7 @@ int __stdio_common_vsscanf(
 #  define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int printf(const char *format, ...)
 {
@@ -1321,7 +1321,7 @@ int fprintf(FILE *stream, const char *restrict format, ...)
 #define __CPROVER_STDARG_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 {
@@ -1366,8 +1366,8 @@ int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
-char __VERIFIER_nondet_char();
-int __VERIFIER_nondet_int();
+char __VERIFIER_nondet_char(void);
+int __VERIFIER_nondet_int(void);
 
 int vasprintf(char **ptr, const char *fmt, va_list ap)
 {
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index b836600bd82..cd0af9374bc 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -104,7 +104,7 @@ void abort(void)
 
 #undef calloc
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef __GNUC__
 _Bool __builtin_mul_overflow();
 #endif
@@ -169,7 +169,7 @@ __CPROVER_HIDE:;
 
 #undef malloc
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef LIBRARY_CHECK
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 #endif
@@ -228,7 +228,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: __builtin_alloca */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 const void *__CPROVER_alloca_object = 0;
 #ifndef LIBRARY_CHECK
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
@@ -272,7 +272,7 @@ __CPROVER_HIDE:;
 #undef free
 
 void __CPROVER_deallocate(void *);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef LIBRARY_CHECK
 const void *__CPROVER_alloca_object = 0;
 #endif
@@ -457,8 +457,8 @@ long atol(const char *nptr)
 #  define __CPROVER_STDDEF_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-ptrdiff_t __VERIFIER_nondet_ptrdiff_t();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+ptrdiff_t __VERIFIER_nondet_ptrdiff_t(void);
 
 char *getenv(const char *name)
 {
@@ -592,7 +592,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: random */
 
-long __VERIFIER_nondet_long();
+long __VERIFIER_nondet_long(void);
 
 long random(void)
 {
@@ -605,7 +605,7 @@ long random(void)
 
 /* FUNCTION: rand */
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int rand(void)
 {
@@ -618,7 +618,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: rand_r */
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int rand_r(unsigned int *seed)
 {
@@ -632,7 +632,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: __CPROVER_deallocate */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 void __CPROVER_deallocate(void *ptr)
 {
diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c
index baf69ef3614..37260fe088e 100644
--- a/src/ansi-c/library/time.c
+++ b/src/ansi-c/library/time.c
@@ -7,7 +7,7 @@
 
 #undef time
 
-time_t __VERIFIER_nondet_time_t();
+time_t __VERIFIER_nondet_time_t(void);
 
 time_t time(time_t *tloc)
 {
@@ -26,7 +26,7 @@ time_t time(time_t *tloc)
 #    define __CPROVER_TIME_H_INCLUDED
 #  endif
 
-time_t __VERIFIER_nondet_time_t();
+time_t __VERIFIER_nondet_time_t(void);
 
 time_t _time64(time_t *tloc)
 {
@@ -47,7 +47,7 @@ time_t _time64(time_t *tloc)
 #    define __CPROVER_TIME_H_INCLUDED
 #  endif
 
-__time32_t __VERIFIER_nondet_time32_t();
+__time32_t __VERIFIER_nondet_time32_t(void);
 
 __time32_t _time32(__time32_t *tloc)
 {
@@ -150,7 +150,7 @@ struct tm *localtime_r(const time_t *clock, struct tm *result)
 
 #undef mktime
 
-time_t __VERIFIER_nondet_time_t();
+time_t __VERIFIER_nondet_time_t(void);
 
 time_t mktime(struct tm *timeptr)
 {
@@ -168,7 +168,7 @@ time_t mktime(struct tm *timeptr)
 
 #undef timegm
 
-time_t __VERIFIER_nondet_time_t();
+time_t __VERIFIER_nondet_time_t(void);
 
 time_t timegm(struct tm *timeptr)
 {
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c
index 7fde194e53e..8563c41f020 100644
--- a/src/ansi-c/library/unistd.c
+++ b/src/ansi-c/library/unistd.c
@@ -1,6 +1,6 @@
 /* FUNCTION: sleep */
 
-unsigned __VERIFIER_nondet_unsigned();
+unsigned __VERIFIER_nondet_unsigned(void);
 
 unsigned int sleep(unsigned int seconds)
 {
@@ -24,7 +24,7 @@ unsigned int _sleep(unsigned int seconds)
 
 /* FUNCTION: unlink */
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int unlink(const char *s)
 {
@@ -50,7 +50,7 @@ extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 extern const int __CPROVER_pipe_offset;
 unsigned __CPROVER_pipe_count = 0;
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int pipe(int fildes[2])
 {
@@ -155,7 +155,7 @@ extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
-ret_type __VERIFIER_nondet_ret_type();
+ret_type __VERIFIER_nondet_ret_type(void);
 
 ret_type write(int fildes, const void *buf, size_type nbyte)
 {
@@ -233,9 +233,9 @@ extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-ret_type __VERIFIER_nondet_ret_type();
-size_type __VERIFIER_nondet_size_type();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+ret_type __VERIFIER_nondet_ret_type(void);
+size_type __VERIFIER_nondet_size_type(void);
 
 ret_type read(int fildes, void *buf, size_type nbyte)
 {
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 592283b59e1..5c2f958cfb5 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -14,7 +14,8 @@ for f in "$@"; do
     perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
     $CC -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
     $CC -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
-      -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
+      -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas \
+      -Wno-gnu-line-marker -Wno-unknown-warning-option
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c
     [ "${ec}" -eq 0 ] || exit "${ec}"
diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h
index cfbc3a9d4d5..ab9e9c69e02 100644
--- a/src/cpp/library/cprover.h
+++ b/src/cpp/library/cprover.h
@@ -24,8 +24,8 @@ void __CPROVER_input(const char *description, ...);
 void __CPROVER_output(const char *description, ...);
 
 // concurrency-related
-void __CPROVER_atomic_begin();
-void __CPROVER_atomic_end();
+void __CPROVER_atomic_begin(void);
+void __CPROVER_atomic_end(void);
 void __CPROVER_fence(const char *kind, ...);
 
 // pointers
diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c
index bf3ce6f364c..81790944455 100644
--- a/src/cpp/library/new.c
+++ b/src/cpp/library/new.c
@@ -1,6 +1,6 @@
 /* FUNCTION: __new */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 const void *__CPROVER_new_object = 0;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
@@ -26,7 +26,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
 
 /* FUNCTION: __new_array */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef LIBRARY_CHECK
 const void *__CPROVER_new_object = 0;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
@@ -66,7 +66,7 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p)
 /* FUNCTION: __delete */
 
 void __CPROVER_deallocate(void *);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef LIBRARY_CHECK
 const void *__CPROVER_new_object = 0;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
@@ -104,7 +104,7 @@ inline void __delete(void *ptr)
 /* FUNCTION: __delete_array */
 
 void __CPROVER_deallocate(void *);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef LIBRARY_CHECK
 const void *__CPROVER_new_object = 0;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 6f86da9a61b..0bb91c25fcb 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -615,33 +615,6 @@ exprt make_va_list(const exprt &expr)
   return result;
 }
 
-void goto_convertt::do_enum_is_in_range(
-  const exprt &lhs,
-  const symbol_exprt &function,
-  const exprt::operandst &arguments,
-  goto_programt &dest)
-{
-  PRECONDITION(arguments.size() == 1);
-  const auto enum_expr = arguments.front();
-  const auto enum_type =
-    type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
-  PRECONDITION(enum_type);
-  const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
-  const c_enum_typet::memberst enum_values = c_enum_type.members();
-
-  exprt::operandst disjuncts;
-  for(const auto &enum_value : enum_values)
-  {
-    constant_exprt val{enum_value.get_value(), *enum_type};
-    disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
-  }
-
-  code_assignt assignment(lhs, simplify_expr(disjunction(disjuncts), ns));
-  assignment.add_source_location() = function.source_location();
-  assignment.add_source_location().add_pragma("disable:enum-range-check");
-  copy(assignment, ASSIGN, dest);
-}
-
 void goto_convertt::do_havoc_slice(
   const exprt &lhs,
   const symbol_exprt &function,
@@ -956,10 +929,6 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
-  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
-  {
-    do_enum_is_in_range(lhs, function, arguments, dest);
-  }
   else if(
     identifier == CPROVER_PREFIX "assert" ||
     identifier == CPROVER_PREFIX "precondition" ||
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index b0c869bd300..84e50bacdce 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -610,26 +610,6 @@ class goto_convertt:public messaget
   bool get_string_constant(const exprt &expr, irep_idt &);
   exprt get_constant(const exprt &expr);
 
-  /// \brief Converts calls to the built in `enum_is_in_range` function to a
-  ///    test that the given enum value is in the valid range of values for that
-  ///    enum type.
-  ///
-  /// Note that the check for the range of values is done by creating a
-  /// disjunction comparing the expression with each possible valid value.
-  /// \param lhs: The destination for the generated assignment.
-  /// \param function: The `enum_is_in_range` symbol of the source function call.
-  /// \param arguments: A collection of arguments, which is expected to contain a
-  ///    single argument which is an expression that resolves to a value of
-  ///    enum type. The arguments are expected to have been prevalidated by the
-  ///    typechecking process.
-  /// \param dest: The goto program into which the generated assignment is
-  ///    copied.
-  void do_enum_is_in_range(
-    const exprt &lhs,
-    const symbol_exprt &function,
-    const exprt::operandst &arguments,
-    goto_programt &dest);
-
   // some built-in functions
   void do_atomic_begin(
     const exprt &lhs,
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index ad1263d89a6..e66f620b755 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -903,6 +903,7 @@ IREP_ID_TWO(overflow_result_shl, overflow_result-shl)
 IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-)
 IREP_ID_ONE(field_sensitive_ssa)
 IREP_ID_ONE(checked_assigns)
+IREP_ID_ONE(enum_is_in_range)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree