diff --git a/tests/spec/module.i b/tests/spec/module.i
new file mode 100644
index 0000000000000000000000000000000000000000..5198060dd0aa0fe31cb8039eea410788c3c6397c
--- /dev/null
+++ b/tests/spec/module.i
@@ -0,0 +1,8 @@
+/* run.config
+   EXIT: 1
+   OPT:
+ */
+
+/*@
+  logic integer next(integer x) = int::Int::add(x,1);
+ */
diff --git a/tests/spec/oracle/module.res.oracle b/tests/spec/oracle/module.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..809701e2a74442563ec63fdaceee2e2364d53805
--- /dev/null
+++ b/tests/spec/oracle/module.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing module.i (no preprocessing)
+[kernel:annot-error] module.i:7: Warning: 
+  lexical error, unexpected long identifier
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] Frama-C aborted: invalid user input.