Bugfix: Unsoundness in QF_UFLIRA

Create equalities between int an real always in the linear arithmetic
solver, so that it can check for integrality.

Added a test case that shows a bug in the Cut-generator.  We currently
diverge on this benchmark.