diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index effa5f411..9a778d6e0 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -391,10 +391,9 @@ extern "C" { Z3_TRY; LOG_Z3_mk_bv_numeral(c, sz, bits); RESET_ERROR_CODE(); - rational r(0), two(2), one(1); + rational r(0); for (unsigned i = 0; i < sz; ++i) { - r *= two; - if (bits[i]) r += one; + if (bits[i]) r += rational::power_of_two(i); } ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz)); RETURN_Z3(of_ast(a)); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d0921c8de..e7d808b2b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -26,7 +26,6 @@ Revision History: #include "util/string_buffer.h" #include "ast/ast_util.h" #include "ast/ast_smt2_pp.h" -#include "ast/bv_decl_plugin.h" // ----------------------------------- //