Merge pull request #15304 from ardislu/fix-show-proved-safe

Docs: Fix showProvedSafe flag and JSON key name
ethereum · Aug 28, 2024 · 9e8369f · 9e8369f
2 parents d5cdf07 + c5b1ac3
commit 9e8369f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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`.