mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
treat division by 0 as non-linearity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e2b6b12215
commit
ca2ad66d03
|
@ -312,7 +312,7 @@ void static_features::update_core(expr * e) {
|
|||
case OP_IDIV:
|
||||
case OP_REM:
|
||||
case OP_MOD:
|
||||
if (!is_numeral(to_app(e)->get_arg(1)))
|
||||
if (!is_numeral(to_app(e)->get_arg(1), r) || r.is_zero())
|
||||
m_num_non_linear++;
|
||||
break;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue