ERRATA : An Alternative to SAT-Based Approaches for Bit-Vectors (TACAS 2010) The version presented in the proceedings of TACAS 2010 contains a small mistake at page 4 (section 2.3). The existence of a best approximation for each concrete element does not follow from the completeness of the abstract lattice, as wrongly stated. We must require that there exists a Galois connexion between the concrete domain D and the abstract domain A. With this hypothesis, the best abstraction function \alpha is well-defined, and is a Galois connexion. The long version of the paper available on my webpage has been corrected. This error has no incidence on the main results of the paper.