3 files changed, 56 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
+  }
+}
diff --git a/test/coq/pass/throw_fact.sail b/test/coq/pass/throw_fact.sail
new file mode 100644
index 00000000..e40267b1
--- /dev/null
+++ b/test/coq/pass/throw_fact.sail
@@ -0,0 +1,25 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+  BadInput : int
+}
+
+val test1 : int -> nat effect {escape}
+
+function test1(n) = {
+  if (n < 0) then {
+    throw (BadInput(n))
+  };
+  n
+}
+
+val test2 : int -> nat effect {escape}
+
+function test2(n) = {
+  m : nat = 0;
+  if (n < 0) then {
+    throw (BadInput(n))
+  } else { m = 1 };
+  n+m
+}
diff --git a/test/coq/pass/var_type_autocast.sail b/test/coq/pass/var_type_autocast.sail
new file mode 100644
index 00000000..6c65b978
--- /dev/null
+++ b/test/coq/pass/var_type_autocast.sail
@@ -0,0 +1,13 @@
+default Order dec
+$include <prelude.sail>
+$include <smt.sail>
+
+val load_bytes : forall 'n, 'n >= 0. int('n) -> bits(8 * 'n)
+
+val foo : forall 'n, 'n in {8,16}. (int('n),bool) -> bits('n)
+
+function foo(n,b) = {
+  let 'bytes = ediv_int(n,8);
+  let data = load_bytes(bytes);
+  if b then data else sail_zeros(n)
+}