(apply qe) does not eliminate all quantifiers at once?

Question

I am asking Z3 to do quantifier elimination in the UFLIA theory, using the SMTLIB 2 interface. So I assert a formula with 21 existentially quantified variables, of them seven are integer and 14 are Boolean. Then I do (apply qe) and Z3 returns a goal that still contains nine existentially quantified variables, named (x!1 Int), (x!14 Int) and (x!14!1 Int) to (x!14!7 Int). Does that mean the qe tactic does not eliminate all quantifiers at once?

If I do (assert qe) twice, the goal stays the same except for the quantified variables renamed. I tried (repeat qe), but that returns unsupported, also setting the :eliminate-variables-as-block parameter to true does not change anything.

However, if I take the quantified formula from the goal, assert it on its own and do assert qe again, Z3 eliminates the remaining quantifiers as I wanted to.

See the link below for the formula, is there some magic I need to do to have Z3 eliminate all quantifiers at once?

https://gist.github.com/chsticksel/edeb350fa4474713f3df#file-apply-qe-does-not-eliminate-all-quantifiers-at-once-smt

Answer 1

Thanks for the bug report. It has been fixed now in the unstable branch.