SMT: Add parser for generated models

Simple parser-combinator style parser for generated models. It's
actually quite tricky to reconstruct the models because we can have:

let x = something

$counterexample
function prop(x: bits(32)) -> bool = ...

where the function argument becomes zx/1 rather than zx/0, which is what
we'd expect for the argument of a property. Might need to do something
smarter with encoding locations into smt names to figure out what SMT
variables correspond to which souce variables exactly. The above
also previously generated incorrect SMT, which has now been fixed.

1 files changed, 10 insertions, 0 deletions

diff --git a/test/smt/tl_let_shadow.sat.sail b/test/smt/tl_let_shadow.sat.sail
new file mode 100644
index 00000000..b8830a09
--- /dev/null
+++ b/test/smt/tl_let_shadow.sat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+let xs = 0xFFFF_FFFF
+
+$counterexample
+function prop(xs: bits(32)) -> bool = {
+  xs == 0xFFFF_FFFF
+}
\ No newline at end of file