I think merging loops should be done in a fixed point iteration.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14069 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
merging manually from branch into trunk: replacing internal SSAMap-increment with external FreshValueProvider.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14070 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
kInduction should not be terminated when invariant generation is interrupted; it is able to continue without further refining the invariants.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14071 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Partially reverted r14025 (fix for single-path-strategy) as it was incomplete and introduced issues with the standard configuration for single loop transformation.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14073 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
manual merge from branch 'bamRecursion' into trunk, adding new method 'rebuildAfterFunctionCall' to interface 'Reducer', adding implementations for some CPAs. Currently the method is never called, but more related code is coming soon.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14075 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug where only the starting line of a multi-line edge was considered for witness automaton matching.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14078 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
manual merge from branch into trunk. this might be the minimum of code needed to analyse recursion, without breaking to much of the existing BAM-implementation. configs added.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14079 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
skipping non-explicit recursion is indeed beneficial, solves ~90 more

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14080 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Not only the FileLocations of the AstNodes of an edge should be collected, but also the FileLocation of the edge itself in case it is not covered by the former.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14085 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
The file location of assumptions now includes the token "if".

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14086 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Line matching in witness checking should not treat artificial edges as compulsory.

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



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14088 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix FindBugs errors: Remove assert whose statement is always true,
ArrayValue.isValidComplexValue(Value) checks for correct type.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14089 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Cleanup some outdated files in test/test-sets/

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14090 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix a problem when Eclipse CDT determines a wrong type for an array
access if the array is a typedef type.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14091 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
when strengthening CEX-check with assumption from automaton, for now, ignore assumptions with incomplete type information (automaton is missing information about callstack of functions, hence, not all types can be resolved)

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

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