Better support for CVC4

- Cast integer literals to reals if returned in a model for a real-valued term or variable
- Fail if using precise quantifier elimination or switching to it