Add lazy strategy for bounded integers to avoid non-terminating unsat cases.  Add regressions.