Z3 变量名导致"unknown"满足

Question

使用Z3检查的可满足性

(declare-fun length ((Array Int Int)) Int)
(declare-const lindx2 (Array Int Int))
(declare-const findx1 (Array Int Int))
(declare-const orig_findx1 (Array Int Int))
(assert (and
(forall ((i Int) (j Int))
(let ((a!1 (and (<= 0 i)
(<= i (- (length findx1) 1))
(<= 0 j)
(<= j (- (length orig_findx1) 1))
(= i j))))
(=> a!1 (= (select findx1 i) (select orig_findx1 j)))))
(= (length lindx2) 11)
(forall ((i Int)) (=> (and (<= 3 i) (<= i 25)) (= (select findx1 i) (- 1))))))
(check-sat)

返回未知。这本质上试图断言findx1和orig_findx1中的所有元素都相等，长度(lindx2(=11，并且对于i=[3，25]，findx1[i]=-1。然而，改变"；findx1"；至"；indx1"；允许Z3返回可满足的。有人知道是什么导致了未知的可满足性吗？我在Ubuntu 18.04 上使用Z3版本4.8.8

Answer 1

不幸的是(尽管是出于技术原因(这并不令人惊讶：以前已经多次观察到语法变化(重命名符号、重新排序SMT命令(会导致性能和未知/sat波动，请参见例如。https://github.com/Z3Prover/z3/issues/909/.Z3的启发式算法似乎受到程序结构的影响，即使在显式设置随机种子时也是如此。

Answer 2

我可以复制它，这真的很奇怪！

我对这个基准测试是unknown并不感到惊讶，因为它充满了量词，而且z3很难求解。但是将findx1更改为indx1应该对此没有影响；即它应该保持为unknown。

我已在https://github.com/Z3Prover/z3/issues/4600.答案是：是MBQI最终未能确定可满足性。它与阵列模型绑定。当您用未解释的函数替换数组时，MBQI更稳定也就是说，不幸的是，这些差异是理所当然的。太糟糕了！