Merge pull request #16147 from radik878/opinashnev

[SMTChecker] Fix comparison of `CHCVerificationTarget` for proper `std::set` ordering

Author: blishko

libsolidity/formal/CHC.h

@@ -74,18 +74,10 @@ class CHC: public SMTEncoder
 
 		friend bool operator<(CHCVerificationTarget const& _a, CHCVerificationTarget const& _b)
 		{
-			return _a.errorId < _b.errorId;
-		}
-	};
-
-	struct SafeTargetsCompare
-	{
-		bool operator()(CHCVerificationTarget const & _lhs, CHCVerificationTarget const & _rhs) const
-		{
-			if (_lhs.errorNode->id() == _rhs.errorNode->id())
-				return _lhs.type  < _rhs.type;
+			if (_a.errorNode->id() == _b.errorNode->id())
+				return _a.type < _b.type;
 			else
-				return _lhs.errorNode->id() == _rhs.errorNode->id();
+				return _a.errorNode->id() < _b.errorNode->id();
 		}
 	};
 
@@ -96,7 +88,7 @@ class CHC: public SMTEncoder
 		std::string message;
 	};
 
-	std::map<ASTNode const*, std::set<CHCVerificationTarget, SafeTargetsCompare>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
 	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; }
 
 	/// This is used if the Horn solver is not directly linked into this binary.
@@ -434,7 +426,7 @@ class CHC: public SMTEncoder
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
 	/// Targets proved safe.
-	std::map<ASTNode const*, std::set<CHCVerificationTarget, SafeTargetsCompare>, smt::EncodingContext::IdCompare> m_safeTargets;
+	std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> m_safeTargets;
 	/// Targets proved unsafe.
 	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
 	/// Targets not proved.