diff --git a/regression/cbmc/gcc_builtin_mul_overflow/main.c b/regression/cbmc/gcc_builtin_mul_overflow/main.c
new file mode 100644
index 00000000000..4d7fd6ec218
--- /dev/null
+++ b/regression/cbmc/gcc_builtin_mul_overflow/main.c
@@ -0,0 +1,116 @@
+#include <assert.h>
+#include <limits.h>
+#include <stdint.h>
+
+#define A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(T)                       \
+  (((T)(1)) << (sizeof(T) * CHAR_BIT) / 2 - 1)
+
+void check_int(void)
+{
+  int result;
+  assert(!__builtin_smul_overflow(1, 1, &result));
+  assert(result == 1);
+  int const lt_isqrt_of_int_max =
+    A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(int);
+  assert(!__builtin_smul_overflow(
+    lt_isqrt_of_int_max, lt_isqrt_of_int_max, &result));
+  assert(result == lt_isqrt_of_int_max * lt_isqrt_of_int_max);
+  assert(__builtin_smul_overflow(
+    lt_isqrt_of_int_max << 1, lt_isqrt_of_int_max << 1, &result));
+  assert(0 && "reachability");
+}
+
+void check_long(void)
+{
+  long result;
+  assert(!__builtin_smull_overflow(1l, 1l, &result));
+  assert(result == 1l);
+  long const lt_isqrt_of_long_max =
+    A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(long);
+  assert(!__builtin_smull_overflow(
+    lt_isqrt_of_long_max, lt_isqrt_of_long_max, &result));
+  assert(result == lt_isqrt_of_long_max * lt_isqrt_of_long_max);
+  assert(__builtin_smull_overflow(
+    lt_isqrt_of_long_max << 1, lt_isqrt_of_long_max << 1, &result));
+  assert(0 && "reachability");
+}
+
+void check_long_long(void)
+{
+  long long result;
+  assert(!__builtin_smulll_overflow(1ll, 1ll, &result));
+  assert(result == 1ll);
+  long long const lt_isqrt_of_long_long_max =
+    A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(long long);
+  assert(!__builtin_smulll_overflow(
+    lt_isqrt_of_long_long_max, lt_isqrt_of_long_long_max, &result));
+  assert(result == lt_isqrt_of_long_long_max * lt_isqrt_of_long_long_max);
+  assert(__builtin_smulll_overflow(
+    lt_isqrt_of_long_long_max << 1, lt_isqrt_of_long_long_max << 1, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned(void)
+{
+  unsigned result;
+  assert(!__builtin_umul_overflow(1u, 1u, &result));
+  assert(result == 1u);
+  unsigned const lt_isqrt_of_unsigned_max =
+    A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(unsigned);
+  assert(!__builtin_umul_overflow(
+    lt_isqrt_of_unsigned_max, lt_isqrt_of_unsigned_max, &result));
+  assert(result == lt_isqrt_of_unsigned_max * lt_isqrt_of_unsigned_max);
+  assert(__builtin_umul_overflow(
+    lt_isqrt_of_unsigned_max << 1, lt_isqrt_of_unsigned_max << 1, &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned_long(void)
+{
+  unsigned long result;
+  assert(!__builtin_umull_overflow(1ul, 1ul, &result));
+  assert(result == 1ul);
+  unsigned long const lt_isqrt_of_unsigned_long_max =
+    A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(unsigned long);
+  assert(!__builtin_umull_overflow(
+    lt_isqrt_of_unsigned_long_max, lt_isqrt_of_unsigned_long_max, &result));
+  assert(
+    result == lt_isqrt_of_unsigned_long_max * lt_isqrt_of_unsigned_long_max);
+  assert(__builtin_umull_overflow(
+    lt_isqrt_of_unsigned_long_max << 1,
+    lt_isqrt_of_unsigned_long_max << 1,
+    &result));
+  assert(0 && "reachability");
+}
+
+void check_unsigned_long_long(void)
+{
+  unsigned long long result;
+  assert(!__builtin_umulll_overflow(1ull, 1ull, &result));
+  assert(result == 1ull);
+  unsigned long long const lt_isqrt_of_unsigned_long_long_max =
+    A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(unsigned long long);
+  assert(!__builtin_umulll_overflow(
+    lt_isqrt_of_unsigned_long_long_max,
+    lt_isqrt_of_unsigned_long_long_max,
+    &result));
+  assert(
+    result ==
+    lt_isqrt_of_unsigned_long_long_max * lt_isqrt_of_unsigned_long_long_max);
+  assert(__builtin_umulll_overflow(
+    lt_isqrt_of_unsigned_long_long_max << 1,
+    lt_isqrt_of_unsigned_long_long_max << 1,
+    &result));
+  assert(0 && "reachability");
+}
+
+int main(void)
+{
+  check_int();
+  check_long();
+  check_long_long();
+  check_unsigned();
+  check_unsigned_long();
+  check_unsigned_long_long();
+  return 0;
+}
diff --git a/regression/cbmc/gcc_builtin_mul_overflow/test.desc b/regression/cbmc/gcc_builtin_mul_overflow/test.desc
new file mode 100644
index 00000000000..e045d26c089
--- /dev/null
+++ b/regression/cbmc/gcc_builtin_mul_overflow/test.desc
@@ -0,0 +1,41 @@
+CORE gcc-only
+main.c
+
+\[check_int.assertion.1\] line \d+ assertion !__builtin_smul_overflow\(1, 1, &result\): SUCCESS
+\[check_int.assertion.2\] line \d+ assertion result == 1: SUCCESS
+\[check_int.assertion.3\] line \d+ assertion !__builtin_smul_overflow\( lt_isqrt_of_int_max, lt_isqrt_of_int_max, &result\): SUCCESS
+\[check_int.assertion.4\] line \d+ assertion result == lt_isqrt_of_int_max \* lt_isqrt_of_int_max: SUCCESS
+\[check_int.assertion.5\] line \d+ assertion __builtin_smul_overflow\( lt_isqrt_of_int_max << 1, lt_isqrt_of_int_max << 1, &result\): SUCCESS
+\[check_int.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_long.assertion.1\] line \d+ assertion !__builtin_smull_overflow\(1l, 1l, &result\): SUCCESS
+\[check_long.assertion.2\] line \d+ assertion result == 1l: SUCCESS
+\[check_long.assertion.3\] line \d+ assertion !__builtin_smull_overflow\( lt_isqrt_of_long_max, lt_isqrt_of_long_max, &result\): SUCCESS
+\[check_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_long_max \* lt_isqrt_of_long_max: SUCCESS
+\[check_long.assertion.5\] line \d+ assertion __builtin_smull_overflow\( lt_isqrt_of_long_max << 1, lt_isqrt_of_long_max << 1, &result\): SUCCESS
+\[check_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_long_long.assertion.1\] line \d+ assertion !__builtin_smulll_overflow\(1ll, 1ll, &result\): SUCCESS
+\[check_long_long.assertion.2\] line \d+ assertion result == 1ll: SUCCESS
+\[check_long_long.assertion.3\] line \d+ assertion !__builtin_smulll_overflow\( lt_isqrt_of_long_long_max, lt_isqrt_of_long_long_max, &result\): SUCCESS
+\[check_long_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_long_long_max \* lt_isqrt_of_long_long_max: SUCCESS
+\[check_long_long.assertion.5\] line \d+ assertion __builtin_smulll_overflow\( lt_isqrt_of_long_long_max << 1, lt_isqrt_of_long_long_max << 1, &result\): SUCCESS
+\[check_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_umul_overflow\(1u, 1u, &result\): SUCCESS
+\[check_unsigned.assertion.2\] line \d+ assertion result == 1u: SUCCESS
+\[check_unsigned.assertion.3\] line \d+ assertion !__builtin_umul_overflow\( lt_isqrt_of_unsigned_max, lt_isqrt_of_unsigned_max, &result\): SUCCESS
+\[check_unsigned.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_max \* lt_isqrt_of_unsigned_max: SUCCESS
+\[check_unsigned.assertion.5\] line \d+ assertion __builtin_umul_overflow\( lt_isqrt_of_unsigned_max << 1, lt_isqrt_of_unsigned_max << 1, &result\): SUCCESS
+\[check_unsigned.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned_long.assertion.1\] line \d+ assertion !__builtin_umull_overflow\(1ul, 1ul, &result\): SUCCESS
+\[check_unsigned_long.assertion.2\] line \d+ assertion result == 1ul: SUCCESS
+\[check_unsigned_long.assertion.3\] line \d+ assertion !__builtin_umull_overflow\( lt_isqrt_of_unsigned_long_max, lt_isqrt_of_unsigned_long_max, &result\): SUCCESS
+\[check_unsigned_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_long_max \* lt_isqrt_of_unsigned_long_max: SUCCESS
+\[check_unsigned_long.assertion.5\] line \d+ assertion __builtin_umull_overflow\( lt_isqrt_of_unsigned_long_max << 1, lt_isqrt_of_unsigned_long_max << 1, &result\): SUCCESS
+\[check_unsigned_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+\[check_unsigned_long_long.assertion.1\] line \d+ assertion !__builtin_umulll_overflow\(1ull, 1ull, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.2\] line \d+ assertion result == 1ull: SUCCESS
+\[check_unsigned_long_long.assertion.3\] line \d+ assertion !__builtin_umulll_overflow\( lt_isqrt_of_unsigned_long_long_max, lt_isqrt_of_unsigned_long_long_max, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.4\] line \d+ assertion result == lt_isqrt_of_unsigned_long_long_max \* lt_isqrt_of_unsigned_long_long_max: SUCCESS
+\[check_unsigned_long_long.assertion.5\] line \d+ assertion __builtin_umulll_overflow\( lt_isqrt_of_unsigned_long_long_max << 1, lt_isqrt_of_unsigned_long_long_max << 1, &result\): SUCCESS
+\[check_unsigned_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
+^EXIT=10$
+^SIGNAL=0$
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 2c559875601..4d2e1e7784c 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -2406,3 +2406,57 @@ _Bool __builtin_usubll_overflow(
   *res = a - b;
   return __CPROVER_overflow_minus(a, b);
 }
+
+/* FUNCTION: __builtin_smul_overflow */
+
+_Bool __builtin_smul_overflow(int a, int b, int *res)
+{
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
+}
+
+/* FUNCTION: __builtin_smull_overflow */
+
+_Bool __builtin_smull_overflow(long a, long b, long *res)
+{
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
+}
+
+/* FUNCTION: __builtin_smulll_overflow */
+
+_Bool __builtin_smulll_overflow(long long a, long long b, long long *res)
+{
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
+}
+
+/* FUNCTION: __builtin_umul_overflow */
+
+_Bool __builtin_umul_overflow(unsigned a, unsigned b, unsigned *res)
+{
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
+}
+
+/* FUNCTION: __builtin_umull_overflow */
+
+_Bool __builtin_umull_overflow(
+  unsigned long a,
+  unsigned long b,
+  unsigned long *res)
+{
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
+}
+
+/* FUNCTION: __builtin_umulll_overflow */
+
+_Bool __builtin_umulll_overflow(
+  unsigned long long a,
+  unsigned long long b,
+  unsigned long long *res)
+{
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
+}