Fixes cvc5#11966.

This PR ensures that we always provide a definitive value for terms in
`get-value`, including those depending on quantified formulas.

In detail, Boolean literals can be eliminated during preprocessing and
equated to quantified formulas, for example, if `(= b (forall ((x Int))
(P x)))` is a top-level assertion. Moreover, if `b` does not appear in
any further assertion, the solver will avoid reasoning about `(forall
((x Int)) (P x))` altogether. In such cases, the solver answers
`sat`/`unsat` soundly but does not know the value of `b`.

Previously, we gave a warning in such cases and returned the quantified
formula itself. We now *invoke a subsolver* inside the call to
`get-value` on the quantified formula in question. This behavior is
enabled by default and can be disabled by `--no-check-model-subsolver`.

The following changes are made by this PR:
- Get value now invokes resource limits in cases where it is possible to
invoke a subsolver.
- A minor fix to check-models for the case where multiple expand
definitions are necessary for evaluating.
- Further fixes to the non-closed converter to guard against queries
that are illegal (e.g. when check-model would depend on assertions that
involve terms that the solver does not support).
- Adds the regression and disables `-q` on several regressions that now
pass `--check-models` without warnings.