5 files changed, 62 insertions, 4 deletions
diff --git a/test/smt/assembly_mapping.sat.sail b/test/smt/assembly_mapping.sat.sail
index a7b0bec5..4aff3605 100644
--- a/test/smt/assembly_mapping.sat.sail
+++ b/test/smt/assembly_mapping.sat.sail
@@ -49,10 +49,10 @@ mapping utype_mnemonic : uop <-> string = {
   RISCV_AUIPC <-> "auipc"
 }
 
-val assembly : ast <-> string
-
 scattered union ast
 
+val assembly : ast <-> string
+
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
 mapping clause assembly = UTYPE(imm, rd, op)
diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail
index d34f3629..0777c904 100644
--- a/test/smt/encdec.sat.sail
+++ b/test/smt/encdec.sat.sail
@@ -49,10 +49,10 @@ mapping utype_mnemonic : uop <-> string = {
   RISCV_AUIPC <-> "auipc"
 }
 
-val assembly : ast <-> string
-
 scattered union ast
 
+val assembly : ast <-> string
+
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
 mapping clause assembly = UTYPE(imm, rd, op)
diff --git a/test/smt/revrev_endianness.sail b/test/smt/revrev_endianness.sail
new file mode 100644
index 00000000..f792871f
--- /dev/null
+++ b/test/smt/revrev_endianness.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <reverse_endianness.sail>
+
+$property
+function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = {
+  if length(xs) == 8 then {
+    let ys: bits(8) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 16 then {
+    let ys: bits(16) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 32 then {
+    let ys: bits(32) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 64 then {
+    let ys: bits(64) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 128 then {
+    let ys: bits(128) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else {
+    true
+  }
+}
diff --git a/test/smt/revrev_endianness2.sail b/test/smt/revrev_endianness2.sail
new file mode 100644
index 00000000..33ba93a2
--- /dev/null
+++ b/test/smt/revrev_endianness2.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <reverse_endianness.sail>
+
+$property
+function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = {
+  if length(xs) == 8 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 16 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 32 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 64 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 128 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else {
+    true
+  }
+}
diff --git a/test/smt/zeros_ones.unsat.sail b/test/smt/zeros_ones.unsat.sail
new file mode 100644
index 00000000..0ebfba42
--- /dev/null
+++ b/test/smt/zeros_ones.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: range(0, 64)) -> bool = {
+  let bv: bits(64) = sail_zeros(64 - x) @ sail_ones(x);
+  if x == 32 then {
+    bv == 0x0000_0000_FFFF_FFFF
+  } else {
+    true
+  }
+}