From 0b7021d2c8481a4a4b67b1f831bf837782e8b7cc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Jan 2019 18:09:19 -0800
Subject: [PATCH] na

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

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 55b2a33ec..4d3e5d312 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1636,7 +1636,10 @@ namespace opt {
                     }
                     // TBD: check that optimal was not changed.
                 }
-                TRACE("opt", tout << "value " << value << "\n";);
+                maxsmt& ms = *m_maxsmts.find(obj.m_id);
+                rational value0 = ms.get_lower();
+                TRACE("opt", tout << "value " << value << " other " << value0 << "\n";);
+                SASSERT(value0 == value);
                 break;
             }
             }