[SMTChecker] Updating old and adding new tests for compound bitwise or operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol

@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	int[1] c;
-	function f(bool b) public {
-		if (b)
-			c[0] |= 1;
-	}
-}
-// ----
-// Warning 9149: (97-106): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol

@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	int[1][20] c;
-	function f(bool b) public {
-		if (b)
-			c[10][0] |= 1;
-	}
-}
-// ----
-// Warning 9149: (101-114): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	struct S {
-		uint x;
-	}
-	S s;
-	function f(bool b) public {
-		if (b)
-			s.x |= 1;
-	}
-}
-// ----
-// Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	struct S {
-		uint[] x;
-	}
-	S s;
-	function f(bool b) public {
-		if (b)
-			s.x[2] |= 1;
-	}
-}
-// ----
-// Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure returns (byte) {
+        byte a = 0xff;
+        byte b = 0xf0;
+        b |= a;
+        assert(a == b);
+
+        a |= ~b;
+        assert(a == 0); // fails
+    }
+}
+// ----
+// Warning 6328: (203-217): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		x |= y;
+		assert(x == 0); // fails
+		x = -1; y = 3;
+		x |= y;
+		assert(x == -1);
+		x = 4;
+		y |= x;
+		assert(y == 7);
+		y = 127;
+		x |= y;
+		assert(x == 127);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+    int[1][20] c;
+    function f(bool b) public {
+	    require(c[10][0] == 0);
+        if (b)
+            c[10][0] |= 1;
+        assert(c[10][0] == 0 || c[10][0] == 1);
+    }
+}
+// ----

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 7;
+        v |= 3;
+        assert(v != 7); // fails, as 7 | 3 = 7
+
+        uint c = 0;
+        c |= v;
+        assert(c == 7);
+
+        uint16 x = 0xff;
+        uint16 y = 0xffff;
+        y |= x;
+        assert(y == 0xff); // fails
+        assert(y == 0xffff);
+
+        y = 0xf1ff;
+        x = 0xff00;
+        x |= y & x;
+        assert(y == 0xffff); // fails
+        assert(x == 0xff00);
+    }
+}
+// ----
+// Warning 6328: (121-135): Assertion violation happens here.
+// Warning 6328: (298-315): Assertion violation happens here.
+// Warning 6328: (424-443): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+    uint[1] c;
+    function f(bool b) public {
+        require(c[0] == 0);
+        if (b)
+            c[0] |= 1;
+        assert(c[0] <= 1);
+    }
+}
+// ----

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    struct S {
+        uint[] x;
+    }
+    S s;
+    function f(bool b) public {
+        if (b)
+            s.x[2] |= 1;
+        assert(s.x[2] != 1);
+    }
+}
+// ----
+// Warning 6328: (173-192): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}
+// ----