[SMTCOMP] The infinite-precision issue again

[Clark Barrett]

I just wanted to add a point that Leonardo brought up:

> (paraphrasing...)
> Anyone entering QF_LIA and QF_LRA will need bignum support because there are
> actual benchmarks that require it.  Thus it should be possible to
> to use the linear arithmetic procedure when the check for fixnums fails in a
> difference logic benchmark.

Because this seems like an easy fix, I am inclined to keep the current scheme
as it encourages everyone to migrate towards a more robust solution.

-Clark