Document some configuration options.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13311 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
BMC+kInduction: Fixed a bug where the option for using esbmc's unsound havocing heuristic was not always applied.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13314 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
bugfixes for Rationals with Z3.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13315 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
The benchmark script truncates log files that are too large (> 20 MB).
This was not working reliably and is now fixed.

The problem was that the whole file was read into memory
before attempting its truncation.
This failed on very large log files (with several GB) due to an OutOfMemoryError,
with the result that the file was kept unchanged.
This led to problems with the VerifierCloud,
which then had to handle the large file.

Now the file is truncated without being read into memory.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13318 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
WpCPA: A first version of the merge operator.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13319 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
BMC+kInduction: Unsound havocing heuristic was now also havocs variables from value analysis states.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13320 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Support for backwards SSAs (not yet for the pointer aliasing implementation)



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13321 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added a backwards version of PredicateCPA.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13322 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed "implies" implementation for path formulas; this was only an intermediate prototype.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13323 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed the information on the origin of disjuncted path formulas.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13324 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
BMC+kInduction: Improved the unsound havocing heuristic: Assertions now also count as loop termination edges.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13325 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Split build.xml into several files.
All the included files can be reused between SoSy-Lab Common,
CPAchecker, and VerifierCloud.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13327 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix build for AppEngine.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13329 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Don't exclude *Test classes from JAR file,
we have real files matching this name.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13330 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Workaround incompatible behavior of ant 1.8 and ant 1.9
that use different prefixes for transitively imported targets.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13331 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Skeleton of a precondition writer.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13332 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add constructor for parameters String, Throwable to CFAGenerationRuntimeException


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13333 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add assertion to JVariableRunTimeType to check that the given
identifier is of a valid type.



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