[SMTChecker] Fix public getter for array of structs.

test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol

@@ -0,0 +1,16 @@
+pragma abicoder v1;
+pragma experimental SMTChecker;
+
+struct Item {
+	uint x;
+	uint y;
+}
+
+contract D {
+	Item[][][] public items;
+
+	function test() public view returns (uint) {
+		(uint a, uint b) = this.items(1, 2, 3);
+		return a + b;
+	}
+}

test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol

@@ -0,0 +1,22 @@
+pragma abicoder v1;
+pragma experimental SMTChecker;
+
+struct Item {
+	uint x;
+	uint y;
+}
+
+contract D {
+	Item[] public items;
+
+	function test() public {
+		delete items;
+		items.push(Item(42, 43));
+		(uint a, uint b) = this.items(0);
+		assert(a == 42); // should hold
+		assert(b == 43); // should hold
+		assert(b == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()

test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol

@@ -0,0 +1,24 @@
+pragma abicoder v1;
+pragma experimental SMTChecker;
+
+struct Item {
+	uint x;
+	uint y;
+	uint[] arr;
+}
+
+contract D {
+	Item[] public items;
+
+	function test() public {
+		delete items;
+		uint[] memory tmp = new uint[](1);
+		items.push(Item(42, 43, tmp));
+		(uint a, uint b) = this.items(0);
+		assert(a == 42); // should hold
+		assert(b == 43); // should hold
+		assert(b == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (355-369): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43, arr: [0]}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()