I am using Z3 version 3.0. I want to assign a value to a bitvector variable, like below. But Z3 reports error "invalid function application, sort mismatch on a开发者_Python百科rgument at position 2 in line 3".
It seems wrong with my constant #x0a? how can i fix this?
Thanks
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0a))
(check-sat)
In the SMT-LIB 2.0 standard, #x0a
is a bitvector of size 8. You get the sort mismatch error because the constant a
is a bitvector of size 32.
You can avoid the type/sort error message by rewriting your example as:
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0000000a))
(check-sat)
SMT-LIB also supports bitvector literals of the form (_ bv[num] [size])
, where [num]
is in decimal notation, and [size]
is the size of the bitvector.
Thus, you can also write the bitvector literal #x0000000a
as (_ bv10 32)
.
BTW, SMT-LIB also supports bitvector literals in binary notation. For example, #b010
is a bitvector of size 3.
精彩评论