diff --git a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
index 2e24eb7f8a7502ffb36cad5f670b90fc673a2b01..b850086cbe94dbafa142e58f40a017022d73a22c 100644
--- a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
@@ -581,24 +581,26 @@ int g(int y)
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧
         aorai_CurStates ≡ aorai_reject ⇒
-        aorai_x_0 ≡ \at(1,Pre) + 0 ∨ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0;
+        aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0 ∨
+        aorai_x_0 ≡ \at((int)1,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧
         aorai_CurStates ≡ aorai_reject ⇒
-        aorai_y ≡ \at(2,Pre) + 0 ∨ aorai_y ≡ \at(aorai_y,Pre) + 0;
+        aorai_y ≡ \at(aorai_y,Pre) + 0 ∨ aorai_y ≡ \at((int)2,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧
         aorai_CurStates ≡ aorai_reject ⇒
-        aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(aorai_x,Pre) + 0;
+        aorai_x ≡ \at(aorai_x,Pre) + 0 ∨ aorai_x ≡ \at((int)1,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
-        aorai_x_0 ≡ \at(1,Pre) + 0 ∨ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0;
+        aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0 ∨
+        aorai_x_0 ≡ \at((int)1,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
-        aorai_y ≡ \at(2,Pre) + 0 ∨ aorai_y ≡ \at(aorai_y,Pre) + 0;
+        aorai_y ≡ \at(aorai_y,Pre) + 0 ∨ aorai_y ≡ \at((int)2,Pre) + 0;
       ensures
         \at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
-        aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(aorai_x,Pre) + 0;
+        aorai_x ≡ \at(aorai_x,Pre) + 0 ∨ aorai_x ≡ \at((int)1,Pre) + 0;
  */
 int main(void)
 {
diff --git a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle b/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
index 91b4e2cc2ad540571330772e709520258a653f9b..480cdbac3e337e91a9a7e27ca0dee315fdfe892b 100644
--- a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
@@ -525,7 +525,12 @@ void g(void)
      behavior buch_state_last_out:
        ensures 0 ≡ last;
      
+     behavior buch_state_step1_in:
+       assumes 1 ≡ init ∧ x ≡ 3;
+       ensures 1 ≡ step1;
+     
      behavior buch_state_step1_out:
+       assumes 0 ≡ init ∨ ¬(x ≡ 3);
        ensures 0 ≡ step1;
    @/
   void main_pre_func(void)
@@ -538,7 +543,9 @@ void g(void)
     init_tmp = init;
     last_tmp = last;
     step1_tmp = step1;
-    step1_tmp = 0;
+    if (init == 1) 
+      if (x == 3) step1_tmp = 1; else step1_tmp = 0;
+    else step1_tmp = 0;
     last_tmp = 0;
     if (init == 1) 
       if (x != 3) init_tmp = 1; else init_tmp = 0;
@@ -644,7 +651,6 @@ void g(void)
 */
 
 /*@ requires 1 ≡ init ∧ 0 ≡ last ∧ 0 ≡ step1;
-    requires 1 ≡ init ⇒ x ≢ 3;
     
     behavior aorai_acceptance:
       ensures 1 ≡ last;