From 81f1f7690df331065f775aa15b9abea6441fa5be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Dec 2013 15:59:56 -0800 Subject: [PATCH] fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/lia2pb_tactic.cpp | 1 + src/util/rational.h | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 6fee55e4b..9ee8f6728 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic { if (m_bm.has_lower(n, l, s) && m_bm.has_upper(n, u, s) && l.is_zero() && + !u.is_neg() && u.get_num_bits() <= m_max_bits) { return true; diff --git a/src/util/rational.h b/src/util/rational.h index fc03228bf..c02a5a2c3 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -104,7 +104,7 @@ public: } bool is_int32() const { - if (is_small()) return true; + if (is_small() && is_int()) return true; // we don't assume that if it is small, then it is int32. if (!is_int64()) return false; int64 v = get_int64();