6 files changed, 24 insertions, 24 deletions
diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail
index df588662..398e814f 100644
--- a/test/c/pattern_concat_nest.sail
+++ b/test/c/pattern_concat_nest.sail
@@ -1,27 +1,6 @@
 default Order dec
 
-type bits ('n : Int) = bitvector('n, dec)
-
-union option ('a : Type) = {None : unit, Some : 'a}
-
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", c: "vector_subrange"}
-		    : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm & 'm <= 'n.
-  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-
-val bitvector_access = {ocaml: "access", lem: "access_vec_dec", c: "vector_access"}
-		     : forall ('n : Int) ('m : Int), 0 <= 'm & 'm + 1 <= 'n.
-  (bits('n), atom('m)) -> bit
-
-overload vector_access = {bitvector_access}
-
-val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"}: (bit, bit) -> bool
-
-overload operator == = {
-  eq_bit
-}
-
-val and_bool = {ocaml: "and_bool", lem: "and_bool", smt: "and_bool", interpreter: "and_bool", c: "and_bool"}: (bool, bool) -> bool
-
+$include <prelude.sail>
 
 ////////////////////////////////////////////////////////////
 
diff --git a/test/c/rv_duopod_bug.expect b/test/c/rv_duopod_bug.expect
new file mode 100644
index 00000000..681c7c43
--- /dev/null
+++ b/test/c/rv_duopod_bug.expect
@@ -0,0 +1,2 @@
+0 0x0000000000000000
+1 0xFFFFFFFFFFFFFFFF
diff --git a/test/c/rv_duopod_bug.sail b/test/c/rv_duopod_bug.sail
new file mode 100644
index 00000000..9a11996c
--- /dev/null
+++ b/test/c/rv_duopod_bug.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+val rX : int -> bits(64)
+
+function rX 0 = sail_zeros(64)
+and rX (r if r > 0) = sail_ones(64)
+
+function main() -> unit = {
+  print_bits("0 ", rX(0));
+  print_bits("1 ", rX(1))
+}
diff --git a/test/run_tests.sh b/test/run_tests.sh
index a228e270..1af340d8 100755
--- a/test/run_tests.sh
+++ b/test/run_tests.sh
@@ -36,6 +36,12 @@ printf "==========================================\n"
 TEST_PAR=8 ./c/run_tests.py
 
 printf "\n==========================================\n"
+printf "SMT tests\n"
+printf "==========================================\n"
+
+TEST_PAR=8 ./smt/run_tests.py
+
+printf "\n==========================================\n"
 printf "Builtins tests\n"
 printf "==========================================\n"
 
diff --git a/test/smt/mem_builtins.unsat.sail b/test/smt/mem_builtins.unsat.sail
index 28e44658..eb003891 100644
--- a/test/smt/mem_builtins.unsat.sail
+++ b/test/smt/mem_builtins.unsat.sail
@@ -5,7 +5,7 @@ $include <regfp.sail>
 
 $property
 function prop() -> bool = {
-  __barrier(Barrier_DSB);
+  __barrier(Barrier_DSB(A64_FullShare, A64_barrier_all));
   let _ = __excl_res();
   __write_mem_ea(Write_exclusive_release, 32, 0xFFFF_FFFF, 8);
   true
diff --git a/test/smt/store_load_scattered.sat.sail b/test/smt/store_load_scattered.sat.sail
index d556295f..c039e87c 100644
--- a/test/smt/store_load_scattered.sat.sail
+++ b/test/smt/store_load_scattered.sat.sail
@@ -6,7 +6,7 @@ $include "test/arch.sail"
 
 scattered union ast
 
-val execute : ast -> bool
+val execute : ast -> bool effect {rmem, rreg, wmv, wreg}
 
 union clause ast = LOAD : (bits(2), bits(2))