examples: fix the specs in the bounded_counter

nyu-acsys · Nov 10, 2024 · baeedf7 · baeedf7
1 parent c50e702
commit baeedf7
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/test/comparison/bounded_counter.rav b/test/comparison/bounded_counter.rav
@@ -7,7 +7,6 @@ inv counterInv(x: Ref, max: Int) {
 proc incr(x: Ref, max: Int)
     returns (res: Int)
     requires counterInv(x, max)
-    ensures counterInv(x, max)
     ensures 0 <= res <= max
 {
   var v: Int;
@@ -33,7 +32,6 @@ proc incr(x: Ref, max: Int)
 proc read(x: Ref, max: Int)
   returns (v: Int)
   requires counterInv(x, max)
-  ensures counterInv(x, max)
 {
   unfold counterInv(x, max);
   v := x.c;