[SMT-LIB] Assign value to a bitvector?

[Levent Erkok]

Jun:

Try #x0000000a.

The number of digits*4 should be the size of the bitvector. (32 =
4*8). See: http://combination.cs.uiowa.edu/smtlib/theories/Fixed_Size_BitVectors.smt2

-Levent.


On Tue, Aug 23, 2011 at 10:36 AM, Jun Koi <junkoi2004 at gmail.com> wrote:
> hi,
>
> In SMTLIB2, I want to assign a value to a bitvector variable, like below.
>
> But Z3 reports error "invalid function application, sort mismatch on
> argument at position 2 in line 3".
>
> How can I fix this error?
>
> Thanks.
> -------
> (set-logic QF_BV)
> (declare-fun a () (_ BitVec 32))
> (assert (= a #x0a))
> (check-sat)
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>