Add signed int overflow behaviour tests for the new SMT backend.

Author: NlightNFotis

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.c

@@ -0,0 +1,14 @@
+#include <limits.h>
+#include <stdlib.h>
+
+int main()
+{
+  int a = INT_MAX;
+  int b = INT_MIN;
+
+  __CPROVER_assert(
+    a + 1 == INT_MIN, "Wrap-around to INT_MIN when adding to INT_MAX");
+  __CPROVER_assert(
+    b - 1 == INT_MAX, "Wrap-around to INT_MAX when subtracting from INT_MIN");
+  __CPROVER_assert(a - b == -1, "INT_MAX minus INT_MIN equals -1");
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc

@@ -0,0 +1,13 @@
+CORE
+overflow_behaviour.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS
+\[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS
+\[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test is designed to test wrap-around behaviour for boundary-values
+of the int domain.