From e3abde43f58e8290b86886d192a72c771f608d26 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 14 Apr 2021 12:56:43 +0200
Subject: [PATCH] Change settings.modelChecker.targets to take an array instead
 of string

---
 Changelog.md                                  |  1 +
 docs/smtchecker.rst                           | 14 ++++----
 docs/using-the-compiler.rst                   |  8 ++---
 libsolidity/formal/ModelCheckerSettings.cpp   | 34 ++++++++++++-------
 libsolidity/formal/ModelCheckerSettings.h     | 10 ++++--
 libsolidity/interface/StandardCompiler.cpp    | 23 +++++++++----
 solc/CommandLineInterface.cpp                 |  2 +-
 .../model_checker_targets_all/args            |  2 +-
 .../model_checker_targets_all_bmc/args        |  2 +-
 .../model_checker_targets_all_chc/args        |  2 +-
 .../input.json                                |  3 +-
 .../input.json                                |  3 +-
 .../input.json                                |  3 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../output.json                               |  1 +
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                |  2 +-
 .../input.json                                | 30 ++++++++++++++++
 .../output.json                               |  1 +
 .../input.json                                | 30 ++++++++++++++++
 .../output.json                               |  1 +
 .../input.json                                | 30 ++++++++++++++++
 .../output.json                               |  0
 41 files changed, 180 insertions(+), 62 deletions(-)
 rename test/cmdlineTests/{standard_model_checker_targets_wrong => standard_model_checker_targets_empty_array}/input.json (94%)
 create mode 100644 test/cmdlineTests/standard_model_checker_targets_empty_array/output.json
 create mode 100644 test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json
 create mode 100644 test/cmdlineTests/standard_model_checker_targets_wrong_target_types/output.json
 create mode 100644 test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json
 create mode 100644 test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/output.json
 create mode 100644 test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json
 rename test/cmdlineTests/{standard_model_checker_targets_wrong => standard_model_checker_targets_wrong_targets}/output.json (100%)

diff --git a/Changelog.md b/Changelog.md
index b8244c205..707a1f76e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -18,6 +18,7 @@ Compiler Features:
  * SMTChecker: Report local variables in CHC counterexamples.
  * SMTChecker: Report out of bounds index access for arrays and fixed bytes.
  * Standard JSON: Model checker option ``settings.modelChecker.targets`` also accepts ``outOfBounds``.
+ * Standard JSON: Model checker option ``settings.modelChecker.targets`` takes an array of string targets instead of string of comma separated targets.
  * Yul Optimizer: Added a new step FunctionSpecializer, that specializes a function with its literal arguments.
  * Yul EVM Code Transform: Stack Optimization: Reuse slots of unused function arguments and defer allocating stack slots for return variables until after expression statements and assignments that do not reference them.
  * NatSpec: Allow ``@notice`` tag on non-public state variables and local variable declarations. The documentation will only be part of the AST, under the field ``documentation``.
diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst
index 737c92836..4d5cf9c9a 100644
--- a/docs/smtchecker.rst
+++ b/docs/smtchecker.rst
@@ -448,10 +448,13 @@ the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeo
 Verification Targets
 ====================
 
-The types of verification targets created by the SMTChecker can also be customized via
-the CLI option ``--model-checker-target <targets>`` or the JSON option
-``settings.modelChecker.targets=<targets>``, where ``<targets>`` is a no-space-comma-separated
-list of one or more verification targets. The keywords that represent the targets are:
+The types of verification targets created by the SMTChecker can also be
+customized via the CLI option ``--model-checker-target <targets>`` or the JSON
+option ``settings.modelChecker.targets=<targets>``.
+In the CLI case, ``<targets>`` is a no-space-comma-separated list of one or
+more verification targets, and an array of one or more targets as strings in
+the JSON input.
+The keywords that represent the targets are:
 
 - Assertions: ``assert``.
 - Arithmetic underflow: ``underflow``.
@@ -461,8 +464,7 @@ list of one or more verification targets. The keywords that represent the target
 - Popping an empty array: ``popEmptyArray``.
 - Out of bounds array/fixed bytes index access: ``outOfBounds``.
 - Insufficient funds for a transfer: ``balance``.
-- All of the above: ``all``.
-- None of the above: ``none``.
+- All of the above: ``default`` (CLI only).
 
 A common subset of targets might be, for example:
 ``--model-checker-targets assert,overflow``.
diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst
index 9cb5df1e0..6ab91bcd0 100644
--- a/docs/using-the-compiler.rst
+++ b/docs/using-the-compiler.rst
@@ -374,16 +374,16 @@ Input Description
             "MyContract": [ "abi", "evm.bytecode.opcodes" ]
           }
         },
+        // The modelChecker object is experimental and subject to changes.
         "modelChecker":
         {
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
-          // Choose which targets should be checked: all (default), constantCondition,
+          // Choose which targets should be checked: constantCondition,
           // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
+          // If the option is not given all targets are checked by default.
           // See the Formal Verification section for the targets description.
-          // Multiple targets can be selected at the same time, separated by a comma
-          // without spaces:
-          "targets": "underflow,overflow,assert",
+          "targets": ["underflow", "overflow", "assert"],
           // Timeout for each SMT query in milliseconds.
           // If this option is not given, the SMTChecker will use a deterministic
           // resource limit by default.
diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp
index 1e311b5bd..495e7a0df 100644
--- a/libsolidity/formal/ModelCheckerSettings.cpp
+++ b/libsolidity/formal/ModelCheckerSettings.cpp
@@ -26,22 +26,22 @@ using namespace ranges;
 using namespace solidity;
 using namespace solidity::frontend;
 
+using TargetType = VerificationTargetType;
+map<string, TargetType> const ModelCheckerTargets::targetStrings{
+	{"constantCondition", TargetType::ConstantCondition},
+	{"underflow", TargetType::Underflow},
+	{"overflow", TargetType::Overflow},
+	{"divByZero", TargetType::DivByZero},
+	{"balance", TargetType::Balance},
+	{"assert", TargetType::Assert},
+	{"popEmptyArray", TargetType::PopEmptyArray},
+	{"outOfBounds", TargetType::OutOfBounds}
+};
+
 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
 {
-	using TargetType = VerificationTargetType;
-	static map<string, TargetType> const targetStrings{
-		{"constantCondition", TargetType::ConstantCondition},
-		{"underflow", TargetType::Underflow},
-		{"overflow", TargetType::Overflow},
-		{"divByZero", TargetType::DivByZero},
-		{"balance", TargetType::Balance},
-		{"assert", TargetType::Assert},
-		{"popEmptyArray", TargetType::PopEmptyArray},
-		{"outOfBounds", TargetType::OutOfBounds}
-	};
-
 	set<TargetType> chosenTargets;
-	if (_targets == "all")
+	if (_targets == "default")
 		for (auto&& v: targetStrings | views::values)
 			chosenTargets.insert(v);
 	else
@@ -54,3 +54,11 @@ std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const&
 
 	return ModelCheckerTargets{chosenTargets};
 }
+
+bool ModelCheckerTargets::setFromString(string const& _target)
+{
+	if (!targetStrings.count(_target))
+		return false;
+	targets.insert(targetStrings.at(_target));
+	return true;
+}
diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h
index a9eba20d5..e528b2af8 100644
--- a/libsolidity/formal/ModelCheckerSettings.h
+++ b/libsolidity/formal/ModelCheckerSettings.h
@@ -58,12 +58,18 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
 
 struct ModelCheckerTargets
 {
-	static ModelCheckerTargets All() { return *fromString("all"); }
-	static ModelCheckerTargets None() { return {}; }
+	static ModelCheckerTargets All() { return *fromString("default"); }
 
 	static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);
 
 	bool has(VerificationTargetType _type) const { return targets.count(_type); }
+
+	/// @returns true if the @p _target is valid,
+	/// and false otherwise.
+	bool setFromString(std::string const& _target);
+
+	static std::map<std::string, VerificationTargetType> const targetStrings;
+
 	std::set<VerificationTargetType> targets;
 };
 
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 931fc46cf..3b933bcd7 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -913,12 +913,23 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 
 	if (modelCheckerSettings.isMember("targets"))
 	{
-		if (!modelCheckerSettings["targets"].isString())
-			return formatFatalError("JSONError", "settings.modelChecker.targets must be a string.");
-		std::optional<ModelCheckerTargets> targets = ModelCheckerTargets::fromString(modelCheckerSettings["targets"].asString());
-		if (!targets)
-			return formatFatalError("JSONError", "Invalid model checker targets requested.");
-		ret.modelCheckerSettings.targets = *targets;
+		auto const& targetsArray = modelCheckerSettings["targets"];
+		if (!targetsArray.isArray())
+			return formatFatalError("JSONError", "settings.modelChecker.targets must be an array.");
+
+		ModelCheckerTargets targets;
+		for (auto const& t: targetsArray)
+		{
+			if (!t.isString())
+				return formatFatalError("JSONError", "Every target in settings.modelChecker.targets must be a string.");
+			if (!targets.setFromString(t.asString()))
+				return formatFatalError("JSONError", "Invalid model checker targets requested.");
+		}
+
+		if (targets.targets.empty())
+			return formatFatalError("JSONError", "settings.modelChecker.targets must be a non-empty array.");
+
+		ret.modelCheckerSettings.targets = targets;
 	}
 
 	if (modelCheckerSettings.isMember("timeout"))
diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp
index d0c9e81ee..1f096be77 100644
--- a/solc/CommandLineInterface.cpp
+++ b/solc/CommandLineInterface.cpp
@@ -1060,7 +1060,7 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerTargets.c_str(),
-			po::value<string>()->value_name("all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("all"),
+			po::value<string>()->value_name("default,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"),
 			"Select model checker verification targets. "
 			"Multiple targets can be selected at the same time, separated by a comma "
 			"and no spaces."
diff --git a/test/cmdlineTests/model_checker_targets_all/args b/test/cmdlineTests/model_checker_targets_all/args
index aac8a1a27..950e7de30 100644
--- a/test/cmdlineTests/model_checker_targets_all/args
+++ b/test/cmdlineTests/model_checker_targets_all/args
@@ -1 +1 @@
---model-checker-engine all --model-checker-targets all
+--model-checker-engine all --model-checker-targets default
diff --git a/test/cmdlineTests/model_checker_targets_all_bmc/args b/test/cmdlineTests/model_checker_targets_all_bmc/args
index 19e3de4f6..a979c9f87 100644
--- a/test/cmdlineTests/model_checker_targets_all_bmc/args
+++ b/test/cmdlineTests/model_checker_targets_all_bmc/args
@@ -1 +1 @@
---model-checker-engine bmc --model-checker-targets all
+--model-checker-engine bmc --model-checker-targets default
diff --git a/test/cmdlineTests/model_checker_targets_all_chc/args b/test/cmdlineTests/model_checker_targets_all_chc/args
index f1b07923f..e715594f8 100644
--- a/test/cmdlineTests/model_checker_targets_all_chc/args
+++ b/test/cmdlineTests/model_checker_targets_all_chc/args
@@ -1 +1 @@
---model-checker-engine chc --model-checker-targets all
+--model-checker-engine chc --model-checker-targets default
diff --git a/test/cmdlineTests/standard_model_checker_targets_all/input.json b/test/cmdlineTests/standard_model_checker_targets_all/input.json
index ef2e8e050..0d913f0ba 100644
--- a/test/cmdlineTests/standard_model_checker_targets_all/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_all/input.json
@@ -23,8 +23,7 @@
 	{
 		"modelChecker":
 		{
-			"engine": "all",
-			"targets": "all"
+			"engine": "all"
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json
index 57ba390a7..d0a068185 100644
--- a/test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json
@@ -23,8 +23,7 @@
 	{
 		"modelChecker":
 		{
-			"engine": "bmc",
-			"targets": "all"
+			"engine": "bmc"
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_all_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_all_chc/input.json
index 0ea4f27e2..d030e0388 100644
--- a/test/cmdlineTests/standard_model_checker_targets_all_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_all_chc/input.json
@@ -23,8 +23,7 @@
 	{
 		"modelChecker":
 		{
-			"engine": "chc",
-			"targets": "all"
+			"engine": "chc"
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json
index 47e49fbed..988417824 100644
--- a/test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "assert"
+			"targets": ["assert"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json
index 11b99ae4b..a9a7b3fcd 100644
--- a/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "assert"
+			"targets": ["assert"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json
index df01286dc..4e6c84dbb 100644
--- a/test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "balance"
+			"targets": ["balance"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json
index e88d2a426..4973a0597 100644
--- a/test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "balance"
+			"targets": ["balance"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json
index ba61db3e3..dd97baae9 100644
--- a/test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "constantCondition"
+			"targets": ["constantCondition"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json
index 27c53682d..365ca122b 100644
--- a/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "constantCondition"
+			"targets": ["constantCondition"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json
index 7514a9af8..53750a1ec 100644
--- a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "divByZero"
+			"targets": ["divByZero"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json
index b65acfb6f..1c7af8d5c 100644
--- a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "divByZero"
+			"targets": ["divByZero"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong/input.json b/test/cmdlineTests/standard_model_checker_targets_empty_array/input.json
similarity index 94%
rename from test/cmdlineTests/standard_model_checker_targets_wrong/input.json
rename to test/cmdlineTests/standard_model_checker_targets_empty_array/input.json
index 2dc6ea56a..cb51e4905 100644
--- a/test/cmdlineTests/standard_model_checker_targets_wrong/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_empty_array/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "all",
-			"targets": "aaa,bbb"
+			"targets": []
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_empty_array/output.json b/test/cmdlineTests/standard_model_checker_targets_empty_array/output.json
new file mode 100644
index 000000000..94163d97d
--- /dev/null
+++ b/test/cmdlineTests/standard_model_checker_targets_empty_array/output.json
@@ -0,0 +1 @@
+{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.targets must be a non-empty array.","message":"settings.modelChecker.targets must be a non-empty array.","severity":"error","type":"JSONError"}]}
diff --git a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json
index c184e2f12..3ae757542 100644
--- a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "outOfBounds"
+			"targets": ["outOfBounds"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json
index 8a409df98..cd0ba6d13 100644
--- a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "outOfBounds"
+			"targets": ["outOfBounds"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json
index 9ccca64fd..de63c4a62 100644
--- a/test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "overflow"
+			"targets": ["overflow"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json
index ef71d8507..522d2480c 100644
--- a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "overflow"
+			"targets": ["overflow"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json
index d580fc397..40f3718ce 100644
--- a/test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "popEmptyArray"
+			"targets": ["popEmptyArray"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json
index 13ad86e94..7d2dc69e3 100644
--- a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "popEmptyArray"
+			"targets": ["popEmptyArray"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json
index 2bcdef3d7..4bd8eded4 100644
--- a/test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "underflow"
+			"targets": ["underflow"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json
index 6e9b92ba3..ca33d2fdc 100644
--- a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "underflow"
+			"targets": ["underflow"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/input.json
index 8598f6772..835a9d46b 100644
--- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "underflow,overflow,assert"
+			"targets": ["underflow", "overflow", "assert"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json
index 06478c45b..50f0e82dc 100644
--- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "underflow,overflow,assert"
+			"targets": ["underflow", "overflow", "assert"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/input.json
index 75ead5336..c8bae009d 100644
--- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "bmc",
-			"targets": "underflow,overflow"
+			"targets": ["underflow", "overflow"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json
index 2f960af19..9fc834fd8 100644
--- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json
+++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json
@@ -24,7 +24,7 @@
 		"modelChecker":
 		{
 			"engine": "chc",
-			"targets": "underflow,overflow"
+			"targets": ["underflow", "overflow"]
 		}
 	}
 }
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json
new file mode 100644
index 000000000..a89271975
--- /dev/null
+++ b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json
@@ -0,0 +1,30 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+						arr[x];
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all",
+			"targets": [2]
+		}
+	}
+}
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/output.json b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/output.json
new file mode 100644
index 000000000..673493cc9
--- /dev/null
+++ b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/output.json
@@ -0,0 +1 @@
+{"errors":[{"component":"general","formattedMessage":"Every target in settings.modelChecker.targets must be a string.","message":"Every target in settings.modelChecker.targets must be a string.","severity":"error","type":"JSONError"}]}
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json
new file mode 100644
index 000000000..136ce0978
--- /dev/null
+++ b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json
@@ -0,0 +1,30 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+						arr[x];
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all",
+			"targets": "assert"
+		}
+	}
+}
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/output.json b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/output.json
new file mode 100644
index 000000000..ee68dbef1
--- /dev/null
+++ b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/output.json
@@ -0,0 +1 @@
+{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.targets must be an array.","message":"settings.modelChecker.targets must be an array.","severity":"error","type":"JSONError"}]}
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json b/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json
new file mode 100644
index 000000000..1788fb6d5
--- /dev/null
+++ b/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json
@@ -0,0 +1,30 @@
+{
+	"language": "Solidity",
+	"sources":
+	{
+		"A":
+		{
+			"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
+					uint[] arr;
+					function f(address payable a, uint x) public {
+						require(x >= 0);
+						--x;
+						x + type(uint).max;
+						2 / x;
+						a.transfer(x);
+						assert(x > 0);
+						arr.pop();
+						arr[x];
+					}
+				}"
+		}
+	},
+	"settings":
+	{
+		"modelChecker":
+		{
+			"engine": "all",
+			"targets": ["aaa", "bbb"]
+		}
+	}
+}
diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong/output.json b/test/cmdlineTests/standard_model_checker_targets_wrong_targets/output.json
similarity index 100%
rename from test/cmdlineTests/standard_model_checker_targets_wrong/output.json
rename to test/cmdlineTests/standard_model_checker_targets_wrong_targets/output.json