This module defines a subset of the SMTLIB format we use to interact with the SMT solver, which mostly corresponds to the theory of quantifier-free bitvectors and arrays.