From 2865f60f8c6514a9e564e23bb7651ad021072d5c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Nov 2015 11:39:34 -0500 Subject: [PATCH] deal with case of unsatisfiable context and bit-vector objectives that are not normalized to maxsmt. Issue #304 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 83d83fdb5..49b5f988f 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -902,6 +902,21 @@ namespace opt { m_hard_constraints.push_back(fml); } } + // fix types of objectives: + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective & obj = m_objectives[i]; + expr* t = obj.m_term; + switch(obj.m_type) { + case O_MINIMIZE: + case O_MAXIMIZE: + if (!m_arith.is_int(t) && !m_arith.is_real(t)) { + obj.m_term = m_arith.mk_numeral(rational(0), true); + } + break; + default: + break; + } + } } void context::purify(app_ref& term) { @@ -1000,7 +1015,10 @@ namespace opt { switch(obj.m_type) { case O_MINIMIZE: { app_ref tmp(m); - tmp = m_arith.mk_uminus(obj.m_term); + tmp = obj.m_term; + if (m_arith.is_int(tmp) || m_arith.is_real(tmp)) { + tmp = m_arith.mk_uminus(obj.m_term); + } obj.m_index = m_optsmt.add(tmp); break; }