From a737639790c1e1881575fdeefe04a1f2f557f711 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Wed, 11 Dec 2013 12:56:48 -0800 Subject: [PATCH] Skip lower bound assertions for unbounded objectives --- src/opt/optsmt.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 012f8c0e4..0eb9706e0 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -291,8 +291,10 @@ namespace opt { m_lower[i] = mid; m_upper[i] = mid; TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << mid << "\n"; - tout << get_lower(i) << ":" << get_upper(i) << "\n";); - m_s->assert_expr(m_s->mk_ge(i, mid)); + tout << get_lower(i) << ":" << get_upper(i) << "\n";); + // Only assert bounds for bounded objectives + if (mid.get_infinity().is_zero()) + m_s->assert_expr(m_s->mk_ge(i, mid)); } std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const {