I am wondering whether large integer values have impact on the performance of SMT. Sometimes I need to work with large values. Mostly I do arithmetic operations (mainly addition and multiplication) on them (i.e., different integer terms) and need to compare the resultant value with constraints (i.e., some other integer term).
Large integers and/or rationals in the input problem is not a definitive indicator of hardness. Z3 may generate large numbers internally even when the input contains only small numbers. I have observed many examples where Z3 spends a lot of time processing large rational numbers. A lot of time is spent computing the GCD of the numerator and denominator. Each GCD computation takes a relatively small amount of time, but on hard problems Z3 will perform millions of them. Note that, Z3 uses rational numbers for solving pure integer problems, because it uses a Simplex-based algorithm for solving linear arithmetic. If you post your example, I can give you a more precise answer.