mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-04 16:10:50 +00:00
Code Activity

Handle SIGXCPU like a regular timeout (#9697)

Browse source 
Z3's -T measures wall clock time, whereas `ulimit -t` measures CPU time.
Currently, an expired ulimit timeout crashes Z3 without printing
statistics; this patch makes it react cleanly (just as if it has
encountered a regular timeout) to SIGXCPU, the signal that ulimit sends
before sending SIGKILL.
This commit is contained in:
Clément Pit-Claudel 2026-06-03 16:26:38 +02:00 • committed by GitHub
parent 922f49e187
commit 1d706e875c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 23 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
RELEASE_NOTES.md
View file

@ -130,6 +130,7 @@ Version 4.17.0
https://github.com/Z3Prover/z3/pull/9303
- Add fold-unfold tactic as an alternative to solve-eqs for variable elimination using
fold-unfold transformations. Also exposed as a simplifier.
- Handle SIGXCPU (OS timeout) like a regular `-T` timeout. Users should make sure to set the soft limit below the hard one, as in `ulimit -S -t 30 -H -t 31` for a 30s soft limit, so SIGXCPU is delivered before SIGKILL.
Version 4.16.0
==============