From 5f24a3c6f5cbca46e54a4cdc48bb4ecb27840d7b Mon Sep 17 00:00:00 2001
From: Golovin Pavel <gopavel0@gmail.com>
Date: Tue, 18 Jun 2024 00:14:46 +0200
Subject: [PATCH] [motoko-san] optimization: add trigger for `array_init`

Problem: in `todo_tuple.mo` it is necessary to finish proofs
---
 src/viper/prelude.ml                      | 2 +-
 test/repl/ok/viper.stdout.ok              | 2 +-
 test/viper/ok/array-of-tuples.vpr.ok      | 2 +-
 test/viper/ok/array.vpr.ok                | 2 +-
 test/viper/ok/assertions.vpr.ok           | 2 +-
 test/viper/ok/async.vpr.ok                | 2 +-
 test/viper/ok/claim-broken.vpr.ok         | 2 +-
 test/viper/ok/claim-reward-naive.vpr.ok   | 2 +-
 test/viper/ok/claim-simple.vpr.ok         | 2 +-
 test/viper/ok/claim.vpr.ok                | 2 +-
 test/viper/ok/counter.vpr.ok              | 2 +-
 test/viper/ok/invariant.vpr.ok            | 2 +-
 test/viper/ok/label-break-continue.vpr.ok | 2 +-
 test/viper/ok/lits.vpr.ok                 | 2 +-
 test/viper/ok/loop-invariant.vpr.ok       | 2 +-
 test/viper/ok/method-call.vpr.ok          | 2 +-
 test/viper/ok/nats.vpr.ok                 | 2 +-
 test/viper/ok/odd-even.vpr.ok             | 2 +-
 test/viper/ok/option.vpr.ok               | 2 +-
 test/viper/ok/polymono.vpr.ok             | 2 +-
 test/viper/ok/private.vpr.ok              | 2 +-
 test/viper/ok/reverse.vpr.ok              | 2 +-
 test/viper/ok/simple-funs.vpr.ok          | 2 +-
 test/viper/ok/text.vpr.ok                 | 2 +-
 test/viper/ok/tuple.vpr.ok                | 2 +-
 test/viper/ok/variants.vpr.ok             | 2 +-
 26 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml
index eb0c119ca70..a09ca05db59 100644
--- a/src/viper/prelude.ml
+++ b/src/viper/prelude.ml
@@ -11,7 +11,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x|prelude}
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x|prelude}
 
 let pp_tup_decl_param  ppf i = Format.fprintf ppf "T%d" i
 let pp_tup_decl_params ppf = function
diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok
index f162e54e90f..774b65d5b94 100644
--- a/test/repl/ok/viper.stdout.ok
+++ b/test/repl/ok/viper.stdout.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/array-of-tuples.vpr.ok b/test/viper/ok/array-of-tuples.vpr.ok
index fbe02e0b835..40fca261497 100644
--- a/test/viper/ok/array-of-tuples.vpr.ok
+++ b/test/viper/ok/array-of-tuples.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
 /* Option encoding */
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
index 4a0dc6590da..7c02134fdf6 100644
--- a/test/viper/ok/array.vpr.ok
+++ b/test/viper/ok/array.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
index e6477bfa8e5..08d1e3ad946 100644
--- a/test/viper/ok/assertions.vpr.ok
+++ b/test/viper/ok/assertions.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
index 95fbb7fff8d..8bbebe05986 100644
--- a/test/viper/ok/async.vpr.ok
+++ b/test/viper/ok/async.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
index ddf3cfb8539..8444dd7c601 100644
--- a/test/viper/ok/claim-broken.vpr.ok
+++ b/test/viper/ok/claim-broken.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
index af15146bb49..9dcad61daa5 100644
--- a/test/viper/ok/claim-reward-naive.vpr.ok
+++ b/test/viper/ok/claim-reward-naive.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
index 9bb67fb702e..e8d419ab59c 100644
--- a/test/viper/ok/claim-simple.vpr.ok
+++ b/test/viper/ok/claim-simple.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
index 64336db61cd..e3129c40dbd 100644
--- a/test/viper/ok/claim.vpr.ok
+++ b/test/viper/ok/claim.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
index af536420704..1bec5cab6b8 100644
--- a/test/viper/ok/counter.vpr.ok
+++ b/test/viper/ok/counter.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
index 96837535704..216165bc6dc 100644
--- a/test/viper/ok/invariant.vpr.ok
+++ b/test/viper/ok/invariant.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/label-break-continue.vpr.ok b/test/viper/ok/label-break-continue.vpr.ok
index 3dcdd47b864..793f877d612 100644
--- a/test/viper/ok/label-break-continue.vpr.ok
+++ b/test/viper/ok/label-break-continue.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 adt Tuple$0  { Tup$0() }
 adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
diff --git a/test/viper/ok/lits.vpr.ok b/test/viper/ok/lits.vpr.ok
index 74a85bd7e90..a9ef9a87e4a 100644
--- a/test/viper/ok/lits.vpr.ok
+++ b/test/viper/ok/lits.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
index 1c2e299a76e..e211e277f21 100644
--- a/test/viper/ok/loop-invariant.vpr.ok
+++ b/test/viper/ok/loop-invariant.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
index 04a82c80f2f..185f01e830c 100644
--- a/test/viper/ok/method-call.vpr.ok
+++ b/test/viper/ok/method-call.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
index 19039b4b400..61348e7d000 100644
--- a/test/viper/ok/nats.vpr.ok
+++ b/test/viper/ok/nats.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/odd-even.vpr.ok b/test/viper/ok/odd-even.vpr.ok
index 9c2f401dec4..8ad16c4d127 100644
--- a/test/viper/ok/odd-even.vpr.ok
+++ b/test/viper/ok/odd-even.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/option.vpr.ok b/test/viper/ok/option.vpr.ok
index c91a72d9209..721f609da73 100644
--- a/test/viper/ok/option.vpr.ok
+++ b/test/viper/ok/option.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok
index 49f4d496952..94fde8378a0 100644
--- a/test/viper/ok/polymono.vpr.ok
+++ b/test/viper/ok/polymono.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
index 0dfe28e119c..b4458df7454 100644
--- a/test/viper/ok/private.vpr.ok
+++ b/test/viper/ok/private.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
index defa0b0d779..55f4e1f5a26 100644
--- a/test/viper/ok/reverse.vpr.ok
+++ b/test/viper/ok/reverse.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
index 975342a500a..9ef78b947bd 100644
--- a/test/viper/ok/simple-funs.vpr.ok
+++ b/test/viper/ok/simple-funs.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {
diff --git a/test/viper/ok/text.vpr.ok b/test/viper/ok/text.vpr.ok
index a8642086106..a062ea196b8 100644
--- a/test/viper/ok/text.vpr.ok
+++ b/test/viper/ok/text.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
 /* Option encoding */
diff --git a/test/viper/ok/tuple.vpr.ok b/test/viper/ok/tuple.vpr.ok
index 4f0152fc9a5..887c418d844 100644
--- a/test/viper/ok/tuple.vpr.ok
+++ b/test/viper/ok/tuple.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
 adt Tuple$10 [T0, T1, T2, T3, T4, T5, T6, T7, T8, T9]
diff --git a/test/viper/ok/variants.vpr.ok b/test/viper/ok/variants.vpr.ok
index e1510ef6fd8..06e3a4bb381 100644
--- a/test/viper/ok/variants.vpr.ok
+++ b/test/viper/ok/variants.vpr.ok
@@ -10,7 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
-define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 /* Option encoding */
 adt Option[T] {