1

From (Z3: Is it possible to sum up a BitVec and a Real?) , I tried to convert an int to bitvec using

x = Int('x')
reg = BitVecRef(Z3_mk_int2bv(BitVecVal(x.ctx_ref(), 16, x)), x.ctx)

but I always get an error saying " 'Ast' object has no attribute 'ref' ", it seems this function can only convert integer to bitvec, is there any other way to convert Int to bitvec?

Also I know this function is treated as uninterpreted for now, do I need to recompile my local version from (bv-enable-int2bv-propagation option) ?

Thanks in advance!

Community
  • 1
  • 1
Pounce
  • 25
  • 4

1 Answers1

0

The code you suggest first tries to convert x to a bit-vector value (BitVecVal), i.e., an actual number, but x is not a value (number). The right expression can be constructed as follows:

x = Int('x')
raw = Z3_mk_int2bv(x.ctx_ref(), 16, x.as_ast())
reg = BitVecRef(raw, x.ctx)
print reg

The int2bv-propagation fix was added long before the last Z3 release, so if the version you use is less than about a year old you shouldn't have to recompile anything.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30