From c5b1ac3532958eed2288e17860171d5e0eb46ee3 Mon Sep 17 00:00:00 2001 From: Ardis Lu Date: Fri, 26 Jul 2024 20:50:59 -0700 Subject: [PATCH] Fix showProvedSafe flag and JSON key name Extend title underline --- docs/smtchecker.rst | 4 ++-- docs/using-the-compiler.rst | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) 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`.