Added a test case for the already resolved issue 4.

viperproject · Nov 20, 2013 · 886e12f · 886e12f
1 parent deb5612
commit 886e12f
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/src/test/resources/all/issues/sil/0004.sil b/src/test/resources/all/issues/sil/0004.sil
@@ -0,0 +1,10 @@
+//:: IgnoreFile(/silicon/issue/31/)
+
+var f: Int
+
+method test(x: Ref)
+  requires acc(x.f)
+{
+  exhale acc(x.f, 3 * write)
+  exhale acc(x.f, 3 * epsilon)
+}