Z3: una excepción con 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)
Estoy confundido acerca de la excepción "int2bv espera un parámetro" causada por el código anterior, ¿cómo usar la función int2bv correctamente?