rlimit regression

[kanigsson]

rlimit.smt2.txt

Hello Z3 team,

On the attached VC, z3 4.8.4 with a certain rlimit terminates immediately:

$ time z3.4.8.4 rlimit=610000 rlimit.smt2.txt 
unknown
user	0m0.230s

But z3 4.8.5 doesn't stop and eats memory very fast (4 Gig in ~30 seconds, when I stopped it)

$ time z3.4.8.5 rlimit=610000 rlimit.smt2.txt 
^C^C
real	0m39.013s
user	0m37.917s

To make it clear this isn't about the memory consumption but about the change in rlimit behavior. I think some rlimit timer isn't updated anymore and z3 just continues to run.

Any idea what could be the issue? Thank you in advance.

[kanigsson]

Thanks for the quick fix! I will try it out as soon as I can.

[kanigsson]

Just to confirm that the issue is fixed using this commit.