[SMTChecker] Support tuples with multiple var decls

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

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

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

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

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);
+	}
+}

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);
+	}
+}

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

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