Refine float-integer casts in `BaseInvariant`

[sim642]

PR #1519 originally tried to handle this from SV-COMP:

analyzer/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c

Lines 6 to 9 in ec06dea

	int64_t data;
	if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL))
	{
	int64_t result = data * data; // TODO NOWARN

The fix involved BaseInvariant refinement of float-integer casts in a possibly incorrect way, so it was reverted in #1519. However, it should still be possible to implement sound refinement of such casts.