proof-solvers: a time limit on every z3 goal, and a deadline on its I/O #239

Merged

dcharlot merged 1 commit from fix/z3-goal-deadline into main 2026-10-13 09:32:22 -04:00

Conversation 0 Commits 1 Files changed 1 +282 -40

2026-10-13

Transaction Science

proof-solvers: a time limit on every z3 goal, and a deadline on its I/O ...

The resident z3 session had no limit. One goal z3 could not decide held the
session, and every goal queued behind it, for as long as z3 kept at it.

Two guards now close that, in the resident session and the one-shot z3 alike:

- z3's own soft limit (`-t:`, GOAL_TIMEOUT = 60 s by default;
  Z3Server::with_goal_timeout). At the limit `(check-sat)` answers
  `unknown`, which counts as undecided, and the session decides on.
- A deadline GOAL_DEADLINE_GRACE (5 s) past that limit, on both the write
  and the read. A goal can lift z3's limit for itself with
  `(set-option :timeout ...)`. Past the deadline the one-shot z3 is killed,
  and the resident session is broken and replaced.

z3 reads its input only as it reaches each command. So a goal with a
`(check-sat)` of its own and more than a pipe's worth of text after it
blocked the write on the calling thread for as long as that check ran.
Both ends of the pipe are now on threads of their own.

Checked on Homebrew z3 (build host) and on Ubuntu's 4.8.12 (the CI
image's version): unknown at the soft limit, the limit lifted by a goal's
:timeout even after (reset), and a 426 KB write that blocks behind the
goal's own check.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

4a137b3cdd

• View at this point in history

2026-10-13 03:02:17 -04:00