From 23b995d3b59627308278960e7b75c25992cce703 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Aug 2021 08:52:20 -0700 Subject: [PATCH] #5499 throw exception when dividing by a small 0 --- src/util/mpz.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index afea0214d..159fc0ed8 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -559,12 +559,13 @@ void mpz_manager::machine_div_rem(mpz const & a, mpz const & b, mpz & q, template void mpz_manager::machine_div(mpz const & a, mpz const & b, mpz & c) { STRACE("mpz", tout << "[mpz-ext] machine-div(" << to_string(a) << ", " << to_string(b) << ") == ";); - if (is_small(a) && is_small(b)) { + if (is_small(b) && i64(b) == 0) + throw default_exception("division by 0"); + + if (is_small(a) && is_small(b)) set_i64(c, i64(a) / i64(b)); - } - else { + else big_div(a, b, c); - } STRACE("mpz", tout << to_string(c) << "\n";); }