diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst
index fc7978256a9d..92aaa847c921 100644
--- a/docs/smtchecker.rst
+++ b/docs/smtchecker.rst
@@ -488,8 +488,8 @@ Proved Targets
 
 If there are any proved targets, the SMTChecker issues one warning per engine stating
 how many targets were proved. If the user wishes to see all the specific
-proved targets, the CLI option ``--model-checker-show-proved`` and
-the JSON option ``settings.modelChecker.showProved = true`` can be used.
+proved targets, the CLI option ``--model-checker-show-proved-safe`` and
+the JSON option ``settings.modelChecker.showProvedSafe = true`` can be used.
 
 Unproved Targets
 ================
diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst
index 97994e1326ff..004bb4a6141d 100644
--- a/docs/using-the-compiler.rst
+++ b/docs/using-the-compiler.rst
@@ -481,7 +481,7 @@ Input Description
           // Choose which types of invariants should be reported to the user: contract, reentrancy.
           "invariants": ["contract", "reentrancy"],
           // Choose whether to output all proved targets. The default is `false`.
-          "showProved": true,
+          "showProvedSafe": true,
           // Choose whether to output all unproved targets. The default is `false`.
           "showUnproved": true,
           // Choose whether to output all unsupported language features. The default is `false`.