Consider skipping SMT solving for integer inequalities against constants

[pschanely]

We use symbolic integers with constant bounds quite often. (container and string lengths, for starters)

It might make sense to layer in something just above the solver which could track constant bounds and skip the solver call when the result is already known to be unsat.
(sat is harder since the SMT variable could appear in other arbitrary clauses)