Exit codes

Since version 1.9.0, Kind 2 returns the standard exit code 0 for success, and a non-zero exit code to indicate an error, or an unsuccessful analysis result. To force Kind 2 to use only non-zero exit codes for errors, pass the option --exit_code_mode only_errors. The precise meaning of the exit codes are described in section Code Convention. For information on the old convention, see section Former Convention.

Code Convention

With the default settings, Kind 2 performs a single, monolithic analysis of the main node. If Kind 2 proves all invariant properties valid and all reachability properties reachable, then it returns (exit code) 0. If no properties are disproven, but some properties could not be proven (e.g. due to a timeout), Kind 2 returns 30. When Kind 2 disproves one or more properties, it returns 40.

In modular mode, the properties of all nodes are checked bottom-up. Moreover, when compositional analysis is enabled too, the same node may be analyzed several times with different levels of abstraction (see section Refinement in compositional and modular analyses for details). In this case, Kind 2 returns 40 if one or more properties were disproven in any analysis. It returns 30 if no properties were disproven, but some nodes were not analyzed (e.g. due to a timeout) or some properties could not be proven. It returns 0 if all properties were proven for all nodes in every analysis.

When contracts of imported nodes are checked for realizability, Kind 2 also reports an exit status following a similar convention. If all the contracts are proven realizable, it returns 0. If some contract is proven unrealizable, it returns 40. When no contract is proven unrealizable, but some contract could not be proven realizable, it returns 30.

If Kind 2 detects a general error, it returns 1. When the error is related to an incorrect command-line argument, it returns 2. If Kind 2 detects a parse error, it returns 3. If Kind 2 cannot find an SMT solver on the PATH, it returns 4. When an unknown or unsupported version of an SMT solver is detected, it returns 5.

Former Convention

Version 1.8.0 and earlier were not following the POSIX convention of returning 0 for success. When all properties were proven, Kind 2 returned 20. If some property was disproven, it returned 10. If no properties were disproven, but some result was unknown, it returned 0. Moreover, Kind 2 returned 2 for any error.