Unsat only with unnecessary asserts, else unknown #8052
Description
In the attached file, z3 reports unsat only if the two asserts between declare-const and push are there. If one of the asserts is commented out, the result turns into unknown, even though the asserts should be given by the quantifier anyway.