Z3: an exception with int2bv

Question

(declare-const a Int)
(declare-const b Int)
(declare-const c (_ BitVec 32))
(declare-const d (_ BitVec 32))

(assert (= b (bv2int c)))
(assert (= c (int2bv a)))

(check-sat)

I am confused about the exception "int2bv expects one parameter" caused by the code above, how to use function int2bv correctly?

The problem is that `int2bv` expects a size (length of the new bitvector being created corresponding to the integer). However, the old syntax for specifying this (`(assert (= c (int2bv[32] a)))`, e.g., to convert `a` to a 32-bit long bitvector) gives an error `unexpected character` (eg: http://rise4fun.com/Z3/uOPG ), so maybe the syntax has changed. Here's an example of the older usage: http://stackoverflow.com/questions/8719764/is-there-any-difference-between-z3-versions-2-19-and-3-2-w-r-t-smtlib-2-code-sy — Taylor T. Johnson, Mar 11 '14 at 14:34

score 1 · Accepted Answer · answered Mar 12 '14 at 12:15

This is because int2bv is a parametric function and the SMT2 syntax for these is (_ f p1 p2 ...), so in this case the correct syntax is

((_ int2bv 32) a)

Note that int2bv is essentially treated as uninterpreted; the API documentation says:

"NB. 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." (from here)

Z3: an exception with int2bv

1 Answers1

Linked