mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
parent
eb205a5a40
commit
c2f6f2e715
1 changed files with 1 additions and 0 deletions
|
@ -68,6 +68,7 @@ class lia2pb_tactic : public tactic {
|
|||
m_bm.has_upper(n, u, s) &&
|
||||
l.is_zero() &&
|
||||
!u.is_neg() &&
|
||||
u.is_int() &&
|
||||
u.get_num_bits() <= m_max_bits) {
|
||||
|
||||
return true;
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue