1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

Changes since CPAchecker 1.1
----------------------------
* r6066: The option analysis.traversal.useTopsort (used in most configuration files)
  was renamed to analysis.traversal.useReversePostorder as this name is more precise.
* r6060: 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.
* r5958: The log level for the console can now be adjusted during runtime.
  You need 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.
* r5953: The option "cpa.removeIrrelevantForErrorLocations" was renamed to
  "cfa.removeIrrelevantForSpecification", as this name is more appropriate.
* r5060: 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
* r4960: 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.