Tests for fixed Silicon issue #856 (#880)

Author: marcoeilers

src/test/resources/all/issues/silicon/0327.vpr

@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field val: Int
+
+function foo(refs: Set[Ref]): Bool
+  requires forall x: Ref :: x in refs ==> acc(x.val)
+
+method test(refs: Set[Ref]) {
+  inhale forall x: Ref :: x in refs ==> acc(x.val)
+  inhale forall subs: Set[Ref] :: subs subset refs ==> foo(subs)
+}

src/test/resources/all/issues/silicon/0856.vpr

@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Bool
+
+function hfun(rs: Set[Ref]): Bool
+  requires (forall r: Ref :: { (r in rs) } (r in rs) ==> acc(r.f))
+
+
+method test1(rs: Set[Ref])
+  requires (forall r: Ref :: { (r in rs) } (r in rs) ==> acc(r.f))
+{
+  assume (forall rs2: Set[Ref] :: { (rs2 subset rs) }
+      (rs2 subset rs) ==> hfun(rs2))
+
+  assert (forall rs3: Set[Ref] :: { (rs3 subset rs) }
+      (rs3 subset rs) ==> hfun(rs3))
+}