From b2a10c92eb45a02cce5e7cb5e0947b331369d54d Mon Sep 17 00:00:00 2001
From: Christopher Pulte <cp526@cam.ac.uk>
Date: Tue, 12 Sep 2023 12:12:08 +0100
Subject: [PATCH] +1 test

---
 tests/cn/incomplete_match.error.c | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/cn/incomplete_match.error.c

diff --git a/tests/cn/incomplete_match.error.c b/tests/cn/incomplete_match.error.c
new file mode 100644
index 000000000..734d6951f
--- /dev/null
+++ b/tests/cn/incomplete_match.error.c
@@ -0,0 +1,22 @@
+
+/*@
+datatype mylist {
+  Nil {},
+  Cons {integer hd, datatype mylist tl}
+}
+
+function (integer) snd (datatype mylist t) {
+  match t {
+    Cons {hd: _, tl: Cons {hd: v, tl: _}} => { v }
+    Nil {} => { 0 }
+  }
+}
+@*/
+
+void
+check_foo (int x)
+/*@ ensures snd(Cons {hd: 10, tl: Cons {hd: 20, tl: Nil {}}}) == 20 @*/
+{
+}
+
+