Removed unused method for creating bitvector and floating-point literals out of a string.
The string was parsed by the solver and thus was solver-specific
and undocumented.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14517 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Do not use String/BigInteger for trivial cases of passing values to the
SMT solver.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14518 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix some warnings of Eclipse and FindBugs.
Some were actual bugs, some were trivial warnings obscuring the important ones.


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


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14520 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Cleanup:
- remove empty directories
- remove exectuable bit from text files
- set correct svn:eol-style property


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14521 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Set exit code of CPAchecker to "1" if invalid command-line arguments are given.
Also change handling of error messages and exit code to always use System.err and a consistent exit code.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14522 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove calls to System.out.print, System.err.print,
and Throwable.printStackTrace (which also uses System.err).
These methods are forbidden in CPAchecker,
because CPAchecker also needs to run in environments
where these methods are not usable
(for example, in unit tests, as Eclipse plugin,
or in the Google App Engine).

Please always use correct logging instead.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14523 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Enable deprecation warnings for builds with javac


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14524 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Copy some fixes to our benchmark scripts from the VerifierCloud repository:
reliable killing of processes, ignore binary stuff in tool output.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14525 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed tracking of addressed (composite) fields

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14526 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add methods for creating literals from doubles and BigIntegers
to NumeralFormulaManager.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14527 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix passing of BigDecimal strings to the SMT solver:
only plain string is supported, not the default string with scientific
notation.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14528 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add an option inside the SMT solver package
to approximate floating-point numbers with rationals,
similar to how we can approximate bitvectors with integers.
The advantage of this is that even in case we do not want to use real
floating-point arithmetic, the calling code can still keep using the
same interfaces and methods,
and it is transparently replaced.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14529 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Change the default values and standard configuration files
to use the new option of replacing floats with rationals,
instead of disabling floats completely if we do not want to use them.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14530 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove the old way of completely disabling the use of floats.
The CtoFormulaConverter now always uses floats,
if the solver does not support them or we do not want them
they are transparently replaced with rationals.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14531 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add test cases with floats to the integration tests for predicate
analysis.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14532 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Webclient mode of benchmark.py:
- support "-skipRecursion"
- support new log file name in the result zip file
- fix handling of energy values

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14533 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
remove assertion that otherwise might be violated in case of repeated counterexamples

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14534 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added code for implementing the paper Counterexample-guided Precondition Inference

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14536 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Array Theory; implementations for Z3 and MathSAT5.

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