diff --git a/src/test/resources/all/issues/silicon/0796.vpr b/src/test/resources/all/issues/silicon/0796.vpr
new file mode 100644
index 000000000..6f6cc1e4f
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0796.vpr
@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+//:: IgnoreFile(/carbon/issue/428/)
+
+field f: Int
+
+method m(xs: Set[Ref], ys: Set[Ref])
+{
+  inhale forall r: Ref :: r in xs ==> acc(r.f, r in ys ? 1/2 : none)
+
+  package true --* true {
+    assert forall r: Ref :: r in xs ==> acc(r.f, r in ys ? 1/2 : none)
+  }
+}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silicon/0816.vpr b/src/test/resources/all/issues/silicon/0816.vpr
new file mode 100644
index 000000000..cdc0bf590
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0816.vpr
@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method keydict___init__() returns (self: Ref)
+    ensures forall key: Ref :: {keydict___item__(self, key)} acc(keydict___item__(self, key).keydict_val) && !keydict___contains__(self, key)
+
+function keydict___item__(self: Ref, key: Ref): Ref
+    ensures keydict___item__inv(self, result) == key
+
+function keydict___item__inv(self: Ref, val_ref: Ref): Ref
+
+field keydict_val: Option[Ref]
+
+
+function keydict___contains__(self: Ref, key: Ref) : Bool
+    requires acc(keydict___item__(self, key).keydict_val, wildcard)
+    ensures result == keydict___item__(self, key).keydict_val.isSome
+
+
+
+adt Option[T] {
+    Some(value:T)
+    None()
+}
\ No newline at end of file
diff --git a/src/test/resources/all/sequences/sequence_incompletenesses.vpr b/src/test/resources/all/sequences/sequence_incompletenesses.vpr
index 9e891b90d..2a47535ce 100644
--- a/src/test/resources/all/sequences/sequence_incompletenesses.vpr
+++ b/src/test/resources/all/sequences/sequence_incompletenesses.vpr
@@ -94,8 +94,8 @@ method colourings1(a: Array)
       invariant 0 <= i && i <= |slot(a,n-1).val|
       invariant acc(slot(a,n).val)
       invariant |slot(a,n).val| == i
-      invariant forall j:Int :: 0 <= j && j < |slot(a,n-1).val| ==>
-        valid(slot(a,n-1).val[j],n-1,true)
+      invariant forall j:Int, n1: Int :: { slot(a,n1).val[j] } n1 == n - 1 && 0 <= j && j < |slot(a,n-1).val| ==>
+        valid(slot(a,n1).val[j],n - 1,true)
       invariant forall j : Int :: {slot(a,n).val[j]} 0 <= j && j < i ==> valid(slot(a,n).val[j],n,true)
     {
       var oldSoln : Seq[Int] := slot(a,n-1).val[i]
@@ -165,8 +165,8 @@ method colourings2(a: Array)
       invariant 0 <= i && i <= |slot(a,n-1).val|
       invariant acc(slot(a,n).val)
       invariant |slot(a,n).val| == i
-      invariant forall j:Int :: 0 <= j && j < |slot(a,n-1).val| ==>
-        valid(slot(a,n-1).val[j],n-1,true)
+      invariant forall j:Int, n1: Int :: { slot(a,n1).val[j] } n1 == n - 1 && 0 <= j && j < |slot(a,n-1).val| ==>
+        valid(slot(a,n1).val[j],n-1,true)
       invariant forall j : Int :: {slot(a,n).val[j]} 0 <= j && j < i ==> valid(slot(a,n).val[j],n,true)
     {
       var oldSoln : Seq[Int] := slot(a,n-1).val[i]
@@ -234,8 +234,8 @@ method colourings(a: Array)
       invariant 0 <= i && i <= |slot(a,n-1).val|
       invariant acc(slot(a,n).val)
       invariant |slot(a,n).val| == i
-      invariant forall j:Int :: 0 <= j && j < |slot(a,n-1).val| ==>
-        valid(slot(a,n-1).val[j],n-1,true)
+      invariant forall j:Int, n1: Int :: { slot(a,n1).val[j] } n1 == n - 1 && 0 <= j && j < |slot(a,n-1).val| ==>
+        valid(slot(a,n1).val[j],n-1,true)
       invariant forall j : Int :: {slot(a,n).val[j]} 0 <= j && j < i ==> valid(slot(a,n).val[j],n,true)
     {
       var oldSoln : Seq[Int] := slot(a,n-1).val[i]