Ich bin ein wenig verwirrt mit der Operation Z3 (SMT2-Format) int2bv. Ich habe einen solchen smt2-Ausdruck geschrieben:

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

wenn ich es mit Z3 löse, bekam es:

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

Ist das korrekt? Sollte nicht t1 3 sein? Ich dachte, die int2bv-Operation transformiert nur den int-Wert in den entsprechenden Bitvektorwert. Aber es scheint nicht!

Vielen Dank