Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver