From 2128ff9f137cd6be7be283a7bfc7cffb08773695 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 29 May 2020 19:13:27 +0200
Subject: [PATCH] Fix ICE on push for member access

---
 libsolidity/formal/SMTEncoder.cpp             |  6 ++++
 .../array_members/push_struct_member_1.sol    | 27 +++++++++++++++
 .../array_members/push_struct_member_2.sol    | 33 +++++++++++++++++++
 3 files changed, 66 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 6729703b7..8ed8d71fa 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1150,6 +1150,12 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 	}
 	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
 		arrayIndexAssignment(*indexAccess, _array);
+	else if (dynamic_cast<MemberAccess const*>(&_expr))
+		m_errorReporter.warning(
+			9599_error,
+			_expr.location(),
+			"Assertion checker does not yet implement this expression."
+		);
 	else
 		solAssert(false, "");
 }
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol
new file mode 100644
index 000000000..4647742db
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol
@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		int[] b;
+	}
+	S s;
+	struct T {
+		S s;
+	}
+	T t;
+	function f() public {
+		s.b.push();
+		t.s.b.push();
+	}
+}
+
+// ----
+// Warning: (72-75): Assertion checker does not yet support the type of this variable.
+// Warning: (100-103): Assertion checker does not yet support the type of this variable.
+// Warning: (130-133): Assertion checker does not yet support this expression.
+// Warning: (130-131): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (130-133): Assertion checker does not yet implement this expression.
+// Warning: (144-149): Assertion checker does not yet support this expression.
+// Warning: (144-147): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (144-147): Assertion checker does not yet support this expression.
+// Warning: (144-145): Assertion checker does not yet implement type struct C.T storage ref
+// Warning: (144-149): Assertion checker does not yet implement this expression.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol
new file mode 100644
index 000000000..353d328fd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol
@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		int[] b;
+	}
+	S s;
+	struct T {
+		S[] s;
+	}
+	T t;
+	function f() public {
+		s.b.push();
+		t.s.push();
+		t.s[0].b.push();
+	}
+}
+
+// ----
+// Warning: (72-75): Assertion checker does not yet support the type of this variable.
+// Warning: (102-105): Assertion checker does not yet support the type of this variable.
+// Warning: (132-135): Assertion checker does not yet support this expression.
+// Warning: (132-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (132-135): Assertion checker does not yet implement this expression.
+// Warning: (146-149): Assertion checker does not yet support this expression.
+// Warning: (146-147): Assertion checker does not yet implement type struct C.T storage ref
+// Warning: (146-156): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (146-149): Assertion checker does not yet implement this expression.
+// Warning: (160-168): Assertion checker does not yet support this expression.
+// Warning: (160-163): Assertion checker does not yet support this expression.
+// Warning: (160-161): Assertion checker does not yet implement type struct C.T storage ref
+// Warning: (160-166): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (160-166): Assertion checker does not yet implement this expression.
+// Warning: (160-168): Assertion checker does not yet implement this expression.