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.

1 files changed, 10 insertions, 0 deletions

diff --git a/test/smt/shiftr_zero_1.sat.sail b/test/smt/shiftr_zero_1.sat.sail
new file mode 100644
index 00000000..9eb75c69
--- /dev/null
+++ b/test/smt/shiftr_zero_1.sat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bits(64)
+
+function check_sat((): unit) -> bool = {
+  let x = sail_shiftright(R, 63);
+  not_bool(x == 0x0000_0000_0000_0000)
+}
\ No newline at end of file