model: replace TreeNode with NodeStack

model: replace TreeNode with NodeStack

Big structural change to the model-checker internal data structure. It's now
tested to work, and hopefully it's still easy enough to understand.

Note that also, we remove the backtrack_list, since this type of structure
depended on keeping around "action lists" of each trace. Instead, I can free up
those lists at the end of each execution, preventing leaks and limiting memory
usage.