From 80450ecef9e97d39f36573d5e85f4c1e3df277bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Sat, 28 Oct 2023 22:34:31 +0200
Subject: [PATCH] tests from Dionisios

---
 .../features/maps/maps-nested.gobra           | 11 +++++++++++
 .../options/options-nested-maps.gobra         | 19 +++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 src/test/resources/regressions/features/maps/maps-nested.gobra
 create mode 100644 src/test/resources/regressions/features/options/options-nested-maps.gobra

diff --git a/src/test/resources/regressions/features/maps/maps-nested.gobra b/src/test/resources/regressions/features/maps/maps-nested.gobra
new file mode 100644
index 000000000..9d0072258
--- /dev/null
+++ b/src/test/resources/regressions/features/maps/maps-nested.gobra
@@ -0,0 +1,11 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+ghost
+func foo(){
+    mm := dict[int](dict[int]int){1 : {2:3}}
+    assert mm[1][2] == 3
+    assert 2 in domain(mm[1])
+}
diff --git a/src/test/resources/regressions/features/options/options-nested-maps.gobra b/src/test/resources/regressions/features/options/options-nested-maps.gobra
new file mode 100644
index 000000000..090ff5c17
--- /dev/null
+++ b/src/test/resources/regressions/features/options/options-nested-maps.gobra
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+ghost
+pure func bar(m dict[int]int, idx int) option[int] {
+    return idx in domain(m) ? some(m[idx]) : none[int]
+}
+
+ghost
+pure func baz(m dict[int]int, idx int) option[int] {
+    return match idx in domain(m){
+        case true:
+            some(m[idx])
+        case false:
+            none[int]
+    }
+}