diff --git a/tests/spec/oracle/array_typedef.res.oracle b/tests/spec/oracle/array_typedef.res.oracle
index f70e7649412bf74a7c3ba31a62b99f88f3cf497d..51da3e81b847059d1e847ddc3d83ac4ff39b6b75 100644
--- a/tests/spec/oracle/array_typedef.res.oracle
+++ b/tests/spec/oracle/array_typedef.res.oracle
@@ -73,9 +73,9 @@ typedef struct __anonstruct_msg_1 msg;
 /*@ assigns \empty; */
 void send_addr(int const * /*[4]*/ addr);
 
-void send_msg(msg const *msg_0)
+void send_msg(msg const *msg)
 {
-  send_addr(msg_0->src);
+  send_addr(msg->src);
   return;
 }
 
@@ -89,13 +89,13 @@ void host_address(int * /*[4]*/ ip)
   return;
 }
 
-void create_msg(msg *msg_0)
+void create_msg(msg *msg)
 {
-  host_address(msg_0->src);
-  host_address(msg_0->dst);
-  /*@ assert msg_0->dst[0] ≡ 192; */ ;
-  /*@ assert msg_0->src[0] ≡ 192; */ ;
-  /*@ assert msg_0->dst[sizeof(ip_address) / sizeof(int) - 1] ≡ 101; */ ;
+  host_address(msg->src);
+  host_address(msg->dst);
+  /*@ assert msg->dst[0] ≡ 192; */ ;
+  /*@ assert msg->src[0] ≡ 192; */ ;
+  /*@ assert msg->dst[sizeof(ip_address) / sizeof(int) - 1] ≡ 101; */ ;
   return;
 }
 
diff --git a/tests/spec/oracle/sizeof_logic.res.oracle b/tests/spec/oracle/sizeof_logic.res.oracle
index 0bc5ea119a70b054dcd245edb0d966a3d446217d..a5f76a76a31a84dd0b3e5437945eb724c26c616a 100644
--- a/tests/spec/oracle/sizeof_logic.res.oracle
+++ b/tests/spec/oracle/sizeof_logic.res.oracle
@@ -10,7 +10,7 @@ struct S {
 /*@ lemma good: ∀ short x; sizeof(x) ≤ sizeof(int);
  */
 /*@ ensures \result ≡ sizeof(struct S volatile); */
-int f(int a_0)
+int f(int a)
 {
   int __retres;
   __retres = (int)sizeof(struct S volatile);
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
index 57fdf7c199509f4598052b6bda6914f92e5934f4..40ab5bd3e4c647a6c27382809667e8c55a56a5e6 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -7,20 +7,20 @@
 typedef int __attribute__((__a1__)) aint;
 typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
 int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4) __attribute__((__f5__, __f4__,
+int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
                                                        __f2__, __f1__));
 
-/*@ requires p4 ≥ 3;
-    requires p4 ≥ 1;
-    requires p4 ≥ 4; */
+/*@ requires p3 ≥ 3;
+    requires p3 ≥ 1;
+    requires p3 ≥ 4; */
 int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4) __attribute__((__f5__, __f4__,
+int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
                                                        __f2__, __f1__));
 int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4)
+int const __attribute__((__arg3__)) p3)
 {
   int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
-  __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p4;
+  __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
   return __retres;
 }
 
@@ -33,9 +33,9 @@ aint g(int __attribute__((__a2__)) i3)
   return __retres;
 }
 
-iptr h(iptr volatile ip3);
+iptr h(iptr volatile ip2);
 
-iptr h(iptr volatile ip3)
+iptr h(iptr volatile ip2)
 {
   iptr __retres;
   __retres = (int __attribute__((__p1__)) *)0;
diff --git a/tests/syntax/oracle/bts0588.res.oracle b/tests/syntax/oracle/bts0588.res.oracle
index 974690514254374dffaeac43e79345266621c961..1bb974c5380efd6ae747bdeb7d28fbda1385ff21 100644
--- a/tests/syntax/oracle/bts0588.res.oracle
+++ b/tests/syntax/oracle/bts0588.res.oracle
@@ -8,10 +8,10 @@ void g(int a)
   return;
 }
 
-/*@ ensures \old(x) > 0; */
-void f(int x)
+/*@ ensures \old(a) > 0; */
+void f(int a)
 {
-  x = 1;
+  a = 1;
   return;
 }
 
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
index dac79fa8c28ed0d122f90ee83dc0ac7e7dd0a8f9..d1362720e3451b7c18a430bd0a496fe5447c5ae8 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
@@ -9,8 +9,8 @@ int main(void)
 {
   int __retres;
   digit x = 4;
-  int digit_0 = 3;
-  __retres = (x + digit_0) + A;
+  int digit = 3;
+  __retres = (x + digit) + A;
   return __retres;
 }