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

fix #4106

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-26 14:55:12 -07:00
parent 530f77281c
commit 51c3778354
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/check_logic.cpp
View file

@ -306,9 +306,8 @@ struct check_logic::imp {
}
// check if the divisor is a numeral
void check_div(app * n) {
SASSERT(n->get_num_args() == 2);
if (!m_nonlinear && !is_numeral(n->get_arg(1)))
void check_div(app * n) {
if (n->get_num_args() != 2 || (!m_nonlinear && !is_numeral(n->get_arg(1))))
fail("logic does not support nonlinear arithmetic");
}