Regression in Z3 timeout?

[aytey]

Hello,

I have two builds of Z3:

• 606754c09 (May 1st)
• b1893f2a5 (June 20th)

Given a particular Z3 Python script, and when using 606754c09, I get a timeout (i.e., Z3 returns unknown). However, when using the same script under b1893f2a5, Z3 never terminates (i.e., it appears that the timeout parameter is being ignored). This timeout is set to 10000 ms.

I have captured the Z3 logs from these two runs:

• 606754c09_z3.log

• b1893f2a5_z3.log

The log for b1893f2a5 ends when I kill the process; the log for 606754c09 has been "artificially truncated" to match that of b1893f2a5 (i.e., after the check gives unknown, we do further work with Z3, which is irrelevant for this issue I believe).

Please let me know if there are any more details I can provide on this issue.

Cheers,

Andrew

[aytey]

I added the following:

z3.set_param("verbose", 10)

and it seems to "get stuck" with output like this:

(smt.delete-inactive-clauses  :num-deleted-clauses 188)
(smt.working :conflicts 245727 :agility 0.314074)
(smt.working :conflicts 247128 :agility 0.311207)
(smt.working :conflicts 248669 :agility 0.311665)
(smt.delete-inactive-clauses  :num-deleted-clauses 8888)
(smt.working :conflicts 250364 :agility 0.269951)
(smt.working :conflicts 252228 :agility 0.334213)
(smt.working :conflicts 253229 :agility 0.295869)
(smt.working :conflicts 254278 :agility 0.325157)
(smt.delete-inactive-clauses  :num-deleted-clauses 4100)
(smt.working :conflicts 255279 :agility 0.339337)
(smt.working :conflicts 256532 :agility 0.250027)
(smt.working :conflicts 257533 :agility 0.326521)

[aytey]

In case it is useful, I captured the verbose output from running under these two different builds:

• 606754c09
• b1893f2a5

For 606754c09, the execution ends with:

(tactic-exception "smt tactic failed to show goal to be sat/unsat timeout")

while b1893f2a5 is "stuck".

[aytey]

Attempted fix in #2356.

I think this is where things got broken: 48fc3d7#diff-5f65287f221a60407bf05209d67c8d9bL3734

[NikolajBjorner]

smt.timeout should really be deprecated.
The "timeout" parameter should be settable directly. The script times out if I replace "smt.timeout" by "timeout". I don't recall why I left smt.timeout

[aytey]

Yep! I can confirm that -- I changed our code to use z3.set_param("timeout", ...) rather than z3.set_param("smt.timeout", ...) and it now seems to work!

[yxliang01]

@NikolajBjorner Hmm, from release note for 4.8.6, I saw this issue. But, the timeout option is not available in z3 4.8.6 when calling solver.set in z3py API ... If I set globally using set_param, the timeout is not so functioning. What's the replacement?

[lexbailey]

I've hit this issue too, @yxliang01 where are the release notes you mentioned? I can't see details of this bug in the main release notes file in the repo

[yxliang01]

@danieljabailey https://github.com/Z3Prover/z3/releases/tag/z3-4.8.6 here

[yxliang01]

No, I didn't see any issue mentioning this. That's why I commented here.

[lexbailey]

ah okay, I see now a link to this issue and a commit that removes the timeout, I see something about "datalog.timeout", not sure what that is but doesn't do what I want.
:(

[yxliang01]

CC: @NikolajBjorner

[lexbailey]

Ah, I think I found my issue, and I'm not sure if it's a bug or intended, I was calling set on the result of Then.solver()...

t = Then(*tactics)
self.solver = t.solver()
if timeout:
    set_param("timeout", timeout*1000) # New way???
    #self.solver.set("timeout", timeout*1000) # Deprecated???

[NikolajBjorner]

There is a gobal timeout:
timeout (unsigned int) (default: 4294967295)

The solver object also admits setting a timeout, though it isn't called solver.timeout. It is called timeout. This works for me:

from z3 import *

s = Solver()
s.set("timeout", 1)
x, y, z = Ints('x y z')
s.add(x * x > 0)
print(s.check())

Arguably, it should have been called "solver.timeout", or for usability, both options are available.
If there is no timeout on the solver object, the global timeout is used.
The timeout on the solver object overwrites the global timeout if it is set.

[asymmetric]

I was doing (or-else (using-params smt :random-seed 3 :timeout 1000) (using-params smt :random-seed 2 :timeout 2000) (using-params smt :random-seed 1))) on 4.8.5 to set timeouts on the individual tactics.

Which timeout am I supposed to configure to achieve the same result?