From 39dcc653df5dd51e3975f69d63c9ac8ff55b6533 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jan 2014 20:20:26 -0800 Subject: [PATCH] fix normalization regression Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 12a52208f..bb5767dad 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -205,6 +205,7 @@ namespace smt { } virtual final_check_status final_check_eh() { + if (m_normalize) normalize(); return FC_DONE; } @@ -356,6 +357,7 @@ namespace smt { m_den = lcm(m_den, denominator(m_rweights[i])); } m_den = lcm(m_den, denominator(m_rmin_cost)); + SASSERT(!m_den.is_zero()); m_zweights.reset(); for (unsigned i = 0; i < m_rweights.size(); ++i) { rational r = m_rweights[i]*m_den;