我目前正在使用 CVC4 来解决以下形式的公式：
exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)
在这里，f1...fn是从某个数量Bool到的函数Bool，以及
b1...bk是布尔值。
我的问题完全属于UFSMT 的片段：它有量词，但除了函数和布尔值之外没有其他种类。
当我尝试使用 CVC4 上的默认设置解决问题时，它立即返回未知，尽管事实上我所有的量化都是在有限域上的。
问题是，CVC4 有非常多的处理量词的选项：有一堆cegqi，一堆fmf，还有mbqi等等。我的印象是这些大部分是从特定的研究项目中添加的，我宁愿不必阅读 20 篇不同的论文就可以让我的解决方案继续下去。
我的问题：是否有一组推荐的选项来解决此类问题？
我知道 CVC4 是可能的，因为他们在 SMT 比赛的UF Track上竞争并表现相当出色，但我找不到用于该比赛的具体论据。