1 files changed, 35 insertions, 1 deletions
diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail
index 0501cf1e..4540f1a5 100644
--- a/test/mono/itself_rewriting.sail
+++ b/test/mono/itself_rewriting.sail
@@ -1,5 +1,6 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
 default Order dec
 type bits ('n : Int) = bitvector('n, dec)
 val operator & = "and_bool" : (bool, bool) -> bool
@@ -67,10 +68,43 @@ function willsplit(x) = {
   shadowed(n);
 }
 
+val execute : forall 'datasize. int('datasize) -> unit
+
+function execute(datasize) = {
+  let x : bits('datasize) = replicate_bits(0b1, datasize);
+  ()
+}
+
+val test_execute : unit -> unit
+
+function test_execute() = {
+  let exp = 4;
+  let 'datasize = shl_int(1, exp);
+  execute(datasize)
+}
+
+val transitive_itself : forall 'n. int('n) -> unit
+
+function transitive_itself(n) = {
+  needs_size_in_guard(n);
+  ()
+}
+
+val transitive_split : bool -> unit
+
+function transitive_split(x) = {
+  let n = if x then 8 else 16;
+  transitive_itself(n);
+}
+
 val run : unit -> unit effect {escape}
 
 function run () = {
   assert(true); /* To force us into the monad */
+  test_execute();
   willsplit(true);
   willsplit(false);
-}
-\ No newline at end of file
+  transitive_itself(16);
+  transitive_split(true);
+  transitive_split(false);
+}