Prevent illegal characters in variable names for SMT formulas.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14734 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Use SMTInterpol as default solver.
It is the only one that is available in all situations
because it its purely Java.
It also supports rationals+integers and is competitive with MathSAT5,
for interpolation with integers it is even better than MathSAT5.
For -predicateAnalysis-bitprecise and for BMC configurations
MathSAT5 is still used because these configurations require
features that are not supported by SMTInterpol.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14735 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Change the default in PredicateCPA from approximating bitvectors
with rationals to approximating bitvectors with integers.
This makes much more sense of course.
Floating-point variables are still approximated with rationals.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14736 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fix some unit tests that unexpectedly failed when enabling integers
in predicate analysis

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14737 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Enable counterexample checks with the value analysis (which is bit-precise)
for the default configuration of predicate analysis and BMC.
This helps to reduce the number of false alarms,
and has very little overhead (5% in our benchmarks).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14739 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add test set for -ldv config.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14740 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
update NEWS,
remove ChangeLog which has not been used for years

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14741 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add @SuppressWarnings to unfinished unit tests
so that the irrelevant warnings there
do not hide important warnings.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14742 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
remove awkward 'delta' from ValueAnalysisState, along with all references; as of now, it does not really have a benefit anymore, as the speed-up is no longer relevant to justify this level of awkwardness

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14745 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
bugfix: only get variable name from variable declarations, and not also from function declaration (which resulted in cast exception)

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14746 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add an accept method for visitory to AExpression
to allow visitors that can handle expressions of all languages.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14747 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Improve the output of the toDotLabel function in LiveVariablesState. Instead of ASimpleDeclarations we now use the qualified names.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14748 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Improve the handling of PointerExpressions, instead of assuming such variables are always live, they should now be only live if they are read.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14749 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Use function-wise live variables collection as fall-back for global collection in cases the global analysis could not be finished (e.g. in programs with recursion).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14750 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
remove the ComponentAwarePrecisionAdjustment operator that was needed before extending the PrecisionAdjustment interface (in commit #14571); now, the abstraction computations of the value analysis are all done in the ValueAnalysisPrecisionAdjustment operator

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14751 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Rationals library: minor clean-up.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14752 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixes subtraction for linear expressions.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14753 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Policy iteration: generate octagon templates.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14754 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix web client mode of benchmark.py.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14756 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove invalid assert from LiveVariablesTransferRelation.

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