diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index a29419961a..1468b5441b 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -197,6 +197,18 @@ void ansi_c_internal_additions(std::string &code)
     "long double __CPROVER_infl(void);\n"
     "int __CPROVER_thread_local __CPROVER_rounding_mode="+
       std::to_string(config.ansi_c.rounding_mode)+";\n"
+    "int __CPROVER_isgreaterf(float f, float g);\n"
+    "int __CPROVER_isgreaterd(double f, double g);\n"
+    "int __CPROVER_isgreaterequalf(float f, float g);\n"
+    "int __CPROVER_isgreaterequald(double f, double g);\n"
+    "int __CPROVER_islessf(float f, float g);\n"
+    "int __CPROVER_islessd(double f, double g);\n"
+    "int __CPROVER_islessequalf(float f, float g);\n"
+    "int __CPROVER_islessequald(double f, double g);\n"
+    "int __CPROVER_islessgreaterf(float f, float g);\n"
+    "int __CPROVER_islessgreaterd(double f, double g);\n"
+    "int __CPROVER_isunorderedf(float f, float g);\n"
+    "int __CPROVER_isunorderedd(double f, double g);\n"
 
     // absolute value
     "int __CPROVER_abs(int x);\n"
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index ac9c529145..251bb828b6 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -92,6 +92,7 @@ double __CPROVER_inf(void);
 float __CPROVER_inff(void);
 long double __CPROVER_infl(void);
 //extern int __CPROVER_thread_local __CPROVER_rounding_mode;
+int __CPROVER_isgreaterd(double f, double g);
 
 // absolute value
 int __CPROVER_abs(int);
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 60968b0fc8..1af12148d8 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -22,33 +22,69 @@ inline long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); }
 
 inline float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); }
 
-/* FUNCTION: __builtin_isgreater */
+/* FUNCTION: __CPROVER_isgreaterf */
 
-int __builtin_isgreater(double f, double g) { return f > g; }
+int __CPROVER_isgreaterf(float f, float g) { return f > g; }
 
-/* FUNCTION: __builtin_isgreaterequal */
+/* FUNCTION: __CPROVER_isgreaterd */
 
-int __builtin_isgreaterequal(float f, float g) { return f >= g; }
+int __CPROVER_isgreaterd(double f, double g) { return f > g; }
 
-/* FUNCTION: __builtin_isless */
+/* FUNCTION: __CPROVER_isgreaterequalf */
 
-int __builtin_isless(float f, float g) { return f < g;}
+int __CPROVER_isgreaterequalf(float f, float g) { return f >= g; }
 
-/* FUNCTION: __builtin_islessequal */
+/* FUNCTION: __CPROVER_isgreaterequald */
 
-int __builtin_islessequal(float f, float g) { return f <= g; }
+int __CPROVER_isgreaterequald(double f, double g) { return f >= g; }
 
-/* FUNCTION: __builtin_islessgreater */
+/* FUNCTION: __CPROVER_islessf */
 
-int __builtin_islessgreater(float f, float g) { return (f < g) || (f > g); }
+int __CPROVER_islessf(float f, float g) { return f < g;}
 
-/* FUNCTION: __builtin_isunordered */
+/* FUNCTION: __CPROVER_islessd */
 
-int __builtin_isunordered(float f, float g) { return isnan(f) || isnan(g); }
+int __CPROVER_islessd(double f, double g) { return f < g;}
+
+/* FUNCTION: __CPROVER_islessequalf */
+
+int __CPROVER_islessequalf(float f, float g) { return f <= g; }
+
+/* FUNCTION: __CPROVER_islessequald */
+
+int __CPROVER_islessequald(double f, double g) { return f <= g; }
+
+/* FUNCTION: __CPROVER_islessgreaterf */
+
+int __CPROVER_islessgreaterf(float f, float g) { return (f < g) || (f > g); }
+
+/* FUNCTION: __CPROVER_islessgreaterd */
+
+int __CPROVER_islessgreaterd(double f, double g) { return (f < g) || (f > g); }
+
+/* FUNCTION: __CPROVER_isunorderedf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+int __CPROVER_isunorderedf(float f, float g) { return isnanf(f) || isnanf(g); }
+
+/* FUNCTION: __CPROVER_isunorderedd */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#include <math.h>
+#define __CPROVER_MATH_H_INCLUDED
+#endif
+
+int __CPROVER_isunorderedd(double f, double g) { return isnan(f) || isnan(g); }
 
 
 /* FUNCTION: isfinite */
 
+#undef isfinite
+
 int isfinite(double d) { return __CPROVER_isfinited(d); }
 
 /* FUNCTION: __finite */
@@ -65,6 +101,8 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
 
 /* FUNCTION: isinf */
 
+#undef isinf
+
 inline int isinf(double d) { return __CPROVER_isinfd(d); }
 
 /* FUNCTION: __isinf */
@@ -89,6 +127,8 @@ inline int __isinfl(long double ld) { return __CPROVER_isinfld(ld); }
 
 /* FUNCTION: isnan */
 
+#undef isnan
+
 inline int isnan(double d) { return __CPROVER_isnand(d); }
 
 /* FUNCTION: __isnan */
@@ -113,6 +153,8 @@ inline int __isnanl(long double ld) { return __CPROVER_isnanld(ld); }
 
 /* FUNCTION: isnormal */
 
+#undef isnormal
+
 inline int isnormal(double d) { return __CPROVER_isnormald(d); }
 
 /* FUNCTION: __isnormalf */
@@ -177,6 +219,8 @@ inline int _fdsign(float f) { return __CPROVER_signf(f); }
 
 /* FUNCTION: signbit */
 
+#undef signbit
+
 inline int signbit(double d) { return __CPROVER_signd(d); }
 
 /* FUNCTION: __signbitd */
@@ -1032,7 +1076,7 @@ float fdimf(float f, float g) { return ((f > g) ? f - g : +0.0f); }
 #define __CPROVER_MATH_H_INCLUDED
 #endif
 
-long double fdim(long double f, long double g) { return ((f > g) ? f - g : +0.0); }
+long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0); }
 
 
 
@@ -1130,7 +1174,7 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d)
 
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d)
 {
-  long double magicConst = 0x1.0p+64d;
+  long double magicConst = 0x1.0p+64;
   long double return_value;
   int saved_rounding_mode = fegetround();
   fesetround(rounding_mode);
@@ -1421,7 +1465,7 @@ float roundf(float x)
     xp = x;
   }
 
-  fegetround(FE_TOWARDZERO);
+  fesetround(saved_rounding_mode);
   
   return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
 }
@@ -1643,7 +1687,7 @@ long int lrint(double x)
 
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
 
-float lrintf(float x)
+long int lrintf(float x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT
@@ -1666,7 +1710,7 @@ float lrintf(float x)
 
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
 
-long double lrintl(long double x)
+long int lrintl(long double x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT
@@ -1711,7 +1755,7 @@ long long int llrint(double x)
 
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
 
-float llrintf(float x)
+long long int llrintf(float x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT
@@ -1734,7 +1778,7 @@ float llrintf(float x)
 
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
 
-long double llrintl(long double x)
+long long int llrintl(long double x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT
@@ -1803,7 +1847,7 @@ long int lround(double x)
 
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
 
-float lroundf(float x)
+long int lroundf(float x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT, plus should use RNA
@@ -1840,7 +1884,7 @@ float lroundf(float x)
 
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
 
-long double lroundl(long double x)
+long int lroundl(long double x)
 {
   int saved_rounding_mode = fegetround();
   fesetround(FE_TOWARDZERO);
@@ -1913,7 +1957,7 @@ long long int llround(double x)
 
 float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
 
-float llroundf(float x)
+long long int llroundf(float x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT, plus should use RNA
@@ -1950,7 +1994,7 @@ float llroundf(float x)
 
 long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
 
-long double llroundl(long double x)
+long long int llroundl(long double x)
 {
   // TODO : should be an all-in-one __CPROVER function to allow
   // conversion to SMT, plus should use RNA
@@ -1969,7 +2013,7 @@ long double llroundl(long double x)
   fesetround(saved_rounding_mode);
   
   long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
-  return (long int)rti;
+  return (long long int)rti;
 }
 
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 3de38da7b8..b4d62bad63 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1767,6 +1767,77 @@ void goto_convertt::do_function_call_symbol(
 
     // void __sync_lock_release (type *ptr, ...)
   }
+  else if(identifier=="__builtin_isgreater" ||
+          identifier=="__builtin_isgreater" ||
+          identifier=="__builtin_isgreaterequal" ||
+          identifier=="__builtin_isless" ||
+          identifier=="__builtin_islessequal" ||
+          identifier=="__builtin_islessgreater" ||
+          identifier=="__builtin_isunordered")
+  {
+    // these support two double or two float arguments; we call the
+    // appropriate internal version
+    if(arguments.size()!=2 ||
+       (arguments[0].type()!=double_type() &&
+        arguments[0].type()!=float_type()) ||
+       (arguments[1].type()!=double_type() &&
+        arguments[1].type()!=float_type()))
+    {
+      error().source_location=function.find_source_location();
+      error() << "`" << identifier
+              << "' expected to have two float/double arguments"
+              << eom;
+      throw 0;
+    }
+
+    exprt::operandst new_arguments=arguments;
+
+    bool use_double=arguments[0].type()==double_type();
+    if(arguments[0].type()!=arguments[1].type())
+    {
+      if(use_double)
+        new_arguments[1].make_typecast(arguments[0].type());
+      else
+      {
+        new_arguments[0].make_typecast(arguments[1].type());
+        use_double=true;
+      }
+    }
+
+    code_typet f_type=to_code_type(function.type());
+    f_type.remove_ellipsis();
+    const typet &a_t=new_arguments[0].type();
+    f_type.parameters()=
+      code_typet::parameterst(2, code_typet::parametert(a_t));
+
+    // replace __builtin_ by CPROVER_PREFIX
+    std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
+    // append d or f for double/float
+    name+=use_double?'d':'f';
+
+    symbol_exprt new_function=function;
+    new_function.set_identifier(name);
+    new_function.type()=f_type;
+
+    code_function_callt function_call;
+    function_call.lhs()=lhs;
+    function_call.function()=new_function;
+    function_call.arguments()=new_arguments;
+    function_call.add_source_location()=function.source_location();
+
+    if(!symbol_table.has_symbol(name))
+    {
+      code_typet();
+      symbolt new_symbol;
+      new_symbol.base_name=name;
+      new_symbol.name=name;
+      new_symbol.type=f_type;
+      new_symbol.location=function.source_location();
+      symbol_table.add(new_symbol);
+    }
+
+    copy(function_call, FUNCTION_CALL, dest);
+  }
   else
   {
     do_function_call_symbol(*symbol);