From fd2910430078c35602cda65ed2c210703f893654 Mon Sep 17 00:00:00 2001
From: Brian Campbell <Brian.Campbell@ed.ac.uk>
Date: Mon, 22 Jul 2024 13:30:20 +0100
Subject: [PATCH] Add test for vector register constraints

---
 test/property/vector_register_reset.unsat.opts |  1 +
 test/property/vector_register_reset.unsat.sail | 10 ++++++++++
 2 files changed, 11 insertions(+)
 create mode 100644 test/property/vector_register_reset.unsat.opts
 create mode 100644 test/property/vector_register_reset.unsat.sail

diff --git a/test/property/vector_register_reset.unsat.opts b/test/property/vector_register_reset.unsat.opts
new file mode 100644
index 0000000..c0e8073
--- /dev/null
+++ 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
new file mode 100644
index 0000000..e3a57b9
--- /dev/null
+++ 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]
+}