additional nested datatype test

verus-lang · Oct 31, 2024 · 8324ea5 · 8324ea5
1 parent da2e55a
commit 8324ea5
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs
@@ -2190,6 +2190,21 @@ fn nested_datatype_field_update_pass() {
     )
 }
 
+#[test]
+fn nested_datatype_field_update_pass2() {
+    yes!(
+        (declare-datatypes ((A 0)) (((A_A (A_A_u Int) (A_A_v Int)))))
+        (declare-datatypes ((B 0)) (((B_B (B_B_a1 A) (B_B_a2 A)))))
+        (check-valid
+            (declare-var b B)
+            (block
+                (assign b ((_ update-field B_B_a1) b ((_ update-field A_A_u) (B_B_a1 b) 3)))
+                (assert (= (A_A_u (B_B_a1 b)) 3))
+            )
+        )
+    )
+}
+
 #[test]
 fn nested_datatype_field_update_fail() {
     no!(