Unsat only with unnecessary asserts, else unknown

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.

issue.smt2.txt