summaryrefslogtreecommitdiff
path: root/test/smt/sail_mask.unsat.sail
diff options
context:
space:
mode:
Diffstat (limited to 'test/smt/sail_mask.unsat.sail')
-rw-r--r--test/smt/sail_mask.unsat.sail10
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
+}