mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

#5499

Browse source 
throw exception when dividing by a small 0
This commit is contained in:
Nikolaj Bjorner 2021-08-24 08:52:20 -07:00
parent dd91cfb47e
commit 23b995d3b5
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/util/mpz.cpp
View file

@ -559,12 +559,13 @@ void mpz_manager<SYNCH>::machine_div_rem(mpz const & a, mpz const & b, mpz & q,
template<bool SYNCH>
void mpz_manager<SYNCH>::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";);
}