From 4aebdcc4424e7cfe69b3bcb6a1f04c932de419bd Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 3 Jul 2019 16:16:42 +0200
Subject: [PATCH] [SMTChecker] Allow FunctionSort to be created via sort and
 not type

---
 libsolidity/formal/SymbolicVariables.cpp | 16 ++++++++++++++++
 libsolidity/formal/SymbolicVariables.h   |  7 +++++++
 2 files changed, 23 insertions(+)

diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index aa02e3b24..d7625ed9d 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -68,6 +68,11 @@ Expression SymbolicVariable::valueAtIndex(int _index) const
 	return m_context.newVariable(uniqueSymbol(_index), m_sort);
 }
 
+string SymbolicVariable::nameAtIndex(int _index) const
+{
+	return uniqueSymbol(_index);
+}
+
 string SymbolicVariable::uniqueSymbol(unsigned _index) const
 {
 	return m_uniqueName + "_" + to_string(_index);
@@ -127,6 +132,17 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
 	solAssert(m_type->category() == solidity::Type::Category::Function, "");
 }
 
+SymbolicFunctionVariable::SymbolicFunctionVariable(
+	SortPointer _sort,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(move(_sort), move(_uniqueName), _context),
+	m_declaration(m_context.newVariable(currentName(), m_sort))
+{
+	solAssert(m_sort->kind == Kind::Function, "");
+}
+
 void SymbolicFunctionVariable::resetDeclaration()
 {
 	m_declaration = m_context.newVariable(currentName(), m_sort);
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index f83936e47..7d65a1aa3 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -54,6 +54,7 @@ public:
 	Expression currentValue() const;
 	std::string currentName() const;
 	virtual Expression valueAtIndex(int _index) const;
+	virtual std::string nameAtIndex(int _index) const;
 	virtual Expression increaseIndex();
 	virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
 	{
@@ -63,6 +64,7 @@ public:
 	unsigned index() const { return m_ssa->index(); }
 	unsigned& index() { return m_ssa->index(); }
 
+	SortPointer const& sort() const { return m_sort; }
 	solidity::TypePointer const& type() const { return m_type; }
 
 protected:
@@ -139,6 +141,11 @@ public:
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
+	SymbolicFunctionVariable(
+		SortPointer _sort,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
 
 	Expression increaseIndex();
 	Expression operator()(std::vector<Expression> _arguments) const;