From 2cbd496576ec790d9a1fec89d140c385d60c6009 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Wed, 6 Oct 2021 11:52:44 +0200
Subject: [PATCH] Adjust ModelCheckerSettings in tools tests

---
 test/solc/CommandLineParser.cpp | 4 ++++
 test/tools/fuzzer_common.cpp    | 1 +
 2 files changed, 5 insertions(+)

diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp
index 3b2998ce1..663bf022c 100644
--- a/test/solc/CommandLineParser.cpp
+++ b/test/solc/CommandLineParser.cpp
@@ -149,6 +149,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
 			"--model-checker-contracts=contract1.yul:A,contract2.yul:B",
 			"--model-checker-div-mod-no-slacks",
 			"--model-checker-engine=bmc",
+			"--model-checker-invariants=contract,reentrancy",
 			"--model-checker-show-unproved",
 			"--model-checker-solvers=z3,smtlib2",
 			"--model-checker-targets=underflow,divByZero",
@@ -212,6 +213,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
 			{{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}},
 			true,
 			{true, false},
+			{{InvariantType::Contract, InvariantType::Reentrancy}},
 			true,
 			{false, true, true},
 			{{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}},
@@ -285,6 +287,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options)
 				"contract2.yul:B",
 			"--model-checker-div-mod-no-slacks", // Ignored in assembly mode
 			"--model-checker-engine=bmc",  // Ignored in assembly mode
+			"--model-checker-invariants=contract,reentrancy",  // Ignored in assembly mode
 			"--model-checker-show-unproved", // Ignored in assembly mode
 			"--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode
 			"--model-checker-targets="     // Ignored in assembly mode
@@ -375,6 +378,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options)
 			"contract2.yul:B",
 		"--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode
 		"--model-checker-engine=bmc",      // Ignored in Standard JSON mode
+		"--model-checker-invariants=contract,reentrancy",      // Ignored in Standard JSON mode
 		"--model-checker-show-unproved",      // Ignored in Standard JSON mode
 		"--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode
 		"--model-checker-targets="         // Ignored in Standard JSON mode
diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp
index 332b9fc04..82066bf52 100644
--- a/test/tools/fuzzer_common.cpp
+++ b/test/tools/fuzzer_common.cpp
@@ -106,6 +106,7 @@ void FuzzerUtil::testCompiler(
 			frontend::ModelCheckerContracts::Default(),
 			/*divModWithSlacks*/true,
 			frontend::ModelCheckerEngine::All(),
+			frontend::ModelCheckerInvariants::All(),
 			/*showUnproved=*/false,
 			smtutil::SMTSolverChoice::All(),
 			frontend::ModelCheckerTargets::Default(),