From 829519b83747992056953cd4d5a69163982e4aac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Mar 2017 10:19:35 +0100 Subject: [PATCH] fix bug for bit-vector optimization. Issue #928 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d1a3ddb8a..cd40944b2 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1002,8 +1002,8 @@ namespace opt { TRACE("opt", tout << "Term does not evaluate " << term << "\n";); return false; } - unsigned bv_size; - if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) { + unsigned bvsz; + if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) { TRACE("opt", tout << "model does not evaluate objective to a value\n";); return false; }