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

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	function f(bool b) public pure {
-		uint v = 0;
-		if (b)
-			v ^= 1;
-		assert(v == 1);
-	}
-}
-// ----
-// Warning 6328: (116-130): Assertion violation happens here.
-// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol

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

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		x ^= y;
+		assert(x != 1); // fails
+		x = -1; y = 1;
+		x ^= y;
+		assert(x == -2);
+		x = 4;
+		y ^= x;
+		assert(y == 5);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 7;
+        v ^= 3;
+        assert(v != 4); // fails, as 7 ^ 3 = 4
+
+        uint c = 0;
+        c ^= v;
+        assert(c == 4);
+
+        uint16 x = 0xff;
+        uint16 y = 0xffff;
+        y ^= x;
+        assert(y == 0xff); // fails
+        assert(y == 0xff00);
+
+        y = 0xf1;
+        x = 0xff00;
+        y ^= x | y;
+        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: (422-441): Assertion violation happens here.