mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix #5320
This commit is contained in:
parent
83e2e7200c
commit
50cf321171
|
@ -184,6 +184,8 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref &
|
|||
kind = inv(kind);
|
||||
r = true;
|
||||
}
|
||||
if (a.is_zero())
|
||||
return false;
|
||||
if (!a.is_one())
|
||||
r = true;
|
||||
if (!r)
|
||||
|
|
Loading…
Reference in a new issue