Model checker should provide full state trace on assert failure

[ahelwer]

Currently, the model checker only provides the very last step taken before an assert() failed. The full state trace is very useful to have when debugging spec bugs, and could be provided via one of the following:

1. Add a model checker option flag to spit out the full state trace through standard output
2. Provide the full state trace through standard output by default
3. Provide the full state trace in a log file by default