2 files changed, 20 insertions, 0 deletions
diff --git a/test/smt/sail_mask.unsat.sail b/test/smt/sail_mask.unsat.sail
new file mode 100644
index 00000000..4afbab90
--- /dev/null
+++ b/test/smt/sail_mask.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 0 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0b0);
+  assert(x == sail_zeros(n));
+  true
+}
diff --git a/test/smt/sail_mask_2.unsat.sail b/test/smt/sail_mask_2.unsat.sail
new file mode 100644
index 00000000..8904bbe9
--- /dev/null
+++ b/test/smt/sail_mask_2.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 1 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0b1);
+  assert(x == sail_zero_extend(0b1, n));
+  true
+}