Z3のドキュメントには、モデルベースの数量化インスタンス化（MBQI）について記載されています。
層化ソートフラグメント
統計化されたソートフラグメントは、多くのソートされた1階論理式のもう1つの決定可能なフラグメントです。これは、冠頭標準形で記述された場合、ソートからナチュラルまで、およびすべての関数に対して関数レベルが存在する式に対応します。
（declare-fun f（S_1 ... S_n）R）
level（R）<level（S_i）。
Z3は、冠頭標準形の数式をサポートしますか、それとも存在記号がすべてスコーレム化によって削除されたユニバーサル数式のみをサポートしますか？
これにより、フラグメントがより制限的になりますね（スコーレム関数が階層化を破る可能性があるため）？
（少なくともMBQIに関する論文[定量化されたSMT公式の完全なインスタンス化、YetingGeとLeonardode Moura、CAV 2009]では、普遍的な公式のみがカバーされているように思われます。）