From 2865f60f8c6514a9e564e23bb7651ad021072d5c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
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 <nbjorner@microsoft.com>
---
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;
}