[SMTChecker] Support array length

libsolidity/formal/CVC4Interface.cpp

@@ -206,6 +206,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			CVC4::Expr s = dt[0][index].getSelector();
 			return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
 		}
+		else if (n == "tuple_constructor")
+		{
+			shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
+			solAssert(tupleSort, "");
+			CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
+			CVC4::Datatype const& dt = tt.getDatatype();
+			CVC4::Expr c = dt[0].getConstructor();
+			return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
+		}
 
 		solAssert(false, "");
 	}

libsolidity/formal/SMTEncoder.cpp

@@ -890,6 +890,33 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 			return false;
 		}
 	}
+	else if (exprType->category() == Type::Category::Array)
+	{
+		_memberAccess.expression().accept(*this);
+		if (_memberAccess.memberName() == "length")
+		{
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_memberAccess.expression()));
+			solAssert(symbArray, "");
+			defineExpr(_memberAccess, symbArray->length());
+			m_uninterpretedTerms.insert(&_memberAccess);
+			setSymbolicUnknownValue(
+				expr(_memberAccess),
+				_memberAccess.annotation().type,
+				m_context
+			);
+		}
+		else
+		{
+			auto const& name = _memberAccess.memberName();
+			solAssert(name == "push" || name == "pop", "");
+			m_errorReporter.warning(
+				9098_error,
+				_memberAccess.location(),
+				"Assertion checker does not yet support array member \"" + name + "\"."
+			);
+		}
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			7650_error,
@@ -939,9 +966,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		return;
 	}
 
-	solAssert(array, "");
+	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
+	solAssert(arrayVar, "");
 	defineExpr(_indexAccess, smt::Expression::select(
-		array->currentValue(),
+		arrayVar->elements(),
 		expr(*_indexAccess.indexExpression())
 	));
 	setSymbolicUnknownValue(
@@ -1013,16 +1041,20 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 					return false;
 				});
 
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
 			smt::Expression store = smt::Expression::store(
-				m_context.variable(*varDecl)->currentValue(),
+				symbArray->elements(),
 				expr(*indexAccess->indexExpression()),
 				toStore
 			);
-			m_context.addAssertion(m_context.newValue(*varDecl) == store);
+			auto oldLength = symbArray->length();
+			symbArray->increaseIndex();
+			m_context.addAssertion(symbArray->elements() == store);
+			m_context.addAssertion(symbArray->length() == oldLength);
 			// Update the SMT select value after the assignment,
 			// necessary for sound models.
 			defineExpr(*indexAccess, smt::Expression::select(
-				m_context.variable(*varDecl)->currentValue(),
+				symbArray->elements(),
 				expr(*indexAccess->indexExpression())
 			));
 
@@ -1030,7 +1062,12 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 		}
 		else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
 		{
-			toStore = smt::Expression::store(expr(*base), expr(*indexAccess->indexExpression()), toStore);
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
+			solAssert(symbArray, "");
+			toStore = smt::Expression::tuple_constructor(
+				smt::Expression(base->annotation().type),
+				{smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+			);
 			indexAccess = base;
 		}
 		else
@@ -1326,7 +1363,14 @@ smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
 {
-	assignment(_variable, expr(_value, _variable.type()));
+	// In general, at this point, the SMT sorts of _variable and _value are the same,
+	// even if there is implicit conversion.
+	// This is a special case where the SMT sorts are different.
+	// For now we are unaware of other cases where this happens, but if they do appear
+	// we should extract this into an `implicitConversion` function.
+	if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral)
+		assignment(_variable, expr(_value, _variable.type()));
+	// TODO else { store each string literal byte into the array }
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value)
@@ -1616,7 +1660,7 @@ SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
 void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 {
 	for (auto const& var: _indices)
-		m_context.variable(*var.first)->index() = var.second;
+		m_context.variable(*var.first)->setIndex(var.second);
 }
 
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

libsolidity/formal/SMTLib2Interface.cpp

@@ -153,7 +153,15 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
 		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.arguments.at(0).sort);
 		unsigned index = std::stoi(_expr.arguments.at(1).name);
 		solAssert(index < tupleSort->members.size(), "");
-		sexpr += tupleSort->members.at(index) + " " + toSExpr(_expr.arguments.at(0));
+		sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0));
+	}
+	else if (_expr.name == "tuple_constructor")
+	{
+		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.sort);
+		solAssert(tupleSort, "");
+		sexpr += "|" + tupleSort->name + "|";
+		for (auto const& arg: _expr.arguments)
+			sexpr += " " + toSExpr(arg);
 	}
 	else
 	{
@@ -182,18 +190,19 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	case Kind::Tuple:
 	{
 		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
-		if (!m_userSorts.count(tupleSort.name))
+		string tupleName = "|" + tupleSort.name + "|";
+		if (!m_userSorts.count(tupleName))
 		{
-			m_userSorts.insert(tupleSort.name);
-			string decl("(declare-datatypes ((" + tupleSort.name + " 0)) (((" + tupleSort.name);
+			m_userSorts.insert(tupleName);
+			string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
 			solAssert(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 += "))))";
 			write(decl);
 		}
 
-		return tupleSort.name;
+		return tupleName;
 	}
 	default:
 		solAssert(false, "Invalid SMT sort");

libsolidity/formal/SSAVariable.cpp

@@ -29,5 +29,12 @@ SSAVariable::SSAVariable()
 void SSAVariable::resetIndex()
 {
 	m_currentIndex = 0;
-	m_nextFreeIndex = make_unique<unsigned>(1);
+	m_nextFreeIndex = 1;
+}
+
+void SSAVariable::setIndex(unsigned _index)
+{
+	m_currentIndex = _index;
+	if (m_nextFreeIndex <= _index)
+		m_nextFreeIndex = _index + 1;
 }

libsolidity/formal/SSAVariable.h

@@ -29,7 +29,10 @@ class SSAVariable
 {
 public:
 	SSAVariable();
+	/// Resets index to 0 and next index to 1.
 	void resetIndex();
+	/// Sets index to _index and only adjusts next if next <= _index.
+	void setIndex(unsigned _index);
 
 	/// This function returns the current index of this SSA variable.
 	unsigned index() const { return m_currentIndex; }
@@ -37,12 +40,12 @@ public:
 
 	unsigned operator++()
 	{
-		return m_currentIndex = (*m_nextFreeIndex)++;
+		return m_currentIndex = m_nextFreeIndex++;
 	}
 
 private:
 	unsigned m_currentIndex;
-	std::unique_ptr<unsigned> m_nextFreeIndex;
+	unsigned m_nextFreeIndex;
 };
 
 }

libsolidity/formal/SolverInterface.h

@@ -28,6 +28,7 @@
 #include <boost/noncopyable.hpp>
 #include <cstdio>
 #include <map>
+#include <memory>
 #include <string>
 #include <vector>
 
@@ -63,7 +64,8 @@ class Expression
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(std::shared_ptr<SortSort> _sort): Expression("", {}, _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) {}
@@ -76,6 +78,13 @@ public:
 
 	bool hasCorrectArity() const
 	{
+		if (name == "tuple_constructor")
+		{
+			auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sort);
+			solAssert(tupleSort, "");
+			return arguments.size() == tupleSort->components.size();
+		}
+
 		static std::map<std::string, unsigned> const operatorsArity{
 			{"ite", 3},
 			{"not", 1},
@@ -138,8 +147,7 @@ public:
 	/// The function is pure and returns the modified array.
 	static Expression store(Expression _array, Expression _index, Expression _element)
 	{
-		solAssert(_array.sort->kind == Kind::Array, "");
-		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
+		auto arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
 		solAssert(arraySort, "");
 		solAssert(_index.sort, "");
 		solAssert(_element.sort, "");
@@ -180,6 +188,20 @@ public:
 		);
 	}
 
+	static Expression tuple_constructor(Expression _tuple, std::vector<Expression> _arguments)
+	{
+		solAssert(_tuple.sort->kind == Kind::Sort, "");
+		auto sortSort = std::dynamic_pointer_cast<SortSort>(_tuple.sort);
+		auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sortSort->inner);
+		solAssert(tupleSort, "");
+		solAssert(_arguments.size() == tupleSort->components.size(), "");
+		return Expression(
+			"tuple_constructor",
+			std::move(_arguments),
+			tupleSort
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);

libsolidity/formal/SymbolicState.cpp

@@ -47,7 +47,7 @@ Expression SymbolicState::balance()
 
 Expression SymbolicState::balance(Expression _address)
 {
-	return Expression::select(m_balances.currentValue(), move(_address));
+	return Expression::select(m_balances.elements(), move(_address));
 }
 
 void SymbolicState::transfer(Expression _from, Expression _to, Expression _value)
@@ -72,11 +72,13 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
 void SymbolicState::addBalance(Expression _address, Expression _value)
 {
 	auto newBalances = Expression::store(
-		m_balances.currentValue(),
+		m_balances.elements(),
 		_address,
 		balance(_address) + move(_value)
 	);
+	auto oldLength = m_balances.length();
 	m_balances.increaseIndex();
-	m_context.addAssertion(newBalances == m_balances.currentValue());
+	m_context.addAssertion(m_balances.elements() == newBalances);
+	m_context.addAssertion(m_balances.length() == oldLength);
 }
 

libsolidity/formal/SymbolicTypes.cpp

@@ -21,6 +21,7 @@
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
 #include <memory>
+#include <vector>
 
 using namespace std;
 
@@ -55,17 +56,18 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 	case Kind::Array:
 	{
+		shared_ptr<ArraySort> array;
 		if (isMapping(_type.category()))
 		{
 			auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
 			solAssert(mapType, "");
-			return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
+			array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
 		else if (isStringLiteral(_type.category()))
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
-			return make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
+			array = make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
 		}
 		else
 		{
@@ -78,8 +80,25 @@ SortPointer smtSort(frontend::Type const& _type)
 				solAssert(false, "");
 
 			solAssert(arrayType, "");
-			return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
+			array = make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
+
+		string tupleName;
+		if (
+			auto arrayType = dynamic_cast<ArrayType const*>(&_type);
+			(arrayType && arrayType->isString()) ||
+			_type.category() == frontend::Type::Category::ArraySlice ||
+			_type.category() == frontend::Type::Category::StringLiteral
+		)
+			tupleName = "bytes_tuple";
+		else
+			tupleName = _type.toString(true) + "_tuple";
+
+		return make_shared<TupleSort>(
+			tupleName,
+			vector<string>{tupleName + "_accessor_array", tupleName + "_accessor_length"},
+			vector<SortPointer>{array, SortProvider::intSort}
+		);
 	}
 	case Kind::Tuple:
 	{
@@ -219,9 +238,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
-	else if (isMapping(_type.category()))
-		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _context);
-	else if (isArray(_type.category()))
+	else if (isMapping(_type.category()) || isArray(_type.category()))
 		var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
 	else if (isTuple(_type.category()))
 		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
@@ -349,11 +366,26 @@ Expression zeroValue(frontend::TypePointer const& _type)
 			return Expression(false);
 		if (isArray(_type->category()) || isMapping(_type->category()))
 		{
+			auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
+			solAssert(tupleSort, "");
+			auto sortSort = make_shared<SortSort>(tupleSort->components.front());
+
+			std::optional<Expression> zeroArray;
+			auto length = bigint(0);
 			if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
-				return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType()));
-			auto mappingType = dynamic_cast<MappingType const*>(_type);
-			solAssert(mappingType, "");
-			return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
+			{
+				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType()));
+				if (!arrayType->isDynamicallySized())
+					length = bigint(arrayType->length());
+			}
+			else if (auto mappingType = dynamic_cast<MappingType const*>(_type))
+				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType()));
+			else
+				solAssert(false, "");
+
+			solAssert(zeroArray, "");
+			return Expression::tuple_constructor(Expression(_type), vector<Expression>{*zeroArray, length});
+
 		}
 		solAssert(false, "");
 	}

libsolidity/formal/SymbolicVariables.cpp

@@ -86,6 +86,12 @@ smt::Expression SymbolicVariable::resetIndex()
 	return currentValue();
 }
 
+smt::Expression SymbolicVariable::setIndex(unsigned _index)
+{
+	m_ssa->setIndex(_index);
+	return currentValue();
+}
+
 smt::Expression SymbolicVariable::increaseIndex()
 {
 	++(*m_ssa);
@@ -179,6 +185,12 @@ smt::Expression SymbolicFunctionVariable::resetIndex()
 	return m_abstract.resetIndex();
 }
 
+smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
+{
+	SymbolicVariable::setIndex(_index);
+	return m_abstract.setIndex(_index);
+}
+
 smt::Expression SymbolicFunctionVariable::increaseIndex()
 {
 	++(*m_ssa);
@@ -197,46 +209,6 @@ void SymbolicFunctionVariable::resetDeclaration()
 	m_declaration = m_context.newVariable(currentName(), m_sort);
 }
 
-SymbolicMappingVariable::SymbolicMappingVariable(
-	frontend::TypePointer _type,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(_type, _type, move(_uniqueName), _context)
-{
-	solAssert(isMapping(m_type->category()), "");
-}
-
-SymbolicArrayVariable::SymbolicArrayVariable(
-	frontend::TypePointer _type,
-	frontend::TypePointer _originalType,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
-{
-	solAssert(isArray(m_type->category()), "");
-}
-
-SymbolicArrayVariable::SymbolicArrayVariable(
-	SortPointer _sort,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(move(_sort), move(_uniqueName), _context)
-{
-	solAssert(m_sort->kind == Kind::Array, "");
-}
-
-smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
-{
-	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
-	if (conversion)
-		return *conversion;
-
-	return SymbolicVariable::currentValue(_targetType);
-}
-
 SymbolicEnumVariable::SymbolicEnumVariable(
 	frontend::TypePointer _type,
 	string _uniqueName,
@@ -286,3 +258,62 @@ smt::Expression SymbolicTupleVariable::component(
 
 	return smt::Expression::tuple_get(currentValue(), _index);
 }
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	frontend::TypePointer _type,
+	frontend::TypePointer _originalType,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(_type, _originalType, move(_uniqueName), _context),
+	m_pair(
+		smtSort(*_type),
+		m_uniqueName + "_length_pair",
+		m_context
+	)
+{
+	solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
+}
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	SortPointer _sort,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(move(_sort), move(_uniqueName), _context),
+	m_pair(
+		std::make_shared<TupleSort>(
+			"array_length_pair",
+			std::vector<std::string>{"array", "length"},
+			std::vector<SortPointer>{m_sort, SortProvider::intSort}
+		),
+		m_uniqueName + "_array_length_pair",
+		m_context
+	)
+{
+	solAssert(m_sort->kind == Kind::Array, "");
+}
+
+smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
+{
+	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
+	if (conversion)
+		return *conversion;
+
+	return m_pair.currentValue();
+}
+
+smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
+{
+	return m_pair.valueAtIndex(_index);
+}
+
+smt::Expression SymbolicArrayVariable::elements()
+{
+	return m_pair.component(0);
+}
+
+smt::Expression SymbolicArrayVariable::length()
+{
+	return m_pair.component(1);
+}

libsolidity/formal/SymbolicVariables.h

@@ -56,6 +56,7 @@ public:
 	virtual Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
 	virtual Expression resetIndex();
+	virtual Expression setIndex(unsigned _index);
 	virtual Expression increaseIndex();
 	virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
 	{
@@ -169,6 +170,7 @@ public:
 	Expression functionValueAtIndex(int _index) const;
 
 	Expression resetIndex() override;
+	Expression setIndex(unsigned _index) override;
 	Expression increaseIndex() override;
 
 	Expression operator()(std::vector<Expression> _arguments) const override;
@@ -189,42 +191,6 @@ private:
 	};
 };
 
-/**
- * Specialization of SymbolicVariable for Mapping
- */
-class SymbolicMappingVariable: public SymbolicVariable
-{
-public:
-	SymbolicMappingVariable(
-		frontend::TypePointer _type,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-};
-
-/**
- * Specialization of SymbolicVariable for Array
- */
-class SymbolicArrayVariable: public SymbolicVariable
-{
-public:
-	SymbolicArrayVariable(
-		frontend::TypePointer _type,
-		frontend::TypePointer _originalTtype,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-	SymbolicArrayVariable(
-		SortPointer _sort,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-
-	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
-
-	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
-};
-
 /**
  * Specialization of SymbolicVariable for Enum
  */
@@ -263,4 +229,38 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for Array
+ */
+class SymbolicArrayVariable: public SymbolicVariable
+{
+public:
+	SymbolicArrayVariable(
+		frontend::TypePointer _type,
+		frontend::TypePointer _originalTtype,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+	SymbolicArrayVariable(
+		SortPointer _sort,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+
+	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
+
+	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	Expression valueAtIndex(int _index) const override;
+	Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
+	Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
+	Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
+	Expression elements();
+	Expression length();
+
+	SortPointer tupleSort() { return m_pair.sort(); }
+
+private:
+	SymbolicTupleVariable m_pair;
+};
+
 }

libsolidity/formal/Z3Interface.cpp

@@ -198,6 +198,15 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			size_t index = std::stoi(_expr.arguments[1].name);
 			return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]);
 		}
+		else if (n == "tuple_constructor")
+		{
+			auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
+			solAssert(constructor.arity() == arguments.size(), "");
+			z3::expr_vector args(m_context);
+			for (auto const& arg: arguments)
+				args.push_back(arg);
+			return constructor(args);
+		}
 
 		solAssert(false, "");
 	}