SMTLib1.QF_AUFBV

Documentation

tArray :: Integer -> Integer -> Sort

'tArray i n' is an array indexed by bitvectors of widht i, and storing bitvectors of width n.

select :: Term -> Term -> Term

select array index

store :: Term -> Term -> Term -> Term

store array index value