From 92145f2bface25910b813bf5ae73824412358eb9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 22 Mar 2014 16:31:48 -0700
Subject: [PATCH] integrate opt with push/pop/check-sat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 849b88e65..a176fb3ee 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -935,6 +935,9 @@ namespace opt {
                     m_model->eval(obj.m_term, val) &&
                     is_numeral(val, r1)) {
                     rational r2 = n.get_rational();
+                    if (obj.m_type == O_MINIMIZE) {
+                        r1.neg();
+                    }
                     CTRACE("opt", r1 != r2, tout << obj.m_term << " evaluates to " << r1 << " but has objective " << r2 << "\n";);
                     CTRACE("opt", r1 != r2, model_smt2_pp(tout, m, *m_model, 0););
                     SASSERT(r1 == r2);