When using rlimit, z3 gives an output but keeps running for a long time

[hmijail]

When run on the attached file, z3 outputs a result after a few seconds, coherent with the rlimit. But then it keeps running (with high CPU consumption) for a long time.

That extra running time seems to grow as the rlmit gets higher.

$ z3  keeps_running.smt rlimit=60000000
unknown
(:reason-unknown "canceled")
(:rlimit 60007344)                     <---------takes 31 s
$                                      <---------takes another ~30 s of high CPU usage

Bug present in current HEAD 374609b but also in previous versions (4.12.1, 4.8.17)
keeps_running.smt.zip

[NikolajBjorner]

It uses time to clear up entries in a hash-table.
I added some optimization to take down the time.
Otherwise, your sample causes a slew of instantiations to be generated, so the main issue is in the interaction of triggers and your formula.

[hmijail]

So if I understand correctly, this might still happen and is not considered a bug, but is just CPU time spent on cleanup.
Could I just kill the z3 process once it has emitted the (:rlimit) line?

[NikolajBjorner]

the bug is basically an inefficiency in the hash tables we use.

[hmijail]

Yes, I understand.
As a user, could I just kill the z3 process once it has emitted the (:rlimit) line?

[hmijail]

Using the HEAD version, the example file I posted in the initial report takes now longer to execute, and much longer for z3 to finish. (Before it was 2x, now I'm seeing 3x/4x)

During that finishing time, the memory usage keeps climbing, causing the whole system to get slower.