Estou um pouco confuso com a operação Z3 (formato smt2)int2bv . Eu escrevi uma expressão smt2:

(declare-const t1 Int)
(assert (= ((_ int2bv 2) t1) #b11))
(check-sat)
(get-model)

quando resolvo com o Z3, obtive:

sat
(model 
  (define-fun t1 () Int
    0)
)

Isso está correto? T1 não deveria ser 3? Eu pensei que a operação int2bv apenas transformava o valor int no valor equivalente do bitvector. Mas parece que não!

Obrigado!