[rrnewton]

It's a good question. We would like to make it usable as a platform for dynamic analysis. The idea being that you can control all these external factors (like thread scheduling), find a crashing run, and then ask introspective questions of what the code is doing in a crashing run.

In practice, one challenge we have is bridging between the runtime view of the software (as a debugger would see) -- raw machine instructions and system calls, and the static view that you would get from analyzing the source code.

Sanitizers, for example (ASAN, TSAN, etc), are typically implemented in the compiler as program instrumenations. If we integrated binary instrumentation tools like Intel Pin or DynamoRio, we could perform additional dynamic analysis, but still at the machine code rather than source code level, which is a big gap from how symbolic execution normally happens, at the source code / AST level.