diff options
| author | Alasdair Armstrong | 2019-04-10 20:11:50 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-10 20:11:50 +0100 |
| commit | 96f679220ee241ac4083ad214fc400be72e0f463 (patch) | |
| tree | cadbc76e16551d4d429309522ee7332bb15767ef /test/smt/lteq_int_antisym.unsat.sail | |
| parent | 2aca5a074a6207997f8bf73e6a42a2c7387e0cc1 (diff) | |
SMT: More builtins and tests
Diffstat (limited to 'test/smt/lteq_int_antisym.unsat.sail')
| -rw-r--r-- | test/smt/lteq_int_antisym.unsat.sail | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/smt/lteq_int_antisym.unsat.sail b/test/smt/lteq_int_antisym.unsat.sail new file mode 100644 index 00000000..1730f417 --- /dev/null +++ b/test/smt/lteq_int_antisym.unsat.sail @@ -0,0 +1,7 @@ +default Order dec + +$include <prelude.sail> + +function check_sat(x: int, y: int) -> bool = { + if x <= y & y <= x then not_bool(x == y) else false +}
\ No newline at end of file |