Klever

Some environment models can result in faults. Typical examples are the following:

1. Assertions can fail within ldv_check_final_state().
2. CPAchecker SMG can reveal, say, memory leaks, when an environment model frees memory for object for which another environment model allocated memory and that was passed to a driver callback that allocated but did not free another memory.

In both cases corresponding actions are not callback actions by definition (although the first one is called so by mistake), so, they are not included in error trace patterns of unsafe marks. This is wrong, since these patterns miss error trace parts important from the point of view of checking.