Klever

Like with auxiliary functions, several components (namely CIL and CPAchecker) can produce temporary variables that will be referred within violation witnesses and thus error traces. We tried to remove some of these variables if this can be done rather safely, but corresponding code is very complicated and buggy.

I suggest to get rid of as many temporary variables as possible (for CIL we will need to fix it or to turn on some options, for CPAchecker as well as all other verifiers we will need to use source file references for showing source code in error traces) and then we will be able to get rid of temporary variables removing code in Core VRP.