summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/mono/itself_rewriting.sail8
1 files changed, 8 insertions, 0 deletions
diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail
index 912cb99d..4d67ee1a 100644
--- a/test/mono/itself_rewriting.sail
+++ b/test/mono/itself_rewriting.sail
@@ -83,6 +83,13 @@ function test_execute() = {
execute(datasize)
}
+val transitive_itself : forall 'n. int('n) -> unit
+
+function transitive_itself(n) = {
+ needs_size_in_guard(n);
+ ()
+}
+
val run : unit -> unit effect {escape}
function run () = {
@@ -90,4 +97,5 @@ function run () = {
test_execute();
willsplit(true);
willsplit(false);
+ transitive_itself(16);
}