diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index c98e4414d..839f2be3e 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -128,11 +128,11 @@ void CHCSmtLib2Interface::declareVariable(std::string const& _name, SortPointer
 	else if (!m_variables.count(_name))
 	{
 		m_variables.insert(_name);
-		write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')');
+		write("(declare-var |" + _name + "| " + toSmtLibSort(_sort) + ')');
 	}
 }
 
-std::string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)
+std::string CHCSmtLib2Interface::toSmtLibSort(SortPointer _sort)
 {
 	return m_smtlib2->toSmtLibSort(_sort);
 }
@@ -149,7 +149,7 @@ std::string CHCSmtLib2Interface::forall()
 	{
 		solAssert(sort, "");
 		if (sort->kind != Kind::Function)
-			vars += " (" + name + " " + toSmtLibSort(*sort) + ")";
+			vars += " (" + name + " " + toSmtLibSort(sort) + ")";
 	}
 	vars += ")";
 	return vars;
@@ -165,7 +165,7 @@ void CHCSmtLib2Interface::declareFunction(std::string const& _name, SortPointer
 		auto fSort = std::dynamic_pointer_cast<FunctionSort>(_sort);
 		smtAssert(fSort->codomain);
 		std::string domain = toSmtLibSort(fSort->domain);
-		std::string codomain = toSmtLibSort(*fSort->codomain);
+		std::string codomain = toSmtLibSort(fSort->codomain);
 		m_variables.insert(_name);
 		write(
 			"(declare-fun |" +
@@ -309,10 +309,9 @@ namespace
 				});
 				if (it != m_smtlib2Interface.sortNames().end()) {
 					if (it->first->kind == Kind::Tuple) {
-						auto const* tupleSort = dynamic_cast<TupleSort const*>(it->first);
+						auto tupleSort = std::dynamic_pointer_cast<TupleSort>(it->first);
 						smtAssert(tupleSort);
-						// TODO: This is cumbersome, we should really store shared_pointer instead of raw pointer in the sortNames
-						return std::make_shared<TupleSort>(tupleSort->name, tupleSort->members, tupleSort->components);
+						return tupleSort;
 					}
 				}
 			} else {
diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h
index 2f71890f0..dd8f4342e 100644
--- a/libsmtutil/CHCSmtLib2Interface.h
+++ b/libsmtutil/CHCSmtLib2Interface.h
@@ -66,7 +66,7 @@ public:
 	SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); }
 
 private:
-	std::string toSmtLibSort(Sort const& _sort);
+	std::string toSmtLibSort(SortPointer _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
 	void writeHeader();
diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
index 2a7bc0c8b..8a185d841 100644
--- a/libsmtutil/SMTLib2Interface.cpp
+++ b/libsmtutil/SMTLib2Interface.cpp
@@ -83,7 +83,7 @@ void SMTLib2Interface::declareVariable(std::string const& _name, SortPointer con
 	else if (!m_variables.count(_name))
 	{
 		m_variables.emplace(_name, _sort);
-		write("(declare-fun |" + _name + "| () " + toSmtLibSort(*_sort) + ')');
+		write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
 	}
 }
 
@@ -96,7 +96,7 @@ void SMTLib2Interface::declareFunction(std::string const& _name, SortPointer con
 	{
 		auto const& fSort = std::dynamic_pointer_cast<FunctionSort>(_sort);
 		std::string domain = toSmtLibSort(fSort->domain);
-		std::string codomain = toSmtLibSort(*fSort->codomain);
+		std::string codomain = toSmtLibSort(fSort->codomain);
 		m_variables.emplace(_name, _sort);
 		write(
 			"(declare-fun |" +
@@ -246,7 +246,7 @@ std::string SMTLib2Interface::toSExpr(Expression const& _expr)
 		smtAssert(sortSort, "");
 		auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
 		smtAssert(arraySort, "");
-		sexpr += "(as const " + toSmtLibSort(*arraySort) + ") ";
+		sexpr += "(as const " + toSmtLibSort(arraySort) + ") ";
 		sexpr += toSExpr(_expr.arguments.at(1));
 	}
 	else if (_expr.name == "tuple_get")
@@ -275,14 +275,14 @@ std::string SMTLib2Interface::toSExpr(Expression const& _expr)
 	return sexpr;
 }
 
-std::string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
+std::string SMTLib2Interface::toSmtLibSort(SortPointer _sort)
 {
-	if (!m_sortNames.count(&_sort))
+	if (!m_sortNames.count(_sort))
 	{
-		auto smtLibName = sortToString(_sort);
-		m_sortNames[&_sort] = smtLibName;
+		auto smtLibName = sortToString(*_sort);
+		m_sortNames[_sort] = smtLibName;
 	}
-	return m_sortNames.at(&_sort);
+	return m_sortNames.at(_sort);
 }
 
 std::string SMTLib2Interface::sortToString(Sort const& _sort)
@@ -299,7 +299,7 @@ std::string SMTLib2Interface::sortToString(Sort const& _sort)
 	{
 		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
 		smtAssert(arraySort.domain && arraySort.range, "");
-		return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
+		return "(Array " + toSmtLibSort(arraySort.domain) + ' ' + toSmtLibSort(arraySort.range) + ')';
 	}
 	case Kind::Tuple:
 	{
@@ -311,7 +311,7 @@ std::string SMTLib2Interface::sortToString(Sort const& _sort)
 			std::string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
 			smtAssert(tupleSort.members.size() == tupleSort.components.size(), "");
 			for (unsigned i = 0; i < tupleSort.members.size(); ++i)
-				decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
+				decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(tupleSort.components.at(i)) + ")";
 			decl += "))))";
 			m_userSorts.emplace_back(tupleName, decl);
 			write(decl);
@@ -328,7 +328,7 @@ std::string SMTLib2Interface::toSmtLibSort(std::vector<SortPointer> const& _sort
 {
 	std::string ssort("(");
 	for (auto const& sort: _sorts)
-		ssort += toSmtLibSort(*sort) + " ";
+		ssort += toSmtLibSort(sort) + " ";
 	ssort += ")";
 	return ssort;
 }
diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h
index 12c5b7e1c..39d73e0d1 100644
--- a/libsmtutil/SMTLib2Interface.h
+++ b/libsmtutil/SMTLib2Interface.h
@@ -62,7 +62,7 @@ public:
 
 	// Used by CHCSmtLib2Interface
 	std::string toSExpr(Expression const& _expr);
-	std::string toSmtLibSort(Sort const& _sort);
+	std::string toSmtLibSort(SortPointer _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
 	std::map<std::string, SortPointer> variables() { return m_variables; }
@@ -90,9 +90,8 @@ private:
 	/// It needs to be a vector so that the declaration order is kept,
 	/// otherwise solvers cannot parse the queries.
 	std::vector<std::pair<std::string, std::string>> m_userSorts;
-	// TODO: Should this remember shared_pointer?
 	// TODO: Shouldn't sorts be unique objects?
-	std::map<Sort const*, std::string> m_sortNames;
+	std::map<SortPointer, std::string> m_sortNames;
 
 
 	std::vector<std::string> m_unhandledQueries;