diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index be67326c3..97268560d 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2547,10 +2547,10 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
 	FunctionDefinition const* funDef = nullptr;
 	Expression const* calledExpr = &_funCall.expression();
 
-	if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(&_funCall.expression()))
+	if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
 	{
 		solAssert(fun->components().size() == 1, "");
-		calledExpr = fun->components().front().get();
+		calledExpr = innermostTuple(*calledExpr);
 	}
 
 	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
@@ -2689,6 +2689,7 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
 	unsigned firstParam = 0;
 	if (funType->bound())
 	{
+		calledExpr = innermostTuple(*calledExpr);
 		auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
 		solAssert(boundFunction, "");
 		args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol
new file mode 100644
index 000000000..a329120cc
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+	function f() public {
+		x = 0;
+		((inc))();
+		assert(x == 1); // should hold
+	}
+
+	function inc() internal returns (uint) {
+		require(x < 100);
+		return ++x;
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol
new file mode 100644
index 000000000..9664722ee
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_2.sol
@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+library L {
+	struct S {
+		uint256[] data;
+	}
+	function f(S memory _s) internal pure returns (uint256) {
+		require(_s.data.length > 0);
+		return 42;
+	}
+}
+
+contract C {
+	using L for L.S;
+	function f() public pure returns (uint256 y) {
+		L.S memory x;
+		y = (x.f)();
+		assert(y == 42); // should hold
+	}
+}
+// ----
+// Warning 6031: (289-292): Internal error: Expression undefined for SMT solver.
+// Warning 6031: (289-292): Internal error: Expression undefined for SMT solver.