/usr/bin/goto-synthesizer

* *    Goto-synthesizer 6.11.0 (cbmc-6.11.0-dirty) 64-bit   * *
* *                    Copyright (C) 2022                   * *
* *                       Qinheping Hu                      * *
* *                     qinhh@amazon.com                    * *

Usage:                       Purpose:

 goto-synthesizer [-?] [-h] [--help]  show this help
 goto-synthesizer --version   show version and exit
 goto-synthesizer in out      synthesize and apply loop invariants.

Main options:
 --dump-loop-contracts         dump synthesized loop contracts as JSON
 --json-output <file>          specify the output destination of the dumped loop contracts
 --loop-contracts-no-unwind   do not unwind transformed loops

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
 --no-sat-preprocessor        disable the SAT solver's simplifier
 --dimacs                     generate CNF in DIMACS format
 --beautify                   beautify the counterexample (greedy heuristic)
 --smt1                       use default SMT1 solver (obsolete)
 --smt2                       use default SMT2 solver (Z3)
 --bitwuzla                   use Bitwuzla
 --boolector                  use Boolector
 --cprover-smt2               use CPROVER SMT2 solver
 --cvc5                       use CVC5
 --mathsat                    use MathSAT
 --yices                      use Yices
 --z3                         use Z3
 --fpa                        use theory of floating-point arithmetic
 --external-smt2-solver cmd   command to invoke SMT2 solver (combine with one
                              of the solver choices for solver-specific
                              constraints)
 --refine                     use refinement procedure (experimental)
 --refine-arrays              use refinement for arrays only
 --refine-arithmetic          refinement of arithmetic expressions only
 --max-node-refinement        maximum refinement iterations for arithmetic
                              expressions
 --incremental-smt2-solver cmd  command to invoke external SMT solver for
                              incremental solving (experimental)
 --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

 --arrays-uf-never            never turn arrays into uninterpreted functions
 --arrays-uf-always           always turn arrays into uninterpreted functions

Other options:
 --xml-ui                     use XML-formatted output
 --json-ui                    use JSON-formatted output
 --verbosity #                verbosity level