Configurable maximum block depth for BAM
The option cpa.callstack.depth
is useful to deal with recursion without powerful fixpoint algorithm. For example, #580 (closed) may be solved by using this option, -ldv
+ cpa.callstack.depth=2
finds false very quickly, while -predicateAnalysis-bam-rec
spends much more time. However, this option does not work in combination with BAM.
I can not suggest a simple solution, how to fix the option for trunk. Maybe, the simplest way is to duplicate the option for BAM. So, enable internal recursive context only after reaching some limit of calls.
Edited by Philipp Wendler