Klever

CPAchecker produces 2 edges for calls of functions which return values are stored to variables. The first edge corresponds to function calls themselves while the second edge is for assignments. This increases error trace sizes when details like assignments are shown. Also it complicates analysis when, say, SMG provides notes for such function calls since they are related to corresponding edges while edges with assignments are most likely hidden by default.