Changes from CPAchecker 1.6.1 to CPAchecker 1.7
-----------------------------------------------
* CPAchecker requires Java 8.

* New Default Configuration '-default'
  This configuration should work reasonably well across a large range
  of programs and properties and is recommended in general,
  unless a more specific configuration for a certain use case exists
  (for example, for SV-COMP tasks the configuration '-svcomp18'
  is better suited).

* New Command-Line Parameter '-benchmark'
  This parameter should always be used when running CPAchecker for
  (performance) benchmarking.
  For example, it disables internal assertions and output files
  for improved performance (cf. doc/Benchmark.md).

* Termination Analysis
  An analysis that supports termination properties
  and is based on finding lassos has been added to CPAchecker.

* Overflow Analysis
  An analysis that supports finding overflows
  and is based on predicate abstraction has been added to CPAchecker.

* Improved Precision of Predicate Analysis
  The predicate analysis now uses an improved encoding of program semantics
  that is more precise for bitvector operations, overflows, and pointers.
  The default SMT solver is now MathSAT5, for which only a Linux binary is bundled.
  Additional binaries are available from the MathSAT homepage: http://mathsat.fbk.eu/
  Please note that the bundled license of MathSAT permits
  only research and evaluation purposes.

* Improved HTML Report
  The HTML report with verification results that is generated by CPAchecker
  has been updated and is now produced directly by CPAchecker
  (no need to call report-generator.py anymore).

* Improved Witness Validation
  The witness validator has been updated and now supports the validation of
  violation witnesses for concurrent programs.