We currently have a number of tests that are quite expensive to run, and these tend to be also more sensitive to SMT solver shenanigans. It would be nice to put these in a separate directory that isn't automatically run, so that we have them as examples but they don't get in the way of day-to-day development.