3 files changed, 36 insertions, 0 deletions
diff --git a/test/smt/sail_mask_3.unsat.sail b/test/smt/sail_mask_3.unsat.sail
new file mode 100644
index 00000000..5f4b5fe4
--- /dev/null
+++ b/test/smt/sail_mask_3.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 32 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  assert(x == sail_zero_extend(0xdeadbeef, n));
+  true
+}
diff --git a/test/smt/sail_mask_4.unsat.sail b/test/smt/sail_mask_4.unsat.sail
new file mode 100644
index 00000000..368a3f2d
--- /dev/null
+++ b/test/smt/sail_mask_4.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 31 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  if n >= 32 then
+     assert(x == sail_zero_extend(0xdeadbeef, n))
+  else
+     assert(x == 0b1011110101011011011111011101111);
+  true
+}
diff --git a/test/smt/sail_mask_5.unsat.sail b/test/smt/sail_mask_5.unsat.sail
new file mode 100644
index 00000000..452c7f6c
--- /dev/null
+++ b/test/smt/sail_mask_5.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 31 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  if n >= 32 then
+     assert(x == sail_zero_extend(0xdeadbeef, n))
+  else
+     assert(0b1011110101011011011111011101111 == x);
+  true
+}