diff --git a/Changelog.md b/Changelog.md
index e884eb380..833487d22 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -35,6 +35,7 @@ Bugfixes:
  * Inheritance: Disallow public state variables overwriting ``pure`` functions.
  * NatSpec: Constructors and functions have consistent userdoc output.
  * SMTChecker: Fix internal error when assigning to a 1-tuple.
+ * SMTChecker: Fix internal error when tuples have extra effectless parenthesis.
  * State Mutability: Constant public state variables are considered ``pure`` functions.
  * Type Checker: Fixing deduction issues on function types when function call has named arguments.
  * Immutables: Fix internal compiler error when immutables are not assigned.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index d690b2b3c..22780122b 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1470,7 +1470,7 @@ void SMTEncoder::assignment(
 
 void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
 {
-	auto lTuple = dynamic_cast<TupleExpression const*>(&_left);
+	auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(dynamic_cast<TupleExpression const&>(_left)));
 	solAssert(lTuple, "");
 
 	auto const& lComponents = lTuple->components();
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_1.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_1.sol
new file mode 100644
index 000000000..e238bd62a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_1.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		((, a)) = (1, 2);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_2.sol
new file mode 100644
index 000000000..30cd2608f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_2.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		(((, a),)) = ((1, 2), 3);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_3.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_3.sol
new file mode 100644
index 000000000..84ceb4e36
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_3.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		(((((((, a),)))))) = ((1, 2), 3);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_4.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_4.sol
new file mode 100644
index 000000000..8243e938e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_4.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		((((((, a)))),)) = ((1, 2), 3);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_5.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_5.sol
new file mode 100644
index 000000000..2288a94ca
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_5.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f2() public pure returns(int) {
+		int a;
+		((((((((((((, a))))))),))))) = ((1, 2), 3);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_6.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_6.sol
new file mode 100644
index 000000000..83b2db4df
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_6.sol
@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public pure {
+		(((,))) = ((2),3);
+	}
+}