kdrag.theories.bitvec.SelectConcat

kdrag.theories.bitvec.SelectConcat(a: ArrayRef, addr: BitVecRef | int, n: int, le=True) → BitVecRef

Concat out of an array. n is number of bytes. Flag is for little endian concatenation vs big endian.

>>> x = smt.Const("x", BitVecSort(8))
>>> a = smt.Lambda([x], x)
>>> smt.simplify(SelectConcat(a, 1, 1))
1
>>> smt.simplify(SelectConcat(a, 0, 2))
256
>>> smt.simplify(SelectConcat(a, 0, 2, le=False))
1

Parameters:

a (ArrayRef)
addr (BitVecRef | int)
n (int)

Return type:

BitVecRef