我要求 Z3 使用 SMTLIB 2 接口在 UFLIA 理论中进行量词消除。所以我断言了一个包含 21 个存在量化变量的公式，其中 7 个是整数，14 个是布尔值。然后我这样做(apply qe)，Z3 返回一个目标，该目标仍然包含九个存在量化变量，(x!1 Int)named(x!14 Int)和(x!14!1 Int)to (x!14!7 Int)。这是否意味着该qe策略不会一次消除所有量词？
如果我做(assert qe)两次，除了重命名的量化变量之外，目标保持不变。我试过(repeat qe)了，但是返回unsupported，也将:eliminate-variables-as-block参数设置为 true 不会改变任何东西。
但是，如果我从目标中获取量化公式，自行断言并assert qe再次执行，Z3 会按照我的意愿消除剩余的量词。
请参阅下面的链接以获取公式，我需要做一些魔术来让 Z3 一次消除所有量词吗？