diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ebe56381a..d1a3ddb8a 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1002,7 +1002,8 @@ namespace opt {
             TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
             return false;
         }
-        if (!m_arith.is_numeral(val, r)) {
+        unsigned bv_size;
+        if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) {
             TRACE("opt", tout << "model does not evaluate objective to a value\n";);
             return false;
         }