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

Viewed 358

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?
1 Answers
Related