TY - JOUR AU - Möller, M. Oliver AU - Ruess, Harald PY - 1999/01/18 Y2 - 2024/03/28 TI - Solving Bit-Vector Equations of Fixed and Non-Fixed Size JF - BRICS Report Series JA - BRICS VL - 6 IS - 18 SE - Articles DO - 10.7146/brics.v6i18.20075 UR - https://tidsskrift.dk/brics/article/view/20075 SP - AB - This report is concerned with solving equations on fixed and<br />non-fixed size bit-vector terms. We define an equational transformation<br />system for solving equations on terms where all sizes of<br />bit-vectors and extraction positions are known. This transformation<br />system suggests a generalization for dealing with bit-vectors<br />of unknown size and unknown extraction positions. Both solvers<br />adhere to the principle of splitting bit-vectors only on demand,<br />thereby making them quite effective in practice. ER -