Modified the single-loop-transformation so that the first CFA subgraph is connected directly to the graph entry, not indirectly via the loop head. This makes it easier for analyses to determine that an initial value is constant in some cases.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12933 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Potential target locations are now determined at the start of the BMC+k-induction deepening cycle to be able to use this information earlier.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12934 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Fixed two bugs in the computation of the value of a boolean flag; a) the expression was inverse to the correct expression, b) the statement was in a location where the expression would always evaluate to the same result.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12935 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added another short cut to BMC+kInduction for cases where invariant generation itself succeeds at proving safety.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12937 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Replaced a sysout by a logging statement.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12938 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed some unnecessary spaces from a string.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12939 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Update documentation about repositories.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12942 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New logo for CPAchecker on Google App Engine
that looks more friendly and cloudy.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12943 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
removed global state from transfer relation

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12944 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Simplified the handling of assume edges.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12945 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Removed a rather imprecise restriction from the assume edge successor computation that was used to ensure termination but is no longer required. 

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12947 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Improved the PushAssumptionToEnvironmentVisitor to also use the new immutable NonRecursiveEnvironment by adding a Builder for NonRecursiveEnvironments to allow for adding a more precise special case handling for extracting environment information from equality formulas.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12948 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug found by FindBugs where a comparison compared an object with itself instead of comparing it with the correct other object.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12949 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed a ToDo that is no longer relevant.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12950 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added modifier for consistency.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12952 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
merge from trunk. compilable, not tested

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