Add comment to explain test

viperproject · Jun 17, 2024 · 1e73802 · 1e73802
1 parent f849533
commit 1e73802
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/test/resources/conditionalizePermissions/let.vpr b/src/test/resources/conditionalizePermissions/let.vpr
@@ -11,5 +11,8 @@ function val(): Ref
 
 method test()
 {
+    // Test that the condition is not pushed inside the let expression to get e.g.
+    // inhale let x == (val()) in acc(x.f, ok() ? write : none)
+    // which would not be well-defined.
     inhale ok() ==> let x == (val()) in acc(x.f)
 }