Solver timeout within loop using z3 Python API

Question

Per an earlier suggestion, I'm trying to set early timeout for a solver while using z3Py.

Again, without all the particulars, this is what I'm attempting:

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

Essentially, timeout never occurs (even with ridiculously small times in ms).

Answer 1

Are you using Z3 on Linux or FreeBSD? There was a bug related to timers on these platforms. I fixed the problem, but it is not part of the official release yet. See the following post for more details.

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