From c2f6f2e7152cc157cc80ef0253d63329c89658a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Feb 2020 21:27:58 -1000 Subject: [PATCH] fix #3010 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/lia2pb_tactic.cpp | 1 + 1 file changed, 1 insertion(+) 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;