Changes from CPAchecker 1.1 to CPAchecker 1.2
---------------------------------------------

CPAchecker now supports several new analyses:

* CEGAR for ExplicitCPA (as submitted to SV-COMP'13)
  (c.f. "Explicit-State Software Model Checking Based on CEGAR and Interpolation", FASE'13)
  This can be enabled with the "explicitAnalysis" and "explicitAnalysis-ItpRefiner*" configurations
  (explicitAnalysis-ItpRefiner-ABElf is recommended)

* Conditional Model Checking (CMC)
  (c.f. "Conditional Model Checking: A Technique to Pass Information between Verifiers", FSE'12)
  To use two or more CMC-enabled configurations, use the "-cmc" command-line argument:
  Example: -cmc explicitAnalysis-100s-generate-cmc-condition -cmc predicateAnalysis-use-cmc-condition

* Sequential composition of analyses (as submitted to SV-COMP'13)
  The "-cmc" command-line argument can be used for this, too.
  Example: -cmc explicitAnalysis-100s -cmc predicateAnalysis

* Predicate-based analysis using the Impact refinement strategy
  (c.f. "Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT", FMCAD'12)
  This can be enabled with the "predicateAnalysis-ImpactRefiner-*" configurations.

* BDD-based analysis tracking a subset of variables,
  with ExplicitCPA tracking the remaining variables.
  This can be enabled with the "explicit-BDD-*" configurations.

Other changes to CPAchecker:
* Pre-processing of C files with CIL is no longer needed.
* MathSAT5 is now used as as SMT solver by default.
  MathSAT4 can still be selected by setting the option
  cpa.predicate.solver=Mathsat4
* In configuration files, #include directives can be used
  to include other configuration files.
* The file format of the file with the initial set of predicates
  (option cpa.predicate.abstraction.initialPredicates) and
  the final set of predicates (option cpa.predicate.predmap.file) was changed.
  It is now the same format for both files, and based on the SMTlib2 format.
  See doc/examples/predmap.txt for an example.
* The option cpa.predicate.machineModel was renamed to analysis.machineModel.
* The Cudd BDD library was removed, now JavaBDD's implementation is used by default
  (it has similar performance, but more features).
* The ARTCPA was renamed to ARGCPA.
  Replace cpa.art with cpa.arg and ARTCPA with ARGCPA in existing configuration files.
* The option analysis.traversal.useTopsort (used in most configuration files)
  was renamed to analysis.traversal.useReversePostorder as this name is more precise.
* SMTInterpol, an SMT solver written in Java, is now integrated into CPAchecker.
  With this solver, predicate analysis works on all platforms.
  Some configuration options were renamed in order to not be MathSAT-specific.
* The log level for the console can now be adjusted during runtime.
  Use a JMX client to do that, e.g., jconsole or VisualVM.
  Connect to the CPAchecker process,
  locate the MXBean "org.sosy_lab.common:type=LogManager",
  and set the attribute.
* The option "cpa.removeIrrelevantForErrorLocations" was renamed to
  "cfa.removeIrrelevantForSpecification", as this name is more appropriate.
* A time limit of 15 minutes is now enabled by default in most configurations.
  If the analysis is not yet finished, CPAchecker will stop after this time and report UNKNOWN.
  The time limit can be controlled with the "cpa.conditions.global.time.wall" option
  and the "-timelimit" command-line argument.
  Example:
  scripts/cpa.sh -predicateAnalysis -timelimit 1min test.c
* If the #include directive of specification automata is used with relative paths,
  the base directory of the relative path is now the directory of the file which contains the #include,
  not the CPAchecker root directory.
  If #include is used with relative paths in a specification file, it most probably needs adjustment.