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