diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 186e88c568..8fcb23f449 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1139,15 +1139,15 @@ extern "C" object * lean_nat_big_sub(object * a1, object * a2) {
 extern "C" object * lean_nat_big_mul(object * a1, object * a2) {
     lean_assert(!lean_is_scalar(a1) || !lean_is_scalar(a2));
     if (lean_is_scalar(a1))
-        return mpz_to_nat_core(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
+        return mpz_to_nat(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
     else if (lean_is_scalar(a2))
-        return mpz_to_nat_core(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
+        return mpz_to_nat(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
     else
         return mpz_to_nat_core(mpz_value(a1) * mpz_value(a2));
 }
 
 extern "C" object * lean_nat_overflow_mul(size_t a1, size_t a2) {
-    return mpz_to_nat_core(mpz::of_size_t(a1) * mpz::of_size_t(a2));
+    return mpz_to_nat(mpz::of_size_t(a1) * mpz::of_size_t(a2));
 }
 
 extern "C" object * lean_nat_big_div(object * a1, object * a2) {
diff --git a/stage0/src/runtime/object.cpp b/stage0/src/runtime/object.cpp
index 186e88c568..8fcb23f449 100644
--- a/stage0/src/runtime/object.cpp
+++ b/stage0/src/runtime/object.cpp
@@ -1139,15 +1139,15 @@ extern "C" object * lean_nat_big_sub(object * a1, object * a2) {
 extern "C" object * lean_nat_big_mul(object * a1, object * a2) {
     lean_assert(!lean_is_scalar(a1) || !lean_is_scalar(a2));
     if (lean_is_scalar(a1))
-        return mpz_to_nat_core(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
+        return mpz_to_nat(mpz::of_size_t(lean_unbox(a1)) * mpz_value(a2));
     else if (lean_is_scalar(a2))
-        return mpz_to_nat_core(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
+        return mpz_to_nat(mpz_value(a1) * mpz::of_size_t(lean_unbox(a2)));
     else
         return mpz_to_nat_core(mpz_value(a1) * mpz_value(a2));
 }
 
 extern "C" object * lean_nat_overflow_mul(size_t a1, size_t a2) {
-    return mpz_to_nat_core(mpz::of_size_t(a1) * mpz::of_size_t(a2));
+    return mpz_to_nat(mpz::of_size_t(a1) * mpz::of_size_t(a2));
 }
 
 extern "C" object * lean_nat_big_div(object * a1, object * a2) {
diff --git a/tests/lean/run/bigmul.lean b/tests/lean/run/bigmul.lean
new file mode 100644
index 0000000000..7b708f861a
--- /dev/null
+++ b/tests/lean/run/bigmul.lean
@@ -0,0 +1,11 @@
+@[noinline] def f (x : Nat) :=
+1000000000000000000000000000000
+
+@[noinline] def tst1 (n : Nat) : IO Unit := do
+IO.println (n * f n)
+
+@[noinline] def tst2 (n : Nat) : IO Unit := do
+IO.println (f n * n)
+
+#eval tst1 0
+#eval tst2 0