diff --git a/regression/cbmc/Overflow_Addition2/main.c b/regression/cbmc/Overflow_Addition2/main.c
new file mode 100644
index 0000000000..c75ed76560
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition2/main.c
@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i++;
+}
diff --git a/regression/cbmc/Overflow_Addition2/test.desc b/regression/cbmc/Overflow_Addition2/test.desc
new file mode 100644
index 0000000000..2615a9d290
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition2/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Overflow_Addition3/main.c b/regression/cbmc/Overflow_Addition3/main.c
new file mode 100644
index 0000000000..0a4c6ec4e5
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition3/main.c
@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i += 1;
+}
diff --git a/regression/cbmc/Overflow_Addition3/test.desc b/regression/cbmc/Overflow_Addition3/test.desc
new file mode 100644
index 0000000000..30ddc3b3ab
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition3/test.desc
@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS
+^\[.*\] .* arithmetic overflow on signed type conversion in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The addition is done in signed int; hence, the overflow is only detected
+on conversion.
+
+See #4208.
diff --git a/regression/cbmc/Overflow_Addition4/main.c b/regression/cbmc/Overflow_Addition4/main.c
new file mode 100644
index 0000000000..aee20d618c
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition4/main.c
@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i = i + 1;
+}
diff --git a/regression/cbmc/Overflow_Addition4/test.desc b/regression/cbmc/Overflow_Addition4/test.desc
new file mode 100644
index 0000000000..56da91e200
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition4/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS
+^\[.*\] .* arithmetic overflow on signed type conversion in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The addition is done in signed int; hence, the overflow is only detected
+on conversion.