Do not apply unconstrained simplification when quantifiers are present (#4532)

Do not apply unconstrained simplification when quantifiers are present (#4532)

Fixes #4437.

This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered.

It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic.