[SMT-LIB] Assign value to a bitvector?

[Jun Koi]

On Wed, Aug 24, 2011 at 1:55 AM, Levent Erkok <erkokl at gmail.com> wrote:
> 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
>

this is awesome, thanks Chris & Levent !!!

Jun


> 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
>>
>