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.

38 files changed, 1251 insertions, 0 deletions

diff --git a/test/smt/basic_1.sat.sail b/test/smt/basic_1.sat.sail
new file mode 100644
index 00000000..d40c5a59
--- /dev/null
+++ b/test/smt/basic_1.sat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+enum E = A | B | C
+
+struct S = {
+  field1 : bits(8),
+  field2 : bits(16),
+  field3 : E
+}
+
+register R1 : bits(16)
+register R2 : bits(8)
+
+function check_sat(x: bool) -> bool = {
+  if x then {
+    R1 = 0x007F
+  } else {
+    R1 = 0xFFFF
+  };
+  R1 == sail_zero_extend(R2, 16)
+}
diff --git a/test/smt/basic_1.unsat.sail b/test/smt/basic_1.unsat.sail
new file mode 100644
index 00000000..cf469d75
--- /dev/null
+++ b/test/smt/basic_1.unsat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+enum E = A | B | C
+
+struct S = {
+  field1 : bits(8),
+  field2 : bits(16),
+  field3 : E
+}
+
+register R1 : bits(16)
+register R2 : bits(8)
+
+function check_sat(x: bool) -> bool = {
+  if false then {
+    R1 = 0x007F
+  } else {
+    R1 = 0xFFFF
+  };
+  R1 == sail_zero_extend(R2, 16)
+}
diff --git a/test/smt/basic_2.sat.sail b/test/smt/basic_2.sat.sail
new file mode 100644
index 00000000..73b18446
--- /dev/null
+++ b/test/smt/basic_2.sat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+enum E = A | B | C
+
+struct S = {
+  field1 : bits(8),
+  field2 : bits(16),
+  field3 : E
+}
+
+register R1 : bits(16)
+register R2 : bits(8)
+
+function check_sat(x: bool) -> bool = {
+  if x then {
+    R1 = 0x00FF
+  } else {
+    R1 = 0xFFFF
+  };
+  R1 == sail_zero_extend(R2, 16)
+}
diff --git a/test/smt/basic_2.unsat.sail b/test/smt/basic_2.unsat.sail
new file mode 100644
index 00000000..1f3d8488
--- /dev/null
+++ b/test/smt/basic_2.unsat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+enum E = A | B | C
+
+struct S = {
+  field1 : bits(8),
+  field2 : bits(16),
+  field3 : E
+}
+
+register R1 : bits(16)
+register R2 : bits(8)
+
+function check_sat(x: bool) -> bool = {
+  if x then {
+    R1 = 0x01FF
+  } else {
+    R1 = 0xFFFF
+  };
+  R1 == sail_zero_extend(R2, 16)
+}
diff --git a/test/smt/concat_prop.unsat.sail b/test/smt/concat_prop.unsat.sail
new file mode 100644
index 00000000..417152d5
--- /dev/null
+++ b/test/smt/concat_prop.unsat.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(32)
+register R2 : bits(32)
+
+function check_sat('sz: range(0, 32)) -> bool = {
+  let z: bits('sz) = sail_zeros(sz);
+  let x: bits('sz + 32) = R1 @ z;
+  let y: bits(32 + 'sz) = R2 @ z;
+  let padding = sail_zeros(32) @ sail_zeros(sz);
+
+  // A and B must be equal
+  let A = x @ y;
+  let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y);
+  not_bool(A == B)
+}
diff --git a/test/smt/concat_prop128.unsat.sail b/test/smt/concat_prop128.unsat.sail
new file mode 100644
index 00000000..3d8ea45f
--- /dev/null
+++ b/test/smt/concat_prop128.unsat.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(64)
+register R2 : bits(64)
+
+function check_sat('sz: range(0, 64)) -> bool = {
+  let z: bits('sz) = sail_zeros(sz);
+  let x: bits('sz + 64) = R1 @ z;
+  let y: bits(64 + 'sz) = R2 @ z;
+  let padding = sail_zeros(64) @ sail_zeros(sz);
+
+  // A and B must be equal
+  let A = x @ y;
+  let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y);
+  not_bool(A == B)
+}
diff --git a/test/smt/exception.unsat.sail b/test/smt/exception.unsat.sail
new file mode 100644
index 00000000..e2455425
--- /dev/null
+++ b/test/smt/exception.unsat.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+union exception = {
+  E_bool : bool,
+  E_unit : unit
+}
+
+function check_sat((): unit) -> bool = {
+  try {
+    throw(E_bool(false))
+  } catch {
+    E_bool(b) => b,
+    E_unit() => true
+  }
+}
diff --git a/test/smt/exception_2.unsat.sail b/test/smt/exception_2.unsat.sail
new file mode 100644
index 00000000..0a540341
--- /dev/null
+++ b/test/smt/exception_2.unsat.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+union exception = {
+  E_bool : bool,
+  E_unit : unit
+}
+
+register R : bool
+
+function check_sat((): unit) -> bool = {
+  try {
+    if R then {
+       throw(E_bool(false))
+    } else {
+       false
+    }
+  } catch {
+    E_bool(b) => b,
+    E_unit() => true
+  }
+}
diff --git a/test/smt/exception_3.unsat.sail b/test/smt/exception_3.unsat.sail
new file mode 100644
index 00000000..f0f71945
--- /dev/null
+++ b/test/smt/exception_3.unsat.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+union exception = {
+  E_bool : bool,
+  E_unit : unit
+}
+
+register R : bool
+
+function check_sat((): unit) -> bool = {
+  try {
+    if R then {
+       throw(E_bool(false))
+    } else {
+       return(false);
+       true
+    }
+  } catch {
+    E_bool(b) => b,
+    E_unit() => true
+  }
+}
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
new file mode 100755
index 00000000..097c0672
--- /dev/null
+++ b/test/smt/run_tests.py
@@ -0,0 +1,53 @@
+#!/usr/bin/env python
+
+import os
+import re
+import sys
+import hashlib
+import distutils.spawn
+
+sail_dir = os.environ['SAIL_DIR']
+os.chdir(os.path.dirname(__file__))
+sys.path.insert(0, os.path.join(sail_dir, 'test'))
+
+from sailtest import *
+
+def test_smt(name, solver, sail_opts):
+    banner('Testing SMT: {}'.format(name))
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
+            basename = os.path.splitext(os.path.basename(filename))[0]
+            tests[filename] = os.fork()
+            if tests[filename] == 0:
+                step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
+                step('{} {}.smt2 1> {}.out'.format(solver, basename, basename))
+                if re.match('.+\.sat\.sail$', filename):
+                    step('grep -q ^sat$ {}.out'.format(basename))
+                else:
+                    step('grep -q ^unsat$ {}.out'.format(basename))
+                print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
+                sys.exit()
+        results.collect(tests)
+    return results.finish()
+    return collect_results(name, tests)
+
+xml = '<testsuites>\n'
+
+if distutils.spawn.find_executable('cvc4'):
+    xml += test_smt('cvc4', 'cvc4 --lang=smt2.6', '')
+else:
+    print '{}Cannot find SMT solver cvc4 skipping tests{}'.format(color.WARNING, color.END)
+
+#if distutils.spawn.find_executable('z3'):
+#    xml += test_smt('z3', 'z3', '')
+#else:
+#    print '{}Cannot find SMT solver cvc4 skipping tests{}'.format(color.WARNING, color.END)
+
+xml += '</testsuites>\n'
+
+output = open('tests.xml', 'w')
+output.write(xml)
+output.close()
+
diff --git a/test/smt/rv_add_0.sat.sail b/test/smt/rv_add_0.sat.sail
new file mode 100644
index 00000000..f1c86c4d
--- /dev/null
+++ b/test/smt/rv_add_0.sat.sail
@@ -0,0 +1,155 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen       : Int  = 32
+type xlen_bytes : Int  = 4
+type xlenbits   : Type = bits(xlen)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = unsigned(b)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+/* Architectural state */
+register R1 : xlenbits
+register R2 : xlenbits
+register R3 : xlenbits
+register R4 : xlenbits
+register R5 : xlenbits
+register R6 : xlenbits
+register R7 : xlenbits
+register R8 : xlenbits
+register R9 : xlenbits
+register R10 : xlenbits
+register R11 : xlenbits
+register R12 : xlenbits
+register R13 : xlenbits
+register R14 : xlenbits
+register R15 : xlenbits
+register R16 : xlenbits
+register R17 : xlenbits
+register R18 : xlenbits
+register R19 : xlenbits
+register R20 : xlenbits
+register R21 : xlenbits
+register R22 : xlenbits
+register R23 : xlenbits
+register R24 : xlenbits
+register R25 : xlenbits
+register R26 : xlenbits
+register R27 : xlenbits
+register R28 : xlenbits
+register R29 : xlenbits
+register R30 : xlenbits
+register R31 : xlenbits
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+
+function rX(r) = {
+  if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
+  else if r == 1 then R1
+  else if r == 2 then R2
+  else if r == 3 then R3
+  else if r == 4 then R4
+  else if r == 5 then R5
+  else if r == 6 then R6
+  else if r == 7 then R7
+  else if r == 8 then R8
+  else if r == 9 then R9
+  else if r == 10 then R10
+  else if r == 11 then R11
+  else if r == 12 then R12
+  else if r == 13 then R13
+  else if r == 14 then R14
+  else if r == 15 then R15
+  else if r == 16 then R16
+  else if r == 17 then R17
+  else if r == 18 then R18
+  else if r == 19 then R19
+  else if r == 20 then R20
+  else if r == 21 then R21
+  else if r == 22 then R22
+  else if r == 23 then R23
+  else if r == 24 then R24
+  else if r == 25 then R25
+  else if r == 26 then R26
+  else if r == 27 then R27
+  else if r == 28 then R28
+  else if r == 29 then R29
+  else if r == 30 then R30
+  else R31
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+
+function wX(r, v) = {
+  if r == 0 then ()
+  else if r == 1 then R1 = v
+  else if r == 2 then R2 = v
+  else if r == 3 then R3 = v
+  else if r == 4 then R4 = v
+  else if r == 5 then R5 = v
+  else if r == 6 then R6 = v
+  else if r == 7 then R7 = v
+  else if r == 8 then R8 = v
+  else if r == 9 then R9 = v
+  else if r == 10 then R10 = v
+  else if r == 11 then R11 = v
+  else if r == 12 then R12 = v
+  else if r == 13 then R13 = v
+  else if r == 14 then R14 = v
+  else if r == 15 then R15 = v
+  else if r == 16 then R16 = v
+  else if r == 17 then R17 = v
+  else if r == 18 then R18 = v
+  else if r == 19 then R19 = v
+  else if r == 20 then R20 = v
+  else if r == 21 then R21 = v
+  else if r == 22 then R22 = v
+  else if r == 23 then R23 = v
+  else if r == 24 then R24 = v
+  else if r == 25 then R25 = v
+  else if r == 26 then R26 = v
+  else if r == 27 then R27 = v
+  else if r == 28 then R28 = v
+  else if r == 29 then R29 = v
+  else if r == 30 then R30 = v
+  else R31 = v
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+val decode : bits(32) -> option(ast) effect pure
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
+  let rs1_val = X(rs1) in
+  let imm_ext : xlenbits = sail_sign_extend(imm, sizeof(xlen)) in
+  let result = rs1_val + imm_ext in
+  X(rd) = result
+
+function clause decode _ = None()
+
+function check_sat(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
+  X(rs1) = v;
+  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
+    Some(instr) => {
+      execute(instr);
+      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0)
+    },
+    _ => true
+  }
+}
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
new file mode 100644
index 00000000..daa2996d
--- /dev/null
+++ b/test/smt/rv_add_0.unsat.sail
@@ -0,0 +1,155 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen       : Int  = 32
+type xlen_bytes : Int  = 4
+type xlenbits   : Type = bits(xlen)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = unsigned(b)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+/* Architectural state */
+register R1 : xlenbits
+register R2 : xlenbits
+register R3 : xlenbits
+register R4 : xlenbits
+register R5 : xlenbits
+register R6 : xlenbits
+register R7 : xlenbits
+register R8 : xlenbits
+register R9 : xlenbits
+register R10 : xlenbits
+register R11 : xlenbits
+register R12 : xlenbits
+register R13 : xlenbits
+register R14 : xlenbits
+register R15 : xlenbits
+register R16 : xlenbits
+register R17 : xlenbits
+register R18 : xlenbits
+register R19 : xlenbits
+register R20 : xlenbits
+register R21 : xlenbits
+register R22 : xlenbits
+register R23 : xlenbits
+register R24 : xlenbits
+register R25 : xlenbits
+register R26 : xlenbits
+register R27 : xlenbits
+register R28 : xlenbits
+register R29 : xlenbits
+register R30 : xlenbits
+register R31 : xlenbits
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+
+function rX(r) = {
+  if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
+  else if r == 1 then R1
+  else if r == 2 then R2
+  else if r == 3 then R3
+  else if r == 4 then R4
+  else if r == 5 then R5
+  else if r == 6 then R6
+  else if r == 7 then R7
+  else if r == 8 then R8
+  else if r == 9 then R9
+  else if r == 10 then R10
+  else if r == 11 then R11
+  else if r == 12 then R12
+  else if r == 13 then R13
+  else if r == 14 then R14
+  else if r == 15 then R15
+  else if r == 16 then R16
+  else if r == 17 then R17
+  else if r == 18 then R18
+  else if r == 19 then R19
+  else if r == 20 then R20
+  else if r == 21 then R21
+  else if r == 22 then R22
+  else if r == 23 then R23
+  else if r == 24 then R24
+  else if r == 25 then R25
+  else if r == 26 then R26
+  else if r == 27 then R27
+  else if r == 28 then R28
+  else if r == 29 then R29
+  else if r == 30 then R30
+  else R31
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+
+function wX(r, v) = {
+  if r == 0 then ()
+  else if r == 1 then R1 = v
+  else if r == 2 then R2 = v
+  else if r == 3 then R3 = v
+  else if r == 4 then R4 = v
+  else if r == 5 then R5 = v
+  else if r == 6 then R6 = v
+  else if r == 7 then R7 = v
+  else if r == 8 then R8 = v
+  else if r == 9 then R9 = v
+  else if r == 10 then R10 = v
+  else if r == 11 then R11 = v
+  else if r == 12 then R12 = v
+  else if r == 13 then R13 = v
+  else if r == 14 then R14 = v
+  else if r == 15 then R15 = v
+  else if r == 16 then R16 = v
+  else if r == 17 then R17 = v
+  else if r == 18 then R18 = v
+  else if r == 19 then R19 = v
+  else if r == 20 then R20 = v
+  else if r == 21 then R21 = v
+  else if r == 22 then R22 = v
+  else if r == 23 then R23 = v
+  else if r == 24 then R24 = v
+  else if r == 25 then R25 = v
+  else if r == 26 then R26 = v
+  else if r == 27 then R27 = v
+  else if r == 28 then R28 = v
+  else if r == 29 then R29 = v
+  else if r == 30 then R30 = v
+  else R31 = v
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+val decode : bits(32) -> option(ast) effect pure
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
+  let rs1_val = X(rs1) in
+  let imm_ext : xlenbits = sail_sign_extend(imm, sizeof(xlen)) in
+  let result = rs1_val + imm_ext in
+  X(rd) = result
+
+function clause decode _ = None()
+
+function check_sat(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
+  X(rs1) = v;
+  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
+    Some(instr) => {
+      execute(instr);
+      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0 | rs1 == 0)
+    },
+    _ => true
+  }
+}
diff --git a/test/smt/rv_add_1.sat.sail b/test/smt/rv_add_1.sat.sail
new file mode 100644
index 00000000..b2a562c4
--- /dev/null
+++ b/test/smt/rv_add_1.sat.sail
@@ -0,0 +1,155 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen       : Int  = 32
+type xlen_bytes : Int  = 4
+type xlenbits   : Type = bits(xlen)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = unsigned(b)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+/* Architectural state */
+register R1 : xlenbits
+register R2 : xlenbits
+register R3 : xlenbits
+register R4 : xlenbits
+register R5 : xlenbits
+register R6 : xlenbits
+register R7 : xlenbits
+register R8 : xlenbits
+register R9 : xlenbits
+register R10 : xlenbits
+register R11 : xlenbits
+register R12 : xlenbits
+register R13 : xlenbits
+register R14 : xlenbits
+register R15 : xlenbits
+register R16 : xlenbits
+register R17 : xlenbits
+register R18 : xlenbits
+register R19 : xlenbits
+register R20 : xlenbits
+register R21 : xlenbits
+register R22 : xlenbits
+register R23 : xlenbits
+register R24 : xlenbits
+register R25 : xlenbits
+register R26 : xlenbits
+register R27 : xlenbits
+register R28 : xlenbits
+register R29 : xlenbits
+register R30 : xlenbits
+register R31 : xlenbits
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+
+function rX(r) = {
+  if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
+  else if r == 1 then R1
+  else if r == 2 then R2
+  else if r == 3 then R3
+  else if r == 4 then R4
+  else if r == 5 then R5
+  else if r == 6 then R6
+  else if r == 7 then R7
+  else if r == 8 then R8
+  else if r == 9 then R9
+  else if r == 10 then R10
+  else if r == 11 then R11
+  else if r == 12 then R12
+  else if r == 13 then R13
+  else if r == 14 then R14
+  else if r == 15 then R15
+  else if r == 16 then R16
+  else if r == 17 then R17
+  else if r == 18 then R18
+  else if r == 19 then R19
+  else if r == 20 then R20
+  else if r == 21 then R21
+  else if r == 22 then R22
+  else if r == 23 then R23
+  else if r == 24 then R24
+  else if r == 25 then R25
+  else if r == 26 then R26
+  else if r == 27 then R27
+  else if r == 28 then R28
+  else if r == 29 then R29
+  else if r == 30 then R30
+  else R31
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+
+function wX(r, v) = {
+  if r == 0 then ()
+  else if r == 1 then R1 = v
+  else if r == 2 then R2 = v
+  else if r == 3 then R3 = v
+  else if r == 4 then R4 = v
+  else if r == 5 then R5 = v
+  else if r == 6 then R6 = v
+  else if r == 7 then R7 = v
+  else if r == 8 then R8 = v
+  else if r == 9 then R9 = v
+  else if r == 10 then R10 = v
+  else if r == 11 then R11 = v
+  else if r == 12 then R12 = v
+  else if r == 13 then R13 = v
+  else if r == 14 then R14 = v
+  else if r == 15 then R15 = v
+  else if r == 16 then R16 = v
+  else if r == 17 then R17 = v
+  else if r == 18 then R18 = v
+  else if r == 19 then R19 = v
+  else if r == 20 then R20 = v
+  else if r == 21 then R21 = v
+  else if r == 22 then R22 = v
+  else if r == 23 then R23 = v
+  else if r == 24 then R24 = v
+  else if r == 25 then R25 = v
+  else if r == 26 then R26 = v
+  else if r == 27 then R27 = v
+  else if r == 28 then R28 = v
+  else if r == 29 then R29 = v
+  else if r == 30 then R30 = v
+  else R31 = v
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+val decode : bits(32) -> option(ast) effect pure
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
+  let rs1_val = X(rs1) in
+  let imm_ext : xlenbits = sail_sign_extend(imm, sizeof(xlen)) in
+  let result = rs1_val + imm_ext in
+  X(rd) = result
+
+function clause decode _ = None()
+
+function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+  let v = X(rs1);
+  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
+    Some(instr) => {
+      execute(instr);
+      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)))
+    },
+    _ => true
+  }
+}
diff --git a/test/smt/rv_add_1.unsat.sail b/test/smt/rv_add_1.unsat.sail
new file mode 100644
index 00000000..d3b784e8
--- /dev/null
+++ b/test/smt/rv_add_1.unsat.sail
@@ -0,0 +1,155 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen       : Int  = 32
+type xlen_bytes : Int  = 4
+type xlenbits   : Type = bits(xlen)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = unsigned(b)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+/* Architectural state */
+register R1 : xlenbits
+register R2 : xlenbits
+register R3 : xlenbits
+register R4 : xlenbits
+register R5 : xlenbits
+register R6 : xlenbits
+register R7 : xlenbits
+register R8 : xlenbits
+register R9 : xlenbits
+register R10 : xlenbits
+register R11 : xlenbits
+register R12 : xlenbits
+register R13 : xlenbits
+register R14 : xlenbits
+register R15 : xlenbits
+register R16 : xlenbits
+register R17 : xlenbits
+register R18 : xlenbits
+register R19 : xlenbits
+register R20 : xlenbits
+register R21 : xlenbits
+register R22 : xlenbits
+register R23 : xlenbits
+register R24 : xlenbits
+register R25 : xlenbits
+register R26 : xlenbits
+register R27 : xlenbits
+register R28 : xlenbits
+register R29 : xlenbits
+register R30 : xlenbits
+register R31 : xlenbits
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+
+function rX(r) = {
+  if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
+  else if r == 1 then R1
+  else if r == 2 then R2
+  else if r == 3 then R3
+  else if r == 4 then R4
+  else if r == 5 then R5
+  else if r == 6 then R6
+  else if r == 7 then R7
+  else if r == 8 then R8
+  else if r == 9 then R9
+  else if r == 10 then R10
+  else if r == 11 then R11
+  else if r == 12 then R12
+  else if r == 13 then R13
+  else if r == 14 then R14
+  else if r == 15 then R15
+  else if r == 16 then R16
+  else if r == 17 then R17
+  else if r == 18 then R18
+  else if r == 19 then R19
+  else if r == 20 then R20
+  else if r == 21 then R21
+  else if r == 22 then R22
+  else if r == 23 then R23
+  else if r == 24 then R24
+  else if r == 25 then R25
+  else if r == 26 then R26
+  else if r == 27 then R27
+  else if r == 28 then R28
+  else if r == 29 then R29
+  else if r == 30 then R30
+  else R31
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+
+function wX(r, v) = {
+  if r == 0 then ()
+  else if r == 1 then R1 = v
+  else if r == 2 then R2 = v
+  else if r == 3 then R3 = v
+  else if r == 4 then R4 = v
+  else if r == 5 then R5 = v
+  else if r == 6 then R6 = v
+  else if r == 7 then R7 = v
+  else if r == 8 then R8 = v
+  else if r == 9 then R9 = v
+  else if r == 10 then R10 = v
+  else if r == 11 then R11 = v
+  else if r == 12 then R12 = v
+  else if r == 13 then R13 = v
+  else if r == 14 then R14 = v
+  else if r == 15 then R15 = v
+  else if r == 16 then R16 = v
+  else if r == 17 then R17 = v
+  else if r == 18 then R18 = v
+  else if r == 19 then R19 = v
+  else if r == 20 then R20 = v
+  else if r == 21 then R21 = v
+  else if r == 22 then R22 = v
+  else if r == 23 then R23 = v
+  else if r == 24 then R24 = v
+  else if r == 25 then R25 = v
+  else if r == 26 then R26 = v
+  else if r == 27 then R27 = v
+  else if r == 28 then R28 = v
+  else if r == 29 then R29 = v
+  else if r == 30 then R30 = v
+  else R31 = v
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+val decode : bits(32) -> option(ast) effect pure
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
+  let rs1_val = X(rs1) in
+  let imm_ext : xlenbits = sail_sign_extend(imm, sizeof(xlen)) in
+  let result = rs1_val + imm_ext in
+  X(rd) = result
+
+function clause decode _ = None()
+
+function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+  let v = X(rs1);
+  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
+    Some(instr) => {
+      execute(instr);
+      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0)
+    },
+    _ => true
+  }
+}
diff --git a/test/smt/rv_add_decode.unsat.sail b/test/smt/rv_add_decode.unsat.sail
new file mode 100644
index 00000000..d5952e09
--- /dev/null
+++ b/test/smt/rv_add_decode.unsat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <prelude.sail>
+
+type regbits = bits(5)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+val decode : bits(32) -> option(ast) effect pure
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause decode _ = None()
+
+function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
+    Some(ITYPE(_)) => false,
+    _ => true
+  }
+}
\ No newline at end of file
diff --git a/test/smt/rv_reg_rw.unsat.sail b/test/smt/rv_reg_rw.unsat.sail
new file mode 100644
index 00000000..5bf419a9
--- /dev/null
+++ b/test/smt/rv_reg_rw.unsat.sail
@@ -0,0 +1,134 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen       : Int  = 32
+type xlen_bytes : Int  = 4
+type xlenbits   : Type = bits(xlen)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = unsigned(b)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+/* Architectural state */
+register R1 : xlenbits
+register R2 : xlenbits
+register R3 : xlenbits
+register R4 : xlenbits
+register R5 : xlenbits
+register R6 : xlenbits
+register R7 : xlenbits
+register R8 : xlenbits
+register R9 : xlenbits
+register R10 : xlenbits
+register R11 : xlenbits
+register R12 : xlenbits
+register R13 : xlenbits
+register R14 : xlenbits
+register R15 : xlenbits
+register R16 : xlenbits
+register R17 : xlenbits
+register R18 : xlenbits
+register R19 : xlenbits
+register R20 : xlenbits
+register R21 : xlenbits
+register R22 : xlenbits
+register R23 : xlenbits
+register R24 : xlenbits
+register R25 : xlenbits
+register R26 : xlenbits
+register R27 : xlenbits
+register R28 : xlenbits
+register R29 : xlenbits
+register R30 : xlenbits
+register R31 : xlenbits
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+
+function rX(r) = {
+  if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
+  else if r == 1 then R1
+  else if r == 2 then R2
+  else if r == 3 then R3
+  else if r == 4 then R4
+  else if r == 5 then R5
+  else if r == 6 then R6
+  else if r == 7 then R7
+  else if r == 8 then R8
+  else if r == 9 then R9
+  else if r == 10 then R10
+  else if r == 11 then R11
+  else if r == 12 then R12
+  else if r == 13 then R13
+  else if r == 14 then R14
+  else if r == 15 then R15
+  else if r == 16 then R16
+  else if r == 17 then R17
+  else if r == 18 then R18
+  else if r == 19 then R19
+  else if r == 20 then R20
+  else if r == 21 then R21
+  else if r == 22 then R22
+  else if r == 23 then R23
+  else if r == 24 then R24
+  else if r == 25 then R25
+  else if r == 26 then R26
+  else if r == 27 then R27
+  else if r == 28 then R28
+  else if r == 29 then R29
+  else if r == 30 then R30
+  else R31
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+
+function wX(r, v) = {
+  if r == 0 then ()
+  else if r == 1 then R1 = v
+  else if r == 2 then R2 = v
+  else if r == 3 then R3 = v
+  else if r == 4 then R4 = v
+  else if r == 5 then R5 = v
+  else if r == 6 then R6 = v
+  else if r == 7 then R7 = v
+  else if r == 8 then R8 = v
+  else if r == 9 then R9 = v
+  else if r == 10 then R10 = v
+  else if r == 11 then R11 = v
+  else if r == 12 then R12 = v
+  else if r == 13 then R13 = v
+  else if r == 14 then R14 = v
+  else if r == 15 then R15 = v
+  else if r == 16 then R16 = v
+  else if r == 17 then R17 = v
+  else if r == 18 then R18 = v
+  else if r == 19 then R19 = v
+  else if r == 20 then R20 = v
+  else if r == 21 then R21 = v
+  else if r == 22 then R22 = v
+  else if r == 23 then R23 = v
+  else if r == 24 then R24 = v
+  else if r == 25 then R25 = v
+  else if r == 26 then R26 = v
+  else if r == 27 then R27 = v
+  else if r == 28 then R28 = v
+  else if r == 29 then R29 = v
+  else if r == 30 then R30 = v
+  else R31 = v
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+function check_sat(r: regbits, v: xlenbits) -> bool = {
+  X(r) = v;
+  not_bool(X(r) == v | r == 0)
+}
diff --git a/test/smt/shift_or_concat.unsat.sail b/test/smt/shift_or_concat.unsat.sail
new file mode 100644
index 00000000..4e562889
--- /dev/null
+++ b/test/smt/shift_or_concat.unsat.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(32)
+register R2 : bits(32)
+
+function check_sat((): unit) -> bool = {
+  let x = sail_zero_extend(R1, 64);
+  let x = sail_shiftleft(x, 32);
+  let y = or_vec(x, sail_zero_extend(R2, 64));
+  let z = R1 @ R2;
+  not_bool(y == z)
+}
\ No newline at end of file
diff --git a/test/smt/shift_or_concat128.unsat.sail b/test/smt/shift_or_concat128.unsat.sail
new file mode 100644
index 00000000..9cb0a0b8
--- /dev/null
+++ b/test/smt/shift_or_concat128.unsat.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(128)
+register R2 : bits(128)
+
+function check_sat((): unit) -> bool = {
+  let x = sail_zero_extend(R1, 256);
+  let x = sail_shiftleft(x, 128);
+  let y = or_vec(x, sail_zero_extend(R2, 256));
+  let z = R1 @ R2;
+  not_bool(y == z)
+}
\ No newline at end of file
diff --git a/test/smt/shift_or_concat4.unsat.sail b/test/smt/shift_or_concat4.unsat.sail
new file mode 100644
index 00000000..b8510151
--- /dev/null
+++ b/test/smt/shift_or_concat4.unsat.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(4)
+register R2 : bits(4)
+
+function check_sat((): unit) -> bool = {
+  let x = sail_zero_extend(R1, 8);
+  let x = sail_shiftleft(x, 4);
+  let y = or_vec(x, sail_zero_extend(R2, 8));
+  let z = R1 @ R2;
+  not_bool(y == z)
+}
\ No newline at end of file
diff --git a/test/smt/shift_or_concat4_2.unsat.sail b/test/smt/shift_or_concat4_2.unsat.sail
new file mode 100644
index 00000000..2c730cbd
--- /dev/null
+++ b/test/smt/shift_or_concat4_2.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(4)
+register R2 : bits(4)
+
+function check_sat((): unit) -> bool = {
+  let w = 4;
+  let x = sail_zero_extend(R1, 8);
+  let x = sail_shiftleft(x, w);
+  let y = or_vec(x, sail_zero_extend(R2, 8));
+  let z = R1 @ R2;
+  not_bool(y == z)
+}
\ No newline at end of file
diff --git a/test/smt/shift_or_concat_1.sat.sail b/test/smt/shift_or_concat_1.sat.sail
new file mode 100644
index 00000000..88107c50
--- /dev/null
+++ b/test/smt/shift_or_concat_1.sat.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(32)
+register R2 : bits(32)
+
+function check_sat((): unit) -> bool = {
+  let x = sail_zero_extend(R1, 64);
+  let x = sail_shiftleft(x, 31);
+  let y = or_vec(x, sail_zero_extend(R2, 64));
+  let z = R1 @ R2;
+  not_bool(y == z)
+}
\ No newline at end of file
diff --git a/test/smt/shift_or_concat_2.sat.sail b/test/smt/shift_or_concat_2.sat.sail
new file mode 100644
index 00000000..f7fd1f4c
--- /dev/null
+++ b/test/smt/shift_or_concat_2.sat.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R1 : bits(32)
+register R2 : bits(32)
+
+function check_sat((): unit) -> bool = {
+  let x = sail_zero_extend(R1, 64);
+  let x = sail_shiftleft(x, 33);
+  let y = or_vec(x, sail_zero_extend(R2, 64));
+  let z = R1 @ R2;
+  not_bool(y == z)
+}
\ No newline at end of file
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
diff --git a/test/smt/shiftr_zero_1.unsat.sail b/test/smt/shiftr_zero_1.unsat.sail
new file mode 100644
index 00000000..bcf60bb8
--- /dev/null
+++ b/test/smt/shiftr_zero_1.unsat.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, 64);
+  not_bool(x == 0x0000_0000_0000_0000)
+}
\ No newline at end of file
diff --git a/test/smt/sign_extend.unsat.sail b/test/smt/sign_extend.unsat.sail
new file mode 100644
index 00000000..835c2ce9
--- /dev/null
+++ b/test/smt/sign_extend.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(xs: bits(16)) -> bool = {
+  var p: bool = false;
+  if xs[15] == bitzero then {
+    p = 0x0000 @ xs == sail_sign_extend(xs, 32);
+  } else {
+    p = 0xFFFF @ xs == sail_sign_extend(xs, 32);
+  };
+  not_bool(p)
+}
\ No newline at end of file
diff --git a/test/smt/sign_extend_2.unsat.sail b/test/smt/sign_extend_2.unsat.sail
new file mode 100644
index 00000000..9c5b4437
--- /dev/null
+++ b/test/smt/sign_extend_2.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+function check_sat(xs: bits(16)) -> bool = {
+  var p: bool = true;
+  if xs[15] == bitzero then {
+    p = 0x0000 @ xs == sail_sign_extend(xs, 32);
+  } else {
+    p = 0xFFFF @ xs == sail_sign_extend(xs, 32);
+  };
+  not_bool(p)
+}
\ No newline at end of file
diff --git a/test/smt/trivial.sat.sail b/test/smt/trivial.sat.sail
new file mode 100644
index 00000000..8b8d67ce
--- /dev/null
+++ b/test/smt/trivial.sat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <flow.sail>
+
+function check_sat((): unit) -> bool = {
+  true
+}
\ No newline at end of file
diff --git a/test/smt/trivial.unsat.sail b/test/smt/trivial.unsat.sail
new file mode 100644
index 00000000..2237a21f
--- /dev/null
+++ b/test/smt/trivial.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <flow.sail>
+
+function check_sat((): unit) -> bool = {
+  false
+}
\ No newline at end of file
diff --git a/test/smt/trivial_funcall.sat.sail b/test/smt/trivial_funcall.sat.sail
new file mode 100644
index 00000000..48166c12
--- /dev/null
+++ b/test/smt/trivial_funcall.sat.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+$include <flow.sail>
+
+function f((): unit) -> bool = true
+
+function check_sat((): unit) -> bool = {
+  f()
+}
\ No newline at end of file
diff --git a/test/smt/trivial_return.sat.sail b/test/smt/trivial_return.sat.sail
new file mode 100644
index 00000000..4cfd709a
--- /dev/null
+++ b/test/smt/trivial_return.sat.sail
@@ -0,0 +1,8 @@
+default Order dec
+
+$include <flow.sail>
+
+function check_sat((): unit) -> bool = {
+  return true;
+  false
+}
\ No newline at end of file
diff --git a/test/smt/trivial_return.unsat.sail b/test/smt/trivial_return.unsat.sail
new file mode 100644
index 00000000..261955a4
--- /dev/null
+++ b/test/smt/trivial_return.unsat.sail
@@ -0,0 +1,8 @@
+default Order dec
+
+$include <flow.sail>
+
+function check_sat((): unit) -> bool = {
+  return false;
+  return true
+}
\ No newline at end of file
diff --git a/test/smt/zeros_1.sat.sail b/test/smt/zeros_1.sat.sail
new file mode 100644
index 00000000..4a813dcc
--- /dev/null
+++ b/test/smt/zeros_1.sat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat((): unit) -> bool = {
+  0x00 == sail_zeros(8)
+}
\ No newline at end of file
diff --git a/test/smt/zeros_1.unsat.sail b/test/smt/zeros_1.unsat.sail
new file mode 100644
index 00000000..ade7cd23
--- /dev/null
+++ b/test/smt/zeros_1.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat((): unit) -> bool = {
+  0x1 == sail_zeros(4)
+}
\ No newline at end of file
diff --git a/test/smt/zeros_2.sat.sail b/test/smt/zeros_2.sat.sail
new file mode 100644
index 00000000..5cea2e99
--- /dev/null
+++ b/test/smt/zeros_2.sat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat((): unit) -> bool = {
+  0x0000_0000_0000_0000 == sail_zeros(64)
+}
\ No newline at end of file
diff --git a/test/smt/zeros_2.unsat.sail b/test/smt/zeros_2.unsat.sail
new file mode 100644
index 00000000..855c46b4
--- /dev/null
+++ b/test/smt/zeros_2.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat((): unit) -> bool = {
+  0b1 == sail_zeros(1)
+}
\ No newline at end of file
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
diff --git a/test/smt/zeros_3.unsat.sail b/test/smt/zeros_3.unsat.sail
new file mode 100644
index 00000000..145ab386
--- /dev/null
+++ b/test/smt/zeros_3.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat((): unit) -> bool = {
+  0x0000_0000_0000_0000_1 == sail_zeros(68)
+}
\ No newline at end of file
diff --git a/test/smt/zeros_4.unsat.sail b/test/smt/zeros_4.unsat.sail
new file mode 100644
index 00000000..416430fc
--- /dev/null
+++ b/test/smt/zeros_4.unsat.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+function check_sat((): unit) -> bool = {
+  0x1000_0000_0000_0000_0 == sail_zeros(68)
+}
\ No newline at end of file