Christoph M. Wintersteiger

On Intervals and Bounds in Bit-vector Arithmetic.

2016 · International Workshop on Satisfiability Modulo Theories

Bit-vector arithmetic operations rely on modular arithmetic semantics, which often complicates algebraic manipulations. One such example are inequalities. Satisfiability of a system of modular inequalities is NP-complete. In this memo we investigate a simple type …