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;
             }
             }