Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
hmijail opened this issue Jul 9, 2024 · 5 comments
Closed

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

hmijail opened this issue Jul 9, 2024 · 5 comments

Comments

@hmijail
Copy link

hmijail commented Jul 9, 2024

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
@hmijail hmijail mentioned this issue Jul 11, 2024
Open
NikolajBjorner added a commit that referenced this issue Aug 3, 2024
@NikolajBjorner
shave some overhead from fingerprint hash function #7281
51fcb10
@NikolajBjorner
Copy link
Contributor

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
Copy link
Author

hmijail commented Aug 26, 2024

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
Copy link
Contributor

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

@hmijail
Copy link
Author

hmijail commented Aug 27, 2024

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

@hmijail
Copy link
Author

hmijail commented Aug 30, 2024 •
edited
Loading

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @hmijail