8 files changed, 86 insertions, 0 deletions
diff --git a/test/smt/lt_int_irrefl.unsat.sail b/test/smt/lt_int_irrefl.unsat.sail
new file mode 100644
index 00000000..984793be
--- /dev/null
+++ b/test/smt/lt_int_irrefl.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(x: int) -> bool = {
+  x < x
+}
+\ No newline at end of file
diff --git a/test/smt/lt_int_trans.unsat.sail b/test/smt/lt_int_trans.unsat.sail
new file mode 100644
index 00000000..efd930b3
--- /dev/null
+++ b/test/smt/lt_int_trans.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(x: int, y: int, z: int) -> bool = {
+  if (x < y & y < z) then not_bool(x < z) else false
+}
+\ No newline at end of file
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
diff --git a/test/smt/lteq_int_def.unsat.sail b/test/smt/lteq_int_def.unsat.sail
new file mode 100644
index 00000000..db3bf1f0
--- /dev/null
+++ b/test/smt/lteq_int_def.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(x: int, y: int) -> bool = {
+  if x <= y then not_bool(x < y | x == y) else not_bool(y < x)
+}
+\ No newline at end of file
diff --git a/test/smt/lteq_int_refl.unsat.sail b/test/smt/lteq_int_refl.unsat.sail
new file mode 100644
index 00000000..eeb7e0d9
--- /dev/null
+++ b/test/smt/lteq_int_refl.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(x: int) -> bool = {
+  not_bool(x <= x)
+}
+\ No newline at end of file
diff --git a/test/smt/lteq_int_trans.unsat.sail b/test/smt/lteq_int_trans.unsat.sail
new file mode 100644
index 00000000..e7a8a3d7
--- /dev/null
+++ b/test/smt/lteq_int_trans.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(x: int, y: int, z: int) -> bool = {
+  if (x <= y & y <= z) then not_bool(x <= z) else false
+}
+\ No newline at end of file
diff --git a/test/smt/order.unsat.sail b/test/smt/order.unsat.sail
new file mode 100644
index 00000000..c25762c9
--- /dev/null
+++ b/test/smt/order.unsat.sail
@@ -0,0 +1,32 @@
+default Order dec
+
+$include <prelude.sail>
+
+overload ~ = {not_bool}
+
+function check_sat(x: int, y: int, z: int) -> bool = {
+  let lteq_refl    = x <= x;
+  let lteq_trans   = (if x <= y & y <= z then x <= z else true);
+  let lteq_antisym = (if x <= y & y <= x then x == y else true);
+
+  let lt_irrefl = ~(x < x);
+  let lt_trans  = (if x < y & y < z then x < z else true);
+
+  let lt_implies_lteq = (if x < y then x <= y else true);
+
+  let gteq_refl    = x >= x;
+  let gteq_trans   = (if x >= y & y >= z then x >= z else true);
+  let gteq_antisym = (if x >= y & y >= x then x == y else true);
+
+  let gt_irrefl = ~(x > x);
+  let gt_trans  = (if x > y & y > z then x > z else true);
+
+  let gt_implies_gteq = (if x > y then x >= y else true);
+
+  let lt_negate = (if x > 0 then negate(x) < x else true);
+  let gt_negate = (if x < 0 then negate(x) > x else true);
+
+  ~(lteq_refl & lteq_trans & lteq_antisym & lt_irrefl & lt_trans & lt_implies_lteq
+  & gteq_refl & gteq_trans & gteq_antisym & gt_irrefl & gt_trans & gt_implies_gteq
+  & lt_negate & gt_negate)
+}
diff --git a/test/smt/update_access.unsat.sail b/test/smt/update_access.unsat.sail
new file mode 100644
index 00000000..26411ff0
--- /dev/null
+++ b/test/smt/update_access.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat(xs: bits(65), x: bit) -> bool = {
+  ys = xs;
+  ys[63] = x;
+  ys[64] = x;
+  ys[42] = x;
+  ys[0] = x;
+  not_bool(ys[64] == x & ys[63] == x & ys[42] == x & ys[0] == x)
+}
+\ No newline at end of file