z3 Python API를 사용하여 루프 내에서 해 찾기 제한 시간

이전 제안에 따라 z3Py를 사용하는 동안 해결사의 초기 제한 시간을 설정하려고합니다.z3 Python API를 사용하여 루프 내에서 해 찾기 제한 시간

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()

는 기본적으로 타임 아웃 (심지어 MS에서 터무니없이 적은 시간으로) 발생하지 :

는 다시 모든 내역없이, 이것은 내가 시도하고있는 무슨이다.

출처

2013-02-06 mborowczak