Manipulate value properties, algebraic characteristics, algebraic models of bit-vector operations, and algebraic characteristic models.