diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
index 6bd8a32285680acda3c4fc43d0dbed0a37767bed..7084d95178be87cdd794eaac63e65d7e67b7eb24 100644
--- a/tests/spec/Extend_recursive_preprocess.i
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -2,7 +2,18 @@
 MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
 OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
 */
+/*@ gl_foo foo1 {
+    gl_fooo must_replace(x);
+    gl_fooo must_replace(x);
+    gl_fooo must_replace(x);
+}*/
+
 
+/*@ gl_foo foo1 {
+    gl_foo foo2 {
+      gl_fooo must_replace(x);
+    }
+}*/
 
 /*@ gl_foo foo1 {
     gl_fooo must_replace(x);
diff --git a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
index ec48b5138f411a0f6f50e8dabb6ac894a15f6aae..0b8592e2baf7f2698a55f9df078ffa54537f2859 100644
--- a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
+++ b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
@@ -1,20 +1,29 @@
 [kernel] Parsing tests/spec/Extend_recursive_preprocess.i (no preprocessing)
 /* Generated by Frama-C */
+/*@ gl_foo foo1_ok {
+      gl_fooo \false;
+      gl_fooo \false;
+      gl_fooo \false;
+      }
+*/
+/*@ gl_foo foo1_ok {
+      gl_foo foo2_ok {
+        gl_fooo \false;
+        }
+      }
+*/
 /*@
 gl_foo foo1_ok {
-         gl_fooo \false;
-         gl_foo foo2_ok {
-                  gl_fooo \false;
-                  gl_foo foo3_ok {
-                           gl_fooo \false;
-                           gl_fooo \false;
-                           }
-                    ;
-                  gl_fooo \false;
-                  }
-           ;
-         gl_fooo \false;
-         }
-  ;
+  gl_fooo \false;
+  gl_foo foo2_ok {
+    gl_fooo \false;
+    gl_foo foo3_ok {
+      gl_fooo \false;
+      gl_fooo \false;
+      }
+    gl_fooo \false;
+    }
+  gl_fooo \false;
+  }
 */