SMT: Support generic vectors and handle lets between specs and functions

If we have e.g.

$property
val prop : ...

let X = 0

function prop(...) = X == ...

then we need to ensure that let X is included when we generate the
property.

4 files changed, 59 insertions, 0 deletions

diff --git a/test/smt/foreach_simple_2.unsat.sail b/test/smt/foreach_simple_2.unsat.sail
new file mode 100644
index 00000000..ce466044
--- /dev/null
+++ b/test/smt/foreach_simple_2.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+let C = 0
+
+$property
+function prop() -> bool = {
+  let n = 3;
+  bv = 0x0;
+  foreach (i from C to n) {
+    bv[i] = bitone
+  };
+  bv == 0xF
+}
diff --git a/test/smt/gvector.unsat.sail b/test/smt/gvector.unsat.sail
new file mode 100644
index 00000000..23054765
--- /dev/null
+++ b/test/smt/gvector.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : vector(32, dec, vector(32, dec, bit))
+
+type is_reg('n: Int) -> Bool = 0 <= 'n <= 31
+
+$property
+function prop forall 'n, is_reg('n). (n: int('n)) -> bool = {
+  foreach (i from 0 to 31) {
+    R[i] = 0xDEAD_BEEF;
+  };
+  R[n] == 0xDEAD_BEEF
+}
\ No newline at end of file
diff --git a/test/smt/gvector_trivial.unsat.sail b/test/smt/gvector_trivial.unsat.sail
new file mode 100644
index 00000000..37a4fbed
--- /dev/null
+++ b/test/smt/gvector_trivial.unsat.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : vector(32, dec, vector(32, dec, bit))
+
+$property
+function prop() -> bool = {
+  R[0] = 0xDEAD_BEEF;
+  R[0] == 0xDEAD_BEEF
+}
\ No newline at end of file
diff --git a/test/smt/let_intervene.unsat.sail b/test/smt/let_intervene.unsat.sail
new file mode 100644
index 00000000..5494848b
--- /dev/null
+++ b/test/smt/let_intervene.unsat.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+val prop : unit -> bool
+
+let C = 0
+let x = bitone
+
+function prop() = {
+  let n = 3;
+  bv = 0x0;
+  foreach (i from C to n) {
+    bv[i] = x
+  };
+  bv == 0xF
+}