This changes the behavior of almost all configurations with a predicate
analysis, except for:
- kinduction-kfInvariants (ki->ki->ai),
  which requires a re-entrant SMT solver, which MathSAT is not
- ldv and ldv-bam, for which this should be evaluated separately
- policy iteration, which fails with this encoding (cf. #365)
- termination analysis, which relies on SMTInterpol
  and only supports linear arithmetic
- old SV-COMP configs, where we want to keep the existing behavior

Configurations with "bitprecise" in their name were renamed
to remove this word (or merged with an existing configuration with the
same name).
For predicate abstraction and k-induction, new configurations
with "linear" in the name wered added, which use the previous
linear approximation of program semantics
(these configurations can be used if for example using MathSAT is not an
option).

For k-induction, the default configuration (-kInduction)
is now a bitprecise configuration with only data-flow invariants (ki->ai),
and not the ki->ki->ai configuration that only supports linear arithmetic.

Counterexample checks were disabled for most of the affected
configurations (we did not enable counterexample checks for
-predicateAnalysis-bitprecise previously, too).
The new "linear" configurations enable counterexample checks
with the value analysis like the standard configurations did previously.

The integration test sets were adjusted such that
integration-predicateAnalysis keeps testing the linear configuration
and integration-predicateAnalysis-bitprecise keeps testing the
bitprecise configuration like previously.
All other test sets use the respective default (bitprecise) configurations.

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