If you represent your problem in a bit vector formula, e.g. QF_ABV, it will be automatically flattened into propositional formula, and solved using a SAT solver. For example, you can represent your less-than-100 integer variables as a bit vectors of 7 bits.
Apart from bit vector, conversion from SMT to SAT will not boost your performance (otherwise SMT would not exist). Because SAT solver is only good at case analysis, and theory-specific decision procedures, e.g. simplex-based algorithms for linear arithmetic, are much more efficient in constraint solving.