From f249f9c86f1a9673cdc5700b326b3cfeee908851 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 17 Apr 2018 23:46:53 +0200
Subject: [PATCH 1/2] [SMTLib2] Fix repeated declarations

---
 libsolidity/formal/SMTLib2Interface.cpp | 37 +++++++++++++++++--------
 libsolidity/formal/SMTLib2Interface.h   |  3 ++
 2 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 8cac3cc67..a6c1f87c7 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -47,6 +47,8 @@ void SMTLib2Interface::reset()
 {
 	m_accumulatedOutput.clear();
 	m_accumulatedOutput.emplace_back();
+	m_constants.clear();
+	m_functions.clear();
 	write("(set-option :produce-models true)");
 	write("(set-logic QF_UFLIA)");
 }
@@ -64,25 +66,38 @@ void SMTLib2Interface::pop()
 
 void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	write(
-		"(declare-fun |" +
-		_name +
-		"| (" +
-		(_domain == Sort::Int ? "Int" : "Bool") +
-		") " +
-		(_codomain == Sort::Int ? "Int" : "Bool") +
-		")"
-	);
+	// TODO Use domain and codomain as key as well
+	if (!m_functions.count(_name))
+	{
+		m_functions.insert(_name);
+		write(
+			"(declare-fun |" +
+			_name +
+			"| (" +
+			(_domain == Sort::Int ? "Int" : "Bool") +
+			") " +
+			(_codomain == Sort::Int ? "Int" : "Bool") +
+			")"
+		);
+	}
 }
 
 void SMTLib2Interface::declareInteger(string _name)
 {
-	write("(declare-const |" + _name + "| Int)");
+	if (!m_constants.count(_name))
+	{
+		m_constants.insert(_name);
+		write("(declare-const |" + _name + "| Int)");
+	}
 }
 
 void SMTLib2Interface::declareBool(string _name)
 {
-	write("(declare-const |" + _name + "| Bool)");
+	if (!m_constants.count(_name))
+	{
+		m_constants.insert(_name);
+		write("(declare-const |" + _name + "| Bool)");
+	}
 }
 
 void SMTLib2Interface::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 61071fe5a..eb876a7f0 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -30,6 +30,7 @@
 #include <string>
 #include <vector>
 #include <cstdio>
+#include <set>
 
 namespace dev
 {
@@ -68,6 +69,8 @@ private:
 
 	ReadCallback::Callback m_queryCallback;
 	std::vector<std::string> m_accumulatedOutput;
+	std::set<std::string> m_constants;
+	std::set<std::string> m_functions;
 };
 
 }

From 41ac3d6cfb7fedd054f8fbdedf5246ec15670941 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 1 Aug 2018 11:12:56 +0200
Subject: [PATCH 2/2] Remove repeated declarations in Z3 and CVC4 as well

---
 libsolidity/formal/CVC4Interface.cpp | 13 +++++++++----
 libsolidity/formal/Z3Interface.cpp   |  9 ++++++---
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 84d36de0a..6cb914834 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -52,18 +52,23 @@ void CVC4Interface::pop()
 
 void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
-	m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
+	if (!m_functions.count(_name))
+	{
+		CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
+		m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
+	}
 }
 
 void CVC4Interface::declareInteger(string _name)
 {
-	m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
 }
 
 void CVC4Interface::declareBool(string _name)
 {
-	m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
 }
 
 void CVC4Interface::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 784fbd282..747c91725 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -53,17 +53,20 @@ void Z3Interface::pop()
 
 void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
+	if (!m_functions.count(_name))
+		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
 }
 
 void Z3Interface::declareInteger(string _name)
 {
-	m_constants.insert({_name, m_context.int_const(_name.c_str())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.int_const(_name.c_str())});
 }
 
 void Z3Interface::declareBool(string _name)
 {
-	m_constants.insert({_name, m_context.bool_const(_name.c_str())});
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.bool_const(_name.c_str())});
 }
 
 void Z3Interface::addAssertion(Expression const& _expr)