From 41e6fafc58f44e379a04e0650ddbb25c84350350 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Mar 2017 10:07:31 +0100
Subject: [PATCH] fix bug for bit-vector optimization. Issue #919
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/opt_context.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
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;
}