mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

bugfix for pb2bv

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-11-07 15:06:36 +00:00
parent 33f941aaec
commit 412f912c46
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -480,7 +480,10 @@ private:
break; 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 // copy lits [0, i) to m_clause
for (unsigned j = 0; j < i; j++) 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) { 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()) { if (m_c.is_nonpos()) {
// constraint is equivalent to true. // constraint is equivalent to true.
r = m.mk_true(); r = m.mk_true();
@ -507,7 +511,7 @@ private:
} }
polynomial::iterator it = m_p.begin(); polynomial::iterator it = m_p.begin();
polynomial::iterator end = m_p.end(); 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) { for (; it != end; ++it) {
if (it->m_a > m_c) if (it->m_a > m_c)
it->m_a = m_c; // trimming coefficients it->m_a = m_c; // trimming coefficients
@ -520,6 +524,7 @@ private:
it->m_a /= a_gcd; it->m_a /= a_gcd;
m_c = ceil(m_c/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(); it = m_p.begin();
numeral a_sum; numeral a_sum;
for (; it != end; ++it) { for (; it != end; ++it) {