Add new tests

test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function h() internal returns (uint[] storage) {
+		if (a[2] == 0)
+			a[2] = 3;
+		return a;
+	}
+	function g() public {
+		h()[2] = 4;
+		assert(h()[2] == 3);
+	}
+}
+// ----
+// Warning 6328: (191-210): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f() public pure {
+		S[] memory s1 = new S[](3);
+		s1[0].x = 2;
+		assert(s1[0].x == 2);
+		s1[1].t.y = 3;
+		assert(s1[1].t.y == 3);
+		s1[2].a[2] = 4;
+		assert(s1[2].a[2] == 4);
+		s1[0].ts[3].y = 5;
+		assert(s1[0].ts[3].y == 5);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == 6);
+	}
+}
+// ----
+// Warning 4588: (217-227): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f(S memory s2) public pure {
+		S[] memory s1 = new S[](3);
+		s1[0].x = 2;
+		assert(s1[0].x == s2.x);
+		s1[1].t.y = 3;
+		assert(s1[1].t.y == s2.t.y);
+		s1[2].a[2] = 4;
+		assert(s1[2].a[2] == s2.a[2]);
+		s1[0].ts[3].y = 5;
+		assert(s1[0].ts[3].y == s2.ts[3].y);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
+	}
+}
+// ----
+// Warning 6328: (257-280): Assertion violation happens here
+// Warning 6328: (301-328): Assertion violation happens here
+// Warning 6328: (350-379): Assertion violation happens here
+// Warning 6328: (404-439): Assertion violation happens here
+// Warning 6328: (467-508): Assertion violation happens here
+// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	S[] s1;
+	function f() public {
+		s1.push();
+		s1.push();
+		s1.push();
+		s1[0].x = 2;
+		assert(s1[0].x == 2);
+		s1[1].t.y = 3;
+		assert(s1[1].t.y == 3);
+		s1[2].a[2] = 4;
+		assert(s1[2].a[2] == 4);
+		s1[0].ts[3].y = 5;
+		assert(s1[0].ts[3].y == 5);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == 6);
+		s1.pop();
+		s1.pop();
+		s1.pop();
+	}
+}

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_memory.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function f(S memory s1, S memory s2, bool b) public pure {
+		S memory s3 = b ? s1 : s2;
+		assert(s3.x == s1.x);
+		assert(s3.x == s2.x);
+		// This is safe.
+		assert(s3.x == s1.x || s3.x == s2.x);
+		// This fails as false positive because of lack of support to aliasing.
+		s3.x = 42;
+		assert(s3.x == s1.x || s3.x == s2.x);
+	}
+}
+// ----
+// Warning 6328: (208-228): Assertion violation happens here
+// Warning 6328: (232-252): Assertion violation happens here
+// Warning 6328: (402-438): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s1;
+	S s2;
+	function f(bool b) public {
+		S storage s3 = b ? s1 : s2;
+		assert(s3.x == s1.x);
+		assert(s3.x == s2.x);
+		// This is safe.
+		assert(s3.x == s1.x || s3.x == s2.x);
+		// This fails as false positive because of lack of support to aliasing.
+		s3.x = 42;
+		assert(s3.x == s1.x || s3.x == s2.x);
+	}
+	function g(bool b, uint _x) public {
+		if (b)
+			s1.x = _x;
+		else
+			s2.x = _x;
+	}
+}
+// ----
+// Warning 6328: (158-178): Assertion violation happens here
+// Warning 6328: (182-202): Assertion violation happens here
+// Warning 6328: (352-388): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_safe.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f() public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x == 2);
+		s1.t.y = 3;
+		assert(s1.t.y == 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] == 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == 6);
+	}
+}

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f() public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x != 2);
+		s1.t.y = 3;
+		assert(s1.t.y != 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] != 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y != 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] != 6);
+	}
+}
+// ----
+// Warning 6328: (228-245): Assertion violation happens here
+// Warning 6328: (263-282): Assertion violation happens here
+// Warning 6328: (301-321): Assertion violation happens here
+// Warning 6328: (343-366): Assertion violation happens here
+// Warning 6328: (391-417): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f(S memory s2) public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x == s2.x);
+		s1.t.y = 3;
+		assert(s1.t.y == s2.t.y);
+		s1.a[2] = 4;
+		assert(s1.a[2] == s2.a[2]);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == s2.ts[3].y);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
+	}
+}
+// ----
+// Warning 6328: (239-259): Assertion violation happens here
+// Warning 6328: (277-301): Assertion violation happens here
+// Warning 6328: (320-346): Assertion violation happens here
+// Warning 6328: (368-400): Assertion violation happens here
+// Warning 6328: (425-463): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_safe.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	S s1;
+	function f() public {
+		s1.x = 2;
+		assert(s1.x == 2);
+		s1.t.y = 3;
+		assert(s1.t.y == 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] == 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == 6);
+	}
+}

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	S s1;
+	function f() public {
+		s1.x = 2;
+		assert(s1.x != 2);
+		s1.t.y = 3;
+		assert(s1.t.y != 3);
+		s1.a[2] = 4;
+		assert(s1.a[2] != 4);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y != 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] != 6);
+	}
+}
+// ----
+// Warning 6328: (181-198): Assertion violation happens here
+// Warning 6328: (216-235): Assertion violation happens here
+// Warning 6328: (254-274): Assertion violation happens here
+// Warning 6328: (296-319): Assertion violation happens here
+// Warning 6328: (344-370): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_delete_memory.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function f(S memory s1, S memory s2) public pure {
+		delete s1;
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a.length == 0);
+	}
+}
+// ----
+// Warning 6328: (184-204): Assertion violation happens here
+// Warning 6328: (208-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_delete_storage.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s1;
+	function g(S memory s2) public {
+		s1.x = s2.x;
+		s1.a = s2.a;
+	}
+	function f(S memory s2) public {
+		delete s1;
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a.length == 0);
+	}
+}
+// ----
+// Warning 6328: (240-260): Assertion violation happens here
+// Warning 6328: (264-298): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		mapping (uint => uint) m;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.m[0] == s2.m[0]);
+	}
+	function g(uint a, uint b) public {
+		s1.m[a] = b;
+	}
+}
+// ----
+// Warning 4661: (143-169): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+	}
+}
+// ----
+// Warning 6328: (124-144): Assertion violation happens here
+// Warning 6328: (148-182): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (131-135): Assertion checker does not yet support this expression.
+// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (139-143): Assertion checker does not yet support this expression.
+// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (155-159): Assertion checker does not yet support this expression.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-174): Assertion checker does not yet support this expression.
+// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol

@@ -0,0 +1,69 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a[0].x == s2.a[0].x);
+	}
+	function g() public {
+		s1.x = 42;
+		s2.x = 42;
+		s1.a.push();
+		s2.a.push();
+		s1.a[0].x = 43;
+		s2.a[0].x = 43;
+	}
+}
+// ----
+// Warning 6328: (124-144): Assertion violation happens here
+// Warning 6328: (148-182): Assertion violation happens here
+// Warning 6328: (186-216): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (131-135): Assertion checker does not yet support this expression.
+// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (139-143): Assertion checker does not yet support this expression.
+// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (155-159): Assertion checker does not yet support this expression.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-174): Assertion checker does not yet support this expression.
+// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (193-202): Assertion checker does not yet support this expression.
+// Warning 7650: (193-197): Assertion checker does not yet support this expression.
+// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (206-215): Assertion checker does not yet support this expression.
+// Warning 7650: (206-210): Assertion checker does not yet support this expression.
+// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (246-250): Assertion checker does not yet support this expression.
+// Warning 8364: (246-248): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (246-250): Assertion checker does not support recursive structs.
+// Warning 7650: (259-263): Assertion checker does not yet support this expression.
+// Warning 8364: (259-261): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (259-263): Assertion checker does not support recursive structs.
+// Warning 7650: (272-276): Assertion checker does not yet support this expression.
+// Warning 8364: (272-274): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (272-283): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (272-276): Assertion checker does not support recursive structs.
+// Warning 7650: (287-291): Assertion checker does not yet support this expression.
+// Warning 8364: (287-289): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (287-298): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (287-291): Assertion checker does not support recursive structs.
+// Warning 7650: (302-311): Assertion checker does not yet support this expression.
+// Warning 7650: (302-306): Assertion checker does not yet support this expression.
+// Warning 8364: (302-304): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (302-309): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (302-311): Assertion checker does not support recursive structs.
+// Warning 7650: (320-329): Assertion checker does not yet support this expression.
+// Warning 7650: (320-324): Assertion checker does not yet support this expression.
+// Warning 8364: (320-322): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (320-327): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (320-329): Assertion checker does not support recursive structs.

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol

@@ -0,0 +1,123 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+		assert(s1.a[0].x == s2.a[0].x);
+		assert(s1.a[0].a.length == s2.a[0].a.length);
+		assert(s1.a[0].a[0].x == s2.a[0].a[0].x);
+	}
+	function g() public {
+		s1.x = 42;
+		s2.x = 42;
+		s1.a.push();
+		s2.a.push();
+		s1.a[0].x = 43;
+		s2.a[0].x = 43;
+		s1.a[0].a.push();
+		s2.a[0].a.push();
+		s1.a[0].a[0].x = 44;
+		s2.a[0].a[0].x = 44;
+	}
+}
+// ----
+// Warning 6328: (124-144): Assertion violation happens here
+// Warning 6328: (148-182): Assertion violation happens here
+// Warning 6328: (186-216): Assertion violation happens here
+// Warning 6328: (220-264): Assertion violation happens here
+// Warning 6328: (268-308): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (131-135): Assertion checker does not yet support this expression.
+// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (139-143): Assertion checker does not yet support this expression.
+// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (155-159): Assertion checker does not yet support this expression.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-174): Assertion checker does not yet support this expression.
+// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (193-202): Assertion checker does not yet support this expression.
+// Warning 7650: (193-197): Assertion checker does not yet support this expression.
+// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (206-215): Assertion checker does not yet support this expression.
+// Warning 7650: (206-210): Assertion checker does not yet support this expression.
+// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (227-236): Assertion checker does not yet support this expression.
+// Warning 7650: (227-231): Assertion checker does not yet support this expression.
+// Warning 8364: (227-229): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (227-234): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (247-256): Assertion checker does not yet support this expression.
+// Warning 7650: (247-251): Assertion checker does not yet support this expression.
+// Warning 8364: (247-249): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (247-254): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (275-289): Assertion checker does not yet support this expression.
+// Warning 7650: (275-284): Assertion checker does not yet support this expression.
+// Warning 7650: (275-279): Assertion checker does not yet support this expression.
+// Warning 8364: (275-277): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (275-282): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (275-287): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (293-307): Assertion checker does not yet support this expression.
+// Warning 7650: (293-302): Assertion checker does not yet support this expression.
+// Warning 7650: (293-297): Assertion checker does not yet support this expression.
+// Warning 8364: (293-295): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (293-300): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (293-305): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (338-342): Assertion checker does not yet support this expression.
+// Warning 8364: (338-340): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (338-342): Assertion checker does not support recursive structs.
+// Warning 7650: (351-355): Assertion checker does not yet support this expression.
+// Warning 8364: (351-353): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (351-355): Assertion checker does not support recursive structs.
+// Warning 7650: (364-368): Assertion checker does not yet support this expression.
+// Warning 8364: (364-366): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (364-375): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (364-368): Assertion checker does not support recursive structs.
+// Warning 7650: (379-383): Assertion checker does not yet support this expression.
+// Warning 8364: (379-381): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (379-390): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (379-383): Assertion checker does not support recursive structs.
+// Warning 7650: (394-403): Assertion checker does not yet support this expression.
+// Warning 7650: (394-398): Assertion checker does not yet support this expression.
+// Warning 8364: (394-396): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (394-401): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (394-403): Assertion checker does not support recursive structs.
+// Warning 7650: (412-421): Assertion checker does not yet support this expression.
+// Warning 7650: (412-416): Assertion checker does not yet support this expression.
+// Warning 8364: (412-414): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (412-419): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (412-421): Assertion checker does not support recursive structs.
+// Warning 7650: (430-439): Assertion checker does not yet support this expression.
+// Warning 7650: (430-434): Assertion checker does not yet support this expression.
+// Warning 8364: (430-432): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (430-437): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (430-446): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (430-439): Assertion checker does not support recursive structs.
+// Warning 7650: (450-459): Assertion checker does not yet support this expression.
+// Warning 7650: (450-454): Assertion checker does not yet support this expression.
+// Warning 8364: (450-452): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (450-457): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (450-466): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (450-459): Assertion checker does not support recursive structs.
+// Warning 7650: (470-484): Assertion checker does not yet support this expression.
+// Warning 7650: (470-479): Assertion checker does not yet support this expression.
+// Warning 7650: (470-474): Assertion checker does not yet support this expression.
+// Warning 8364: (470-472): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (470-477): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (470-482): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (470-484): Assertion checker does not support recursive structs.
+// Warning 7650: (493-507): Assertion checker does not yet support this expression.
+// Warning 7650: (493-502): Assertion checker does not yet support this expression.
+// Warning 7650: (493-497): Assertion checker does not yet support this expression.
+// Warning 8364: (493-495): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (493-500): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (493-505): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (493-507): Assertion checker does not support recursive structs.

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol

@@ -0,0 +1,56 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f(bool b1, bool b2) public {
+		S storage s3 = b1 ? s1 : s2;
+		S storage s4 = b2 ? s1 : s2;
+		assert(s3.x == s1.x || s3.x == s2.x);
+		assert(s4.x == s1.x || s4.x == s2.x);
+		s3.x = 44;
+		// Fails as false positive because of lack of support to aliasing.
+		assert(s1.x == 44 || s2.x == 44);
+	}
+}
+// ----
+// Warning 6328: (197-233): Assertion violation happens here
+// Warning 6328: (237-273): Assertion violation happens here
+// Warning 6328: (359-391): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (135-147): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (166-178): Assertion checker does not yet support the type of this variable.
+// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (160-162): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (150-162): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 8364: (186-188): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (191-193): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (181-193): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (204-208): Assertion checker does not yet support this expression.
+// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (212-216): Assertion checker does not yet support this expression.
+// Warning 8364: (212-214): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (220-224): Assertion checker does not yet support this expression.
+// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (228-232): Assertion checker does not yet support this expression.
+// Warning 8364: (228-230): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (244-248): Assertion checker does not yet support this expression.
+// Warning 8364: (244-246): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (252-256): Assertion checker does not yet support this expression.
+// Warning 8364: (252-254): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (260-264): Assertion checker does not yet support this expression.
+// Warning 8364: (260-262): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 7650: (268-272): Assertion checker does not yet support this expression.
+// Warning 8364: (268-270): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (277-281): Assertion checker does not yet support this expression.
+// Warning 8364: (277-279): Assertion checker does not yet implement type struct C.S storage pointer
+// Warning 4375: (277-281): Assertion checker does not support recursive structs.
+// Warning 7650: (366-370): Assertion checker does not yet support this expression.
+// Warning 8364: (366-368): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (380-384): Assertion checker does not yet support this expression.
+// Warning 8364: (380-382): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S[] sa;
+	S[][] sa2;
+	function f() public {
+		sa.push();
+		sa2.push();
+		sa2[0].push();
+		sa2[0][0].a.push();
+		assert(sa2[0][0].a.length == sa[0].a.length);
+	}
+}
+// ----
+// Warning 6328: (192-236): Assertion violation happens here
+// Warning 8364: (126-135): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (153-166): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (170-181): Assertion checker does not yet support this expression.
+// Warning 8364: (170-179): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (170-188): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (170-181): Assertion checker does not support recursive structs.
+// Warning 7650: (199-210): Assertion checker does not yet support this expression.
+// Warning 8364: (199-208): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (221-228): Assertion checker does not yet support this expression.
+// Warning 8364: (221-226): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol

@@ -0,0 +1,66 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public {
+		s1.x = 10;
+		++s1.x;
+		s1.x++;
+		s2.x = 20;
+		--s2.x;
+		s2.x--;
+		assert(s1.x == s2.x + 6);
+		assert(s1.a.length == s2.a.length);
+		delete s1;
+		assert(s1.x == 0);
+	}
+}
+// ----
+// Warning 4984: (200-208): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 6328: (185-209): Assertion violation happens here
+// Warning 6328: (213-247): Assertion violation happens here
+// Warning 6328: (264-281): Assertion violation happens here
+// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (119-123): Assertion checker does not yet support this expression.
+// Warning 8364: (119-121): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (119-123): Assertion checker does not support recursive structs.
+// Warning 7650: (134-138): Assertion checker does not yet support this expression.
+// Warning 8364: (134-136): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (134-138): Assertion checker does not support recursive structs.
+// Warning 7650: (142-146): Assertion checker does not yet support this expression.
+// Warning 8364: (142-144): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (142-146): Assertion checker does not support recursive structs.
+// Warning 7650: (152-156): Assertion checker does not yet support this expression.
+// Warning 8364: (152-154): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (152-156): Assertion checker does not support recursive structs.
+// Warning 7650: (167-171): Assertion checker does not yet support this expression.
+// Warning 8364: (167-169): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (167-171): Assertion checker does not support recursive structs.
+// Warning 7650: (175-179): Assertion checker does not yet support this expression.
+// Warning 8364: (175-177): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (175-179): Assertion checker does not support recursive structs.
+// Warning 7650: (192-196): Assertion checker does not yet support this expression.
+// Warning 8364: (192-194): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (200-204): Assertion checker does not yet support this expression.
+// Warning 8364: (200-202): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (220-224): Assertion checker does not yet support this expression.
+// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (235-239): Assertion checker does not yet support this expression.
+// Warning 8364: (235-237): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (271-275): Assertion checker does not yet support this expression.
+// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4144: (132-138): Underflow (resulting value less than 0) happens here
+// Warning 2661: (132-138): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4144: (142-148): Underflow (resulting value less than 0) happens here
+// Warning 2661: (142-148): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4144: (165-171): Underflow (resulting value less than 0) happens here
+// Warning 2661: (165-171): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4144: (175-181): Underflow (resulting value less than 0) happens here
+// Warning 2661: (175-181): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		T[] a;
+	}
+	struct T {
+		uint y;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.x == s2.x);
+		assert(s1.a.length == s2.a.length);
+	}
+}
+// ----
+// Warning 6328: (158-178): Assertion violation happens here
+// Warning 6328: (182-216): Assertion violation happens here
+// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (165-169): Assertion checker does not yet support this expression.
+// Warning 8364: (165-167): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (173-177): Assertion checker does not yet support this expression.
+// Warning 8364: (173-175): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (189-193): Assertion checker does not yet support this expression.
+// Warning 8364: (189-191): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (204-208): Assertion checker does not yet support this expression.
+// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol

@@ -0,0 +1,57 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		T[] a;
+	}
+	struct T {
+		uint y;
+		S[] a;
+	}
+	S s1;
+	S s2;
+	function f() public {
+		s1.a.push();
+		s2.a.push();
+		s1.a[0].a.push();
+		s2.a[0].a.push();
+		assert(s1.a[0].a[0].x == s2.a[0].a[0].x);
+	}
+}
+// ----
+// Warning 6328: (223-263): Assertion violation happens here
+// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable.
+// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable.
+// Warning 7650: (153-157): Assertion checker does not yet support this expression.
+// Warning 8364: (153-155): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (153-164): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 4375: (153-157): Assertion checker does not support recursive structs.
+// Warning 7650: (168-172): Assertion checker does not yet support this expression.
+// Warning 8364: (168-170): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (168-179): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 4375: (168-172): Assertion checker does not support recursive structs.
+// Warning 7650: (183-192): Assertion checker does not yet support this expression.
+// Warning 7650: (183-187): Assertion checker does not yet support this expression.
+// Warning 8364: (183-185): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (183-190): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (183-199): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (183-192): Assertion checker does not support recursive structs.
+// Warning 7650: (203-212): Assertion checker does not yet support this expression.
+// Warning 7650: (203-207): Assertion checker does not yet support this expression.
+// Warning 8364: (203-205): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (203-210): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (203-219): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 4375: (203-212): Assertion checker does not support recursive structs.
+// Warning 7650: (230-244): Assertion checker does not yet support this expression.
+// Warning 7650: (230-239): Assertion checker does not yet support this expression.
+// Warning 7650: (230-234): Assertion checker does not yet support this expression.
+// Warning 8364: (230-232): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (230-237): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (230-242): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 7650: (248-262): Assertion checker does not yet support this expression.
+// Warning 7650: (248-257): Assertion checker does not yet support this expression.
+// Warning 7650: (248-252): Assertion checker does not yet support this expression.
+// Warning 8364: (248-250): Assertion checker does not yet implement type struct C.S storage ref
+// Warning 8364: (248-255): Assertion checker does not yet implement type struct C.T storage ref
+// Warning 8364: (248-260): Assertion checker does not yet implement type struct C.S storage ref

test/libsolidity/smtCheckerTests/types/struct/struct_return.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function s() internal pure returns (S memory s1) {
+		s1.x = 42;
+		s1.a[2] = 43;
+	}
+	function f() public pure {
+		S memory s2 = s();
+		assert(s2.x == 42);
+		assert(s2.a[2] == 43);
+		assert(s2.a[3] == 43);
+	}
+}
+// ----
+// Warning 6328: (265-286): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_state_var.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s;
+	function f(uint _x) public {
+		s.x = _x;
+		s.a[0] = _x;
+		assert(s.a[1] == s.a[0]);
+	}
+}
+// ----
+// Warning 6328: (148-172): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s;
+	function f(uint _x) public {
+		s.a.pop();
+		s.a.length;
+		s.a.push();
+		s.x = _x;
+		s.a.pop();
+		s.a.push();
+		s.a.push();
+		s.a[0] = _x;
+		assert(s.a[1] == s.a[0]);
+		s.a.pop();
+		s.a.pop();
+	}
+}
+// ----
+// Warning 2529: (121-130): Empty array "pop" detected here
+// Warning 6328: (230-254): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	S s;
+	function f(uint _x) public {
+		s.x = _x;
+		s.a.pop();
+		s.a.push();
+		s.a.push();
+		s.a[0] = _x;
+		assert(s.a[1] == s.a[0]);
+		s.a.pop();
+		s.a.pop();
+	}
+}
+// ----
+// Warning 2529: (133-142): Empty array "pop" detected here.
+// Warning 6328: (189-213): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function f(S memory s1, S memory s2) public pure {
+		delete s1;
+		s1.x++;
+		++s1.x;
+		assert(s1.x == 2);
+		assert(s1.x == s2.x);
+	}
+}
+// ----
+// Warning 6328: (225-245): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct S {
+		uint x;
+		uint[] a;
+	}
+	function f(S memory s1, S memory s2) public pure {
+		delete s1;
+		s1.x = 100;
+		s1.x--;
+		--s1.x;
+		assert(s1.x == 98);
+		assert(s1.x == s2.x);
+	}
+}
+// ----
+// Warning 6328: (240-260): Assertion violation happens here