From 7a91c9b971ad8d2bb67aaa00374abeb4acda39f4 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 19 May 2020 14:23:41 +0200
Subject: [PATCH] Remove Type from SolverInterface

---
 libsmtutil/SolverInterface.h         | 7 +------
 libsolidity/formal/SMTEncoder.cpp    | 3 ++-
 libsolidity/formal/SymbolicTypes.cpp | 5 ++++-
 3 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index 260dcc7a7..0dd8e5bcd 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -19,7 +19,6 @@
 
 #include <libsmtutil/Sorts.h>
 
-#include <libsolidity/ast/Types.h>
 #include <liblangutil/Exceptions.h>
 #include <libsolutil/Common.h>
 #include <libsolutil/Exceptions.h>
@@ -54,17 +53,13 @@ enum class CheckResult
 	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
-// Forward declaration.
-SortPointer smtSort(frontend::Type const& _type);
-
 /// C++ representation of an SMTLIB2 expression.
 class Expression
 {
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
-	explicit Expression(std::shared_ptr<SortSort> _sort): Expression("", {}, _sort) {}
+	explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index afaf8ea7e..a8e0e32b7 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1061,8 +1061,9 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi
 		{
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
 			solAssert(symbArray, "");
+			auto baseType = base->annotation().type;
 			toStore = smtutil::Expression::tuple_constructor(
-				smtutil::Expression(base->annotation().type),
+				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
 				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
 			);
 			indexAccess = base;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index bf4f38daa..38f72cb66 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -385,7 +385,10 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 				solAssert(false, "");
 
 			solAssert(zeroArray, "");
-			return smtutil::Expression::tuple_constructor(smtutil::Expression(_type), vector<smtutil::Expression>{*zeroArray, length});
+			return smtutil::Expression::tuple_constructor(
+				smtutil::Expression(std::make_shared<SortSort>(smtSort(*_type)), _type->toString(true)),
+				vector<smtutil::Expression>{*zeroArray, length}
+			);
 
 		}
 		solAssert(false, "");