diff --git a/Changelog.md b/Changelog.md
index 29498feac..c3ffc0ed9 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -21,6 +21,7 @@ Bugfixes:
  * SMTChecker: Fix internal error on array implicit conversion.
  * SMTChecker: Fix internal error on fixed bytes index access.
  * SMTChecker: Fix internal error on lvalue unary operators with tuples.
+ * SMTChecker: Fix internal error on tuple assignment.
  * SMTChecker: Fix soundness of array ``pop``.
  * References Resolver: Fix internal bug when using constructor for library.
  * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 2f7313bc6..7cb8c0367 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1490,13 +1490,14 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
 {
 	auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(_left));
 	solAssert(lTuple, "");
+	Expression const* right = innermostTuple(_right);
 
 	auto const& lComponents = lTuple->components();
 
 	// If both sides are tuple expressions, we individually and potentially
 	// recursively assign each pair of components.
 	// This is because of potential type conversion.
-	if (auto rTuple = dynamic_cast<TupleExpression const*>(&_right))
+	if (auto rTuple = dynamic_cast<TupleExpression const*>(right))
 	{
 		auto const& rComponents = rTuple->components();
 		solAssert(lComponents.size() == rComponents.size(), "");
@@ -1517,13 +1518,13 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
 	}
 	else
 	{
-		auto rType = dynamic_cast<TupleType const*>(_right.annotation().type);
+		auto rType = dynamic_cast<TupleType const*>(right->annotation().type);
 		solAssert(rType, "");
 
 		auto const& rComponents = rType->components();
 		solAssert(lComponents.size() == rComponents.size(), "");
 
-		auto symbRight = expr(_right);
+		auto symbRight = expr(*right);
 		solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, "");
 
 		for (unsigned i = 0; i < lComponents.size(); ++i)
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol
new file mode 100644
index 000000000..b0861b3b5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_1.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public pure returns(int) {
+		int a;
+		(,, a) = ((((((1, 3, (((((2)))))))))));
+		assert(a == 2);
+		assert(a == 3);
+	}
+}
+// ----
+// Warning 6328: (157-171): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol
new file mode 100644
index 000000000..02a14c1b4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_different_count_assignment_2.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public pure returns(int) {
+		int a;
+		((,, a)) = ((((((1, 3, (((((2)))))))))));
+		assert(a == 2);
+		assert(a == 3);
+	}
+}
+// ----
+// Warning 6328: (159-173): Assertion violation happens here