Listening to the Firehose: Sonifying Z3’s Behavior

Modern formal methods rely heavily on Satisfiability Modulo Theory (SMT) solvers like Z3. Unfortunately, these solvers are complex, have unpredictable runtime behavior, and are highly sensitive to the structure of the input query. As a result, when a Z3 query runs for tens of minutes and/or times out inconclusively, there is little that an end-user can do to figure out what went wrong. They can attempt to inspect the gigabytes of logged information that these tools produce every minute. But, no existing tool provides a broad understanding of Z3 behavior.We propose Z3Hydrant, a scalable approach that converts Z3 logs into sound. By relying on the innate abilities of the human ear to pick out patterns, Z3Hydrant encodes raw Z3 logs into an audio stream. The result is accessible to anyone who can hear and helps to provide a general flavor of what occurred during a particular run. We describe our approach and include several example audio files that capture complex Z3 runs.