From 238b8a929e5a6502e59ac95443350c6675e2e06a Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 31 Aug 2020 16:45:52 +0200
Subject: [PATCH] [SMTChecker] Fix ICE on tuples of one element that actually
 have tuple type

---
 Changelog.md                                       |  1 +
 libsolidity/formal/SMTEncoder.cpp                  | 12 ++++--------
 .../smtCheckerTests/types/tuple_extra_parens_7.sol | 14 ++++++++++++++
 3 files changed, 19 insertions(+), 8 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol

diff --git a/Changelog.md b/Changelog.md
index c3ffc0ed9..9c54eabe5 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -22,6 +22,7 @@ Bugfixes:
  * 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 internal error on tuples of one element that have tuple type.
  * 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 7cb8c0367..8cbed6712 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -420,8 +420,11 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 			_tuple.location(),
 			"Assertion checker does not yet implement inline arrays."
 		);
-	else if (_tuple.annotation().type->category() == Type::Category::Tuple)
+	else if (_tuple.components().size() == 1)
+		defineExpr(_tuple, expr(*_tuple.components().front()));
+	else
 	{
+		solAssert(_tuple.annotation().type->category() == Type::Category::Tuple, "");
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
 		auto const& symbComponents = symbTuple->components();
@@ -445,13 +448,6 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 			}
 		}
 	}
-	else
-	{
-		/// Parenthesized expressions are also TupleExpression regardless their type.
-		auto const& components = _tuple.components();
-		solAssert(components.size() == 1, "");
-		defineExpr(_tuple, expr(*components.front()));
-	}
 }
 
 void SMTEncoder::endVisit(UnaryOperation const& _op)
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
new file mode 100644
index 000000000..824d84c3e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() internal pure returns (uint, uint) {
+		return (2, 3);
+	}
+	function f() public {
+		(address(1).call(""));
+		(uint x, uint y) = ((g()));
+		assert(x == 2);
+		assert(y == 3);
+	}
+}
+// ----
+// Warning 5084: (142-152): Type conversion is not yet fully supported and might yield false positives.