Merge pull request #9227 from a3d4/incorporate-error-codes-into-syntaxtest

Added error codes to SyntaxTest expectations

liblangutil/Exceptions.h

@@ -64,7 +64,11 @@ struct InvalidAstError: virtual util::Exception {};
  * To create a new ID, one can add 0000_error and then run "python ./scripts/fix_error_ids.py"
  * from the root of the repo.
  */
-struct ErrorId { unsigned long long error = 0; };
+struct ErrorId
+{
+	unsigned long long error = 0;
+	bool operator==(ErrorId const& _rhs) const { return error == _rhs.error; }
+};
 constexpr ErrorId operator"" _error(unsigned long long _error) { return ErrorId{ _error }; }
 
 class Error: virtual public util::Exception

test/CommonSyntaxTest.cpp

@@ -165,8 +165,10 @@ void CommonSyntaxTest::printErrorList(
 		{
 			{
 				AnsiColorized scope(_stream, _formatted, {BOLD, (error.type == "Warning") ? YELLOW : RED});
-				_stream << _linePrefix;
-				_stream << error.type << ": ";
+				_stream << _linePrefix << error.type;
+				if (error.errorId.has_value())
+					_stream << ' ' << error.errorId->error;
+				_stream << ": ";
 			}
 			if (!error.sourceName.empty() || error.locationStart >= 0 || error.locationEnd >= 0)
 			{
@@ -206,13 +208,17 @@ vector<SyntaxTestError> CommonSyntaxTest::parseExpectations(istream& _stream)
 		if (it == line.end()) continue;
 
 		auto typeBegin = it;
-		while (it != line.end() && *it != ':')
+		while (it != line.end() && isalpha(*it))
 			++it;
 		string errorType(typeBegin, it);
 
-		// skip colon
-		if (it != line.end()) it++;
+		skipWhitespace(it, line.end());
 
+		optional<ErrorId> errorId;
+		if (it != line.end() && isdigit(*it))
+			errorId = ErrorId{static_cast<unsigned long long>(parseUnsignedInteger(it, line.end()))};
+
+		expect(it, line.end(), ':');
 		skipWhitespace(it, line.end());
 
 		int locationStart = -1;
@@ -242,6 +248,7 @@ vector<SyntaxTestError> CommonSyntaxTest::parseExpectations(istream& _stream)
 		string errorMessage(it, line.end());
 		expectations.emplace_back(SyntaxTestError{
 			move(errorType),
+			move(errorId),
 			move(errorMessage),
 			move(sourceName),
 			locationStart,

test/CommonSyntaxTest.h

@@ -33,6 +33,7 @@ namespace solidity::test
 struct SyntaxTestError
 {
 	std::string type;
+	std::optional<langutil::ErrorId> errorId;
 	std::string message;
 	std::string sourceName;
 	int locationStart = -1;
@@ -40,6 +41,7 @@ struct SyntaxTestError
 	bool operator==(SyntaxTestError const& _rhs) const
 	{
 		return type == _rhs.type &&
+			errorId == _rhs.errorId &&
 			message == _rhs.message &&
 			sourceName == _rhs.sourceName &&
 			locationStart == _rhs.locationStart &&

test/libsolidity/SMTCheckerJSONTest.cpp

@@ -127,6 +127,7 @@ TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _li
 				end -= preamble.size();
 			m_errorList.emplace_back(SyntaxTestError{
 				error["type"].asString(),
+				error["errorId"].isNull() ?  nullopt : optional<langutil::ErrorId>(langutil::ErrorId{error["errorId"].asUInt()}),
 				error["message"].asString(),
 				sourceName,
 				static_cast<int>(start),

test/libsolidity/SyntaxTest.cpp

@@ -79,6 +79,7 @@ void SyntaxTest::parseAndAnalyze()
 		{
 			m_errorList.emplace_back(SyntaxTestError{
 				"UnimplementedFeatureError",
+				nullopt,
 				errorMessage(_e),
 				"",
 				-1,
@@ -106,6 +107,7 @@ void SyntaxTest::filterObtainedErrors()
 		}
 		m_errorList.emplace_back(SyntaxTestError{
 			currentError->typeName(),
+			currentError->errorId(),
 			errorMessage(*currentError),
 			sourceName,
 			locationStart,

test/libsolidity/errorRecoveryTests/constructor_recovers.sol

@@ -16,5 +16,5 @@ contract Error1 {
   }
 }
 // ----
-// ParserError: (95-96): Expected primary expression.
-// Warning: (95-96): Recovered in Statement at ';'.
+// ParserError 6933: (95-96): Expected primary expression.
+// Warning 3347: (95-96): Recovered in Statement at ';'.

test/libsolidity/errorRecoveryTests/contract_recovery.sol

@@ -3,5 +3,5 @@ contract Errort6 {
 }
 
 // ----
-// ParserError: (36-37): Expected type name
-// Warning: (59-60): Recovered in ContractDefinition at '}'.
+// ParserError 3546: (36-37): Expected type name
+// Warning 3796: (59-60): Recovered in ContractDefinition at '}'.

test/libsolidity/errorRecoveryTests/do_not_delete_at_error.sol

@@ -10,4 +10,4 @@ contract Error2 {
 	mapping (address => uint balances; // missing ) before "balances"
 }
 // ----
-// ParserError: (417-425): Expected ')' but got identifier
+// ParserError 6635: (417-425): Expected ')' but got identifier

test/libsolidity/errorRecoveryTests/error_to_eos.sol

@@ -17,7 +17,7 @@ contract SendCoin {
 }
 
 // ----
-// ParserError: (212-220): Expected ')' but got identifier
-// ParserError: (220-221): Expected ';' but got ')'
-// ParserError: (220-221): Function, variable, struct or modifier declaration expected.
-// Warning: (235-236): Recovered in ContractDefinition at '}'.
+// ParserError 6635: (212-220): Expected ')' but got identifier
+// ParserError 6635: (220-221): Expected ';' but got ')'
+// ParserError 9182: (220-221): Function, variable, struct or modifier declaration expected.
+// Warning 3796: (235-236): Recovered in ContractDefinition at '}'.

test/libsolidity/errorRecoveryTests/missing_rhs.sol

@@ -7,5 +7,5 @@ contract Error3 {
 
 }
 // ----
-// ParserError: (95-96): Expected primary expression.
-// Warning: (95-96): Recovered in Statement at ';'.
+// ParserError 6933: (95-96): Expected primary expression.
+// Warning 3347: (95-96): Recovered in Statement at ';'.

test/libsolidity/errorRecoveryTests/multiple_errors.sol

@@ -21,9 +21,9 @@ contract Error4 {
 
 }
 // ----
-// ParserError: (249-250): Expected ';' but got 'Number'
-// ParserError: (471-479): Expected ';' but got identifier
-// ParserError: (529-533): Expected ';' but got 'emit'
-// ParserError: (577-583): Expected ',' but got 'return'
-// ParserError: (577-583): Expected primary expression.
-// Warning: (588-589): Recovered in Statement at ';'.
+// ParserError 6635: (249-250): Expected ';' but got 'Number'
+// ParserError 6635: (471-479): Expected ';' but got identifier
+// ParserError 6635: (529-533): Expected ';' but got 'emit'
+// ParserError 6635: (577-583): Expected ',' but got 'return'
+// ParserError 6933: (577-583): Expected primary expression.
+// Warning 3796: (588-589): Recovered in Statement at ';'.

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol

@@ -11,10 +11,10 @@ contract C {
 	}
 }
 // ----
-// Warning: (76-80): Assertion checker does not yet support the type of this variable.
-// Warning: (83-87): Assertion checker does not yet support the type of this variable.
-// Warning: (126-132): Assertion checker does not yet support this expression.
-// Warning: (126-128): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (143-149): Assertion checker does not yet support this expression.
-// Warning: (143-145): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (119-157): Assertion violation happens here
+// Warning 8115: (76-80): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (83-87): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (126-132): Assertion checker does not yet support this expression.
+// Warning 8364: (126-128): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (143-149): Assertion checker does not yet support this expression.
+// Warning 8364: (143-145): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4661: (119-157): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol

@@ -11,12 +11,12 @@ contract C {
 	}
 }
 // ----
-// Warning: (78-82): Assertion checker does not yet support the type of this variable.
-// Warning: (85-89): Assertion checker does not yet support the type of this variable.
-// Warning: (128-134): Assertion checker does not yet support this expression.
-// Warning: (128-130): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (128-137): Assertion checker does not yet implement this expression.
-// Warning: (148-154): Assertion checker does not yet support this expression.
-// Warning: (148-150): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (148-157): Assertion checker does not yet implement this expression.
-// Warning: (121-165): Assertion violation happens here
+// Warning 8115: (78-82): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (85-89): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (128-134): Assertion checker does not yet support this expression.
+// Warning 8364: (128-130): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 9118: (128-137): Assertion checker does not yet implement this expression.
+// Warning 7650: (148-154): Assertion checker does not yet support this expression.
+// Warning 8364: (148-150): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 9118: (148-157): Assertion checker does not yet implement this expression.
+// Warning 4661: (121-165): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_basic.sol

@@ -10,4 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (153-176): Assertion violation happens here
+// Warning 4661: (153-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol

@@ -14,6 +14,6 @@ contract C {
 	}
 }
 // ----
-// Warning: (198-224): Assertion violation happens here
-// Warning: (228-254): Assertion violation happens here
-// Warning: (258-281): Assertion violation happens here
+// Warning 4661: (198-224): Assertion violation happens here
+// Warning 4661: (228-254): Assertion violation happens here
+// Warning 4661: (258-281): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol

@@ -16,7 +16,7 @@ contract C {
 	}
 }
 // ----
-// Warning: (222-248): Assertion violation happens here
-// Warning: (252-278): Assertion violation happens here
-// Warning: (282-305): Assertion violation happens here
-// Warning: (309-335): Assertion violation happens here
+// Warning 4661: (222-248): Assertion violation happens here
+// Warning 4661: (252-278): Assertion violation happens here
+// Warning 4661: (282-305): Assertion violation happens here
+// Warning 4661: (309-335): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (82-89): Empty array "pop" detected here.
+// Warning 2529: (82-89): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (111-121): Empty array "pop" detected here.
+// Warning 2529: (111-121): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol

@@ -7,4 +7,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (83-90): Empty array "pop" detected here.
+// Warning 2529: (83-90): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol

@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (150-157): Empty array "pop" detected here.
+// Warning 2529: (150-157): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol

@@ -10,5 +10,5 @@ contract C {
 	}
 }
 // ----
-// Warning: (162-177): Underflow (resulting value less than 0) happens here
-// Warning: (150-184): Assertion violation happens here
+// Warning 4144: (162-177): Underflow (resulting value less than 0) happens here
+// Warning 4661: (150-184): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol

@@ -12,5 +12,5 @@ contract C {
 	}
 }
 // ----
-// Warning: (217-232): Underflow (resulting value less than 0) happens here
-// Warning: (205-239): Assertion violation happens here
+// Warning 4144: (217-232): Underflow (resulting value less than 0) happens here
+// Warning 4661: (205-239): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

@@ -12,4 +12,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (167-188): Assertion violation happens here
+// Warning 4661: (167-188): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol

@@ -18,6 +18,6 @@ contract C {
 	}
 }
 // ----
-// Warning: (193-217): Assertion violation happens here
-// Warning: (309-333): Assertion violation happens here
-// Warning: (419-436): Assertion violation happens here
+// Warning 4661: (193-217): Assertion violation happens here
+// Warning 4661: (309-333): Assertion violation happens here
+// Warning 4661: (419-436): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol

@@ -15,13 +15,13 @@ contract C {
 }
 
 // ----
-// Warning: (72-75): Assertion checker does not yet support the type of this variable.
-// Warning: (100-103): Assertion checker does not yet support the type of this variable.
-// Warning: (130-133): Assertion checker does not yet support this expression.
-// Warning: (130-131): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (130-133): Assertion checker does not yet implement this expression.
-// Warning: (144-149): Assertion checker does not yet support this expression.
-// Warning: (144-147): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (144-147): Assertion checker does not yet support this expression.
-// Warning: (144-145): Assertion checker does not yet implement type struct C.T storage ref
-// Warning: (144-149): Assertion checker does not yet implement this expression.
+// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (100-103): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (130-133): Assertion checker does not yet support this expression.
+// Warning 8364: (130-131): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 9599: (130-133): Assertion checker does not yet implement this expression.
+// Warning 7650: (144-149): Assertion checker does not yet support this expression.
+// Warning 8364: (144-147): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (144-147): Assertion checker does not yet support this expression.
+// Warning 8364: (144-145): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 9599: (144-149): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol

@@ -16,18 +16,18 @@ contract C {
 }
 
 // ----
-// Warning: (72-75): Assertion checker does not yet support the type of this variable.
-// Warning: (102-105): Assertion checker does not yet support the type of this variable.
-// Warning: (132-135): Assertion checker does not yet support this expression.
-// Warning: (132-133): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (132-135): Assertion checker does not yet implement this expression.
-// Warning: (146-149): Assertion checker does not yet support this expression.
-// Warning: (146-147): Assertion checker does not yet implement type struct C.T storage ref
-// Warning: (146-156): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (146-149): Assertion checker does not yet implement this expression.
-// Warning: (160-168): Assertion checker does not yet support this expression.
-// Warning: (160-163): Assertion checker does not yet support this expression.
-// Warning: (160-161): Assertion checker does not yet implement type struct C.T storage ref
-// Warning: (160-166): Assertion checker does not yet implement type struct C.S storage ref
-// Warning: (160-166): Assertion checker does not yet implement this expression.
-// Warning: (160-168): Assertion checker does not yet implement this expression.
+// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (102-105): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (132-135): Assertion checker does not yet support this expression.
+// Warning 8364: (132-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 9599: (132-135): Assertion checker does not yet implement this expression.
+// Warning 7650: (146-149): Assertion checker does not yet support this expression.
+// Warning 8364: (146-147): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (146-156): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 9599: (146-149): Assertion checker does not yet implement this expression.
+// Warning 7650: (160-168): Assertion checker does not yet support this expression.
+// Warning 7650: (160-163): Assertion checker does not yet support this expression.
+// Warning 8364: (160-161): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (160-166): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 9118: (160-166): Assertion checker does not yet implement this expression.
+// Warning 9599: (160-168): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (111-144): Assertion violation happens here
+// Warning 4661: (111-144): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

@@ -8,4 +8,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (94-124): Assertion violation happens here
+// Warning 4661: (94-124): Assertion violation happens here

test/libsolidity/smtCheckerTests/complex/MerkleProof.sol

@@ -34,7 +34,7 @@ library MerkleProof {
 }
 
 // ----
-// Warning: (988-991): Assertion checker does not yet implement type abi
-// Warning: (988-1032): Assertion checker does not yet implement this type of function call.
-// Warning: (1175-1178): Assertion checker does not yet implement type abi
-// Warning: (1175-1219): Assertion checker does not yet implement this type of function call.
+// Warning 8364: (988-991): Assertion checker does not yet implement type abi
+// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call.
+// Warning 8364: (1175-1178): Assertion checker does not yet implement type abi
+// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol

@@ -51,7 +51,7 @@ contract MyConc{
 
 }
 // ----
-// Warning: (773-792): This declaration shadows an existing declaration.
-// Warning: (1009-1086): Function state mutability can be restricted to view
-// Warning: (985-1002): Underflow (resulting value less than 0) happens here.
-// Warning: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2519: (773-792): This declaration shadows an existing declaration.
+// Warning 2018: (1009-1086): Function state mutability can be restricted to view
+// Warning 6084: (985-1002): Underflow (resulting value less than 0) happens here.
+// Warning 6084: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol

@@ -117,23 +117,23 @@ contract PropagateThroughReturnValue {
   }
 }
 // ----
-// Warning: (1886-1954): Function state mutability can be restricted to view
-// Warning: (318-332): Assertion checker does not yet support the type of this variable.
-// Warning: (338-347): Assertion checker does not yet support the type of this variable.
-// Warning: (353-378): Assertion checker does not yet support the type of this variable.
-// Warning: (384-409): Assertion checker does not yet support the type of this variable.
-// Warning: (464-479): Assertion checker does not yet support this expression.
-// Warning: (464-475): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning: (464-494): Assertion checker does not yet implement such assignments.
-// Warning: (539-554): Assertion checker does not yet support this expression.
-// Warning: (539-550): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning: (557-567): Assertion checker does not yet support this expression.
-// Warning: (557-563): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning: (539-567): Assertion checker does not yet implement such assignments.
-// Warning: (629-643): Assertion checker does not yet support the type of this variable.
-// Warning: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref
-// Warning: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer
-// Warning: (748-755): Assertion checker does not yet support this expression.
-// Warning: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer
-// Warning: (748-770): Assertion checker does not yet implement such assignments.
+// Warning 2018: (1886-1954): Function state mutability can be restricted to view
+// Warning 8115: (318-332): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (338-347): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (353-378): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (384-409): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (464-479): Assertion checker does not yet support this expression.
+// Warning 8364: (464-475): Assertion checker does not yet implement type struct Reference.St storage ref
+// Warning 8182: (464-494): Assertion checker does not yet implement such assignments.
+// Warning 7650: (539-554): Assertion checker does not yet support this expression.
+// Warning 8364: (539-550): Assertion checker does not yet implement type struct Reference.St storage ref
+// Warning 7650: (557-567): Assertion checker does not yet support this expression.
+// Warning 8364: (557-563): Assertion checker does not yet implement type struct Reference.St storage ref
+// Warning 8182: (539-567): Assertion checker does not yet implement such assignments.
+// Warning 8115: (629-643): Assertion checker does not yet support the type of this variable.
+// Warning 8364: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref
+// Warning 8364: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref
+// Warning 8364: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer
+// Warning 7650: (748-755): Assertion checker does not yet support this expression.
+// Warning 8364: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer
+// Warning 8182: (748-770): Assertion checker does not yet implement such assignments.

test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

@@ -73,17 +73,17 @@ contract InternalCall {
 
 }
 // ----
-// Warning: (760-815): Return value of low-level calls not used.
-// Warning: (117-126): Unused local variable.
-// Warning: (260-269): Unused local variable.
-// Warning: (667-676): Unused local variable.
-// Warning: (75-137): Function state mutability can be restricted to pure
-// Warning: (218-280): Function state mutability can be restricted to pure
-// Warning: (470-539): Function state mutability can be restricted to pure
-// Warning: (1144-1206): Function state mutability can be restricted to pure
-// Warning: (1212-1274): Function state mutability can be restricted to pure
-// Warning: (1280-1342): Function state mutability can be restricted to pure
-// Warning: (771-774): Assertion checker does not yet implement type abi
-// Warning: (782-813): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (771-814): Assertion checker does not yet implement this type of function call.
-// Warning: (1403-1408): Assertion checker does not yet implement this type of function call.
+// Warning 9302: (760-815): Return value of low-level calls not used.
+// Warning 2072: (117-126): Unused local variable.
+// Warning 2072: (260-269): Unused local variable.
+// Warning 2072: (667-676): Unused local variable.
+// Warning 2018: (75-137): Function state mutability can be restricted to pure
+// Warning 2018: (218-280): Function state mutability can be restricted to pure
+// Warning 2018: (470-539): Function state mutability can be restricted to pure
+// Warning 2018: (1144-1206): Function state mutability can be restricted to pure
+// Warning 2018: (1212-1274): Function state mutability can be restricted to pure
+// Warning 2018: (1280-1342): Function state mutability can be restricted to pure
+// Warning 8364: (771-774): Assertion checker does not yet implement type abi
+// Warning 5084: (782-813): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol

@@ -7,8 +7,8 @@ contract C {
     }
 }
 // ----
-// Warning: (133-143): Unused local variable.
-// Warning: (133-143): Assertion checker does not yet support the type of this variable.
-// Warning: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
-// Warning: (146-163): Assertion checker does not yet implement type struct C.A memory
-// Warning: (146-163): Assertion checker does not yet implement this expression.
+// Warning 2072: (133-143): Unused local variable.
+// Warning 8115: (133-143): Assertion checker does not yet support the type of this variable.
+// Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
+// Warning 8364: (146-163): Assertion checker does not yet implement type struct C.A memory
+// Warning 4639: (146-163): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol

@@ -5,4 +5,4 @@ contract C {
     }
 }
 // ----
-// Warning: (106-114): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (106-114): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol

@@ -15,6 +15,6 @@ contract C
 	}
 }
 // ----
-// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (208-218): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (208-218): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol

@@ -20,8 +20,8 @@ contract C
 	}
 }
 // ----
-// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (186-196): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (186-196): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (271-281): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol

@@ -20,8 +20,8 @@ contract C
 	}
 }
 // ----
-// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (189-199): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol

@@ -25,7 +25,7 @@ contract C
 
 }
 // ----
-// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (189-199): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (275-285): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol

@@ -16,6 +16,6 @@ contract C
 	}
 }
 // ----
-// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (134-144): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (219-229): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (134-144): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (219-229): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol

@@ -19,6 +19,6 @@ contract C
 	}
 }
 // ----
-// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (118-128): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (249-259): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (118-128): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (249-259): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol

@@ -20,6 +20,6 @@ contract C
 	}
 }
 // ----
-// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (162-172): Type conversion is not yet fully supported and might yield false positives.
-// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (247-257): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (162-172): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (247-257): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (227-236): Assertion violation happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (227-236): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -17,6 +17,6 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (202-218): Assertion violation happens here
-// Warning: (242-252): Assertion violation happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (202-218): Assertion violation happens here
+// Warning 4661: (242-252): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (225-235): Assertion violation happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_touched.sol

@@ -12,8 +12,8 @@ contract C
 	}
 }
 // ----
-// Warning: (84-110): Condition is always false.
-// Warning: (121-147): Condition is always true.
-// Warning: (158-183): Condition is always false.
-// Warning: (194-221): Condition is always false.
-// Warning: (232-247): Condition is always true.
+// Warning 6838: (84-110): Condition is always false.
+// Warning 6838: (121-147): Condition is always true.
+// Warning 6838: (158-183): Condition is always false.
+// Warning 6838: (194-221): Condition is always false.
+// Warning 6838: (232-247): Condition is always true.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_touched_function.sol

@@ -16,8 +16,8 @@ contract C
 	}
 }
 // ----
-// Warning: (156-179): Condition is always false.
-// Warning: (190-213): Condition is always true.
-// Warning: (224-243): Condition is always false.
-// Warning: (254-277): Condition is always false.
-// Warning: (288-300): Condition is always true.
+// Warning 6838: (156-179): Condition is always false.
+// Warning 6838: (190-213): Condition is always true.
+// Warning 6838: (224-243): Condition is always false.
+// Warning 6838: (254-277): Condition is always false.
+// Warning 6838: (288-300): Condition is always true.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (225-235): Assertion violation happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol

@@ -24,5 +24,5 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (360-370): Assertion violation happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (360-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol

@@ -15,4 +15,4 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol

@@ -15,5 +15,5 @@ contract c {
 	}
 }
 // ----
-// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (225-235): Assertion violation happens here
+// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_touched.sol

@@ -12,8 +12,8 @@ contract C
 	}
 }
 // ----
-// Warning: (84-110): Condition is always true.
-// Warning: (121-147): Condition is always true.
-// Warning: (158-183): Condition is always true.
-// Warning: (194-221): Condition is always true.
-// Warning: (232-248): Condition is always false.
+// Warning 6838: (84-110): Condition is always true.
+// Warning 6838: (121-147): Condition is always true.
+// Warning 6838: (158-183): Condition is always true.
+// Warning 6838: (194-221): Condition is always true.
+// Warning 6838: (232-248): Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_touched_function.sol

@@ -16,8 +16,8 @@ contract C
 	}
 }
 // ----
-// Warning: (156-179): Condition is always true.
-// Warning: (190-213): Condition is always true.
-// Warning: (224-243): Condition is always true.
-// Warning: (254-277): Condition is always true.
-// Warning: (288-301): Condition is always false.
+// Warning 6838: (156-179): Condition is always true.
+// Warning 6838: (190-213): Condition is always true.
+// Warning 6838: (224-243): Condition is always true.
+// Warning 6838: (254-277): Condition is always true.
+// Warning 6838: (288-301): Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol

@@ -8,5 +8,5 @@ contract C {
 // ====
 // EVMVersion: >=byzantium
 // ----
-// Warning: (98-121): Assertion checker does not support try/catch clauses.
-// Warning: (124-159): Assertion checker does not support try/catch clauses.
+// Warning 7645: (98-121): Assertion checker does not support try/catch clauses.
+// Warning 7645: (124-159): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol

@@ -10,5 +10,5 @@ contract C {
 // ====
 // EVMVersion: >=byzantium
 // ----
-// Warning: (83-85): Assertion checker does not support try/catch clauses.
-// Warning: (88-122): Assertion checker does not support try/catch clauses.
+// Warning 7645: (83-85): Assertion checker does not support try/catch clauses.
+// Warning 7645: (88-122): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (159-173): Assertion violation happens here
+// Warning 4661: (159-173): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (159-173): Assertion violation happens here
+// Warning 4661: (159-173): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol

@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (161-175): Assertion violation happens here
+// Warning 4661: (161-175): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol

@@ -5,7 +5,7 @@ contract C {
     }
 }
 // ----
-// Warning: (162-165): Assertion checker does not yet implement type abi
-// Warning: (162-176): Assertion checker does not yet implement this type of function call.
-// Warning: (178-181): Assertion checker does not yet implement type abi
-// Warning: (178-203): Assertion checker does not yet implement this type of function call.
+// Warning 8364: (162-165): Assertion checker does not yet implement type abi
+// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call.
+// Warning 8364: (178-181): Assertion checker does not yet implement type abi
+// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol

@@ -13,4 +13,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning: (166-180): Assertion violation happens here
+// Warning 4661: (166-180): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol

@@ -4,4 +4,4 @@ contract A is C { constructor() C(2) public { assert(a == 2); } }
 contract B is C { constructor() C(3) public { assert(a == 3); } }
 contract J is C { constructor() C(3) public { assert(a == 4); } }
 // ----
-// Warning: (271-285): Assertion violation happens here
+// Warning 4661: (271-285): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -19,6 +19,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (265-270): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (253-271): Assertion violation happens here
+// Warning 2661: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (265-270): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (253-271): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol

@@ -18,6 +18,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (221-226): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (212-217): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (251-256): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (221-226): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (212-217): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (251-256): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol

@@ -25,7 +25,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (330-348): Assertion violation happens here
+// Warning 2661: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (330-348): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol

@@ -25,7 +25,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (330-348): Assertion violation happens here
+// Warning 2661: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (330-348): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -27,11 +27,11 @@ contract A is B2, B1 {
 	}
 }
 // ----
-// Warning: (174-179): Underflow (resulting value less than 0) happens here
-// Warning: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (362-378): Assertion violation happens here
+// Warning 4144: (174-179): Underflow (resulting value less than 0) happens here
+// Warning 2661: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (362-378): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol

@@ -19,5 +19,5 @@ contract A is B, B2 {
 	}
 }
 // ----
-// Warning: (171-177): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning: (208-222): Assertion violation happens here
+// Warning 5667: (171-177): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 4661: (208-222): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol

@@ -18,5 +18,5 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (201-207): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning: (238-252): Assertion violation happens here
+// Warning 5667: (201-207): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 4661: (238-252): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol

@@ -16,5 +16,5 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning: (186-200): Assertion violation happens here
+// Warning 5667: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 4661: (186-200): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol

@@ -15,5 +15,5 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning: (164-178): Assertion violation happens here
+// Warning 5667: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 4661: (164-178): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol

@@ -26,5 +26,5 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (275-281): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning: (312-326): Assertion violation happens here
+// Warning 5667: (275-281): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 4661: (312-326): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol

@@ -31,5 +31,5 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (317-323): Unused function parameter. Remove or comment out the variable name to silence this warning.
-// Warning: (385-400): Assertion violation happens here
+// Warning 5667: (317-323): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 4661: (385-400): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol

@@ -25,6 +25,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (356-370): Assertion violation happens here
+// Warning 2661: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 2661: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (356-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol

@@ -23,5 +23,5 @@ contract B is C {
 contract A is B {
 }
 // ----
-// Warning: (287-301): Assertion violation happens here
-// Warning: (287-301): Assertion violation happens here
+// Warning 4661: (287-301): Assertion violation happens here
+// Warning 4661: (287-301): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol

@@ -14,4 +14,4 @@ contract A is C {
 	}
 }
 // ----
-// Warning: (202-216): Assertion violation happens here
+// Warning 4661: (202-216): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol

@@ -13,5 +13,5 @@ contract A is C {
 	}
 }
 // ----
-// Warning: (148-162): Assertion violation happens here
-// Warning: (166-182): Assertion violation happens here
+// Warning 4661: (148-162): Assertion violation happens here
+// Warning 4661: (166-182): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_simple.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (148-162): Assertion violation happens here
+// Warning 4661: (148-162): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning: (152-166): Assertion violation happens here
+// Warning 4661: (152-166): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol

@@ -15,4 +15,4 @@ contract C is B {
 	}
 }
 // ----
-// Warning: (172-186): Assertion violation happens here
+// Warning 4661: (172-186): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol

@@ -13,5 +13,5 @@ contract C {
 	}
 }
 // ----
-// Warning: (169-183): Assertion violation happens here
-// Warning: (122-127): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (169-183): Assertion violation happens here
+// Warning 2661: (122-127): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/constructor_this.sol

@@ -9,5 +9,5 @@ contract C {
     }
 }
 // ----
-// Warning: (204-208): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.
-// Warning: (223-227): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.
+// Warning 5805: (204-208): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.
+// Warning 5805: (223-227): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.

test/libsolidity/smtCheckerTests/functions/function_call_state_var_init.sol

@@ -9,5 +9,5 @@ contract C {
 	}
 }
 // ----
-// Warning: (116-132): Assertion violation happens here
-// Warning: (116-132): Assertion violation happens here
+// Warning 4661: (116-132): Assertion violation happens here
+// Warning 4661: (116-132): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol

@@ -16,4 +16,4 @@ contract C
 	}
 }
 // ----
-// Warning: (209-223): Assertion violation happens here
+// Warning 4661: (209-223): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol

@@ -24,5 +24,5 @@ contract C
 
 }
 // ----
-// Warning: (209-223): Assertion violation happens here
-// Warning: (321-335): Assertion violation happens here
+// Warning 4661: (209-223): Assertion violation happens here
+// Warning 4661: (321-335): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol

@@ -18,4 +18,4 @@ contract C
 	}
 }
 // ----
-// Warning: (261-277): Assertion violation happens here
+// Warning 4661: (261-277): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_1.sol

@@ -17,4 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning: (257-271): Assertion violation happens here
+// Warning 4661: (257-271): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_2.sol

@@ -17,4 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning: (297-321): Assertion violation happens here
+// Warning 4661: (297-321): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_3.sol

@@ -18,4 +18,4 @@ contract C
 	}
 }
 // ----
-// Warning: (355-379): Assertion violation happens here
+// Warning 4661: (355-379): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -16,4 +16,4 @@ contract D
 	}
 }
 // ----
-// Warning: (191-206): Assertion violation happens here
+// Warning 4661: (191-206): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol

@@ -12,4 +12,4 @@ contract C
 }
 
 // ----
-// Warning: (161-174): Assertion violation happens here
+// Warning 4661: (161-174): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol

@@ -16,4 +16,4 @@ contract C
 }
 
 // ----
-// Warning: (229-242): Assertion violation happens here
+// Warning 4661: (229-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol

@@ -12,4 +12,4 @@ contract C
 }
 
 // ----
-// Warning: (163-176): Assertion violation happens here
+// Warning 4661: (163-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_library_1.sol

@@ -17,4 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning: (228-229): Assertion checker does not yet implement type type(library L)
+// Warning 8364: (228-229): Assertion checker does not yet implement type type(library L)

test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol

@@ -17,5 +17,5 @@ contract C
 	}
 }
 // ----
-// Warning: (228-229): Assertion checker does not yet implement type type(library L)
-// Warning: (245-261): Assertion violation happens here
+// Warning 8364: (228-229): Assertion checker does not yet implement type type(library L)
+// Warning 4661: (245-261): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol

@@ -13,4 +13,4 @@ contract C
 }
 
 // ----
-// Warning: (144-157): Assertion violation happens here
+// Warning 4661: (144-157): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol

@@ -14,4 +14,4 @@ contract C
 }
 
 // ----
-// Warning: (152-165): Assertion violation happens here
+// Warning 4661: (152-165): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol

@@ -5,4 +5,4 @@ contract C
 	function f(bool x) public pure { require(x); for (;x;) {} }
 }
 // ----
-// Warning: (98-99): Condition is always true.
+// Warning 6838: (98-99): Condition is always true.

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol

@@ -4,4 +4,4 @@ contract C
 	function f(bool x) public pure { require(x); if (x) {} }
 }
 // ----
-// Warning: (95-96): Condition is always true.
+// Warning 6838: (95-96): Condition is always true.