Clever Geek Handbook

Z3: exception from int2bv

(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 "int2bv expects one parameter" exception caused by the above code, how to use the int2bv function correctly?

+1


source to share


1 answer


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

((_ int2bv 32) a)


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

"NB. This function is essentially interpreted as uninterpreted. Therefore, you cannot expect the Z3 to accurately reflect the semantics of this function when solving constraints with this function." (from here )

+1


source






More articles:


All Articles