Add trace-generator capability to support SMT solvers.
MARK and SAY will provide at least one example of some property the user is looking for even in billions of traces WITHOUT having to generate those traces -- it has three outcomes: a) found a trace meeting the constraints and displays the one it found and allows -- "Find the next one" function b) no traces will ever have that property. c) runs forever -- provides a button to stop the SMT specifically because we may want to switch SMT solvers and try again.
Will follow the model of this used by CRYPTOL