Fix special casing for PI in model value (#8189)

Fix special casing for PI in model value (#8189)

PI should be considered a model value but not a "base" model value. This avoid spurious debug assertion failures, which are now treated as warnings. This makes a difference when another theory e.g. UF says that PI is currently equal to a constant value c. Since our lemma schemas are model-based, we may require building a spurious model where PI is c, and refine afterwards.

This also fixes a bug in our extended function rewriting which would mistakenly think that PI was reduced, and hence skip a full effort check if PI was the only extended function in the current context. This was previously causing a final model to be one where PI = 0.0.

Fixes #8183.