Z3 : Questions About Z3 int2bv?

问题:

I'm a little confused with the Z3 (smt2 format ) operation int2bv . I wrote a such smt2 expression :

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

when I solve it with Z3 ,it got:

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

Is that correct? Shouldn't t1 be 3? I thought the int2bv operation just transform the int value to the equivalent bitvector value. But it seems not!

Thanks!

回答1:

The int2bv function is essentially handled as uninterpreted (as stated in the documentation), so the semantics are not precise. There have previously been a few questions about those conversion functions, they might be helpful here too:

Z3: an exception with int2bv

Check overflow with Z3

bv-enable-int2bv-propagation option