Open
Description
Related: runtimeverification/kontrol#21 (comment)
As reported by @nwatson22 in runtimeverification/kontrol#21 (comment), passing in a very short timeout in Kontrol gives this error:
The definitions sent to the solver may not be consistent (Z3 timed out).
which might mean Z3 is being called to validate the definitions even before any symbolic execution job is requested. This causes the server to crash even before we manage to read which connection the process opened (in _get_host_and_port()
).
Having exit codes for failures that happen during server startup might help us handle such issues in pyk
and kontrol
.