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

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	function f(bool b) public pure {
-		uint v = 1;
-		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_and_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 != 0); // fails
+    }
+}
+// ----
+// Warning 6328: (203-217): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_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;
+		y &= x;
+		assert(y == 3);
+		y = -1;
+		y &= x;
+		assert(y == -1);
+		y = 127;
+		x &= y;
+		assert(x == 127);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 1;
+        v &= 1;
+        assert(v == 1);
+
+        v = 7;
+        v &= 3;
+        assert(v != 3); // fails, as 7 & 3 = 3
+
+        uint c = 0;
+        c &= v;
+        assert(c == 0);
+
+        uint8 x = 0xff;
+        uint16 y = 0xffff;
+        y &= x;
+        assert(y == 0xff);
+        assert(y == 0xffff); // fails
+
+        y = 0xffff;
+        x = 0xff;
+        y &= y | x;
+        assert(y == 0xffff);
+        assert(y == 0xff); // fails
+    }
+}
+// ----
+// Warning 6328: (177-191): Assertion violation happens here.
+// Warning 6328: (380-399): Assertion violation happens here.
+// Warning 6328: (506-523): Assertion violation happens here.