summaryrefslogtreecommitdiff
path: root/test/smt/update_subrange.unsat.sail
diff options
context:
space:
mode:
Diffstat (limited to 'test/smt/update_subrange.unsat.sail')
-rw-r--r--test/smt/update_subrange.unsat.sail12
1 files changed, 12 insertions, 0 deletions
diff --git a/test/smt/update_subrange.unsat.sail b/test/smt/update_subrange.unsat.sail
new file mode 100644
index 00000000..5a6b2094
--- /dev/null
+++ b/test/smt/update_subrange.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+$property
+function prop(xs: bits(65), ys: bits(5)) -> bool = {
+ xs' = xs;
+ xs'[63..59] = ys;
+ xs'[46..42] = ys;
+ xs'[4..0] = ys;
+ xs'[63..59] == ys & xs'[46..42] == ys & xs'[4..0] == ys
+}