@@ -931,7 +931,6 @@ void cbmc_parse_optionst::help()
931931 " --show-parse-tree show parse tree\n "
932932 " --show-symbol-table show loaded symbol table\n "
933933 HELP_SHOW_GOTO_FUNCTIONS
934- " --drop-unused-functions drop functions trivially unreachable from main function\n " // NOLINT(*)
935934 " \n "
936935 " Program instrumentation options:\n "
937936 HELP_GOTO_CHECK
@@ -942,6 +941,7 @@ void cbmc_parse_optionst::help()
942941 " --mm MM memory consistency model for concurrent programs\n " // NOLINT(*)
943942 HELP_REACHABILITY_SLICER
944943 " --full-slice run full slicer (experimental)\n " // NOLINT(*)
944+ " --drop-unused-functions drop functions trivially unreachable from main function\n " // NOLINT(*)
945945 " \n "
946946 " Semantic transformations:\n "
947947 // NOLINTNEXTLINE(whitespace/line_length)
@@ -955,7 +955,6 @@ void cbmc_parse_optionst::help()
955955 " --dimacs generate CNF in DIMACS format\n "
956956 " --beautify beautify the counterexample (greedy heuristic)\n " // NOLINT(*)
957957 " --localize-faults localize faults (experimental)\n "
958- " --smt1 use default SMT1 solver (obsolete)\n "
959958 " --smt2 use default SMT2 solver (Z3)\n "
960959 " --boolector use Boolector\n "
961960 " --mathsat use MathSAT\n "
@@ -966,7 +965,7 @@ void cbmc_parse_optionst::help()
966965 " --refine-strings use string refinement (experimental)\n "
967966 " --string-printable add constraint that strings are printable (experimental)\n " // NOLINT(*)
968967 " --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 "
970969 " (deprecated: use string-max-input-length instead)\n " // NOLINT(*)
971970 " --outfile filename output formula to given file\n "
972971 " --arrays-uf-never never turn arrays into uninterpreted functions\n " // NOLINT(*)
0 commit comments