Merge pull request viperproject#824 from viperproject/meilers_test_822

Adding test for PR viperproject#822
viper-admin · Mar 25, 2024 · bda86d2 · bda86d2
2 parents 9e3d0f8 + 344ec32
commit bda86d2
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/src/test/resources/moreCompleteExhale/0822.vpr b/src/test/resources/moreCompleteExhale/0822.vpr
@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field val : Int
+
+method test(x: Ref, y: Ref) {
+    inhale acc(x.val) && acc(y.val, x != y ? write : none)
+    x.val := 4
+    y.val := 3
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert x.val == 4
+}