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.

1 files changed, 11 insertions, 0 deletions

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