[SMT-LIB] BVDIV on Bitvector (SMTLIB2) ?

[Jun Koi]

On Wed, Aug 24, 2011 at 11:28 AM, Christopher L Conway
<cconway at cs.nyu.edu> wrote:
> On Tue, Aug 23, 2011 at 10:49 PM, Jun Koi <junkoi2004 at gmail.com> wrote:
>> another question: i found bvule, bvugt, etc. but i cannot find
>> anything to compare 2 vectors, so i can know if 2 vectors are equal.
>> or did i miss something?
>
>
> Yeah, you missed =.
>
> ;-)
>
> The equality operator is overloaded to work on any type.

hmm, this is confused for me. i always think that "=" is for
assignment, but it is used for comparison, too?

so the 2nd line below should be understood as assignment, or comparison??

(declare-fun a () (_ BitVec 4))
(assert (= a #x4))


thanks,
Jun