Open
Description
It would be nice to have an option to interleave the attempted proof of side-conditions with symbolic simulation. This would allow us to report safety condition violations earlier, especially in cases where symbolic simulation would otherwise not terminate, or terminate only with timeout or iteration limits.
In addition, perhaps, it would be good to have an option to spawn off separate concurrent threads to attempt proofs while symbolic simulation proceeds. This might allow us to make better use of multiple cores (although the memory additional memory pressure might cause this to be problematic).