a bit-precise word-level format that allows to model SMT problems over the quantifier-free theory of bit-vectors in combination with one-dimensional arrays; can be seen as a word-level generalisation of the initial version of the bit-level format AIGER (its old version, the counterpart of the new one is BTOR2)
