Tests

Leo Alt · Leo Alt · commit 3c1f555f713c · 2021-08-04T13:54:50.000+02:00
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
@@ -958,7 +958,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 			return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");
 		ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
 	}
-	
+
 	if (modelCheckerSettings.isMember("solvers"))
 	{
 		auto const& solversArray = modelCheckerSettings["solvers"];
diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
@@ -27,6 +27,14 @@ using namespace solidity::frontend::test;
 
 SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{})
 {
+	auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes");
+	if (showUnproved == "no")
+		m_modelCheckerSettings.showUnproved = false;
+	else if (showUnproved == "yes")
+		m_modelCheckerSettings.showUnproved = true;
+	else
+		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice."));
+
 	auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
 	if (choice == "any")
 		m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All();
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
@@ -22,14 +22,14 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (226-256): CHC: Assertion violation happens here.
 // Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (310-340): CHC: Assertion violation might happen here.
 // Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (483-513): CHC: Assertion violation might happen here.
 // Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (568-598): CHC: Assertion violation might happen here.
 // Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (226-256): CHC: Assertion violation happens here.
+// Warning 6328: (310-340): CHC: Assertion violation might happen here.
+// Warning 6328: (483-513): CHC: Assertion violation might happen here.
+// Warning 6328: (568-598): CHC: Assertion violation might happen here.
 // Warning 6328: (654-684): CHC: Assertion violation might happen here.
 // Warning 4661: (310-340): BMC: Assertion violation happens here.
 // Warning 4661: (483-513): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
@@ -0,0 +1,35 @@
+contract C {
+	function abiencodePackedStringLiteral() public pure {
+		bytes memory b1 = abi.encodePacked("");
+		bytes memory b2 = abi.encodePacked("");
+		// should hold, but currently fails due to string literal abstraction
+		assert(b1.length == b2.length);
+
+		bytes memory b3 = abi.encodePacked(bytes(""));
+		assert(b1.length == b3.length); // should fail
+
+		bytes memory b4 = abi.encodePacked(bytes24(""));
+		// should hold, but currently fails due to string literal abstraction
+		assert(b1.length == b4.length);
+
+		bytes memory b5 = abi.encodePacked(string(""));
+		assert(b1.length == b5.length); // should fail
+
+		bytes memory b6 = abi.encode("");
+		assert(b1.length == b6.length); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTShowUnproved: no
+// ----
+// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (226-256): CHC: Assertion violation happens here.
+// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+// Warning 4661: (310-340): BMC: Assertion violation happens here.
+// Warning 4661: (483-513): BMC: Assertion violation happens here.
+// Warning 4661: (568-598): BMC: Assertion violation happens here.
+// Warning 4661: (654-684): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
@@ -19,12 +19,12 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (208-238): CHC: Assertion violation happens here.
 // Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (286-316): CHC: Assertion violation might happen here.
 // Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (453-483): CHC: Assertion violation might happen here.
 // Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (208-238): CHC: Assertion violation happens here.
+// Warning 6328: (286-316): CHC: Assertion violation might happen here.
+// Warning 6328: (453-483): CHC: Assertion violation might happen here.
 // Warning 6328: (532-562): CHC: Assertion violation might happen here.
 // Warning 4661: (286-316): BMC: Assertion violation happens here.
 // Warning 4661: (453-483): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (325-355): CHC: Assertion violation happens here.
 // Warning 6328: (578-608): CHC: Assertion violation happens here.
-// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (691-721): CHC: Assertion violation might happen here.
-// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (959-989): CHC: Assertion violation might happen here.
-// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
 // Warning 4661: (691-721): BMC: Assertion violation happens here.
 // Warning 4661: (959-989): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (326-356): CHC: Assertion violation happens here.
 // Warning 6328: (579-609): CHC: Assertion violation happens here.
-// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (692-722): CHC: Assertion violation might happen here.
-// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (960-990): CHC: Assertion violation might happen here.
-// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
 // Warning 4661: (692-722): BMC: Assertion violation happens here.
 // Warning 4661: (960-990): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
@@ -14,8 +14,8 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (333-371): CHC: Assertion violation might happen here.
 // Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (333-371): CHC: Assertion violation might happen here.
 // Warning 6328: (390-428): CHC: Assertion violation might happen here.
 // Warning 4661: (333-371): BMC: Assertion violation happens here.
 // Warning 4661: (390-428): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
@@ -22,14 +22,14 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (252-282): CHC: Assertion violation happens here.
 // Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (347-377): CHC: Assertion violation might happen here.
 // Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (531-561): CHC: Assertion violation might happen here.
 // Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (627-657): CHC: Assertion violation might happen here.
 // Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (252-282): CHC: Assertion violation happens here.
+// Warning 6328: (347-377): CHC: Assertion violation might happen here.
+// Warning 6328: (531-561): CHC: Assertion violation might happen here.
+// Warning 6328: (627-657): CHC: Assertion violation might happen here.
 // Warning 6328: (746-776): CHC: Assertion violation might happen here.
 // Warning 4661: (347-377): BMC: Assertion violation happens here.
 // Warning 4661: (531-561): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (334-364): CHC: Assertion violation happens here.
 // Warning 6328: (588-618): CHC: Assertion violation happens here.
-// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (702-732): CHC: Assertion violation might happen here.
-// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (971-1001): CHC: Assertion violation might happen here.
-// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
 // Warning 4661: (702-732): BMC: Assertion violation happens here.
 // Warning 4661: (971-1001): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
@@ -25,13 +25,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (335-365): CHC: Assertion violation happens here.
 // Warning 6328: (589-619): CHC: Assertion violation happens here.
-// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (703-733): CHC: Assertion violation might happen here.
-// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (972-1002): CHC: Assertion violation might happen here.
-// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
 // Warning 4661: (703-733): BMC: Assertion violation happens here.
 // Warning 4661: (972-1002): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
@@ -14,8 +14,8 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (337-375): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (337-375): CHC: Assertion violation might happen here.
 // Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (337-375): CHC: Assertion violation might happen here.
 // Warning 6328: (394-432): CHC: Assertion violation might happen here.
 // Warning 4661: (337-375): BMC: Assertion violation happens here.
 // Warning 4661: (394-432): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
@@ -22,14 +22,14 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (261-291): CHC: Assertion violation happens here.
 // Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (357-387): CHC: Assertion violation might happen here.
 // Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (542-572): CHC: Assertion violation might happen here.
 // Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (639-669): CHC: Assertion violation might happen here.
 // Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (261-291): CHC: Assertion violation happens here.
+// Warning 6328: (357-387): CHC: Assertion violation might happen here.
+// Warning 6328: (542-572): CHC: Assertion violation might happen here.
+// Warning 6328: (639-669): CHC: Assertion violation might happen here.
 // Warning 6328: (753-783): CHC: Assertion violation might happen here.
 // Warning 4661: (357-387): BMC: Assertion violation happens here.
 // Warning 4661: (542-572): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol
@@ -0,0 +1,15 @@
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}
+// ====
+// SMTEngine: bmc
+// SMTShowUnproved: no
+// ----
+// Warning 2788: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
@@ -46,12 +46,12 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (693-712): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (693-712): CHC: Assertion violation might happen here.
 // Warning 1218: (716-735): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (716-735): CHC: Assertion violation might happen here.
 // Warning 1218: (739-758): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (739-758): CHC: Assertion violation might happen here.
 // Warning 1218: (762-781): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (693-712): CHC: Assertion violation might happen here.
+// Warning 6328: (716-735): CHC: Assertion violation might happen here.
+// Warning 6328: (739-758): CHC: Assertion violation might happen here.
 // Warning 6328: (762-781): CHC: Assertion violation might happen here.
 // Warning 4661: (693-712): BMC: Assertion violation happens here.
 // Warning 4661: (716-735): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
@@ -20,6 +20,5 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (156-170): CHC: Assertion violation happens here.
 // Warning 2661: (113-116): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
@@ -27,7 +27,6 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (302-333): CHC: Assertion violation might happen here.
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (302-333): CHC: Assertion violation might happen here.
 // Warning 4661: (302-333): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/file_level/recursion.sol b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
@@ -25,4 +25,3 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// ----
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
@@ -21,5 +21,5 @@ contract A is B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (200-218): CHC: Assertion violation happens here.
 // Warning 4984: (171-176): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (200-218): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
@@ -19,5 +19,5 @@ contract A is B {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
 // Warning 4984: (166-171): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
+// Warning 4984: (175-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nA.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
@@ -29,6 +29,6 @@ contract A is B2, B1 {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (193-198): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (209-214): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (302-318): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
@@ -14,5 +14,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (129-143): CHC: Assertion violation happens here.
 // Warning 4984: (82-87): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (129-143): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
@@ -21,8 +21,8 @@ contract C{
 // SMTEngine: all
 // ----
 // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
 // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
 // Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
 // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
 // Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
-// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
@@ -21,6 +21,6 @@ contract C{
 // SMTEngine: all
 // ----
 // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
 // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
 // Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call\n    C.g() -- internal call
-// Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
@@ -28,5 +28,5 @@ contract C is B {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
 // Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n    A.f() -- internal call\n        C.v() -- internal call
+// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
@@ -23,6 +23,6 @@ contract A is B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (243-261): CHC: Assertion violation happens here.
 // Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (184-189): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (243-261): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
@@ -23,6 +23,6 @@ contract A is B {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (241-259): CHC: Assertion violation happens here.
 // Warning 4984: (125-131): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (185-190): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (241-259): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol b/test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol
diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp

Original file line number	Diff line number	Diff line change
`@@ -958,7 +958,7 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:`
`958`	`958`	`return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");`
`959`	`959`	`ret.modelCheckerSettings.showUnproved = showUnproved.asBool();`
`960`	`960`	`}`
`961`		`-`
	`961`	`+`
`962`	`962`	`if (modelCheckerSettings.isMember("solvers"))`
`963`	`963`	`{`
`964`	`964`	`auto const& solversArray = modelCheckerSettings["solvers"];`