SMT: Fix sail_truncate and sail_mask for unusual argument types

1 files changed, 10 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
+}