inconsistent interpretation of __VERIFIER_assume in termination analysis
Created by: holznerst
__VERIFIER_assume seems not to be interpreted consistently in termination analysis.
There are benchmark tasks for which __VERIFIER_assume is considered as endless loop (see PR 1028) and other tasks for which not pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.
But if this tasks termination verdict is false due to __VERIFIER_assume, then there is at least one counterexample (pals_floodmax.3.2.ufo.BOUNDED-6.pals.c) in other benchmarks
Originally posted by @holznerst in https://github.com/sosy-lab/sv-benchmarks/pull/1028#issuecomment-558965368