Matching Multiplications in Bit-Vector Formulas

Supratik Chakraborty, Ashutosh Gupta, Rahul Jain

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 v…