在循环中使用z3 Python API时的求解器超时

Question

根据之前的建议，我正在尝试在使用z3Py时为求解器设置一个较早的超时时间。

虽然没有详细说明所有情况，但我正在尝试做的就是：

for bits in range(A, B, incrmt)
    s = Solver();
    s.set("timeout", 30) #30, 3000, 30000, 60000 no change
    s.add(some constraints)
    if(s.check() == sat):
        print "Sat, %d," %(bits)
    else:
        print "Sat Unknown, %d," %(bits)
        break
    sys.stdout.flush()

基本上，超时从来没有发生过（即使设置的时间小到毫秒级别也不行）。

Answer 1

你是在Linux或FreeBSD上使用Z3吗？这两个平台上有个跟计时器有关的bug。我已经修复了这个问题，但还没有包含在正式版本里。想了解更多细节，可以看看下面的帖子。

• 如何使用C-API为z3_solver设置超时？