Efficient tools for checking SMT formulas with two quantifiers ($\exists\forall$)
Since your integer variables are from a finite domain, you could &quot;bit-blast&quot; to SAT, then use a 2QBF solver.
In other words, you translate formulas over these int variables into formulas over boolean variables, by building a boolean circuit to represent each of the operations (multiplication and comparison, in your example), and then using the Tseitin transform.

Another approach is to apply one of the methods for 2QBF to your problem directly.  You'd have to implement this yourself.  For example, here is a naive approach.  Suppose your formula is $\exists x \forall y \varphi$:

Let $b_1,\dots,b_n$ be some values.

Testing the satisfiability of $\varphi[b_1/y] \land \dots \land \varphi[b_n/y]$.  If this is not satisfiable, then you can terminate, as it implies that $\exists x \forall y \varphi$ is not satisfiable.  If it is satisfiable, suppose it is satisfied by $x=a$.

Then try to satisfy $\neg \varphi[a/x]$.  If it cannot be satisfied, then you can terminate, as it implies that $\exists x \forall y \varphi$ is satisfiable with $x=a$.  If it can be satisfied, say by $y=b$, let $b_{n+1}=b$, increment $n$, and go back to step 2.


You could implement each of these steps in Z3, and this would take advantage of Z3's SMT theories, without requiring you to &quot;bit-blast&quot; to SAT.  Note that in this procedure, you only invoke Z3 to test satisfiability of singly-quantified formulas; there are no nested quantifiers.  You might even be able to use Z3's incremental solving abilities for better performance.