Fixing test annotation

viperproject · May 4, 2024 · e15d356 · e15d356
1 parent 068f121
commit e15d356
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/test/resources/wands/new_syntax/QPWands.vpr b/src/test/resources/wands/new_syntax/QPWands.vpr
@@ -41,8 +41,6 @@ requires acc(y.f) {
 
 method test1(x: Ref)
 requires forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) {
-    // ME: Can we actually expect this to go through? How Would it trigger the QP we have?
-    //:: UnexpectedOutput(exhale.failed:wand.not.found, /silicon/issue/000/)
     exhale forall i: Int :: true ==> acc(x.f) && x.f == i-1 --* acc(x.f)
 
     //:: ExpectedOutput(assert.failed:wand.not.found)