Opt out of Termination-{MainControlFlow, BitVector} and Concurrency-Memsafety Subcategory
CPAchecker opts out of the following subcategories:
Termination BitVector & Termination MainControlFlow
Both categories require non-linear arithmetic (nla). CPAchecker's termination analysis is based on LassoRanker and does not support nla. Thus, we are unable to handle and confirm witnesses in these categories.
Concurrency-Memsafety
We use BDDs as abstract domain for concurrent programs. This analysis does not handle heap memory soundly and is thus unsuited for witness validation in this category.
Edited by Henrik Wachowitz