From 10a10b38d8993e7aca7c1cfb9151bbd349130abd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Feb 2021 07:53:18 -0800 Subject: [PATCH] fix: fixes #303 --- src/runtime/object.cpp | 13 +++++++++---- tests/lean/run/303.lean | 1 + 2 files changed, 10 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/303.lean diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index d68dea6fdd..163ea227db 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -1336,12 +1336,17 @@ extern "C" object * lean_int_big_mul(object * a1, object * a2) { } extern "C" object * lean_int_big_div(object * a1, object * a2) { - if (lean_is_scalar(a1)) + if (lean_is_scalar(a1)) { return mpz_to_int(lean_scalar_to_int(a1) / mpz_value(a2)); - else if (lean_is_scalar(a2)) - return mpz_to_int(mpz_value(a1) / lean_scalar_to_int(a2)); - else + } else if (lean_is_scalar(a2)) { + int d = lean_scalar_to_int(a2); + if (d == 0) + return a2; + else + return mpz_to_int(mpz_value(a1) / d); + } else { return mpz_to_int(mpz_value(a1) / mpz_value(a2)); + } } extern "C" object * lean_int_big_mod(object * a1, object * a2) { diff --git a/tests/lean/run/303.lean b/tests/lean/run/303.lean new file mode 100644 index 0000000000..d02e7f51d1 --- /dev/null +++ b/tests/lean/run/303.lean @@ -0,0 +1 @@ +#eval (2147483648 / 0) + (-0)