diff options
Diffstat (limited to 'test/smt/inline_regression.unsat.sail')
| -rw-r--r-- | test/smt/inline_regression.unsat.sail | 20 |
1 files changed, 20 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 |
