diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 22780122b..b101a3147 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1100,7 +1100,11 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 
 void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array)
 {
-	if (auto const* id = dynamic_cast<Identifier const*>(&_expr))
+	Expression const* expr = &_expr;
+	if (auto const* tupleExpr = dynamic_cast<TupleExpression const*>(expr))
+		expr = innermostTuple(*tupleExpr);
+
+	if (auto const* id = dynamic_cast<Identifier const*>(expr))
 	{
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
@@ -1108,9 +1112,9 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 			resetReferences(*varDecl);
 		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
 	}
-	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
+	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(expr))
 		arrayIndexAssignment(*indexAccess, _array);
-	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(&_expr))
+	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
 	{
 		FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
 		if (funType.kind() == FunctionType::Kind::ArrayPush)
@@ -1132,7 +1136,7 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 			arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 		}
 	}
-	else if (dynamic_cast<MemberAccess const*>(&_expr))
+	else if (dynamic_cast<MemberAccess const*>(expr))
 		m_errorReporter.warning(
 			9599_error,
 			_expr.location(),
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_array_pop_1.sol b/test/libsolidity/smtCheckerTests/types/tuple_array_pop_1.sol
new file mode 100644
index 000000000..e297cffd7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_array_pop_1.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	int[] a;
+	function f() public { (a).pop();}
+}
+// ----
+// Warning 2529: (78-87): Empty array "pop" detected here.
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_array_pop_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_array_pop_2.sol
new file mode 100644
index 000000000..76c8e3cb3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_array_pop_2.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	int[] a;
+	function f() public { (((((a))))).pop();}
+}
+// ----
+// Warning 2529: (78-95): Empty array "pop" detected here.