Minor fixes of policy for eliminating quantifiers (#7033)

Minor fixes of policy for eliminating quantifiers (#7033)

PR #7017 fixed the policy for eliminating quantifiers but introduced
some minor issues, which this commit fixes:

the InstantiationEngine::checkOwnership() method was changed to look
for patterns in the wrong node.
the PR changed the modes of the --user-pat=MODE method but reused
one of the names. This commit fixes the name and adds a check in the
options script.
fixing the policy caused cvc5 to answer unsat instead of the
expected unknown for regress0/use_approx/bug812_approx.smt2. The
commit updates the expected result.