Reference for .sby file format
==============================

A ``.sby`` file consists of sections. Each section start with a single-line
section header in square brackets. The order of sections in a ``.sby`` file
is irrelevant, but by convention the usual order is ``[options]``,
``[engines]``, ``[script]``, and ``[files]``.

Options section
---------------

The ``[options]`` section contains lines with key-value pairs. The ``mode``
option is mandatory. The possible values for the ``mode`` option are:

========= ===========
Mode      Description
========= ===========
``bmc``   Bounded model check to verify safety properties (assert() statements)
``prove`` Unbounded model check to verify safety properties (assert() statements)
``cover`` Generate set of shortest trace required to reach all cover() statements
========= ===========

All other options have default values and thus are optional. The available
options are:

+-------------+-----------+---------------------------------------------------------+
|   Option    |   Modes   | Description                                             |
+=============+===========+=========================================================+
| ``expect``  |   All     | Expected result as comma-separated list of the tokens   |
|             |           | ``pass``, ``fail``, ``unknown``, ``error``, and         |
|             |           | ``timeout``. Unexpected results yield a nonzero return  |
|             |           | code . Default: ``pass``                                |
+-------------+-----------+---------------------------------------------------------+
| ``timeout`` |   All     | Timeout in seconds. Default: ``none`` (i.e. no timeout) |
+-------------+-----------+---------------------------------------------------------+
| ``depth``   | ``bmc``,  | Depth of the bounded model check. Only the specified    |
|             | ``cover`` | number of cycles are considered. Default: ``20``        |
|             +-----------+---------------------------------------------------------+
|             | ``prove`` | Depth for the k-induction performed by the ``smtbmc``   |
|             |           | engine. Other engines ignore this option in ``prove``   |
|             |           | mode. Default: ``20``                                   |
+-------------+-----------+---------------------------------------------------------+

Engines section
---------------

TBD

Script section
--------------

TBD

Files section
-------------

TBD