diff --git a/src/plugins/wp/tests/wp_region/affectations.c b/src/plugins/wp/tests/wp_region/affectations.c
new file mode 100644
index 0000000000000000000000000000000000000000..601aa47036e6badcfe4b339ce47cc1141c8ecc9f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/affectations.c
@@ -0,0 +1,22 @@
+/*@ predicate pointed(int *p, int* q) = p==q || \separated(p,q);
+*/
+
+/*@
+ requires \valid(p);
+ requires \valid(q);
+ requires pointed(p,q);
+ assigns *p, *q;
+ region PQ: *p, *q;
+ behavior EQ:
+ assumes p == q;
+ ensures P: *p == \old(*p);
+ ensures Q: *q == \old(*q);
+ behavior SEP:
+ assumes p != q;
+ ensures Q: *p == \old(*p)+1;
+ ensures Q: *q == \old(*q)-1;
+*/
+void f(int* p, int* q) {
+ (*p)++;
+ (*q)--;
+}
diff --git a/src/plugins/wp/tests/wp_region/heterogenous_cast.c b/src/plugins/wp/tests/wp_region/heterogenous_cast.c
new file mode 100644
index 0000000000000000000000000000000000000000..ef9c1c52cfb71e9dc96f179ee7a16596c2b3557d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/heterogenous_cast.c
@@ -0,0 +1,10 @@
+/*@
+ assigns *p;
+@*/
+void g (int *p) {
+ *p = 42;
+ short *q = (short*) p;
+ q[0] = -1;
+ q[1] = -1;
+ //@ assert *p == -1;
+}
diff --git a/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle b/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..90b845e92270d85fecec252c6d7b263039d4c3f6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
@@ -0,0 +1,86 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (1/2):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (2/2):
+Effect at line 21
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior EQ
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'P' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'Q' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior SEP
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = 1 + x.
+Let m = Msint32_0[p <- x_1].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Let x_4 = m[q <- x_3][p].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(Msint32_0[q]) /\ is_sint32(x_2) /\
+ is_sint32(x_3) /\ is_sint32(x_4).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, p, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, q, 4).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Pre-condition for 'SEP' *)
+ Have: q != p.
+}
+Prove: x_4 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = Msint32_0[q].
+Let m = Msint32_0[p <- 1 + x].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(m[q <- x_3][p]).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, p, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, q, 4).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Pre-condition for 'SEP' *)
+ Have: q != p.
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f7b3f9e10a0a8fe3c6adcd6578592bb6f035ea1d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
@@ -0,0 +1,85 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Assertion (file heterogenous_cast.c, line 9):
+Let x = read_sint32(write_sint16(write_sint16(write_sint32(mem_0, p, 42),
+ shift_sint16(p, 0), -1),
+ shift_sint16(p, 1), -1), p).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (1/3):
+Effect at line 5
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (2/3):
+Effect at line 7
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (3/3):
+Effect at line 8
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3679fc28e57abf2c942f179a5ce6933da56953e9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Valid] region_f_assigns_part1 (Qed)
+[wp] [Valid] region_f_assigns_part2 (Qed)
+[wp] [Valid] region_f_EQ_ensures_P (Qed)
+[wp] [Valid] region_f_EQ_ensures_Q (Qed)
+[wp] [Valid] region_f_SEP_ensures_Q (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_SEP_ensures_Q_2 (Alt-Ergo) (Cached)
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
+ Qed: 4
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 4 2 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5ef48e91de1c916556cd874542a66ad21d7b6f90
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
@@ -0,0 +1,65 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[wp] 4 goals scheduled
+[wp] [Valid] region_g_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_g_assigns_part1 (Qed)
+[wp] [Valid] region_g_assigns_part2 (Qed)
+[wp] [Valid] region_g_assigns_part3 (Qed)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 3
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ g 3 1 4 100%
+------------------------------------------------------------