Constrained REwriting Sortware Tool version 0.8.8.1 for analyzing LCTRSs.

Usage: crest-sn FILEPATH [-t|--timeout TIMEOUT] [-j|--threads THREADS] [--sccs] 
                [-v|--verb] [--debug] [--result] [--z3] [--cvc5] [--yices] 
                [-s|--strategy STRING]

  (Non-)Termination analysis executable of the Constrained REwriting Sortware
  Tool version 0.8.8.1.

Available options:
  -h,--help                Show this help text
  FILEPATH                 Path to the source file
  -t,--timeout TIMEOUT     Timeout of the analysis
  -j,--threads THREADS     Number of Threads for the analysis
  --sccs                   Print the strongly connected components of the
                           Dependency Graph
  -v,--verb                Get more verbose output
  --debug                  Debug mode which shows also internal errors
  --result                 Suppress any output except result and time
  --z3                     Use Z3 as SMT solver (default)
  --cvc5                   Use CVC5 as SMT solver
  --yices                  Use Yices as SMT solver
  -s,--strategy STRING     Specify a comma-separated list of methods (if not
                           set, all are used): {'dpg' = DP graph with no SCCs
                           'crodp' = Constrained Reduction Order on DP problem
                           'cro' = Constrained Reduction Order 'vc' = Value
                           Criterion 'vclin' = Value Criterion with linear
                           combination projection 'sc' = Subterm Criterion 'mis'
                           = Matrix Interpretations given a dimension, e.g. 'mis
                           2' and optional upper bound for entries, e.g. 'misp 2
                           4' for naturals with less or equal than 4 bits.
                           'misdp' = Matrix Interpretations on DP problem given
                           a dimension, e.g. 'misdp 2' and optional upper bound
                           for entries, e.g. 'misdp 2 4' for naturals with less
                           or equal than 4 bits. 'misbv' = Matrix
                           Interpretations given a dimension and number of bits
                           used in bit vector arithmetic; e.g. 'misbv 2 4' for
                           dimension 2 with 4 bits. 'misbvdp' = Matrix
                           Interpretations on DP problem given a dimension and
                           number of bits used in bit vector arithmetic; e.g.
                           'misbv 2 4' for dimension 2 with 4 bits. 'miscons' =
                           Matrix Interpretations given a dimension; e.g.
                           'miscons 2' for dimension 2. 'misconsdp' = Matrix
                           Interpretations on DP problem given a dimension; e.g.
                           'misconsdp 2' for dimension 2. 'rpair' = Reduction
                           Pair (using some of 'cro', 'vc', 'sc', 'vclin', 'mis
                           DIM ?BITS', 'misbv DIM BITS', 'miscons DIM'); e.g.:
                           'rpair[cro,vclin, misbv 3 15]'}