Unit-Test: Created a method that can generate a CFA for test purposes.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15184 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Counterexample: Implemented merge for multi edges.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15185 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Small fix in multi edges.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15186 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Expression Statements will be used instead of Assignments.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15187 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Refactored, replace null with empty String.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15188 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Made Addresses symbolic.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15189 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Fixed Bug.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15190 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Started working on J-Unit test.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15191 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: Fixed unit test.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15192 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
CEX: The last 4 commits got squashed due to forgetting to erase a sys
out in between staging commits. Just some bug fixing and working on unit
tests

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15193 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
FindBugs: Don't need to box a primitive to transform it to a String.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15194 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
We must not use classes from the JUnit package within runtime code.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15195 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Setting the lib path in the formula manager is useless.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15196 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Predicate inference: Fixed some of the rules; made them more general and robust. 



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15197 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
for global refinement with value analysis: add possibility to sort targets (and targets path) for interpolation

based on (expected) quality of interpolants, target path are sorted,
so that paths with favourable interpolants are interpolated first,
which may result in the fact, that others paths do not have to be
interpolated anymore, because existing interpolants are strong enough 


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15198 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New methods in the FormulaManagerView. 



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15199 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New method that provides the names of the live variables.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15200 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Working WPs...



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15201 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding sequential interpolation for Z3 again, it was removed due to a change in the API.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15202 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding Junit-test for the interpolation-API of our solvers.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@15203 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c