Quantifier elimination for the theory of bit vectors

[AnzhelaSukhanova]

PR implements the quantifier elimination for BV formulas of a certain structure according to the paper. Supported structure: a conjunction of inequalities/equalities between a bound variable in a linear term and a term without that variable.