Is the timeout parameter in the Z3 python API meant to be a strict upper bound for the execution time? Because if I set it to ten minutes it runs for a few minutes more than that. The solver always terminates. That’s not the problem. It’s just that it always overshoots the timeout specified.
Are you looking at elapsed (i.e., wall-)time or CPU-time?
I believe z3's timeout mechanism uses rlimit: https://www.rdocumentation.org/packages/unix/versions/1.5.5/topics/rlimit
As noted in that page:
RLIMIT_CPU : a limit in seconds on the amount of CPU time (not elapsed time) that the process may consume. When the process reaches the soft limit, it is sent a SIGXCPU signal.
So, elapsed time doesn't necessarily match CPU time, as there might be other processes that stop z3 from running.