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

[Christopher L Conway]

Be careful not to think of SMT-LIB is as a programming language. It's
not. It's a language for expressing logical constraints. Variables are
not mutable. (assert (= a 4)) expresses the constraint that a must be
equal to 4. If you later execute (assert (= a 5)), you're not updating
the value of a, you're expressing the contradictory constraint that a
is also equal to 5. There's no way to "change" the value of a except
to push and pop constraints that affect the value of a.

-Chris

On Wed, Aug 24, 2011 at 5:09 AM, Jun Koi <junkoi2004 at gmail.com> wrote:
> 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))
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>