From e5080e3f018fcd222906bf8129e53f32c138f8d8 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 23 Apr 2019 21:35:14 +0100
Subject: 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.
---
 test/smt/tl_let_shadow.sat.sail | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test/smt/tl_let_shadow.sat.sail

(limited to 'test')

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
-- 
cgit v1.2.3