Separate ill-typed portion of arith models (#8734)

Separate ill-typed portion of arith models (#8734)

This makes it so that the ill-typed portion of arithmetic models is not included in the main arithModel map.

Conceptually, we should not include entries in the arithmetic model that violate type constraints since these should never be used e.g. in non-linear to justify whether a model is correct. Instead, by not including that value, we assume that no value was given for that variable. Sanity checking of the arithmetic model then needs only to access the ill-typed portion of the model directly.

This makes it so that strict type invariants can be enforced in the non-linear solver's model.