What is the relation between options `rlimit` and `timeout`?

Question

It was suggested in this Z3 issue comment that option rlimit is to be preferred over timeout:

Combining timeouts with a search algorithm makes everything non-deterministic, so now you don't even have to change the random seed to make it fail! Use rlimits ((set-option :rlimit <n>) and similar) for a deterministic way of resource bounding.

I tried to find more information about rlimit in Z3's help (z3 -pd) but the description provided there is only very short.

Specifically, I have the following questions:

• Q1: What kind of "solver resources" does rlimit restrict - just time or also memory?
• Q2: Is :rlimit 1000 equivalent to :timeout 1000 in that the solver must terminate after 1000 milliseconds?
• Q3: Can rlimit be set repeatedly (as timeout can) or just once?

Mussman

Answer 1

Q1: What kind of "solver resources" does rlimit restrict - just time or also memory?
A1: Whatever we think makes sense. The idea is to count something like "basic operations", but that definition changes as we go ahead and add new "operations". There is no guarantee that it will stay the same for different versions of Z3. However, as long as you keep using the same binary, it is deterministic.

Q2: Is :rlimit 1000 equivalent to :timeout 1000 in that the solver must terminate after 1000 milliseconds?
A2: No, there is no equivalence, but once the rlimit is exceeded Z3 will terminate. We recently fixed a number of bugs where it didn't terminate and I'm sure there still are a few of those bugs in there somewhere, but we'll fix them of course.

Q3: Can rlimit be set repeatedly (as timeout can) or just once?
A3: Yes, you can do

(set-option :rlimit 12345)
(check-sat)
...```

Claudineclaudio