Z3 int2bv operation

Question

I am experiencing some issues with the bitvector operations. In particular, given the following model. I was expecting var0 to be 11.

(declare-const var1 Int)
(declare-const var0 Int)
(assert (= var1 10))
(assert (= var0 ((_ bv2int 32) (bvor ((_ int2bv 32) var1) ((_ int2bv 32) 1)))))
(check-sat)
(get-model)
(exit)

However, the solution given by Z3 for fun was:

sat (model 
(define-fun var1 () Int 10) 
(define-fun var0 () Int (- 1)) 
)

This means, -1 instead of 10. Am I doing something wrong?

Answer 1

Unfortunately, int2bv and bv2int are uninterpreted functions. The semantics might not work as you expected.

See Z3 : Questions About Z3 int2bv?