From a3c386191ebc9c0be40ab453712ba2be18cdaec6 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Wed, 22 Jun 2022 16:12:38 +0200
Subject: [PATCH] Add variable type to smt unique name

---
 libsolidity/ast/AST.cpp                | 17 +++++++++++++++++
 libsolidity/ast/AST.h                  |  1 +
 libsolidity/formal/EncodingContext.cpp | 14 +++++++++++++-
 3 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index 04c47a155..326377e44 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -685,6 +685,23 @@ bool VariableDeclaration::isLocalOrReturn() const
 	return isReturnParameter() || (isLocalVariable() && !isCallableOrCatchParameter());
 }
 
+bool VariableDeclaration::isInputParameter() const
+{
+	vector<ASTPointer<VariableDeclaration>> const* parameters = nullptr;
+
+	if (auto const* funTypeName = dynamic_cast<FunctionTypeName const*>(scope()))
+		parameters = &funTypeName->parameterTypes();
+	else if (auto const* callable = dynamic_cast<CallableDeclaration const*>(scope()))
+		parameters = &callable->parameters();
+
+	if (parameters)
+		for (auto const& variable: *parameters)
+			if (variable.get() == this)
+				return true;
+	return false;
+}
+
+
 bool VariableDeclaration::isReturnParameter() const
 {
 	vector<ASTPointer<VariableDeclaration>> const* returnParameters = nullptr;
diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h
index 4eba73c5d..1122ac954 100644
--- a/libsolidity/ast/AST.h
+++ b/libsolidity/ast/AST.h
@@ -1052,6 +1052,7 @@ public:
 	bool isCallableOrCatchParameter() const;
 	/// @returns true if this variable is a return parameter of a function.
 	bool isReturnParameter() const;
+	bool isInputParameter() const;
 	/// @returns true if this variable is a parameter of the success or failure clausse
 	/// of a try/catch statement.
 	bool isTryCatchParameter() const;
diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp
index f9edd7db3..f749082bb 100644
--- a/libsolidity/formal/EncodingContext.cpp
+++ b/libsolidity/formal/EncodingContext.cpp
@@ -61,7 +61,19 @@ bool EncodingContext::createVariable(frontend::VariableDeclaration const& _varDe
 {
 	solAssert(!knownVariable(_varDecl), "");
 	auto const& type = _varDecl.type();
-	auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *this);
+	unsigned varType;
+	if (_varDecl.isStateVariable())
+		varType = 0;
+	else if (_varDecl.isInputParameter())
+		varType = 1;
+	else if (_varDecl.isReturnParameter())
+		varType = 2;
+	else
+	{
+		solAssert(_varDecl.isLocalVariable());
+		varType = 3;
+	}
+	auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()) + "_" + to_string(varType), *this);
 	m_variables.emplace(&_varDecl, result.second);
 	return result.first;
 }