From d1db41a5c8296b0d7e49943547e189e3802a88a6 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Thu, 25 Mar 2021 15:12:56 +0100
Subject: [PATCH] Fix target warning order nondeterminism

---
 libsolidity/formal/CHC.cpp | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 92ff0254c..f4930d0b9 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -920,10 +920,15 @@ void CHC::setCurrentBlock(Predicate const& _block)
 set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 {
 	set<unsigned> verificationTargetsIds;
-	solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
-		verificationTargetsIds.insert(m_functionTargetIds[function].begin(), m_functionTargetIds[function].end());
-		for (auto const* called: m_callGraph[function])
-		_addChild(called);
+	struct ASTNodeCompare: EncodingContext::IdCompare
+	{
+		bool operator<(ASTNodeCompare _other) const { return operator()(node, _other.node); }
+		ASTNode const* node;
+	};
+	solidity::util::BreadthFirstSearch<ASTNodeCompare>{{{{}, _txRoot}}}.run([&](auto _node, auto&& _addChild) {
+		verificationTargetsIds.insert(m_functionTargetIds[_node.node].begin(), m_functionTargetIds[_node.node].end());
+		for (ASTNode const* called: m_callGraph[_node.node])
+			_addChild({{}, called});
 	});
 	return verificationTargetsIds;
 }