diff --git a/Changelog.md b/Changelog.md
index 0936535b6..4397fae49 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -10,6 +10,7 @@ Compiler Features:
 
 Bugfixes:
  * Error Reporter: Fix handling of carriage return.
+ * SMTChecker: Fix internal error on ``array.pop`` nested inside 1-tuple.
  * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
  * SMTChecker: Fix internal error on array slices.
  * SMTChecker: Fix internal error on calling public getter on a state variable of type array (possibly nested) of structs.
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 328804d3e..1f6594d06 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -774,7 +774,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_arrayPop.expression().annotation().type);
 	solAssert(funType.kind() == FunctionType::Kind::ArrayPop, "");
 
-	auto memberAccess = dynamic_cast<MemberAccess const*>(&_arrayPop.expression());
+	auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_arrayPop.expression()));
 	solAssert(memberAccess, "");
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index b7c864d1c..cacf83c95 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -444,6 +444,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 
 void SMTEncoder::endVisit(TupleExpression const& _tuple)
 {
+	if (_tuple.annotation().type->category() == Type::Category::Function)
+		return;
+
 	createExpr(_tuple);
 
 	if (_tuple.isInlineArray())
@@ -1624,7 +1627,7 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
 
 void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 {
-	auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
+	auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_funCall.expression()));
 	solAssert(memberAccess, "");
 	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol
index 9664722ee..5ea45e963 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol
@@ -19,5 +19,3 @@ contract C {
 	}
 }
 // ----
-// Warning 6031: (289-292): Internal error: Expression undefined for SMT solver.
-// Warning 6031: (289-292): Internal error: Expression undefined for SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_3.sol
new file mode 100644
index 000000000..3ebf8804d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_3.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+    int[]data;
+
+    function f() public {
+        (data.pop)();
+    }
+}
+// ----
+// Warning 2529: (95-107): CHC: Empty array "pop" happens here.\nCounterexample:\ndata = []\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f()