3 files changed, 39 insertions, 1 deletions
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index bb1bc952..e8fbabb0 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -33,6 +33,14 @@ function foo(n, x) =
     64 => let z = y@y@y@y in let dfsf = 4 in z
   }
 
+val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
+
+function foo_if(n, x) =
+  let y : bits(16) = extzv(x) in
+  if n == 32
+  then y@y
+  else /* 64 */ let z = y@y@y@y in let dfsf = 4 in z
+
 val use : bits(16) -> unit effect pure
 
 function use(x) = ()
@@ -45,6 +53,13 @@ function bar(x) =
    16 => use(x)
   }
 
+val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure
+
+function bar_if(x) =
+  if 'n == 8
+  then use(x@x)
+  else /* 16 */ use(x)
+
 val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef}
 
 function ret(n, x) =
@@ -116,4 +131,4 @@ function run () = {
     assert(foo2(64,0x12) == 0x0012001200120012);
     assert(foo3(4,0x12) == 0x00120012);
     assert(foo3(8,0x12) == 0x0012001200120012);
-}
-\ No newline at end of file
+}
diff --git a/test/mono/pass/repeatedint b/test/mono/pass/repeatedint
new file mode 100644
index 00000000..ff26c84d
--- /dev/null
+++ b/test/mono/pass/repeatedint
@@ -0,0 +1 @@
+repeatedint.sail -auto_mono
diff --git a/test/mono/repeatedint.sail b/test/mono/repeatedint.sail
new file mode 100644
index 00000000..2d01e814
--- /dev/null
+++ b/test/mono/repeatedint.sail
@@ -0,0 +1,22 @@
+/* Silly, but it did appear in a model, and we didn't handle it... */
+
+default Order dec
+$include <prelude.sail>
+
+union ast = {
+  SomeInstr : {'size, 'size in {8,16}. (int('size), int('size))}
+}
+
+val test : ast -> bits(32)
+
+function test(SomeInstr(s as int('size),r)) = {
+  x : bits('size) = sail_zero_extend(0x80, s);
+  sail_sign_extend(x,32)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test(SomeInstr(8,8)) == 0xffffff80);
+  assert(test(SomeInstr(16,16)) == 0x00000080);
+}