diff options
| author | Alasdair Armstrong | 2019-04-05 14:45:21 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-09 16:16:32 +0100 |
| commit | 97cc026337ea5cfc33586b6725c312c1a507f922 (patch) | |
| tree | 93d9682e005855b58e8eec6cf6e649d22df1f5c3 /test/smt/zeros_3.sat.sail | |
| parent | 76bf4a3853e547ae2e0327b20e4f4b89d16820b7 (diff) | |
SMT: Experimental Jib->SMT translation
Currently only works with CVC4, test cases are in test/smt. Can prove
that RISC-V add instruction actually adds values in registers and
that's about it for now.
Diffstat (limited to 'test/smt/zeros_3.sat.sail')
| -rw-r--r-- | test/smt/zeros_3.sat.sail | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/smt/zeros_3.sat.sail b/test/smt/zeros_3.sat.sail new file mode 100644 index 00000000..3da36e1f --- /dev/null +++ b/test/smt/zeros_3.sat.sail @@ -0,0 +1,7 @@ +default Order dec + +$include <vector_dec.sail> + +function check_sat((): unit) -> bool = { + 0x0000_0000_0000_0000_0 == sail_zeros(68) +}
\ No newline at end of file |