the documentation of Z3 says for the Model-based Quantifier Instantiation (MBQI):
Stratified Sorts Fragment
The statified sorts fragment is another decidable fragment of many sorted first-order logic formulas. It corresponds to formulas which, when written in prenex normal form, there is a function level from sorts to naturals, and for every function
(declare-fun f (S_1 ... S_n) R)
level(R) < level(S_i).
Does Z3 support any formula that is in prenex normal form, or only universal ones where all existential quantifiers have been removed by skolemization?
This would make the fragment more restrictive, wouldn't it (as the skolem functions might break the stratification)?
( At least in the paper on MBQI [Complete instantiation for quantified SMT formulas, Yeting Ge and Leonardo de Moura, CAV 2009] it seems to me that only universal formulas were covered. )
