Deciding Bit−Vector Arithmetic with Abstraction - Bryant, R; Kroening, D; Ouaknine, J; Seshia, S; Strichman, O; Brady, B (Springer, 2007)