Add regression tests for simplification of singleton intervals

Author: NlightNFotis

regression/cbmc/simplify_singleton_interval_7690/negative_test.desc

@@ -0,0 +1,18 @@
+CORE 
+--trace
+singleton_interval_simp_neg.c
+^VERIFICATION FAILED$
+^\[main\.assertion\.1\] line \d expected failure: paths where x is unbounded explored: FAILURE$
+^\[main\.assertion\.2\] line \d+ expected failure: paths where 0 \<= x \<= 15 explored: FAILURE$
+^\[main\.assertion\.3\] line \d+ expected success: paths where x \<= 15 explored: SUCCESS$
+y=-6 \(11111111 11111111 11111111 11111010\)
+x=14 \(00000000 00000000 00000000 00001110\)
+y=34 \(00000000 00000000 00000000 00100010\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests the negative case of the simplification of the singleton interval
+(i.e when the presented interval *is* the *not* the singleton interval - 
+the set of possible values that the bounded variable can take has cardinality
+> 1).

regression/cbmc/simplify_singleton_interval_7690/positive_test.desc

@@ -0,0 +1,14 @@
+CORE 
+--trace
+singleton_interval_simp.c
+^VERIFICATION FAILED$
+^\[main\.assertion\.1\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$
+^\[main\.assertion\.2\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$
+x=15 \(00000000 00000000 00000000 00001111\)
+y=35 \(00000000 00000000 00000000 00100011\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests the positive case of the simplification of the singleton interval
+(i.e when the presented interval *is* the singleton interval)

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c

@@ -0,0 +1,17 @@
+// Positive test for singleton interval simplification.
+// Notice that the sequence of the inequalities in this
+// expression is different to the one in
+// `singleton_interval_in_assume_7690.c`.
+
+int main()
+{
+  int x;
+  __CPROVER_assume(x >= 15 && x <= 15);
+  int y = x + 20;
+
+  __CPROVER_assert(
+    y != 35, "expected failure: only paths where x == 15 explored");
+  __CPROVER_assert(
+    y == 34, "expected failure: only paths where x == 15 explored");
+  return 0;
+}

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c

@@ -0,0 +1,18 @@
+// Negative test for singleton interval simplification.
+
+int main()
+{
+  int x;
+  int y = x + 20;
+
+  __CPROVER_assert(
+    y != -6, "expected failure: paths where x is unbounded explored");
+
+  __CPROVER_assume(x >= 0 && x <= 15);
+  __CPROVER_assert(
+    y != 34, "expected failure: paths where 0 <= x <= 15 explored");
+
+  int z = x + 20;
+  __CPROVER_assert(z != 36, "expected success: paths where x <= 15 explored");
+  return 0;
+}