diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index c177f35be..08f588829 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -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;