thomasjball/PyExZ3 — pull request #3 by OlliSaarikivi (2014-06-11 11:46:28+00:00)
Title: Path cutting by checking for state subsumption

I've implemented cutting paths when it is detected that a state is subsumed by one already visited on another path. Whenever the same control location is reached again, it is checked whether the new state is included in an old one.

The check is done with a call to Z3. The solving times can sometimes be quite large (probably due to the forall quantification). This can be seen in a variation of the `diamonds.py` test with one more diamond.

The feature is off by default and can be enabled with `--cutting`

This feature is quite experimental, so including it in the main line might not be the best choice.