Command-line interface#

BLACK’s main interface to the user is the command-line tool black. Here we document its usage. For the input syntax accepted by the tool, look at the Input syntax page.


The main purpose of black is to tell you whether a given temporal logic formula (see Supported logics) is satisfiable. Let’s suppose you have written such a formula in the file spec.pltl:

$ cat spec.pltl
!p & X !p & F p

Then, asking black about this formula is as easy as:

$ black solve spec.pltl

black replies SAT on the standard output, so the formula is satisfiable. Let us try an unsatisfiable formula:

$ cat unsat-spec.pltl
G((p & q) & c) & F((w & r) & !c)

$ black solve unsat-spec.pltl

If the filename is -, black reads from the standard input:

$ cat spec.pltl | black solve -

$ cat unsat-spec.pltl | black solve -

This is useful when the formulas are generated by other programs.

Alternatively, we may give the formulas on the command line with the -f option:

$ black solve -f '!p & X !p & F p'

$ black solve -f 'G((p & q) & c) & F((w & r) & !c)'


Formulas usually contain spaces so they have to be quoted. Moreover, they usually contain many symbols which have special meaning for the shell, therefore it is recommended to use single quotes ('like this') rather than double quotes ("not this") to tell the shell to not interpret the quoted contents.

Satisfiable formulas can correspond e.g., to bugged specifications or planning problems that admit a solution plan. In these cases, one may want to obtain the counter-example showing the bug or the solution plan to the planning problem. To do this, we can ask black to print the model of a satisfiable formula with the -m option:

$ black solve -m -f '!p & X !p & F p'
- t = 0: {¬p}
- t = 1: {¬p}
- t = 2: {p} ⬅︎ loops here

By default, black solves formulas with the infinite trace semantics (see Supported logics). So here it is telling us that the model of the formula starts with two states at t=0 and t=1 where p does not hold, followed by a state where p holds, and then the model infinitely loops through this last state. LTL models always loop in this way.

If, instead, we want to interpret the formula over finite traces, we can tell so to black by passing the --finite option:

$ black solve --finite -m -f '!p & X !p & F p'
Finite model:
- t = 0: {¬p}
- t = 1: {¬p}
- t = 2: {p}

Note that the model does not loop anymore, but ends at t=2.

Complex specifications may have huge and complex models, and we probably want to process the output model with other scripts or programs. In this case, we need black to print the model in a more easily parsable format. The -o option lets us choose the output format. Currently supported formats are readable (the default, that we saw above), or json:

$ black solve -o json -m -f '!p & X !p & F p'
   "result": "SAT",
   "k": 1,
   "model": {
      "size": 3,
      "loop": 2,
      "states": [
            "p": "false"
            "p": "false"
            "p": "true"


If you need to parse black’s output from shell scripts or from the command line, consider using the json output format and the jq command-line JSON manipulation tool.

BLACK supports many backends. The list of available backends can be retrieved with the --sat-backends option:

$ black --sat-backends

BLACK - Bounded Lᴛʟ sAtisfiability ChecKer
     version 0.10.1

Available SAT backends:
- z3 *
- cmsat
- cvc5
- mathsat
- minisat

The one marked with * is the default used when no explicit choice is made. To choose the backend, use the -B option:

$ black solve -B cvc5 -f '!p & X !p & F p'

Note that not all backends support the same features. In particular, first-order formulas are only supported with SMT solver backends (z3, cvc5 and mathsat), and only z3 and cvc5 support quantified first-order formulas.

Now, let’s consider again the unsatisfiable formula above. Why is it unsatisfiable? black can help us answer this question by finding a minimum unsatisfiable core (MUC). This can be done by passing the -c option:

$ black solve -c -f 'G((p & q) & c) & F((w & r) & !c)'
MUC: G({0} & c) & F({1} & !c)

Let us look at the output. UNSAT is printed because the formula is unsatisfiable. Then, the MUC is shown to be G({0} & c) & F({1} & !c). This is a reduction of the original formulas, where the subformula (p & q) has been replaced by {0} and the subformula (w & r) has been replaced by {1}. Let’s try to give this formula back to black:

$ black solve -f 'G({0} & c) & F({1} & !c)'

The formula is unsatisfiable. Indeed, the MUC is the smallest unsatisfiable formula obtained by replacing some subformulas of the original one with propositional placeholders. It tells us that the replaced subformulas are not involved at all in the unsatisfiability of the formula. In this case, from the MUC it can be seen directly that the formula is unsatisfiable because we require c to always hold and then we require !c to hold eventually.

Until now, we have always given to black propositional formulas. But as you can see in the Supported logics page, black also supports first-order formulas in place of propositional letters (i.e., the LTL\({}_f\)MT logic).

In this logic, we can use variables that take values over certains domains. Since BLACK supports the LIA and LRA theories (possibly combined with EUF), variables can be either integer- or real-valued. When giving a LTL\({}_f\)MT formula as input, we have to choose the domain using the -d option. Accepted values are Int and Real:

$ black solve -d Int -f 'x = y + 2'


The -m option is not (yet) supported for LTL\({}_f\)MT formulas.


The --finite option is implied when solving LTL\({}_f\)MT formulas, since the infinite-trace semantics is not supported for such formulas.

We can refer to the value of a variable at the next state using the strong or the weak next term constructors. For example:

$ black solve -d Int -f 'x = 0 & G(wnext(x) = x + 1) & F(x = 42)'
black: warning: use of `next`/`prev` terms implies the --semi-decision option.
black: warning: execution may not terminate.
black: warning: pass the --semi-decision option explicitly to silence this warning.

As you can see, black warns you about the fact that, by using such terms, the solving procedure may not terminate (in the case of unsatisfiable formulas), hence black turns on implicitly the --semi-decision option which disables the termination checks. To silence the warning, you can pass the option yourself (here we use the -s short option):

$ black solve -s -d Int -f 'x = 0 & G(wnext(x) = x + 1) & F(x = 42)'


You can use the -s option on propositional formulas as well. This may cause black to not terminate on unsatisfiable instances, but can substantially speed up it on satisfiable ones.

Usage reference#


$ black solve [-k <bound>] [-B <backend>] [--remove-past] [--finite] [-m] \
        [-c] [-d <sort>] [-s] [-o <fmt>] [-f <formula>] [--debug <debug>] \

$ black check -t <trace> [-e <result>] [-i <state>] [--finite] [--verbose] \
        [-f <formula>] [<file>]

$ black --sat-backends
$ black -v
$ black -h


black solve mode#

Check the satisfiability of a temporal logic formula.

-k, --bound <bound>#

maximum bound for BMC procedures

-B, --sat-backend <backend>#

select the SAT backend to use


translate LTL+Past formulas into LTL before checking satisfiability


treat formulas as LTLf and look for finite models

-m, --model#

print the model of the formula, if any

-c, --unsat-core#

for unsatisfiable formulas, compute the minimum unsat core

-d, --domain <sort>#

select the domain for first-order variables. Mandatory for first-order formulas.

Accepted domains: Int, Real

-s, --semi-decision#

disable termination checks for unsatisfiable formulas, speeding up the execution for satisfiable ones.

Note: the use of next(x) and similar terms in formulas implies this option.

-o, --output-format <fmt>#

Output format.

Accepted formats: readable, json

Default: readable

-f, --formula <formula>#

LTL formula to solve


input formula file name. If '-', reads from standard input.

black check mode#

Check the correctness of a trace (a model) against a temporal logic formula.

-t, --trace <trace>#

trace file to check against the formula. If ‘-’, reads from standard input.

-e, --expected <result>#

expected result (useful in testing).

-i, --initial-state <state>#

index of the initial state over which to evaluate the formula.

Default: 0


treat formulas as LTLf and expect a finite model


output a verbose log

-f, --formula <formula>#

formula against which to check the trace


formula file against which to check the trace

Other options#


print the list of available SAT backends

-v, --version#

show version and license information

-h, --help#

print this help message