diff --git a/stage0/src/include/lean/lean.h b/stage0/src/include/lean/lean.h
index 9c61f1df9f..7a66f0311a 100644
--- a/stage0/src/include/lean/lean.h
+++ b/stage0/src/include/lean/lean.h
@@ -1553,7 +1553,7 @@ static inline lean_obj_res lean_int_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
         int v1 = lean_scalar_to_int(a1);
         int v2 = lean_scalar_to_int(a2);
         if (v2 == 0)
-            return lean_box(0);
+            return v1 >= 0 ? a1 : lean_int_to_int(-1 - v1);
         else
             return lean_int_to_int(v1 % v2);
     } else {
diff --git a/stage0/src/runtime/object.cpp b/stage0/src/runtime/object.cpp
index 8226c1823b..ec36a41c78 100644
--- a/stage0/src/runtime/object.cpp
+++ b/stage0/src/runtime/object.cpp
@@ -1340,12 +1340,22 @@ extern "C" object * lean_int_big_div(object * a1, object * a2) {
 }
 
 extern "C" object * lean_int_big_mod(object * a1, object * a2) {
-    if (lean_is_scalar(a1))
+    if (lean_is_scalar(a1)) {
         return mpz_to_int(mpz(lean_scalar_to_int(a1)) % mpz_value(a2));
-    else if (lean_is_scalar(a2))
-        return mpz_to_int(mpz_value(a1) % mpz(lean_scalar_to_int(a2)));
-    else
+    } else if (lean_is_scalar(a2)) {
+        int i2 = lean_scalar_to_int(a2);
+        if (i2 == 0) {
+            if (mpz_value(a1) >= 0) {
+                return a1;
+            } else {
+                return mpz_to_int(mpz(-1) - mpz_value(a1));
+            }
+        } else {
+            return mpz_to_int(mpz_value(a1) % mpz(i2));
+        }
+    } else {
         return mpz_to_int(mpz_value(a1) % mpz_value(a2));
+    }
 }
 
 extern "C" bool lean_int_big_eq(object * a1, object * a2) {