diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i
index f69d26eaa2c682768fac5d5e49134f1eeee1c044..dd42b2180708242016365f0c6c3518062ca0b972 100644
--- a/tests/spec/Extend.i
+++ b/tests/spec/Extend.i
@@ -43,9 +43,9 @@ int k(int z) {
 /*@ global_foo \forall integer x; x < x + 1
 ; */
 
-
+//@ behavior ca_foo: ensures ca_foo: \true;
 void loop (void) {
-  //@ ca_foo \true;
+  //@ for ca_foo: ca_foo \true;
   //@ ns_foo \true;
   //@ baz \true;
   /*@ loop invariant \true; */
diff --git a/tests/spec/oracle/Extend.res.oracle b/tests/spec/oracle/Extend.res.oracle
index da72437c2ec75953a1a792fe19cde406a578e188..6fb85da86bac26486fff0df9fa0c8dfba1551d99 100644
--- a/tests/spec/oracle/Extend.res.oracle
+++ b/tests/spec/oracle/Extend.res.oracle
@@ -48,9 +48,11 @@ int k(int z)
 
 /*@ global_foo ∀ ℤ x; x < x + 1;
 */
+/*@ behavior ca_foo:
+      ensures ca_foo: \true; */
 void loop(void)
 {
-  /*@ ca_foo \true; */ ;
+  /*@ for ca_foo: ca_foo \true; */ ;
   /*@ ns_foo \true; */
   /*@ baz \true; */
   /*@ loop invariant \true; */