@techreport{BRICS-RS-99-18, author = "M{\"o}ller, M. Oliver and Rue{\ss}, Harald", title = "Solving Bit-Vector Equations of Fixed and Non-Fixed Size", institution = "{BRICS}", year = 1999, type = "Research Series", number = "RS-99-18", address = "Department of Computer Science, University of Aarhus", month = jun, note = "18~pp. Revised version of an article appearing under the title {\em Solving Bit-Vector Equations\/} in " # lncs1522 # ", pages 36--48", abstract = "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", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" }