mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
clean up bv_numeral code and fix bug in how they are initialized
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
795e0c641a
commit
7f13cf13f2
|
@ -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));
|
||||
|
|
|
@ -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"
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
Loading…
Reference in a new issue