diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 93a00b75b286d86d371db4ea118b5ad6d3951fe3..f5006fd95ba3ffa91d98ab0e8eee3dbaa053259a 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1187,7 +1187,7 @@ struct
          match outcome with
          | Warning.Result(warn , wp) -> { wp with vcs = add_warnings warn wp.vcs }
          | Warning.Failed warn ->
-             let v_post = do_assigns_everything ~stmt ~warn p_post.effects p_exit.vcs in
+             let v_post = do_assigns_everything ~stmt ~warn p_post.effects p_post.vcs in
              let v_exit = do_assigns_everything ~stmt ~warn p_exit.effects p_exit.vcs in
              let effects = Eset.union p_post.effects p_exit.effects in
              let vcs = gmerge v_post v_exit in
diff --git a/src/plugins/wp/tests/wp/bad_cast_call.i b/src/plugins/wp/tests/wp/bad_cast_call.i
new file mode 100644
index 0000000000000000000000000000000000000000..96a0ef6a0e3939e5bee114e6a541d9a69b199f8e
--- /dev/null
+++ b/src/plugins/wp/tests/wp/bad_cast_call.i
@@ -0,0 +1,7 @@
+char *m(void);
+
+void foo() {
+	char** pages = (void*)0;
+	pages = m();
+	/*@ assert MUST_FAIL: pages == (void*) 0; */
+}
diff --git a/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a95bbd54e16d6a4cae6e6a32171928aeebb00fbd
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
@@ -0,0 +1,16 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/bad_cast_call.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/bad_cast_call.i:3: Warning: 
+  Neither code nor specification for function m, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/bad_cast_call.i:5: Warning: 
+  Cast with incompatible pointers types (source: sint8*) (target: char**)
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Assertion 'MUST_FAIL' (file tests/wp/bad_cast_call.i, line 6):
+Prove: null = pages_0.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b750c3303f52fe9e24e573eea551f823e94d1757
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
@@ -0,0 +1,16 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/bad_cast_call.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/bad_cast_call.i:3: Warning: 
+  Neither code nor specification for function m, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/bad_cast_call.i:5: Warning: 
+  Cast with incompatible pointers types (source: sint8*) (target: char**)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_foo_assert_MUST_FAIL : Unsuccess
+[wp] Proved goals:    0 / 1
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  foo                       -        -        1       0.0%
+------------------------------------------------------------