  Bit-vector formulas arising from hardware verification problems often contain
word-level arithmetic operations. Empirical evidence shows that
state-of-the-art SMT solvers are not very efficient at reasoning about
bit-vector formulas with multiplication. This is particularly true when
multiplication operators are decomposed and represented in alternative ways in
the formula.We present a pre-processing heuristic that identifies certain types
of decomposed multipliers, and adds special assertions to the input formula
encoding the equivalence of sub-terms to word-level multiplication. The
pre-processed formulas are then solved using an SMT solver. Our experiments
with three SMT solvers show that our heuristic allows several formulas to be
solved quickly, while the same formulas time out without the pre-processing
step.
