diff --git a/tests/spec/assigns_array.c b/tests/spec/assigns_array.c
index ae1e717e53bed3b7d2436d784cf0f4187a56a93d..c044389fd8aa335d00ecff39d25c189c94955b29 100644
--- a/tests/spec/assigns_array.c
+++ b/tests/spec/assigns_array.c
@@ -9,7 +9,7 @@
   assigns ghost_loctable;
 
  */
-void acquire_lock(int m) { ghost_loctable[m]++; }
+void acquire_lock(int m) { /*@ ghost ghost_loctable[m]++; */ }
 
 // The specification above should be accepted
 /*@
@@ -18,7 +18,7 @@ void acquire_lock(int m) { ghost_loctable[m]++; }
   ensures !ghost_loctable[m];
   assigns ghost_loctable[..];
  */
-void release_lock(int m) { ghost_loctable[m]--; }
+void release_lock(int m) { /*@ ghost ghost_loctable[m]--; */ }
 
 
 
diff --git a/tests/spec/oracle/assigns_array.res.oracle b/tests/spec/oracle/assigns_array.res.oracle
index 4a571e41bf10b05c1f1fcdd69cf45181decc140a..6e4846e218d9c35e30edec7a74b34aa5e7f1492c 100644
--- a/tests/spec/oracle/assigns_array.res.oracle
+++ b/tests/spec/oracle/assigns_array.res.oracle
@@ -5,7 +5,7 @@
 /*@ ghost int ghost_loctable[100]; */
 void acquire_lock(int m)
 {
-  (ghost_loctable[m]) ++;
+  /*@ ghost (ghost_loctable[m]) ++; */
   return;
 }
 
@@ -16,7 +16,7 @@ void acquire_lock(int m)
  */
 void release_lock(int m)
 {
-  (ghost_loctable[m]) --;
+  /*@ ghost (ghost_loctable[m]) --; */
   return;
 }