diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 930f3e439067597fe0408e5a2fd5c98396a940b2..fd5b6e5a5c32096042f5811ff950a968173b19d2 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -392,7 +392,7 @@ let get_stmt_assigns kf stmt =
               ) l s.spec_behavior
         | _ -> l
       end stmt []
-  in if asgn = [] then [WpPropId.empty_assigns_info] else asgn
+  in if asgn = [] then [WpPropId.mk_stmt_any_assigns_info stmt] else asgn
 
 (* -------------------------------------------------------------------------- *)
 (* --- Code Assertions                                                    --- *)
diff --git a/src/plugins/wp/tests/wp/default-stmt-assigns.i b/src/plugins/wp/tests/wp/default-stmt-assigns.i
new file mode 100644
index 0000000000000000000000000000000000000000..e18bff86ffc83ae76c0908329ef88c2301f41fc2
--- /dev/null
+++ b/src/plugins/wp/tests/wp/default-stmt-assigns.i
@@ -0,0 +1,4 @@
+void automaton_state_accessor() {
+  __asm__("");
+  //@ assert \false ;
+}
diff --git a/src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle b/src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..eed81d759ff4b59ae006601688a01868b8b513dc
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/default-stmt-assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/default-stmt-assigns.i:2: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
+------------------------------------------------------------
+  Function automaton_state_accessor
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp/default-stmt-assigns.i, line 3):
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..67146a0bc6c066304064669f98dfadfd786dacf4
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/default-stmt-assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/default-stmt-assigns.i:2: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_automaton_state_accessor_assert : Unsuccess
+[wp] Proved goals:    0 / 1
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  automaton_state_accessor   -       -        1       0.0%
+------------------------------------------------------------