Update help message for engines

usi-verification-and-security · Sep 3, 2024 · 7f01167 · 7f01167
1 parent 69c6c65
commit 7f01167
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/src/Options.cc b/src/Options.cc
@@ -35,15 +35,15 @@ void printUsage() {
         "--version                  Print version number of Golem\n"
         "-l,--logic <name>          SMT-LIB logic to use (required); possible values: QF_LRA, QF_LIA\n"
         "-e,--engine <name>         Select engine to use; supported engines:\n"
-        "                               bmc - Bounded Model Checking (only transition systems)\n"
-        "                               imc - McMillan's original Interpolation-based model checking (only transition systems)\n"
+        "                               bmc - Bounded Model Checking (only linear systems)\n"
+        "                               imc - McMillan's original Interpolation-based model checking (only linear systems)\n"
         "                               kind - basic k-induction algorithm (only transition systems)\n"
-        "                               lawi - Lazy Abstraction with Interpolants (only linear CHC systems)\n"
-        "                               pa - basic predicate abstraction (any CHC system)\n"
-        "                               pdkind - Property directed k-induction\n"
-        "                               spacer - custom implementation of Spacer (any CHC system)\n"
-        "                               split-tpa - Split Transition Power Abstraction (only transition systems)\n"
-        "                               tpa - Transition Power Abstraction (only transition systems)\n"
+        "                               lawi - Lazy Abstraction with Interpolants (only linear systems)\n"
+        "                               pa - basic predicate abstraction with CEGAR (any system)\n"
+        "                               pdkind - Property directed k-induction (only linear systems)\n"
+        "                               spacer - custom implementation of Spacer (any system)\n"
+        "                               split-tpa - Split Transition Power Abstraction (only linear systems)\n"
+        "                               tpa - Transition Power Abstraction (only linear systems)\n"
         "--validate                 Internally validate computed solution\n"
         "--print-witness            Print computed solution\n"
         "--proof-format <name>      Proof format to use; supported formats:\n"