Add a regression test that drives the left shift behaviour in the new SMT backend

Author: NlightNFotis

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

@@ -0,0 +1,10 @@
+int main()
+{
+  int starting_val = 1;
+  int shifting_places;
+  __CPROVER_assume(shifting_places > 0);
+  __CPROVER_assume(shifting_places < 32);
+  int result = starting_val << shifting_places;
+
+  __CPROVER_assert(result > 1, "Shifted result should be greater than one");
+}

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

@@ -0,0 +1,8 @@
+CORE
+shift_left.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+\[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--