[SMTChecker] Fix ICEs with tuples

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
 Bugfixes:
  * isoltest: Added new keyword `wei` to express function value in semantic tests
  * Standard-JSON-Interface: Fix a bug related to empty filenames and imports.
+ * SMTChecker: Fix internal errors when analysing tuples.
 
 
 ### 0.6.3 (2020-02-18)

libsolidity/formal/SMTEncoder.cpp

@@ -407,19 +407,26 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
 		auto const& symbComponents = symbTuple->components();
-		auto const& tupleComponents = _tuple.components();
+		auto const* tupleComponents = &_tuple.components();
-		solAssert(symbComponents.size() == _tuple.components().size(), "");
+		while (tupleComponents->size() == 1)
+		{
+			auto innerTuple = dynamic_pointer_cast<TupleExpression>(tupleComponents->front());
+			solAssert(innerTuple, "");
+			tupleComponents = &innerTuple->components();
+		}
+		solAssert(symbComponents.size() == tupleComponents->size(), "");
 		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
 			auto sComponent = symbComponents.at(i);
-			auto tComponent = tupleComponents.at(i);
+			auto tComponent = tupleComponents->at(i);
 			if (sComponent && tComponent)
 			{
 				if (auto varDecl = identifierToVariable(*tComponent))
 					m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl));
 				else
 				{
-					solAssert(m_context.knownExpression(*tComponent), "");
+					if (!m_context.knownExpression(*tComponent))
+						createExpr(*tComponent);
 					m_context.addAssertion(sComponent->currentValue() == expr(*tComponent));
 				}
 			}

test/libsolidity/smtCheckerTests/types/function_in_tuple_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract K {
+	function f() public pure {
+		(abi.encode, 2);
+	}
+}
+// ----
+// Warning: (76-91): Statement has no effect.
+// Warning: (77-80): Assertion checker does not yet implement type abi

test/libsolidity/smtCheckerTests/types/function_in_tuple_2.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract K {
+	function f() public pure {
+		(abi.encode, "");
+	}
+}
+// ----
+// Warning: (76-92): Statement has no effect.
+// Warning: (77-80): Assertion checker does not yet implement type abi

test/libsolidity/smtCheckerTests/types/tuple_single_element_1.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		(("", 2));
+	}
+}
+// ----
+// Warning: (76-85): Statement has no effect.

test/libsolidity/smtCheckerTests/types/tuple_single_element_2.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		(("", ""));
+	}
+}
+// ----
+// Warning: (76-86): Statement has no effect.

test/libsolidity/smtCheckerTests/types/tuple_single_non_tuple_element.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		(2);
+	}
+}
+// ----
+// Warning: (76-79): Statement has no effect.