# Matching Multiplications in Bit-Vector Formulas

arXiv: https://arxiv.org/abs/1611.10146 · HTML: https://mlsanity.com/paper/1611.10146/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Nov 2016.

## Built on by (most cited first, 1 of 1)

- [Schwarz: Solver-Aware Agentic Program Verification](https://mlsanity.com/paper/2608.30803/) (2026)

## Abstract (arXiv)

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.