@@ -931,7 +931,6 @@ void cbmc_parse_optionst::help()
931
931
" --show-parse-tree show parse tree\n "
932
932
" --show-symbol-table show loaded symbol table\n "
933
933
HELP_SHOW_GOTO_FUNCTIONS
934
- " --drop-unused-functions drop functions trivially unreachable from main function\n " // NOLINT(*)
935
934
" \n "
936
935
" Program instrumentation options:\n "
937
936
HELP_GOTO_CHECK
@@ -942,6 +941,7 @@ void cbmc_parse_optionst::help()
942
941
" --mm MM memory consistency model for concurrent programs\n " // NOLINT(*)
943
942
HELP_REACHABILITY_SLICER
944
943
" --full-slice run full slicer (experimental)\n " // NOLINT(*)
944
+ " --drop-unused-functions drop functions trivially unreachable from main function\n " // NOLINT(*)
945
945
" \n "
946
946
" Semantic transformations:\n "
947
947
// NOLINTNEXTLINE(whitespace/line_length)
@@ -955,7 +955,6 @@ void cbmc_parse_optionst::help()
955
955
" --dimacs generate CNF in DIMACS format\n "
956
956
" --beautify beautify the counterexample (greedy heuristic)\n " // NOLINT(*)
957
957
" --localize-faults localize faults (experimental)\n "
958
- " --smt1 use default SMT1 solver (obsolete)\n "
959
958
" --smt2 use default SMT2 solver (Z3)\n "
960
959
" --boolector use Boolector\n "
961
960
" --mathsat use MathSAT\n "
@@ -966,7 +965,7 @@ void cbmc_parse_optionst::help()
966
965
" --refine-strings use string refinement (experimental)\n "
967
966
" --string-printable add constraint that strings are printable (experimental)\n " // NOLINT(*)
968
967
" --string-max-input-length add constraint on the length of input strings\n " // NOLINT(*)
969
- " --string-max-length add constraint on the length of strings"
968
+ " --string-max-length add constraint on the length of strings\n "
970
969
" (deprecated: use string-max-input-length instead)\n " // NOLINT(*)
971
970
" --outfile filename output formula to given file\n "
972
971
" --arrays-uf-never never turn arrays into uninterpreted functions\n " // NOLINT(*)
0 commit comments