Solving Bit-Vector Equations of Fixed and Non-Fixed Size - Möller, M. Oliver; Ruess, Harald (BRICS Report Series, 1999)
This report is concerned with solving equations on fixed and non-fixed size bit-vector terms. We define an equational transformation system for solving equations on terms where all sizes of bit-vectors and extraction positions are known. This transformation system suggests a generalization for dealing with bit-vectors of unknown size and unknown extraction positions. Both solvers adhere to the principle of splitting bit-vectors only on demand, thereby making them quite effective in practice.