GOTO-SYNTHESIZER(1) User Commands GOTO-SYNTHESIZER(1)

goto-synthesizer - Synthesize and apply loop contracts of goto binaries.

show help
show version and exit
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
specify the output destination of the loop-contracts JSON

number of bits used for object addresses
use specified SAT solver
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
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.

output formula to given file
output smt incremental formula to the given file
collect the solver query complexity
never turn arrays into uninterpreted functions
always turn arrays into uninterpreted functions

use XML-formatted output
use JSON-formatted output
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 https://github.com/diffblue/cbmc/issues

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

2022, Qinheping Hu

December 2022 goto-synthesizer-5.59.0