Explicitly promote BoolExprs and IntExprs in mixed int/real arithmetic using `to_real` and `ite`.

[elsoroka]

(1) Updated ite(x,y,z) to allow non-Boolean values for y and z and simplified code. (2) Added promote_type and convert rules to codify promotion rules for IntExpr, BoolExpr and Real Expr. (3) Added integer division and cleaned up type conversion around integer and real-valued division. (4) Added to_real and to_int SMT-LIB functions. (5) Fixed #21 using (2) and (4) to ensure correct promotion by wrapping promoted BoolExprs using ite and wrapping promoted IntExprs using to_real.

[codecov-commenter]

Codecov Report

Attention: 28 lines in your changes are missing coverage. Please review.

Comparison is base (e718c1f) 86.62% compared to head (41539fb) 85.90%. Report is 12 commits behind head on main.

:exclamation: Current head 41539fb differs from pull request most recent head 125a965. Consider uploading reports for the commit 125a965 to get more accurate results

Files	Patch %	Lines
src/IntExpr.jl	66.66%	15 Missing :warning:
src/BitVectorExpr.jl	86.00%	7 Missing :warning:
src/smt_representation.jl	33.33%	6 Missing :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #23 +/- ## ========================================== - Coverage 86.62% 85.90% -0.73% ========================================== Files 12 12 Lines 905 986 +81 ========================================== + Hits 784 847 +63 - Misses 121 139 +18 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.