SMT: Fix inlining issues

2 files changed, 42 insertions, 0 deletions

diff --git a/test/smt/inline_regression.unsat.sail b/test/smt/inline_regression.unsat.sail
new file mode 100644
index 00000000..245ad8b7
--- /dev/null
+++ b/test/smt/inline_regression.unsat.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <prelude.sail>
+
+function id(c: bits(64)) -> bits(64) = c
+
+function g(c__arg: bits(64), c': bits(64)) -> bool = {
+  c = c__arg;
+  c == c'
+}
+
+function f(c: bits(64), c': bits(64)) -> bool = {
+  let c = c;
+  g(c', c)
+}
+
+$property
+function prop(c: bits(64)) -> bool = {
+  f(c, c) & g(c, c)
+}
\ No newline at end of file
diff --git a/test/smt/inline_test_1.unsat.sail b/test/smt/inline_test_1.unsat.sail
new file mode 100644
index 00000000..990afd3e
--- /dev/null
+++ b/test/smt/inline_test_1.unsat.sail
@@ -0,0 +1,22 @@
+default Order dec
+
+$include <prelude.sail>
+
+function id(c: bits(64)) -> bits(64) = c
+
+function g(c: bits(64), c': bits(64)) -> bool = {
+  {
+    let c = c;
+    c == c'
+  }
+}
+
+function f(c: bits(64), c': bits(64)) -> bool = {
+  let c = c;
+  c == c' & ({ g(c, c') }) & g(c', c)
+}
+
+$property
+function prop(c: bits(64)) -> bool = {
+  f(c, c) & g(c, c)
+}
\ No newline at end of file