Fixed a bug in BMC-induction where an unsound SAFE result was reported when the target location was syntactically unreachable from the loop head.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12972 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a synchronization issue in BMC+induction.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12973 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug in the single loop transformation introduced by a recent change: The initial subgraph actually must be syntactically reachable from the loop head, otherwise there might be multiple loop entry edges, which is not supported by the LoopstackCPA.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12975 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed the hack introduced in revision r12132, because it has successfully been replaced with the additional loop invariant guessing introduced in revision r12894.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12976 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
update benchmark, now only contain one run for each partial certificate evaluation, considering strategy with smallest certificate which can successfully be verified

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12977 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
benchmark for parallel validation of certification, total and partial certificate

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12978 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: When determining syntactically reachable target locations, it should be okay to skip recursion.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12980 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Some refactoring on the BMC/k-induction algorithm.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12981 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Output message if -heap is not specified
asking for more RAM.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12982 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding new parameter 'rlimits' for tool-cmdline. It can/will be used to set limits for the tool directly in the cmdline. also see #156 .

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12983 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
if no explicit time-limit is given for a CPAchecker-benchmark, use the soft-time-limit from the benchmark-xml.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12984 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
added new method to obtain shortest CEX-prefix

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12988 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
added a few methods to alter the ARG reached set

some methods might introduce unsoundness to the analysis - those cases are well documented

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12990 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
another merge (this time with latest trunk)

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