diff --git a/Changelog.md b/Changelog.md
index e2ca2f6f8..043bb9e9a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,7 +6,7 @@ Language Features:
 
 Compiler Features:
  * SMTChecker: Support inherited state variables.
- * SMTChecker: Support tuple assignments and function calls with multiple return values.
+ * SMTChecker: Support tuples and function calls with multiple return values.
  * SMTChecker: Support ``delete``.
 
 
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 2110118ff..0071efd99 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -330,20 +330,35 @@ bool SMTChecker::visit(ForStatement const& _node)
 void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 {
 	if (_varDecl.declarations().size() != 1)
-		m_errorReporter.warning(
-			_varDecl.location(),
-			"Assertion checker does not yet support such variable declarations."
-		);
-	else if (knownVariable(*_varDecl.declarations()[0]))
+	{
+		if (auto init = _varDecl.initialValue())
+		{
+			auto symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[init]);
+			/// symbTuple == nullptr if it is the return of a non-inlined function call.
+			if (symbTuple)
+			{
+				auto const& components = symbTuple->components();
+				auto const& declarations = _varDecl.declarations();
+				for (unsigned i = 0; i < declarations.size(); ++i)
+				{
+					solAssert(components.at(i), "");
+					if (declarations.at(i) && knownVariable(*declarations.at(i)))
+						assignment(*declarations.at(i), components.at(i)->currentValue(), declarations.at(i)->location());
+				}
+			}
+		}
+	}
+	else if (knownVariable(*_varDecl.declarations().front()))
 	{
 		if (_varDecl.initialValue())
-			assignment(*_varDecl.declarations()[0], *_varDecl.initialValue(), _varDecl.location());
+			assignment(*_varDecl.declarations().front(), *_varDecl.initialValue(), _varDecl.location());
 	}
 	else
 		m_errorReporter.warning(
 			_varDecl.location(),
 			"Assertion checker does not yet implement such variable declarations."
 		);
+
 }
 
 void SMTChecker::endVisit(Assignment const& _assignment)
diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol
index 05c423406..d6d165591 100644
--- a/test/libsolidity/smtCheckerTests/types/address_call.sol
+++ b/test/libsolidity/smtCheckerTests/types/address_call.sol
@@ -19,5 +19,4 @@ contract C
 // EVMVersion: >spuriousDragon
 // ----
 // Warning: (224-240): Unused local variable.
-// Warning: (209-256): Assertion checker does not yet support such variable declarations.
 // Warning: (260-275): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
index ce49350ef..06925a66b 100644
--- a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
+++ b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
@@ -19,5 +19,4 @@ contract C
 // EVMVersion: >spuriousDragon
 // ----
 // Warning: (224-240): Unused local variable.
-// Warning: (209-264): Assertion checker does not yet support such variable declarations.
 // Warning: (268-283): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol
index 5336a14e6..529ce7ac0 100644
--- a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol
+++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol
@@ -19,5 +19,4 @@ contract C
 // EVMVersion: >spuriousDragon
 // ----
 // Warning: (224-240): Unused local variable.
-// Warning: (209-262): Assertion checker does not yet support such variable declarations.
 // Warning: (266-281): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations.sol
index 98ac97298..2f09308d1 100644
--- a/test/libsolidity/smtCheckerTests/types/tuple_declarations.sol
+++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations.sol
@@ -9,5 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning: (76-101): Assertion checker does not yet support such variable declarations.
-// Warning: (105-119): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_empty.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_empty.sol
new file mode 100644
index 000000000..3d31aa361
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_empty.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function g() public pure {
+		(uint x, ) = (2, 4);
+		assert(x == 2);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function.sol
new file mode 100644
index 000000000..424786635
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() internal pure returns (uint, bool, uint) {
+		uint x = 3;
+		bool b = true;
+		uint y = 999;
+		return (x, b, y);
+	}
+	function g() public pure {
+		(uint x, bool b, uint y) = f();
+		assert(x == 3);
+		assert(b);
+		assert(y == 999);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol
new file mode 100644
index 000000000..4ae855137
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) internal pure returns (uint, bool, uint) {
+		bool b = true;
+		uint y = 999;
+		return (x * 2, b, y);
+	}
+	function g() public pure {
+		(uint x, bool b, uint y) = f(7);
+		assert(x == 14);
+		assert(b);
+		assert(y == 999);
+	}
+}
+// ----
+// Warning: (152-157): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol
new file mode 100644
index 000000000..1d4c333be
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() internal pure returns (uint, bool, uint) {
+		uint x = 3;
+		bool b = true;
+		uint y = 999;
+		return (x, b, y);
+	}
+	function g() public pure {
+		(, bool b,) = f();
+		assert(!b);
+	}
+}
+// ----
+// Warning: (224-234): Assertion violation happens here