Add branch and bound lemma if linear arithmetic generates a non-integer assignment...

Add branch and bound lemma if linear arithmetic generates a non-integer assignment (#6868)

This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.

This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.

This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.