1 files changed, 18 insertions, 0 deletions
diff --git a/test/coq/pass/non_exh_exc.sail b/test/coq/pass/non_exh_exc.sail
new file mode 100644
index 00000000..8ce99163
--- /dev/null
+++ b/test/coq/pass/non_exh_exc.sail
@@ -0,0 +1,18 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+  Error_foo : unit,
+  Error_bar : int
+}
+
+val f : int -> int effect {escape}
+
+function f(n) = {
+  try {
+    let m : int = if n > 5 then n - 3 else throw(Error_bar(n)) in
+    m + 1
+  } catch {
+    Error_bar(n) => n
+  }
+}