diff --git a/regression/cbmc-library/imaxabs-01/main.c b/regression/cbmc-library/imaxabs-01/main.c
new file mode 100644
index 00000000000..aba774f1262
--- /dev/null
+++ b/regression/cbmc-library/imaxabs-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <inttypes.h>
+#include <stdlib.h>
+
+int main()
+{
+  assert(imaxabs(INTMAX_MIN + 1) == INTMAX_MAX);
+  return 0;
+}
diff --git a/regression/cbmc-library/imaxabs-01/test.desc b/regression/cbmc-library/imaxabs-01/test.desc
new file mode 100644
index 00000000000..f456d4fb459
--- /dev/null
+++ b/regression/cbmc-library/imaxabs-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --signed-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index ad49c01a802..02b313a4833 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2872,12 +2872,13 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(infl_expr);
   }
-  else if(identifier==CPROVER_PREFIX "abs" ||
-          identifier==CPROVER_PREFIX "labs" ||
-          identifier==CPROVER_PREFIX "llabs" ||
-          identifier==CPROVER_PREFIX "fabs" ||
-          identifier==CPROVER_PREFIX "fabsf" ||
-          identifier==CPROVER_PREFIX "fabsl")
+  else if(
+    identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
+    identifier == CPROVER_PREFIX "llabs" ||
+    identifier == CPROVER_PREFIX "imaxabs" ||
+    identifier == CPROVER_PREFIX "fabs" ||
+    identifier == CPROVER_PREFIX "fabsf" ||
+    identifier == CPROVER_PREFIX "fabsl")
   {
     if(expr.arguments().size()!=1)
     {
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 6454ef92383..e1ecf12964e 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -25,6 +25,22 @@ long long int llabs(long long int i)
   return __CPROVER_llabs(i);
 }
 
+/* FUNCTION: imaxabs */
+
+#ifndef __CPROVER_INTTYPES_H_INCLUDED
+#  include <inttypes.h>
+#  define __CPROVER_INTTYPES_H_INCLUDED
+#endif
+
+#undef imaxabs
+
+intmax_t __CPROVER_imaxabs(intmax_t);
+
+intmax_t imaxabs(intmax_t i)
+{
+  return __CPROVER_imaxabs(i);
+}
+
 /* FUNCTION: __builtin_abs */
 
 int __builtin_abs(int i)