我要求Z3使用SMTLIB2接口在UFLIA理论中进行量词消除。因此，我断言了一个包含21个存在量化变量的公式，其中7个是整数，14个是布尔值。然后我执行(apply qe)，Z3返回一个目标，该目标仍然包含九个存在量化的变量，分别命名为(x!1 Int)、(x!14 Int)和(x!14!1 Int)到(x!14!7 Int)。这是否意味着qe策略不能同时消除所有量词？
如果我做两次(assert qe)，那么除了重命名的量化变量之外，目标保持不变。我尝试了(repeat qe)，但它返回unsupported，并且将:eliminate-variables-as-block参数设置为true也不会更改任何内容。
然而，如果我从目标中提取量化公式，单独断言它，并再次执行assert qe，Z3会按照我的意愿消除剩余的量词。
请参阅下面的链接了解公式，我需要做一些魔术来让Z3一次消除所有量词吗？
https://gist.github.com/chsticksel/edeb350fa4474713f3df#file-apply-qe不会同时消除所有量词smt-
感谢您的错误报告。它现在已经在不稳定的分支中得到了修复。