diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index ac670796907..75988d1eab0 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -1070,8 +1070,9 @@ void jbmc_parse_optionst::help()
     HELP_SHOW_PROPERTIES
     " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n" // NOLINT(*)
     " --property id                only check one specific property\n"
-    " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)
+    " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
+    "                              (implies --trace)\n"
     HELP_JAVA_TRACE_VALIDATION
     "\n"
     "Program representations:\n"
diff --git a/src/cbmc/README.md b/src/cbmc/README.md
index 32fccb387f2..f3d54afc6f6 100644
--- a/src/cbmc/README.md
+++ b/src/cbmc/README.md
@@ -48,7 +48,8 @@ formula using two different possible procedures:
 
 1. When `--stop-on-fail` is passed on the command-line, the formula is solved
    once to find any violated assertion. This is implemented directly in
-   class `bmct`.
+   class `bmct`. If the formula is satisfiable, a counter-example trace is
+   generated.
 2. When `--stop-on-fail` is not passed, BMC is run in "all-properties" mode.
    This categorises the assertions into groups that represent the same property,
    and the solver is run repeatedly to try to satisfy each property at least
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index cf1c034c6a2..3978733a5ec 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -1064,8 +1064,9 @@ void cbmc_parse_optionst::help()
     HELP_SHOW_PROPERTIES
     " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n" // NOLINT(*)
     " --property id                only check one specific property\n"
-    " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)
+    " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
+    "                              (implies --trace)\n"
     "\n"
     "C/C++ frontend options:\n"
     " -I path                      set include path (C/C++)\n"