Disallow overflow in bitvector literals (parser only)

* For example, (_ bv5 1) is now an error instead of being silently truncated.
* Probably inappropriate for 1.0.x because it changes exception specifications.
ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization
Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.
fix to build system: #include the proper file when they are in both builds and src
Fix warning (line annotation)
Merge branch '1.0.x'
changed default option for quantifier instantiation
fix up build system for swig (d242c30 introduced a subtle error)
Merge branch '1.0.x'
Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context
Minor fixes to build system
Remove PropositionalQuery class and all CUDD-related build stuff (and references)
Fixes for miplib-trick application (and a new testcase)
Minor cleanup of sources
Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.
merged master with dejan's constant evaluating equality engine
merged dejan's stuff