[SMT-LIB] "typecast" for bitvec?

[Christopher L Conway]

Jun,

You can use concat, e.g.,
    (assert (= a64 (concat #x00000000 a32)))

Alternatively, if you want sign-extension,
    (define-fun sign-extend-32-64 ((x (_ BitVec 32))) (_ BitVec 64)
      (concat (if (= ((_ extract 31 31) x) #b0) #x00000000 #xffffffff) x))
    (assert (= a64 (sign-extend-32-64 a32))

-Chris

On Wed, Sep 7, 2011 at 9:58 PM, Jun Koi <junkoi2004 at gmail.com> wrote:
> hi,
>
> how can we "typecast" when we assert 2 bitvec vars of different size?
> the below code reports "sort mismatch" with Z3.
>
> naturally, a dirty hack is to set a32 to 64 bit, but i dont want that.
>
> many thanks,
> J
>
> ;;;;;;;;
> (set-logic QF_BV)
> (declare-fun a64 () (_ BitVec 64))
> (declare-fun a32 () (_ BitVec 32))
> (assert (= a64 a32))
> (check-sat)
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>