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

[Jun Koi]

hi Matt,

On Wed, Aug 24, 2011 at 4:56 PM, Matthieu Wipliez <mwipliez at yahoo.fr> wrote:
> Hi Jun,
> the second line means "make sure that a equals 4".
> I don't know if that should be considered an assignment, because you don't
> give a the value 4 explicitly,

so how can i do "give a the value 4 explicitly"?

thanks a lot,
Jun

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