Remove dependency on SlicingAbstractionUtils from core code
Original issue created by @PhilippWendler on 2018-06-26 at 05:08:04, last modified on 2018-06-26 at 05:08:04
Currently CounterexampleCheckAlgorithm.checkErrorPaths
calls a method from SlicingAbstractionUtils
. In general, core code (i.e., analysis-independent code) should not have dependencies on analysis-dependent code.
Furthermore, the option counterexample.ambigiousARG
is necessary to activate the code for slicing abstraction in CounterexampleCheckAlgorithm
. This is an option that CPAchecker should not have: it is always better to something correctly automatically instead of relying on the user to specify a specific option.
Thus, both the dependency and the option should be removed.