From 360fa851090c9b9d085bb3814fdc351dd72721bf Mon Sep 17 00:00:00 2001
From: Mattias Ulbrich <ulbrich@kit.edu>
Date: Wed, 21 Oct 2020 14:39:15 +0200
Subject: [PATCH] adding a testcase for #194

---
 .../boogie/heap/field_array_select.boogie     | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 modules/dafny/test-res/edu/kit/iti/algover/boogie/heap/field_array_select.boogie

diff --git a/modules/dafny/test-res/edu/kit/iti/algover/boogie/heap/field_array_select.boogie b/modules/dafny/test-res/edu/kit/iti/algover/boogie/heap/field_array_select.boogie
new file mode 100644
index 000000000..1f43f2ff7
--- /dev/null
+++ b/modules/dafny/test-res/edu/kit/iti/algover/boogie/heap/field_array_select.boogie
@@ -0,0 +1,34 @@
+### project:
+class C { var f : int; }
+
+### decls:
+o : C
+a : array<int>
+
+### sequent:
+|- o.f == o.f@$heap[a[0] := 0]
+
+### result:
+prove
+
+### translation:
+const _$heap : Heap;
+const _a : ref;
+const _o : ref;
+const unique TClass_C : Ty;
+const unique _C$$f : Field (int);
+
+axiom (forall x:ref :: $Is(x, TClass_C) <==> dtype(x) == TClass_C || x == null);
+axiom $Is(_$heap, THeap);
+axiom $Is(_o, TClass_C);
+axiom $Is(_C$$f, TField(TInt));
+axiom $Is(_a, TArray(TInt));
+
+procedure Sequent()
+  ensures false;
+{
+  assume !((read(_$heap, _o, _C$$f) == read(update(_$heap, _a, IndexField(0) : Field int, 0), _o, _C$$f)));
+}
+
+### comments:
+was a bug : IndexField(0) could alias with _C$$f