From e698a22ca30223a1e941c9e7f954bd38f75c6353 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Thu, 16 Mar 2023 13:11:33 +0100
Subject: [PATCH] change SMTChecker default settings

---
 docs/smtchecker.rst                           |  36 ++--
 libsolidity/formal/ModelCheckerSettings.cpp   |  11 +-
 libsolidity/formal/ModelCheckerSettings.h     |   9 +-
 libsolidity/formal/SMTEncoder.cpp             |   2 +-
 libsolidity/interface/CompilerStack.cpp       |   9 +
 .../args                                      |   2 +-
 .../args                                      |   2 +-
 .../args                                      |   2 +-
 .../model_checker_divModSlacks_false_all/args |   2 +-
 .../model_checker_divModSlacks_false_bmc/args |   2 +-
 .../model_checker_divModSlacks_false_chc/args |   2 +-
 .../err                                       |  64 ------
 .../model_checker_targets_default_bmc/err     |  32 ---
 .../model_checker_targets_default_chc/err     |  45 -----
 .../model_checker_timeout_all/args            |   2 +-
 .../model_checker_timeout_bmc/args            |   2 +-
 .../model_checker_timeout_chc/args            |   2 +-
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../output.json                               |   3 +-
 .../output.json                               | 182 ------------------
 .../output.json                               | 111 -----------
 .../output.json                               | 114 -----------
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 .../input.json                                |   1 +
 test/libsolidity/SMTCheckerTest.cpp           |   3 +
 32 files changed, 66 insertions(+), 583 deletions(-)

diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst
index 9c862e530..240f6e7de 100644
--- a/docs/smtchecker.rst
+++ b/docs/smtchecker.rst
@@ -22,8 +22,7 @@ specification given by ``require`` and ``assert`` statements. That is, it consid
 ``require`` statements as assumptions and tries to prove that the conditions
 inside ``assert`` statements are always true.  If an assertion failure is
 found, a counterexample may be given to the user showing how the assertion can
-be violated. If no warning is given by the SMTChecker for a property,
-it means that the property is safe.
+be violated. Safe properties are also reported accordingly.
 
 The other verification targets that the SMTChecker checks at compile time are:
 
@@ -34,16 +33,27 @@ The other verification targets that the SMTChecker checks at compile time are:
 - Out of bounds index access.
 - Insufficient funds for a transfer.
 
-All the targets above are automatically checked by default if all engines are
-enabled, except underflow and overflow for Solidity >=0.8.7.
+By default, for Solidity >=0.8.20 only assertions are checked.  For Solidity
+>=0.8.7 all the targets above are checked by default except for underflow and
+overflow.  Underflow and overflow are also in the default set for Solidity
+<0.8.7.  The above only applies for the default targets which can be
+overridden by the users' choices.
 
 The potential warnings that the SMTChecker reports are:
 
 - ``<failing  property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
+- ``X verification condition(s) could not be proved.``. This is a summary of how many properties the SMTChecker was not able to prove. The list can be expanded where the warning below is shown for each of those properties.
 - ``<failing property> might happen here``. This means that the solver could not prove either case within the given timeout. Since the result is unknown, the SMTChecker reports the potential failure for soundness. This may be solved by increasing the query timeout, but the problem might also simply be too hard for the engine to solve.
 
+The potential information messages that the SMTChecker reports are:
+
+- ``X verification condition(s) proved safe!``. This is a summary of how many properties the SMTChecker was able to prove. The list can be expanded where the information below is shown for each proved property.
+- ``<property> check is safe!``. This means that the SMTChecker managed to prove that the property is safe.
+- ``Contract invariant(s)``. This may be shown if the model checker ``invariants`` option is chosen with ``contract`` and the SMTChecker was able to infer contract invariants.
+- ``Reentrancy property(ies)``. This may be shown if the model checker ``invariants`` option is chosen with ``reentrancy`` and the SMTChecker was able to infer reentrancy properties for external calls.
+
 To enable the SMTChecker, you must select :ref:`which engine should run<smtchecker_engines>`,
-where the default is no engine. Selecting the engine enables the SMTChecker on all files.
+where the compiler default is no engine. Selecting the engine enables the SMTChecker on all files.
 
 .. note::
 
@@ -442,16 +452,15 @@ SMTChecker Options and Tuning
 Timeout
 =======
 
-The SMTChecker uses a hardcoded resource limit (``rlimit``) chosen per solver,
-which is not precisely related to time. We chose the ``rlimit`` option as the default
-because it gives more determinism guarantees than time inside the solver.
-
-This options translates roughly to "a few seconds timeout" per query. Of course many properties
-are very complex and need a lot of time to be solved, where determinism does not matter.
-If the SMTChecker does not manage to solve the contract properties with the default ``rlimit``,
-a timeout can be given in milliseconds via the CLI option ``--model-checker-timeout <time>`` or
+By default the SMTChecker uses a timeout of 1 second per query.
+If the SMTChecker does not manage to solve the contract properties with the default timeout,
+the user may modify the timeout duration (given in milliseconds) via the CLI option ``--model-checker-timeout <time>`` or
 the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeout.
 
+Note that some SMT/CHC solvers do not consider counterexample generation as
+part of the solving timeout, so one may experience longer times for properties
+that are false.
+
 .. _smtchecker_targets:
 
 Verification Targets
@@ -478,6 +487,7 @@ The keywords that represent the targets are:
 A common subset of targets might be, for example:
 ``--model-checker-targets assert,overflow``.
 
+Only assertions are checked by default for Solidity >=0.8.20.
 All targets are checked by default, except underflow and overflow for Solidity >=0.8.7.
 
 There is no precise heuristic on how and when to split verification targets,
diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp
index d1e383d63..fb1b38699 100644
--- a/libsolidity/formal/ModelCheckerSettings.cpp
+++ b/libsolidity/formal/ModelCheckerSettings.cpp
@@ -85,16 +85,11 @@ map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
 {
 	set<TargetType> chosenTargets;
-	if (_targets == "default" || _targets == "all")
-	{
-		bool all = _targets == "all";
+	if (_targets == "all")
 		for (auto&& v: targetStrings | ranges::views::values)
-		{
-			if (!all && (v == TargetType::Underflow || v == TargetType::Overflow))
-				continue;
 			chosenTargets.insert(v);
-		}
-	}
+	else if (_targets == "default")
+		chosenTargets.insert(TargetType::Assert);
 	else
 		for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>())
 		{
diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h
index fafb2cdac..e5ce16418 100644
--- a/libsolidity/formal/ModelCheckerSettings.h
+++ b/libsolidity/formal/ModelCheckerSettings.h
@@ -117,7 +117,7 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
 
 struct ModelCheckerTargets
 {
-	/// Adds the default targets, that is, all except underflow and overflow.
+	/// By default adds only assertions as targets.
 	static ModelCheckerTargets Default() { return *fromString("default"); }
 	/// Adds all targets, including underflow and overflow.
 	static ModelCheckerTargets All() { return *fromString("all"); }
@@ -164,7 +164,7 @@ struct ModelCheckerSettings
 	/// This is the default because Spacer prefers that over precise / and mod.
 	/// This option allows disabling this mechanism since other solvers
 	/// might prefer the precise encoding.
-	bool divModNoSlacks = false;
+	std::optional<bool> divModNoSlacks = {};
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
 	ModelCheckerExtCalls externalCalls = {};
 	ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
@@ -173,7 +173,10 @@ struct ModelCheckerSettings
 	bool showUnsupported = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();
-	std::optional<unsigned> timeout;
+	// Default timeout per query in milliseconds.
+	// We keep it as optional because tests may overwrite this to use
+	// resource limit for reproducibility.
+	std::optional<unsigned> timeout = 1000;
 
 	bool operator!=(ModelCheckerSettings const& _other) const noexcept { return !(*this == _other); }
 	bool operator==(ModelCheckerSettings const& _other) const noexcept
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 8f22ab824..ddbfe5908 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2041,7 +2041,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 	IntegerType const& _type
 )
 {
-	if (m_settings.divModNoSlacks)
+	if (m_settings.divModNoSlacks.has_value() && *m_settings.divModNoSlacks)
 		return {_left / _right, _left % _right};
 
 	IntegerType const* intType = &_type;
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index dae509ed5..3d514553f 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -600,6 +600,15 @@ bool CompilerStack::analyze()
 			if (m_modelCheckerSettings.engine.any())
 				m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter);
 
+			// Tiny automatic optimization for Eldarica if the user
+			// has not forcefully chosen `divModNoSlacks = false` which
+			// is the default for Spacer but worse for Eldarica.
+			if (
+				m_modelCheckerSettings.solvers.eld &&
+				!m_modelCheckerSettings.divModNoSlacks.has_value()
+			)
+				m_modelCheckerSettings.divModNoSlacks = true;
+
 			ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
 			modelChecker.checkRequestedSourcesAndContracts(allSources);
 			for (Source const* source: m_sourceOrder)
diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_all/args b/test/cmdlineTests/model_checker_divModSlacks_default_all/args
index 5aeb1490e..79002c911 100644
--- a/test/cmdlineTests/model_checker_divModSlacks_default_all/args
+++ b/test/cmdlineTests/model_checker_divModSlacks_default_all/args
@@ -1 +1 @@
---model-checker-engine all
+--model-checker-engine all --model-checker-targets divByZero
diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args b/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args
index 549f20236..30959921a 100644
--- a/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args
+++ b/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args
@@ -1 +1 @@
---model-checker-engine bmc
+--model-checker-engine bmc --model-checker-targets divByZero
diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_chc/args b/test/cmdlineTests/model_checker_divModSlacks_default_chc/args
index 7458a47d3..b1fe70fc8 100644
--- a/test/cmdlineTests/model_checker_divModSlacks_default_chc/args
+++ b/test/cmdlineTests/model_checker_divModSlacks_default_chc/args
@@ -1 +1 @@
---model-checker-engine chc
+--model-checker-engine chc --model-checker-targets divByZero
diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_all/args b/test/cmdlineTests/model_checker_divModSlacks_false_all/args
index 75bfbf194..1465bd414 100644
--- a/test/cmdlineTests/model_checker_divModSlacks_false_all/args
+++ b/test/cmdlineTests/model_checker_divModSlacks_false_all/args
@@ -1 +1 @@
---model-checker-engine all --model-checker-div-mod-no-slacks
+--model-checker-engine all --model-checker-div-mod-no-slacks --model-checker-targets divByZero
diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args b/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args
index 2579bdc1e..a5a691bdc 100644
--- a/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args
+++ b/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args
@@ -1 +1 @@
---model-checker-engine bmc --model-checker-div-mod-no-slacks
+--model-checker-engine bmc --model-checker-div-mod-no-slacks --model-checker-targets divByZero
diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_chc/args b/test/cmdlineTests/model_checker_divModSlacks_false_chc/args
index b0679b1c6..ea92f2512 100644
--- a/test/cmdlineTests/model_checker_divModSlacks_false_chc/args
+++ b/test/cmdlineTests/model_checker_divModSlacks_false_chc/args
@@ -1 +1 @@
---model-checker-engine chc --model-checker-div-mod-no-slacks
+--model-checker-engine chc --model-checker-div-mod-no-slacks --model-checker-targets divByZero
diff --git a/test/cmdlineTests/model_checker_targets_default_all_engines/err b/test/cmdlineTests/model_checker_targets_default_all_engines/err
index c1fe2f5b3..01272b8b7 100644
--- a/test/cmdlineTests/model_checker_targets_default_all_engines/err
+++ b/test/cmdlineTests/model_checker_targets_default_all_engines/err
@@ -1,18 +1,3 @@
-Warning: CHC: Division by zero happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
- --> model_checker_targets_default_all_engines/input.sol:9:3:
-  |
-9 | 		2 / x;
-  | 		^^^^^
-
 Warning: CHC: Assertion violation happens here.
 Counterexample:
 arr = []
@@ -27,52 +12,3 @@ test.f(0x0, 1)
    |
 11 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
-
-Warning: CHC: Empty array "pop" happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> model_checker_targets_default_all_engines/input.sol:12:3:
-   |
-12 | 		arr.pop();
-   | 		^^^^^^^^^
-
-Warning: CHC: Out of bounds access happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> model_checker_targets_default_all_engines/input.sol:13:3:
-   |
-13 | 		arr[x];
-   | 		^^^^^^
-
-Warning: BMC: Condition is always true.
- --> model_checker_targets_default_all_engines/input.sol:6:11:
-  |
-6 | 		require(x >= 0);
-  | 		        ^^^^^^
-Note: Callstack:
-
-Warning: BMC: Insufficient funds happens here.
-  --> model_checker_targets_default_all_engines/input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
diff --git a/test/cmdlineTests/model_checker_targets_default_bmc/err b/test/cmdlineTests/model_checker_targets_default_bmc/err
index 1122be36b..5cc36c933 100644
--- a/test/cmdlineTests/model_checker_targets_default_bmc/err
+++ b/test/cmdlineTests/model_checker_targets_default_bmc/err
@@ -1,35 +1,3 @@
-Warning: BMC: Condition is always true.
- --> model_checker_targets_default_bmc/input.sol:6:11:
-  |
-6 | 		require(x >= 0);
-  | 		        ^^^^^^
-Note: Callstack:
-
-Warning: BMC: Division by zero happens here.
- --> model_checker_targets_default_bmc/input.sol:9:3:
-  |
-9 | 		2 / x;
-  | 		^^^^^
-Note: Counterexample:
-  <result> = 0
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
-Warning: BMC: Insufficient funds happens here.
-  --> model_checker_targets_default_bmc/input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
 Warning: BMC: Assertion violation happens here.
   --> model_checker_targets_default_bmc/input.sol:11:3:
    |
diff --git a/test/cmdlineTests/model_checker_targets_default_chc/err b/test/cmdlineTests/model_checker_targets_default_chc/err
index bd2aa0b4d..3d820ecd8 100644
--- a/test/cmdlineTests/model_checker_targets_default_chc/err
+++ b/test/cmdlineTests/model_checker_targets_default_chc/err
@@ -1,18 +1,3 @@
-Warning: CHC: Division by zero happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
- --> model_checker_targets_default_chc/input.sol:9:3:
-  |
-9 | 		2 / x;
-  | 		^^^^^
-
 Warning: CHC: Assertion violation happens here.
 Counterexample:
 arr = []
@@ -27,33 +12,3 @@ test.f(0x0, 1)
    |
 11 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
-
-Warning: CHC: Empty array "pop" happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> model_checker_targets_default_chc/input.sol:12:3:
-   |
-12 | 		arr.pop();
-   | 		^^^^^^^^^
-
-Warning: CHC: Out of bounds access happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> model_checker_targets_default_chc/input.sol:13:3:
-   |
-13 | 		arr[x];
-   | 		^^^^^^
diff --git a/test/cmdlineTests/model_checker_timeout_all/args b/test/cmdlineTests/model_checker_timeout_all/args
index aad210472..3d991bd1d 100644
--- a/test/cmdlineTests/model_checker_timeout_all/args
+++ b/test/cmdlineTests/model_checker_timeout_all/args
@@ -1 +1 @@
---model-checker-engine all --model-checker-timeout 1000
+--model-checker-engine all --model-checker-timeout 1000 --model-checker-targets all
diff --git a/test/cmdlineTests/model_checker_timeout_bmc/args b/test/cmdlineTests/model_checker_timeout_bmc/args
index 6c50b2711..b8241e113 100644
--- a/test/cmdlineTests/model_checker_timeout_bmc/args
+++ b/test/cmdlineTests/model_checker_timeout_bmc/args
@@ -1 +1 @@
---model-checker-engine bmc --model-checker-timeout 1000
+--model-checker-engine bmc --model-checker-timeout 1000 --model-checker-targets all
diff --git a/test/cmdlineTests/model_checker_timeout_chc/args b/test/cmdlineTests/model_checker_timeout_chc/args
index 8e3a1efb7..a7625f825 100644
--- a/test/cmdlineTests/model_checker_timeout_chc/args
+++ b/test/cmdlineTests/model_checker_timeout_chc/args
@@ -1 +1 @@
---model-checker-engine chc --model-checker-timeout 1000
+--model-checker-engine chc --model-checker-timeout 1000 --model-checker-targets all
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json
index 7ede51865..d50a9a40f 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "all"
 		}
 	}
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json
index ccb4839bb..6ff083425 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "bmc"
 		}
 	}
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json
index e33e97706..678e05799 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "chc"
 		}
 	}
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json
index efa209cf9..67ad5f4bb 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "all",
 			"divModNoSlacks": true
 		}
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json
index 167b849f4..4bf255b7a 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "bmc",
 			"divModNoSlacks": true
 		}
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json
index ac29b462b..e57702f57 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "chc",
 			"divModNoSlacks": true
 		}
diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json
index 09be5d735..8fc5924ab 100644
--- a/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json
+++ b/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json
@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],
 			"engine": "chc",
 			"divModNoSlacks": 42
 		}
diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
index bf59a0d9d..e3aa6c03d 100644
--- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
+++ b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
@@ -3,7 +3,8 @@
     {
         "smtlib2queries":
         {
-            "0x75b95497d56c30e254a59358d72ddd4e78f9e90db621cfe677e85d05b2252411": "(set-option :produce-models true)
+            "0x1709577b0e186388ed08c2cf085f20c115c4c94745fb102c5be552ff2e4c7028": "(set-option :produce-models true)
+(set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |x_3_3| () Int)
 (declare-fun |error_0| () Int)
diff --git a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
index 4c967fa5d..5c43fe6b5 100644
--- a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
+++ b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
@@ -1,44 +1,6 @@
 {
     "errors":
     [
-        {
-            "component": "general",
-            "errorCode": "4281",
-            "formattedMessage": "Warning: CHC: Division by zero happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> A:10:7:
-   |
-10 | \t\t\t\t\t\t2 / x;
-   | \t\t\t\t\t\t^^^^^
-
-",
-            "message": "CHC: Division by zero happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)",
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 216,
-                "file": "A",
-                "start": 211
-            },
-            "type": "Warning"
-        },
         {
             "component": "general",
             "errorCode": "6328",
@@ -76,150 +38,6 @@ test.f(0x0, 1)",
                 "start": 245
             },
             "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "2529",
-            "formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> A:13:7:
-   |
-13 | \t\t\t\t\t\tarr.pop();
-   | \t\t\t\t\t\t^^^^^^^^^
-
-",
-            "message": "CHC: Empty array \"pop\" happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)",
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 275,
-                "file": "A",
-                "start": 266
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "6368",
-            "formattedMessage": "Warning: CHC: Out of bounds access happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> A:14:7:
-   |
-14 | \t\t\t\t\t\tarr[x];
-   | \t\t\t\t\t\t^^^^^^
-
-",
-            "message": "CHC: Out of bounds access happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)",
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 289,
-                "file": "A",
-                "start": 283
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "6838",
-            "formattedMessage": "Warning: BMC: Condition is always true.
- --> A:7:15:
-  |
-7 | \t\t\t\t\t\trequire(x >= 0);
-  | \t\t\t\t\t\t        ^^^^^^
-Note: Callstack:
-
-",
-            "message": "BMC: Condition is always true.",
-            "secondarySourceLocations":
-            [
-                {
-                    "message": "Callstack:"
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 165,
-                "file": "A",
-                "start": 159
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "1236",
-            "formattedMessage": "Warning: BMC: Insufficient funds happens here.
-  --> A:11:7:
-   |
-11 | \t\t\t\t\t\ta.transfer(x);
-   | \t\t\t\t\t\t^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
-",
-            "message": "BMC: Insufficient funds happens here.",
-            "secondarySourceLocations":
-            [
-                {
-                    "message": "Counterexample:
-  a = 0
-  x = 0
-"
-                },
-                {
-                    "message": "Callstack:"
-                },
-                {
-                    "message": ""
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 237,
-                "file": "A",
-                "start": 224
-            },
-            "type": "Warning"
         }
     ],
     "sources":
diff --git a/test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json b/test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json
index 1be99ca45..18452ccbc 100644
--- a/test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json
+++ b/test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json
@@ -1,117 +1,6 @@
 {
     "errors":
     [
-        {
-            "component": "general",
-            "errorCode": "6838",
-            "formattedMessage": "Warning: BMC: Condition is always true.
- --> A:7:15:
-  |
-7 | \t\t\t\t\t\trequire(x >= 0);
-  | \t\t\t\t\t\t        ^^^^^^
-Note: Callstack:
-
-",
-            "message": "BMC: Condition is always true.",
-            "secondarySourceLocations":
-            [
-                {
-                    "message": "Callstack:"
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 165,
-                "file": "A",
-                "start": 159
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "3046",
-            "formattedMessage": "Warning: BMC: Division by zero happens here.
-  --> A:10:7:
-   |
-10 | \t\t\t\t\t\t2 / x;
-   | \t\t\t\t\t\t^^^^^
-Note: Counterexample:
-  <result> = 0
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
-",
-            "message": "BMC: Division by zero happens here.",
-            "secondarySourceLocations":
-            [
-                {
-                    "message": "Counterexample:
-  <result> = 0
-  a = 0
-  x = 0
-"
-                },
-                {
-                    "message": "Callstack:"
-                },
-                {
-                    "message": ""
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 216,
-                "file": "A",
-                "start": 211
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "1236",
-            "formattedMessage": "Warning: BMC: Insufficient funds happens here.
-  --> A:11:7:
-   |
-11 | \t\t\t\t\t\ta.transfer(x);
-   | \t\t\t\t\t\t^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
-",
-            "message": "BMC: Insufficient funds happens here.",
-            "secondarySourceLocations":
-            [
-                {
-                    "message": "Counterexample:
-  a = 0
-  x = 0
-"
-                },
-                {
-                    "message": "Callstack:"
-                },
-                {
-                    "message": ""
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 237,
-                "file": "A",
-                "start": 224
-            },
-            "type": "Warning"
-        },
         {
             "component": "general",
             "errorCode": "4661",
diff --git a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
index c3df366c9..5c43fe6b5 100644
--- a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
+++ b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
@@ -1,44 +1,6 @@
 {
     "errors":
     [
-        {
-            "component": "general",
-            "errorCode": "4281",
-            "formattedMessage": "Warning: CHC: Division by zero happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> A:10:7:
-   |
-10 | \t\t\t\t\t\t2 / x;
-   | \t\t\t\t\t\t^^^^^
-
-",
-            "message": "CHC: Division by zero happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)",
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 216,
-                "file": "A",
-                "start": 211
-            },
-            "type": "Warning"
-        },
         {
             "component": "general",
             "errorCode": "6328",
@@ -76,82 +38,6 @@ test.f(0x0, 1)",
                 "start": 245
             },
             "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "2529",
-            "formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> A:13:7:
-   |
-13 | \t\t\t\t\t\tarr.pop();
-   | \t\t\t\t\t\t^^^^^^^^^
-
-",
-            "message": "CHC: Empty array \"pop\" happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)",
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 275,
-                "file": "A",
-                "start": 266
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "6368",
-            "formattedMessage": "Warning: CHC: Out of bounds access happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)
-  --> A:14:7:
-   |
-14 | \t\t\t\t\t\tarr[x];
-   | \t\t\t\t\t\t^^^^^^
-
-",
-            "message": "CHC: Out of bounds access happens here.
-Counterexample:
-arr = []
-a = 0x0
-x = 0
-
-Transaction trace:
-test.constructor()
-State: arr = []
-test.f(0x0, 1)",
-            "severity": "warning",
-            "sourceLocation":
-            {
-                "end": 289,
-                "file": "A",
-                "start": 283
-            },
-            "type": "Warning"
         }
     ],
     "sources":
diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/input.json b/test/cmdlineTests/standard_model_checker_timeout_all/input.json
index 72c742375..6bb879169 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_all/input.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_all/input.json
@@ -11,6 +11,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["assert", "divByZero"],
 			"engine": "all",
 			"timeout": 1000
 		}
diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json
index 94b70a354..494ac3796 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json
@@ -11,6 +11,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["assert", "divByZero"],
 			"engine": "bmc",
 			"timeout": 1000
 		}
diff --git a/test/cmdlineTests/standard_model_checker_timeout_chc/input.json b/test/cmdlineTests/standard_model_checker_timeout_chc/input.json
index 156f9580d..646de2671 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_chc/input.json
@@ -11,6 +11,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["assert", "divByZero"],
 			"engine": "chc",
 			"timeout": 1000
 		}
diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
index 949589527..0497857a1 100644
--- a/test/libsolidity/SMTCheckerTest.cpp
+++ b/test/libsolidity/SMTCheckerTest.cpp
@@ -82,6 +82,9 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none())
 		m_shouldRun = false;
 
+	// Disable the default timeout to force resource limit.
+	m_modelCheckerSettings.timeout = {};
+
 	auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "yes");
 	if (ignoreCex == "no")
 		m_ignoreCex = false;