Report SMT solver timeout in CLI output

[palinatolmach]

Related: #396

At the moment, Kontrol doesn't report if an SMT solver timeout has occured—to identify that the solver has timed out, one needs to look at the backend's bug report. We should add the corresponding message to the output, perhaps with a suggestion to increase the --smt-timeout value.

As discussed with the backend team last week, an smt solver error during the execution can be safely interpreted as a timeout. We should

• in pyk, handle an smt solver error (with error code 5) separately and add the term causing the error to output (that was done previously in Make KCFGExplore aware of aborting requests due to unknwon predicates pyk#744)
• in kontrol, add a corresponding error message suggesting increased timeout via --smt-timeout N

[yale-vinson]

Next step: determine LoE to close this issue

[nwatson22]

I examined this issue some, and I think the main difficulty here is that, firstly the haskell and booster backends handle logging differently, and neither in a way conducive to what we want to do here. The former allows you to requests certain types of log entries at a very granular level, but just dumps all logs into a file, and I don't think just examining this file, e.g. searching for certain strings after failure, is a very robust way to go about it. The booster backend has a verbosity option that can write the relevant types of log messages, but only to stderr.

It might be worth considering creating an issue to see if we can get both backends to give us an actual RPC response that we can interpret in this case rather than just crashing.

While trying to reproduce the solver timeout crash that occurs during proof execution, I noticed it's not straightforward to do because just passing in a very short timeout gives this error:

 The definitions sent to the solver may not be consistent (Z3 timed out).

which I assume means that 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()).

[palinatolmach]

Related pyk PR: runtimeverification/pyk#744

[palinatolmach]

Related issue: #396

[ovatman]

I've opened an issue for the backend (see #3747), until it's been figured out we may issue timeout errors for all the SmtSolverErrors since timeouts seems to be the most frequently encountered errors form Z3