1

There are several posts regarding the conversion of bit vectors to integers (and vice versa) in z3. See for example here, here and here.

The documentation says that Z3_mk_bv2int is uninterpreted:

"...This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function..."

However, I could not find a simple example where it does fail to reflect the expected semantics. For instance, whenever I use queries like this:

(declare-const s String)
(declare-const someBitVec10 (_ BitVec 10))

(assert (= s "74g\x00!!#2#$$"))

(assert (str.in.re (str.at s (bv2int someBitVec10)) (re.range "1" "3")))

(check-sat)
(get-value (s someBitVec10))

I get a correct answer (index should 7, and it is)

sat
((s "74g\x00!!#2#$$")
 (someBitVec10 #b0000000111))

Could anyone please provide a simple example where z3's bv2int and/or int2bv fail?? thanks!

OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87

1 Answers1

2

This issue is now resolved, as it turns out that both int2bv and bv2int are indeed interpreted. The documentation hasn't been updated, and this might have caused the confusion (at least in my case it did). All the details are in this GitHub/z3/issues post.

OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87