diff --git a/regression/cbmc-library/feraiseexcept-01/main.c b/regression/cbmc-library/feraiseexcept-01/main.c
new file mode 100644
index 000000000000..e4d6dd90771b
--- /dev/null
+++ b/regression/cbmc-library/feraiseexcept-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <fenv.h>
+
+int main()
+{
+  int exceptions;
+  feraiseexcept(exceptions);
+  return 0;
+}
diff --git a/regression/cbmc-library/feraiseexcept-01/test.desc b/regression/cbmc-library/feraiseexcept-01/test.desc
new file mode 100644
index 000000000000..e2d2d714649f
--- /dev/null
+++ b/regression/cbmc-library/feraiseexcept-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/fenv.c b/src/ansi-c/library/fenv.c
index 31e17d615d29..0c3ba94f45ba 100644
--- a/src/ansi-c/library/fenv.c
+++ b/src/ansi-c/library/fenv.c
@@ -40,3 +40,12 @@ __CPROVER_HIDE:;
     0;
   return 0; // we never fail
 }
+
+/* FUNCTION: feraiseexcept */
+
+int feraiseexcept(int excepts)
+{
+__CPROVER_HIDE:;
+  __CPROVER_assert(excepts == 0, "floating-point exception");
+  return 0; // we never fail
+}