Refactoring to prepare for MBQI with integer quantification.  Minor bug fixes.
For SMT-LIBv2: to_real support; to_int and is_int support for constant expressions