SMT: Make bitvector equality work between vectors of different lengths

1 files changed, 13 insertions, 0 deletions

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
+}