Constrained REwriting Sortware Tool version 0.8.8.1 for analyzing LCTRSs. Usage: crest-sn-benchmark BENCHMARKPATH [-t|--timeout TIMEOUT] [-j|--threads THREADS] [--z3] [--cvc5] [--yices] [-s|--strategy STRING] [--html] (Non-)Termination analysis benchmarking executable of the Constrained REwriting Sortware Tool version 0.8.8.1. Searches for files with ".ari" file extension in the given directory. Available options: -h,--help Show this help text BENCHMARKPATH Path to directory containing benchmarks -t,--timeout TIMEOUT Timeout of the analysis -j,--threads THREADS Number of threads for the analysis --z3 Use Z3 (default) --cvc5 Use CVC5 --yices Use Yices -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]'} --html Print proofs to files and produce a "crest-sn-benchmark.html".