z3 - 是否可以强制 Z3 模型评估涉及数组的布尔表达式？

Question

有时，评估模型中的布尔表达式不会返回具体的布尔值，即使表达式显然具有具体值。我已经能够将其简化为涉及数组表达式的情况，例如这个测试用例：

from z3 import *

x = K(IntSort(), 0)
s = Solver()
s.check()
m = s.model()
print m.evaluate(x == Store(x, 0, 1), model_completion=True)

我希望这可以打印False，但它会打印K(Int, 0) == Store(K(Int, 0), 0, 1)。其他示例产生类似的结果。将第一行替换x = Array('x', IntSort(), IntSort())为相同的结果（尽管这取决于默认解释）。有趣的是，将第一行替换为x = Store(K(IntSort(), 0), 0, 1)导致示例打印True。

有没有办法强制 Z3 将这些表达式评估为具体值？