diff --git a/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a22e16a5c310bb1d8147af73a86dcb698042c5d4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_usage/ref-usage-lemmas.i (no preprocessing)
+[wp] Running WP plugin...
+.................................................
+... Ref Usage
+.................................................
+Init: { &a b }
+Function foo: { &a b *x }
+Function main: { &a b __retres }
+.................................................
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Pre-condition (file tests/wp_usage/ref-usage-lemmas.i, line 30) in 'main':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i b/src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i
new file mode 100644
index 0000000000000000000000000000000000000000..77c4c5855222fecd05b80fbedddb39f2758757ed
--- /dev/null
+++ b/src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i
@@ -0,0 +1,34 @@
+/* run.config
+  OPT: -wp-msg-key refusage
+*/
+/* run.config_qualif
+  DONTRUN:
+*/
+
+int a ;
+int b ;
+
+/*@ axiomatic A{
+    logic int* get reads \nothing ;
+    logic int* get_h = &a ;
+
+    axiom a: get_h == get ;
+    }
+
+*/
+
+/*@ axiomatic B{
+  logic integer value reads \nothing ;
+  axiom b: value == b ;
+  }
+*/
+
+void foo(int* x){
+  *x = a = b ;
+}
+
+/*@ requires a <= b ; */
+int main(void){
+  int e ;
+  foo(&e) ;
+}