Я немного запутался с операцией Z3 (формат smt2)int2bv , Я написал такое выражение smt2:

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

когда я решаю это с Z3, он получил:

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

Это верно? Не должно ли t1 быть 3? Я думал, что операция int2bv просто преобразует значение int в эквивалентное значение битового вектора. Но, похоже, нет!

Спасибо!