Add tests for the bitwise operators (and, or, not, xor)

Author: NlightNFotis

regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc

@@ -0,0 +1,10 @@
+CORE
+bitwise_ops.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+\[main\.assertion\.1\] line \d+ A and B should be satisfiable: FAILURE
+\[main\.assertion\.2\] line \d+ A or B should be satisfiable: SUCCESS
+\[main\.assertion\.3\] line \d+ Not A equals B should be satisfiable: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise_ops.c

@@ -0,0 +1,12 @@
+int main()
+{
+    int a;
+    int b;
+
+    __CPROVER_assume(a != 0);
+
+    __CPROVER_assert(a & b, "A and B should be satisfiable");
+    __CPROVER_assert(a | b, "A or B should be satisfiable");
+    // __CRPOVER_assert(a ^ b, "A xor B should be satisfiable");
+    __CPROVER_assert(~a == b, "Not A equals B should be satisfiable");
+}