我有两个 SMT 问题实例。第一个在这里：
http://gist.github.com/1232766
Z3 在我不太好的机器上大约 2 分钟后返回了一个模型，这很棒。我也有这个：
http://gist.github.com/1232769
我已经在这个问题上运行了 z3 一夜之间，没有 Z3 完成。如果您检查这些文件的内容，您会发现第二个与第一个相同，只是它有一个额外的断言来“拒绝”第一个实例返回的模型。（你可以在它们之间做一个“差异”来了解我的意思。）我碰巧知道这个问题有多个令人满意的模型，我正在尝试使用 z3 来找到所有令人满意的模型。
我知道这可能完全在意料之中，但我很想知道为什么与第一个相比，第二个对 Z3 来说是一个更棘手的问题。有没有更好的方法来制定第二个问题，这样 Z3 会更轻松？
谢谢..
如果不了解您的应用程序，很难给您一个准确的答案。正如您所建议的，建模在您使用的逻辑中起着重要作用：AUFBV. Z3采用的策略对整体性能也有很大影响。Z3 配备了多种内置策略。它有许多可用于影响搜索的参数。Z3 还有一种策略规范语言。这是一个新功能。我没有宣传它，因为它正在进行中，并且语言很可能会在下一个版本中发生变化。您可以通过执行以下命令访问有关策略语言的更多信息：
(help check-sat-using)
(help-strategy)
话虽如此，Z3 中有一个内置策略似乎对您的问题有效。它是用于逻辑的策略UFBV。您的问题使用数组，但可以通过将 table0 转换为具有两个参数的函数来避免它们：
(declare-fun table0 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8))
(select (table0 s65) t)并且用(table0 s65 t)where替换形式的每个术语t是一个任意术语。最后，您还必须(set-logic UFBV)在文件开头添加命令。使用此设置，我设法为您的查询生成 4 个不同的模型。我没有尝试产生更多。每个呼叫消耗大约 75 秒。