Add regression tests for the right shifting behaviour of the new SMT backend

Author: NlightNFotis

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

@@ -0,0 +1,24 @@
+int main()
+{
+  // In C, whether a right-shift is arithmetic or logical depends on the
+  // original type being shifted. An unsigned value will be shifted to
+  // the right in a logical manner (this assigns `0` to the leftmost bit).
+  // If the type is signed, right shift will assign the sign bit to the
+  // leftmost digit.
+
+  int bitmask_2 = 0x2;
+  int bitmask_3 = 0x3;
+
+  int first;
+  unsigned int second;
+
+  int place;
+  __CPROVER_assume(place >= 1);
+
+  int result_signed = first >> place;
+  unsigned int result_unsigned = second >> place;
+
+  __CPROVER_assert(result_signed && bitmask_2, "This should be satisfiable");
+  __CPROVER_assert(
+    result_unsigned && bitmask_3, "This should also be satisfiable");
+}

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

@@ -0,0 +1,13 @@
+CORE
+shift_right.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+\[main\.assertion\.1\] line \d+ This should be satisfiable: FAILURE
+\[main\.assertion\.2\] line \d+ This should also be satisfiable: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The assertions in the C file for this test are designed to be satisfiable,
+by certain results that we get back from the solver. This is so that we can
+test the driving of the new SMT backend, and to make sure we do get results
+back that are the result of a verification run.