goto-synthesizer - Man Page

Synthesize and apply loop contracts of goto binaries.


goto-synthesizer [-?] [-h] [--help]

show help

goto-synthesizer --version

show version and exit

goto-synthesizer [options] in [out]

perform synthesis and loop-contracts transformation


goto-synthesis reads a GOTO binary, performs loop-contracts synthesis and program transformation for the synthesized contracts, and then writes the resulting program as GOTO binary on disk.



do not unwind transformed loops after applying the synthesized loop contracts


dump the synthesized loop contracts as JSON

--json-output file

specify the output destination of the loop-contracts JSON

Accepts all of cbmc's options plus the following backend options

--object-bits n

number of bits used for object addresses

--sat-solver solver

use specified SAT solver

--external-sat-solver cmd

command to invoke SAT solver process


disable the SAT solver's simplifier


generate CNF in DIMACS format


beautify the counterexample (greedy heuristic)


use default SMT1 solver (obsolete)


use default SMT2 solver (Z3)


use Bitwuzla


use Boolector


use CPROVER SMT2 solver


use CVC3


use CVC4


use CVC5


use MathSAT


use Yices


use Z3


use theory of floating-point arithmetic


use refinement procedure (experimental)


use refinement for arrays only


refinement of arithmetic expressions only


maximum refinement iterations for arithmetic expressions

--incremental-smt2-solver cmd

Use the incremental SMT backend where cmd is the command to invoke the SMT solver of choice.
Example invocations:
 --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
 --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver).

Note that:
The solver name must be in the "PATH" or be an executable with full path.
The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
The SMT solver should support the QF_AUFBV logic.

--outfile filename

output formula to given file

--dump-smt-formula filename

output smt incremental formula to the given file

--write-solver-stats-to json-file

collect the solver query complexity


never turn arrays into uninterpreted functions


always turn arrays into uninterpreted functions

User-interface options


use XML-formatted output


use JSON-formatted output

--verbosity n

verbosity level


All tools honor the TMPDIR environment variable when generating temporary files and directories.


If you encounter a problem please create an issue at

See Also

cbmc(1), goto-cc(1) goto-instrument(1)


December 2022 goto-synthesizer-5.59.0