Add tests

test/libsolidity/smtCheckerTests/types/array_dynamic_1.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint y) public {
+		array[x] = 200;
+		require(x == y);
+		assert(array[y] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_dynamic_1_fail.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint y) public {
+		array[x] = 200;
+		require(x == y);
+		assert(array[y] > 300);
+	}
+}
+// ----
+// Warning: (137-159): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_2.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][] array;
+	function f(uint x, uint y, uint z, uint t) public view {
+		require(array[x][y] == 200);
+		require(x == z && y == t);
+		assert(array[z][t] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][] array;
+	function f(uint x, uint y, uint z, uint t) public view {
+		require(array[x][y] == 200);
+		require(x == z && y == t);
+		assert(array[z][t] > 300);
+	}
+}
+// ----
+// Warning: (183-208): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_3.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][][] array;
+	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
+		require(array[x][y][z] == 200);
+		require(x == t && y == w && z == v);
+		assert(array[t][w][v] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][][] array;
+	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
+		require(array[x][y][z] == 200);
+		require(x == t && y == w && z == v);
+		assert(array[t][w][v] > 300);
+	}
+}
+// ----
+// Warning: (214-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint[] memory array, uint x, uint y) public pure {
+		array[x] = 200;
+		require(x == y);
+		assert(array[y] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint[] memory array, uint x, uint y) public pure {
+		array[x] = 200;
+		require(x == y);
+		assert(array[y] > 300);
+	}
+}
+// ----
+// Warning: (148-170): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_literal_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint[3] memory array = [uint(1), 2, 3];
+	}
+}
+// ----
+// Warning: (76-96): Unused local variable.
+// Warning: (99-114): Assertion checker does not yet implement tuples and inline arrays.
+// Warning: (99-114): Internal error: Expression undefined for SMT solver.

test/libsolidity/smtCheckerTests/types/array_static_1.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[10] array;
+	function f(uint x, uint y) public {
+		array[x] = 200;
+		require(x == y);
+		assert(array[y] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_static_1_fail.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[10] array;
+	function f(uint x, uint y) public {
+		array[x] = 200;
+		require(x == y);
+		assert(array[y] > 300);
+	}
+}
+// ----
+// Warning: (139-161): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_2.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[10][20] array;
+	function f(uint x, uint y, uint z, uint t) public view {
+		require(array[x][y] == 200);
+		require(x == z && y == t);
+		assert(array[z][t] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[10][20] array;
+	function f(uint x, uint y, uint z, uint t) public view {
+		require(array[x][y] == 200);
+		require(x == z && y == t);
+		assert(array[z][t] > 300);
+	}
+}
+// ----
+// Warning: (187-212): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_3.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[10][20][30] array;
+	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
+		require(array[x][y][z] == 200);
+		require(x == t && y == w && z == v);
+		assert(array[t][w][v] > 100);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[10][20][30] array;
+	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
+		require(array[x][y][z] == 200);
+		require(x == t && y == w && z == v);
+		assert(array[t][w][v] > 300);
+	}
+}
+// ----
+// Warning: (220-248): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/bytes_2.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bytes memory b1, bytes memory b2) public pure {
+		b1 = b2;
+		assert(b1[1] == b2[1]);
+	}
+}

test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bytes memory b1, bytes memory b2) public pure {
+		b1 = b2;
+		assert(b1[1] == b2[2]);
+	}
+}
+// ----
+// Warning: (119-141): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/string_1.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(string memory s1, string memory s2) public pure {
+		assert(bytes(s1).length == bytes(s2).length);
+	}
+}
+// ----
+// Warning: (117-133): Assertion checker does not yet support this expression.
+// Warning: (137-153): Assertion checker does not yet support this expression.
+// Warning: (117-133): Internal error: Expression undefined for SMT solver.
+// Warning: (137-153): Internal error: Expression undefined for SMT solver.
+// Warning: (110-154): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/string_2.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		string memory s = "Hello World";
+	}
+}
+// ----
+// Warning: (76-91): Unused local variable.
+// Warning: (94-107): Assertion checker does not yet support the type of this literal (literal_string "Hello World").