In a discussion between some Munich Goblint folks and @MartinSpiessl and others from the CPAChecker team on Friday we identified that as a first step of a possible co-operation (e.g. combining the strengths of Goblint as an Abstract Interpreter and Model Checkers such as CPAChecker), it would be helpful for us to produce the YAML-based invariant format (https://github.com/sosy-lab/sv-witnesses).

Since no complicated re-construction of the call-stack is needed here, I'd suggest we implement this as an additional output format for the assert instrumentation from #157 as opposed to integrating it with all the weirdness we have for producing automaton-based witnesses.