From 7145a9ac41f80551f911a2bf8f78a5500b1636d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 May 2018 07:38:30 -0700 Subject: [PATCH] fix #1647 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1ebbc9ebc..1ba107b19 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -499,7 +499,7 @@ namespace opt { case O_MINIMIZE: is_ge = !is_ge; case O_MAXIMIZE: - if (mdl->eval(obj.m_term, val) && is_numeral(val, k)) { + if (mdl->eval(obj.m_term, val, true) && is_numeral(val, k)) { if (is_ge) { result = mk_ge(obj.m_term, val); } @@ -519,7 +519,7 @@ namespace opt { for (unsigned i = 0; i < sz; ++i) { terms.push_back(obj.m_terms[i]); coeffs.push_back(obj.m_weights[i]); - if (mdl->eval(obj.m_terms[i], val) && m.is_true(val)) { + if (mdl->eval(obj.m_terms[i], val, true) && m.is_true(val)) { k += obj.m_weights[i]; } } @@ -1046,7 +1046,7 @@ namespace opt { model_ref mdl = md->copy(); fix_model(mdl); - if (!mdl->eval(term, val)) { + if (!mdl->eval(term, val, true)) { TRACE("opt", tout << "Term does not evaluate " << term << "\n";); return false; }