Checking that every Number of sort Int in mkConst is indeed integer

[Tomaqa]

This assertion fails with substitutions and also in FarkasInterpolator::getFlexibleInterpolant in TEST_F(LIAInterpolationTest, test_InterpolationLRASat). We should probably forbid such substitutions. In the interpolation, I am not sure if the test makes sense or if the situation must be handled more properly.

[Tomaqa]

As a consequence of the check, I removed substitutions for integers when it introduces rational coefficients.
I also disable flexible Farkas interpolants where the current implementation IMO does not make sense for integers.

We should probably run SMT-LIB benchmarks to see if it affects the performance (and of course the soundness).

[blishko]

I think flexible interpolation still makes sense even for interger arithmetic. But the interpolant probably needs some normalization to avoid rational coefficients.