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
rlimitrestrict - just time or also memory? - Q2: Is
:rlimit 1000equivalent to:timeout 1000in that the solver must terminate after1000milliseconds? - Q3: Can
rlimitbe set repeatedly (astimeoutcan) or just once?