使用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上使用Z3还是FreeBSD？在这些平台上有一个与计时器相关的bug。 我修复了这个问题，但它还没有正式发布。 更多细节请参阅以下帖子。在

• how to set timeout for z3_solver using C-API?