Add test for vector register constraints

rems-project · Jul 22, 2024 · fd29104 · fd29104
1 parent 17b0db5
commit fd29104
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/test/property/vector_register_reset.unsat.opts b/test/property/vector_register_reset.unsat.opts
@@ -0,0 +1 @@
+--reset-constraint '(= R[3] true)'
diff --git a/test/property/vector_register_reset.unsat.sail b/test/property/vector_register_reset.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+$include <prelude.sail>
+$include <isla.sail>
+
+register R: vector(16, bool)
+
+function prop() -> bool = {
+  isla_reset_registers();
+  R[3]
+}