- *
- * Each part of the state of the model chercker represented as a global
- * variable prevents some sharing between snapshots and must be ignored.
- * By moving as much state as possible in this structure allocated
- * on the model-checker heap, we avoid those issues.