Skip to content

Commit 8ce8786

Browse files
author
Leo Alt
committed
Make show unproved CLI a flag
1 parent 74ec3c1 commit 8ce8786

File tree

19 files changed

+9
-72
lines changed

19 files changed

+9
-72
lines changed

docs/smtchecker.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -488,7 +488,7 @@ Unproved Targets
488488

489489
If there are any unproved targets, the SMTChecker issues one warning stating
490490
how many unproved targets there are. If the user wishes to see all the specific
491-
unproved targets, the CLI option ``--model-checker-show-unproved true`` and
491+
unproved targets, the CLI option ``--model-checker-show-unproved`` and
492492
the JSON option ``settings.modelChecker.showUnproved = true`` can be used.
493493

494494
Verified Contracts

solc/CommandLineParser.cpp

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -733,8 +733,7 @@ General Information)").c_str(),
733733
)
734734
(
735735
g_strModelCheckerShowUnproved.c_str(),
736-
po::value<bool>()->value_name("false,true")->default_value(false),
737-
"Select whether to show all unproved targets."
736+
"Show all unproved targets separately."
738737
)
739738
(
740739
g_strModelCheckerSolvers.c_str(),
@@ -1114,10 +1113,7 @@ General Information)").c_str(),
11141113
}
11151114

11161115
if (m_args.count(g_strModelCheckerShowUnproved))
1117-
{
1118-
bool showUnproved = m_args[g_strModelCheckerShowUnproved].as<bool>();
1119-
m_options.modelChecker.settings.showUnproved = showUnproved;
1120-
}
1116+
m_options.modelChecker.settings.showUnproved = true;
11211117

11221118
if (m_args.count(g_strModelCheckerSolvers))
11231119
{

test/cmdlineTests/model_checker_show_unproved_false_all_engines/args

Lines changed: 0 additions & 1 deletion
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_all_engines/err

Lines changed: 0 additions & 3 deletions
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol

Lines changed: 0 additions & 12 deletions
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_bmc/args

Lines changed: 0 additions & 1 deletion
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_bmc/err

Lines changed: 0 additions & 1 deletion
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol

Lines changed: 0 additions & 12 deletions
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_chc/args

Lines changed: 0 additions & 1 deletion
This file was deleted.

test/cmdlineTests/model_checker_show_unproved_false_chc/err

Lines changed: 0 additions & 1 deletion
This file was deleted.

0 commit comments

Comments
 (0)