diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index 7b004bdb1c4bdd7cfd53c29df6933595ed89201e..eb7b4e0b8fb456a73b66648f3d8fbd1b4cb9fd81 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -9,6 +9,7 @@ assert behavior = 0;
     ensures behavior >= 0;
 */
 int main () {
+  //@ slevel 4;
   behavior++;
   return 0;
 }
@@ -31,6 +32,10 @@ model{L}(l1,ll1) ==> model(Cons(0,l1),Cons(0,ll1));
 volatile int assigns;
 
 int ensures(volatile int* a) { return *a; }
-void requires(volatile int*a, int v) { *a = v; }
+int requires(volatile int*a, int v) { *a = v; return v; }
 
 /*@ volatile assigns reads ensures writes requires; */
+
+int slevel = 1000000;
+
+//@ lemma bar: slevel >= 0;
diff --git a/tests/spec/oracle/behavior_names.res.oracle b/tests/spec/oracle/behavior_names.res.oracle
index 2bb78b303affead82ba4b673af4472e0bab8d6e0..f24db2ef02802cafbde4da8907ddda15be054a5c 100644
--- a/tests/spec/oracle/behavior_names.res.oracle
+++ b/tests/spec/oracle/behavior_names.res.oracle
@@ -78,7 +78,7 @@ void j(void)
     behavior while:
       ensures while: \true;
     
-    behavior normal:
+    behavior ensures:
       ensures ensures: \true;
     
     behavior logic:
diff --git a/tests/spec/oracle/kw.res.oracle b/tests/spec/oracle/kw.res.oracle
index 916e6673c1c89285920152a2cb1ee4c22b6e12f1..b9d920cb849457f0161ca7ed3551f23b325e6cd8 100644
--- a/tests/spec/oracle/kw.res.oracle
+++ b/tests/spec/oracle/kw.res.oracle
@@ -12,6 +12,7 @@ assert behavior = 0;
 int main(void)
 {
   int __retres;
+  /*@ slevel 4; */
   behavior ++;
   __retres = 0;
   return __retres;
@@ -25,6 +26,32 @@ inductive model{L}(List<ℤ>  root, List<ℤ>  logic_list) {
   case cons{L}: ∀ List<ℤ>  l1, List<ℤ>  ll1;
                   model(l1, ll1) ⇒ model(Cons(0, l1), Cons(0, ll1));
   }
+ */
+/*@ axiomatic foo {
+      logic ℤ func{L}(ℤ i) 
+        reads behavior;
+      
+      }
+
+*/
+int volatile assigns;
+int ensures(int volatile *a)
+{
+  int __retres;
+  __retres = *a;
+  return __retres;
+}
+
+int requires(int volatile *a, int v)
+{
+  *a = v;
+  return v;
+}
+
+/*@ volatile assigns reads ensures writes requires;
+*/
+int slevel = 1000000;
+/*@ lemma bar{L}: slevel ≥ 0;
 
 */