解決方案在使用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？在這些平臺上有一個與定時器相關的錯誤。 我解決了這個問題，但它不是官方發佈的一部分。 有關更多詳細信息，請參閱以下文章。

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