Add a test for the exercise of the signed-overflow-check flag under the new SMT backend.

Author: NlightNFotis

regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.c

@@ -0,0 +1,10 @@
+#include <limits.h>
+
+int main()
+{
+  int x = INT_MAX;
+  int y;
+  int z = x + y;
+
+  __CPROVER_assert(z < INT_MIN, "This assertion is falsifiable");
+}

regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+signed_overflow.c
+--incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+Invariant check failed
+Reason: Reached unimplemented Generation of SMT formula for unknown kind of expression: overflow-\+
+--
+This tests exercise the driving of the `--signed-overflow-check` flag.