From 412f912c4628f84cc3ca9036c8512ba9d6d8b2c2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 7 Nov 2013 15:06:36 +0000 Subject: [PATCH] bugfix for pb2bv Signed-off-by: Christoph M. Wintersteiger --- src/tactic/arith/pb2bv_tactic.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 83a949579..89195a9d5 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -480,7 +480,10 @@ private: break; } - SASSERT (i < sz); + if (i >= sz) { + // [Christoph]: In this case, all the m_a are equal to m_c. + return; + } // copy lits [0, i) to m_clause for (unsigned j = 0; j < i; j++) @@ -500,6 +503,7 @@ private: } void mk_pbc(polynomial & m_p, numeral & m_c, expr_ref & r, bool enable_split) { + TRACE("mk_pbc", display(tout, m_p, m_c); ); if (m_c.is_nonpos()) { // constraint is equivalent to true. r = m.mk_true(); @@ -507,7 +511,7 @@ private: } polynomial::iterator it = m_p.begin(); polynomial::iterator end = m_p.end(); - numeral a_gcd = it->m_a; + numeral a_gcd = (it->m_a > m_c) ? m_c : it->m_a; for (; it != end; ++it) { if (it->m_a > m_c) it->m_a = m_c; // trimming coefficients @@ -520,6 +524,7 @@ private: it->m_a /= a_gcd; m_c = ceil(m_c/a_gcd); } + TRACE("mk_pbc", tout << "GCD = " << a_gcd << "; Normalized: "; display(tout, m_p, m_c); tout << "\n"; ); it = m_p.begin(); numeral a_sum; for (; it != end; ++it) {