3

An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors

We define four concrete approximation steps for the multiplication, division and remainder operators and combine them into an incremental abstraction scheme.