Z3: исключение с 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)
Меня смущает исключение "int2bv ожидает один параметр", вызванное приведенным выше кодом, как правильно использовать функцию int2bv?