Improvements for evaluation in model (#8738)

Improvements for evaluation in model (#8738)

This marks APPLY_SELECTOR and SEQ_NTH as unevaluatable kinds.

This means that get-value applied to applications of them e.g. (seq.nth t) will evaluate to c if (seq.nth t) is in the same equivalence class as constant c. (Note that this could be further improved to reason by congruence for (seq.nth s) where s = t, which I'm considering to do on a followup PR).

This removes many of the required -q from the command line arguments of our regressions. This also does some minor cleanup to our regressions to remove -q from further regressions.