[SMTChecker] Fix ICE when inlining function with tuple expression

Changelog.md

@@ -18,6 +18,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error when inlining functions that contain tuple expressions.
  * View/Pure Checker: Properly detect state variable access through base class.
  * Yul analyzer: Check availability of data objects already in analysis phase.
  * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.

libsolidity/formal/SMTEncoder.cpp

@@ -266,24 +266,27 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 		);
 	else if (_tuple.annotation().type->category() == Type::Category::Tuple)
 	{
-		vector<shared_ptr<smt::SymbolicVariable>> components;
-		for (auto const& component: _tuple.components())
-			if (component)
-			{
-				if (auto varDecl = identifierToVariable(*component))
-					components.push_back(m_context.variable(*varDecl));
-				else
-				{
-					solAssert(m_context.knownExpression(*component), "");
-					components.push_back(m_context.expression(*component));
-				}
-			}
-			else
-				components.push_back(nullptr);
-		solAssert(components.size() == _tuple.components().size(), "");
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
-		symbTuple->setComponents(move(components));
+		if (symbTuple->components().empty())
+		{
+			vector<shared_ptr<smt::SymbolicVariable>> components;
+			for (auto const& component: _tuple.components())
+				if (component)
+				{
+					if (auto varDecl = identifierToVariable(*component))
+						components.push_back(m_context.variable(*varDecl));
+					else
+					{
+						solAssert(m_context.knownExpression(*component), "");
+						components.push_back(m_context.expression(*component));
+					}
+				}
+				else
+					components.push_back(nullptr);
+			solAssert(components.size() == _tuple.components().size(), "");
+			symbTuple->setComponents(move(components));
+		}
 	}
 	else
 	{

test/libsolidity/smtCheckerTests/types/tuple_assignment_multiple_calls.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure returns (uint, uint) {
+		return (x, x);
+	}
+
+	function g() public pure {
+		(uint a, uint b) = f(0);
+		(uint c, uint d) = f(0);
+		assert(a == c && b == d);
+	}
+}