diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index 940b1ebb0..a709c16f3 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -118,8 +118,8 @@ namespace bv { } } - if (glue < max_glue) - v.m_glue = (sz > 6 && 2*glue <= sz) ? 0 : glue; + if (glue < max_glue) + v.m_glue = glue; // (sz > 6 && 2 * glue <= sz) ? 0 : glue; } void ackerman::remove(vv* p) {