1 files changed, 13 insertions, 0 deletions
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)
+}