Constrained REwriting Sortware Tool version 0.8.3.0 for analyzing LCTRSs.

Usage: crest-sn FILEPATH [-t|--timeout TIMEOUT] [-j|--threads THREADS] [--sccs] 
                [-v|--verb] [--debug] [--result] [--z3] [--cvc5] [--yices] 
                [-m|--methods [Int]]

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

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
  -m,--methods [Int]       Specify an integer list of methods (if not set, all
                           are used): 1 = DP graph with no SCCs 2 = Constrained
                           Reduction Order, 3 = Value Criterion, 4 = Constrained
                           Reduction Order on DP problem, 5 = Reduction Pair
                           (using RPO, Value Criterion and Polynomial
                           Interpretations)