1 files changed, 17 insertions, 0 deletions
diff --git a/test/typecheck/pass/floor_pow2.sail b/test/typecheck/pass/floor_pow2.sail
new file mode 100644
index 00000000..fa8680cf
--- /dev/null
+++ b/test/typecheck/pass/floor_pow2.sail
@@ -0,0 +1,17 @@
+$include <arith.sail>
+
+val "pow2" : forall 'n, 'n >= 0. int('n) -> int(2 ^ 'n)
+
+val floor_pow2 : forall ('x : Int), 'x >= 0. int('x) -> int
+
+function floor_pow2 x = {
+    if x == 0 then {
+        return(0);
+    } else {
+        n : {'n, 'n >= 1. int('n)} = 1;
+        while x >= pow2(n) do {
+            n = n + 1
+        };
+        return(pow2(n - 1))
+    }
+}