61 files changed, 449 insertions, 28 deletions
diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh
index b24cc584..9d7af14f 100755
--- a/test/arm/run_tests.sh
+++ b/test/arm/run_tests.sh
@@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n"
 
 cd $SAILDIR/aarch64
 
-if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail no_vector.sail 1> /dev/null 2> /dev/null;
+if $SAILDIR/sail -undefined_gen -no_lexp_bounds_check -is $DIR/test.isail no_vector.sail 1> /dev/null 2> /dev/null;
 then
     green "loaded no_vector specification" "ok";
 
diff --git a/test/arm/test.isail b/test/arm/test.isail
index 8775ed8f..f3f4dfa1 100644
--- a/test/arm/test.isail
+++ b/test/arm/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 :elf ../test/arm/test_O2.elf
 :output ../test/arm/iresult
 initialize_registers()
diff --git a/test/builtins/div_int.sail b/test/builtins/div_int.sail
index fed6de6e..e8da4f4b 100644
--- a/test/builtins/div_int.sail
+++ b/test/builtins/div_int.sail
@@ -5,6 +5,8 @@ $include <flow.sail>
 $include <vector_dec.sail>
 $include <arith.sail>
 
+overload div_int = {tdiv_int}
+
 function main (() : unit) -> unit = {
   assert(div_int(48240160, 8) == 6030020);
   assert(div_int(48240168, 8) == 6030021);
diff --git a/test/builtins/div_int2.sail b/test/builtins/div_int2.sail
index d3df278d..8ce97cc0 100644
--- a/test/builtins/div_int2.sail
+++ b/test/builtins/div_int2.sail
@@ -5,6 +5,8 @@ $include <flow.sail>
 $include <vector_dec.sail>
 $include <arith.sail>
 
+overload div_int = {tdiv_int}
+
 function main (() : unit) -> unit = {
   assert(div_int(0, 8) == 0);
   assert(div_int(1000, 12) == 83);
diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail
new file mode 100644
index 00000000..f9d7e7c5
--- /dev/null
+++ b/test/builtins/divmod.sail
@@ -0,0 +1,43 @@
+default Order dec
+
+$include <exception_basic.sail>
+$include <arith.sail>
+$include <smt.sail>
+
+function main (() : unit) -> unit = {
+  assert(ediv_int( 7 ,  5) ==  1);
+  assert(ediv_int( 7 , -5) == -1);
+  assert(ediv_int(-7 ,  5) == -2);
+  assert(ediv_int(-7 , -5) ==  2);
+  assert(ediv_int( 12 ,  3) ==  4);
+  assert(ediv_int( 12 , -3) == -4);
+  assert(ediv_int(-12 ,  3) == -4);
+  assert(ediv_int(-12 , -3) ==  4);
+  
+  assert(emod_int( 7 ,  5) ==  2);
+  assert(emod_int( 7 , -5) ==  2);
+  assert(emod_int(-7 ,  5) ==  3);
+  assert(emod_int(-7 , -5) ==  3);
+  assert(emod_int( 12 ,  3) == 0);
+  assert(emod_int( 12 , -3) == 0);
+  assert(emod_int(-12 ,  3) == 0);
+  assert(emod_int(-12 , -3) == 0);
+
+  assert(tdiv_int( 7 ,  5) ==  1);
+  assert(tdiv_int( 7 , -5) == -1);
+  assert(tdiv_int(-7 ,  5) == -1);
+  assert(tdiv_int(-7 , -5) ==  1);
+  assert(tdiv_int( 12 ,  3) ==  4);
+  assert(tdiv_int( 12 , -3) == -4);
+  assert(tdiv_int(-12 ,  3) == -4);
+  assert(tdiv_int(-12 , -3) ==  4);
+  
+  assert(tmod_int( 7 ,  5) ==  2);
+  assert(tmod_int( 7 , -5) ==  2);
+  assert(tmod_int(-7 ,  5) == -2);
+  assert(tmod_int(-7 , -5) == -2);
+  assert(tmod_int( 12 ,  3) == 0);
+  assert(tmod_int( 12 , -3) == 0);
+  assert(tmod_int(-12 ,  3) == 0);
+  assert(tmod_int(-12 , -3) == 0);
+}
+\ No newline at end of file
diff --git a/test/c/anf_as_pattern.expect b/test/c/anf_as_pattern.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/anf_as_pattern.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/anf_as_pattern.sail b/test/c/anf_as_pattern.sail
new file mode 100644
index 00000000..9b9196b1
--- /dev/null
+++ b/test/c/anf_as_pattern.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function test () : unit -> option(int) = {
+  match Some(3) {
+    Some(_) as x => x,
+    _ => None()
+  }
+}
+
+function main() : unit -> unit = {
+  match test() {
+    Some(3) => print_endline("ok"),
+    _ => print_endline("fail")
+  }
+}
+\ No newline at end of file
diff --git a/test/c/anon_rec.expect b/test/c/anon_rec.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/anon_rec.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/anon_rec.sail b/test/c/anon_rec.sail
new file mode 100644
index 00000000..17dd1e07
--- /dev/null
+++ b/test/c/anon_rec.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+union Foo ('a : Type) = {
+  MkFoo : { field1 : 'a, field2 : int }
+}
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let _: Foo(unit) = MkFoo(struct { field1 = (), field2 = 22 });
+  print_endline("ok")
+}
diff --git a/test/c/execute.isail b/test/c/execute.isail
index f4b5ea0f..018dd92c 100644
--- a/test/c/execute.isail
+++ b/test/c/execute.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 main()
diff --git a/test/c/flow_restrict.expect b/test/c/flow_restrict.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/flow_restrict.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/flow_restrict.sail b/test/c/flow_restrict.sail
new file mode 100644
index 00000000..ef2ec412
--- /dev/null
+++ b/test/c/flow_restrict.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+$include <flow.sail>
+$include <exception_basic.sail>
+
+val "print_endline" : string -> unit
+
+register R : bool
+
+function main((): unit) -> unit = {
+  R = false;
+  let 'x = 3180327502475943573495720457203572045720485720458724;
+  y : range(0, 'x) = 1;
+  if R then {
+    assert(constraint('x <= 2));
+    y = 2;
+    let z = y;
+    let x = 2;
+    ()
+  } else {
+    print_endline("ok")
+  }
+}
diff --git a/test/c/poly_int_record.expect b/test/c/poly_int_record.expect
new file mode 100644
index 00000000..a8a10253
--- /dev/null
+++ b/test/c/poly_int_record.expect
@@ -0,0 +1,3 @@
+x = 1
+y = 2
+ok
diff --git a/test/c/poly_int_record.sail b/test/c/poly_int_record.sail
new file mode 100644
index 00000000..ebb18713
--- /dev/null
+++ b/test/c/poly_int_record.sail
@@ -0,0 +1,21 @@
+default Order dec
+
+val "print_endline" : string -> unit
+val "print_int" : (string, int) -> unit
+
+struct S('a: Type) = {
+  field1 : ('a, 'a),
+  field2 : unit
+}
+
+function main((): unit) -> unit = {
+  var s : S(range(0, 3)) = struct { field1 = (0, 3), field2 = () };
+  s.field1 = (1, 2);
+  match s.field1 {
+    (x, y) => {
+      print_int("x = ", x);
+      print_int("y = ", y);
+    }
+  };
+  print_endline("ok");
+}
diff --git a/test/c/poly_record.expect b/test/c/poly_record.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/poly_record.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/poly_record.sail b/test/c/poly_record.sail
new file mode 100644
index 00000000..afe1f144
--- /dev/null
+++ b/test/c/poly_record.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+val "print_endline" : string -> unit
+
+struct S('a: Type) = {
+  field1 : 'a,
+  field2 : unit
+}
+
+function f forall ('a :Type). (s: S('a)) -> unit = {
+  s.field2
+}
+
+function main((): unit) -> unit = {
+  let s : S(unit) = struct { field1 = (), field2 = () };
+  f(s);
+  print_endline("ok");
+}
diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 2ee44fca..be953749 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -40,7 +40,7 @@ def test_interpreter(name):
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
-                step('sail -is execute.isail -iout {}.iresult {}'.format(basename, filename))
+                step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename))
                 step('diff {}.iresult {}.expect'.format(basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
diff --git a/test/c/tuple_union.expect b/test/c/tuple_union.expect
new file mode 100644
index 00000000..d8ea9f4f
--- /dev/null
+++ b/test/c/tuple_union.expect
@@ -0,0 +1,42 @@
+y = 1
+z = 2
+y = 1
+z = 2
+y = 1
+z = 2
+
+y = 3
+z = 4
+y = 3
+z = 4
+y = 3
+z = 4
+
+y = 5
+z = 6
+y = 5
+z = 6
+y = 5
+z = 6
+
+y = 7
+z = 8
+y = 7
+z = 8
+y = 7
+z = 8
+
+y = 9
+z = 10
+y = 9
+z = 10
+y = 9
+z = 10
+
+y = 11
+z = 12
+y = 11
+z = 12
+y = 11
+z = 12
+
diff --git a/test/c/tuple_union.sail b/test/c/tuple_union.sail
new file mode 100644
index 00000000..1914038f
--- /dev/null
+++ b/test/c/tuple_union.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+union U('a: Type) = {
+  Ctor : 'a
+}
+
+type pair = (int, int)
+
+function foo(x: U(pair)) -> unit = {
+  match x {
+    Ctor(y, z) => {
+      print_int("y = ", y);
+      print_int("z = ", z)
+    }
+  };
+  match x {
+    Ctor((y, z)) => {
+      print_int("y = ", y);
+      print_int("z = ", z)
+    }
+  };
+  match x {
+    Ctor(x) => match x {
+      (y, z) => {
+	print_int("y = ", y);
+	print_int("z = ", z)
+      }
+    }
+  };
+  print_endline("")
+}
+
+function main((): unit) -> unit = {
+  foo(Ctor(1, 2));
+  foo(Ctor((3, 4)));
+  let x = (5, 6);
+  foo(Ctor(x));
+  let x = Ctor(7, 8);
+  foo(x);
+  let x = Ctor(((9, 10)));
+  foo(x);
+  let x = (11, 12);
+  foo(Ctor(x));
+}
diff --git a/test/c/unused_poly_ctor.expect b/test/c/unused_poly_ctor.expect
new file mode 100644
index 00000000..e55551e8
--- /dev/null
+++ b/test/c/unused_poly_ctor.expect
@@ -0,0 +1 @@
+y = 0xFFFF
diff --git a/test/c/unused_poly_ctor.sail b/test/c/unused_poly_ctor.sail
new file mode 100644
index 00000000..c752cb33
--- /dev/null
+++ b/test/c/unused_poly_ctor.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+union U('a: Type) = {
+  Err : 'a,
+  Ok : bits(16)
+}
+
+function main((): unit) -> unit = {
+  let x : U(unit) = Ok(0xFFFF);
+  match x {
+    Err() => print_endline("error"),
+    Ok(y) => print_bits("y = ", y)
+  }
+}
diff --git a/test/coq/_CoqProject b/test/coq/_CoqProject
new file mode 100644
index 00000000..a694372c
--- /dev/null
+++ b/test/coq/_CoqProject
@@ -0,0 +1,2 @@
+-R ../../../bbv/theories bbv
+-R ../../lib/coq/ Sail
diff --git a/test/coq/pass/foreach_using_tyvar.sail b/test/coq/pass/foreach_using_tyvar.sail
new file mode 100644
index 00000000..8aabe00c
--- /dev/null
+++ b/test/coq/pass/foreach_using_tyvar.sail
@@ -0,0 +1,11 @@
+$include <arith.sail>
+
+val f : forall 'n, 'n != 5. int('n) -> unit
+
+val magic : forall 'n. int('n) -> bool effect {rreg}
+
+val g : int -> unit effect {rreg}
+
+function g(x) =
+  foreach (n from 0 to x)
+    if n != 5 & magic(n) then f(n)
diff --git a/test/coq/pass/rebind.sail b/test/coq/pass/rebind.sail
new file mode 100644
index 00000000..247c1d6d
--- /dev/null
+++ b/test/coq/pass/rebind.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+val foo : forall 'n, 'n >= 0. (int('n),bits('n)) -> bits(5 + 'n)
+
+function foo(n,x) = {
+  let (n as 'm) = 5 in
+  (append((x : bits('n)),sail_ones(n)) : bits('m + 'n))
+}
diff --git a/test/coq/pass/unbound_ex_tyvars.sail b/test/coq/pass/unbound_ex_tyvars.sail
new file mode 100644
index 00000000..f99b1bd1
--- /dev/null
+++ b/test/coq/pass/unbound_ex_tyvars.sail
@@ -0,0 +1,16 @@
+$include <prelude.sail>
+
+/* We currently produce a rich type for the guard of the if that's
+   visible in the Coq output.  The raw Sail type involves unbound type
+   variables that were existentially bound in x, so in order to print
+   out a useful Coq type we now rewrite it in terms of x. */
+
+val isA : unit -> bool effect {rreg}
+val isB : unit -> bool effect {rreg}
+val isC : unit -> bool effect {rreg}
+val foo : bool -> bool effect {rreg}
+
+function foo(b) = {
+  let x = (b | isA()) & isB();
+  if x | isC() then true else false
+}
diff --git a/test/coq/pass/unpacking.sail b/test/coq/pass/unpacking.sail
new file mode 100644
index 00000000..d0143f40
--- /dev/null
+++ b/test/coq/pass/unpacking.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val f : int -> {'n, 'n >= 0. int('n)} effect {rreg}
+val g : int -> {'n, 'n >= 0. int('n)}
+
+val test : unit -> int effect {rreg}
+
+function test() = {
+  let x1 : {'n, 'n >= 0. int('n)} = f(5);
+  let x2 : int = f(6);
+  let y1 : {'n, 'n >= 0. int('n)} = g(7);
+  let y2 : int = g(8);
+  x1 + x2 + y1 + y2
+}
diff --git a/test/coq/skip b/test/coq/skip
index e0096643..49744fce 100644
--- a/test/coq/skip
+++ b/test/coq/skip
@@ -5,11 +5,40 @@ option_tuple.sail
 pat_completeness.sail
 XXXXX tests which need inline extern definitions adjusted
 patternrefinement.sail
-procstate1.sail
 vector_subrange_gen.sail
 XXXXX currently unsupported use of a bitvector in a parametric vector type
 pure_record.sail
 pure_record2.sail
 pure_record3.sail
 vector_access_dec.sail
-vector_access.sail
-\ No newline at end of file
+vector_access.sail
+XXXXX unsupported existential quantification of a vector length
+bind_typ_var.sail
+XXXXX needs impliciation in constraints fixed
+bool_constraint.sail
+XXXXX needs some smart existential instantiation
+complex_exist_sat.sail
+XXXXX needs name collision avoidance due to type/constructor punning
+constraint_ctor.sail
+XXXXX Complex existential type - probably going to need this for ARM instruction ASTs
+execute_decode_hard.sail
+existential_ast.sail
+existential_ast2.sail
+existential_ast3.sail
+XXXXX Needs an existential witness
+exist1.sail
+exist2.sail
+XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere
+exist_synonym.sail
+reg_32_64.sail
+XXXXX Examples where int(...) should be expanded internally, but not yet supported
+exit1.sail
+exit2.sail
+inline_typ.sail
+XXXXX Examples with exponentials that the solver can't handle
+pow_32_64.sail
+XXXXX Register constructor doesn't use expanded type from type checker - need environment for type definition to fix this easily
+reg_mod.sail
+reg_ref.sail
+XXXXX Dodgy division/modulo stuff
+Replicate.sail
diff --git a/test/mono/exint.sail b/test/mono/exint.sail
index 639e7d45..855b689c 100644
--- a/test/mono/exint.sail
+++ b/test/mono/exint.sail
@@ -39,7 +39,7 @@ function test(x) = {
     0b00 => n = 1,
     0b01 => n = 2,
     0b10 => n = 4,
-    0b11 => ()
+    0b11 => n = 8
   };
   let 'n2 = ex_int(n) in {
     assert(constraint('n2 >= 0));
@@ -54,4 +54,4 @@ function run () = {
   test(0b01);
   test(0b10);
   test(0b11);
-}
-\ No newline at end of file
+}
diff --git a/test/ocaml/bitfield/test.isail b/test/ocaml/bitfield/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/bitfield/test.isail
+++ b/test/ocaml/bitfield/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/hello_world/test.isail b/test/ocaml/hello_world/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/hello_world/test.isail
+++ b/test/ocaml/hello_world/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/loop/test.isail b/test/ocaml/loop/test.isail
index 6a9595e3..009d3eab 100644
--- a/test/ocaml/loop/test.isail
+++ b/test/ocaml/loop/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 :output result
 main()
 :run
diff --git a/test/ocaml/lsl/test.isail b/test/ocaml/lsl/test.isail
index 6a9595e3..009d3eab 100644
--- a/test/ocaml/lsl/test.isail
+++ b/test/ocaml/lsl/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 :output result
 main()
 :run
diff --git a/test/ocaml/pattern1/test.isail b/test/ocaml/pattern1/test.isail
index 6a9595e3..009d3eab 100644
--- a/test/ocaml/pattern1/test.isail
+++ b/test/ocaml/pattern1/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 :output result
 main()
 :run
diff --git a/test/ocaml/reg_alias/test.isail b/test/ocaml/reg_alias/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/reg_alias/test.isail
+++ b/test/ocaml/reg_alias/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/reg_passing/test.isail b/test/ocaml/reg_passing/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/reg_passing/test.isail
+++ b/test/ocaml/reg_passing/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/reg_ref/test.isail b/test/ocaml/reg_ref/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/reg_ref/test.isail
+++ b/test/ocaml/reg_ref/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index c160ef9f..d077cd80 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -96,7 +96,7 @@ cd $DIR
 for i in `ls -d */`;
 do
     cd $DIR/$i;
-    if $SAILDIR/sail -no_warn -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null;
+    if $SAILDIR/sail -no_warn -undefined_gen -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null;
     then
 	if diff expect result;
 	then
diff --git a/test/ocaml/short_circuit/test.isail b/test/ocaml/short_circuit/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/short_circuit/test.isail
+++ b/test/ocaml/short_circuit/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/string_equality/test.isail b/test/ocaml/string_equality/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/string_equality/test.isail
+++ b/test/ocaml/string_equality/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/string_of_struct/test.isail b/test/ocaml/string_of_struct/test.isail
index 6a9595e3..009d3eab 100644
--- a/test/ocaml/string_of_struct/test.isail
+++ b/test/ocaml/string_of_struct/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 :output result
 main()
 :run
diff --git a/test/ocaml/trycatch/test.isail b/test/ocaml/trycatch/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/trycatch/test.isail
+++ b/test/ocaml/trycatch/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/types/test.isail b/test/ocaml/types/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/types/test.isail
+++ b/test/ocaml/types/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/vec_32_64/test.isail b/test/ocaml/vec_32_64/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/vec_32_64/test.isail
+++ b/test/ocaml/vec_32_64/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/ocaml/void/test.isail b/test/ocaml/void/test.isail
index b3eb5d41..e5926ff5 100644
--- a/test/ocaml/void/test.isail
+++ b/test/ocaml/void/test.isail
@@ -1,3 +1,4 @@
+:rewrites interpreter
 initialize_registers()
 :run
 :output result
diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
index 03954a9f..291b7e16 100644
--- a/test/typecheck/pass/Replicate.sail
+++ b/test/typecheck/pass/Replicate.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index 92c6d7cd..c40aa5ec 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -1,8 +1,8 @@
 Type error:
-[[96mReplicate/v1.sail[0m]:11:4-30
-11[96m |[0m    replicate_bits(x, 'N / 'M)
+[[96mReplicate/v1.sail[0m]:14:4-30
+14[96m |[0m    replicate_bits(x, 'N / 'M)
   [91m |[0m    [91m^------------------------^[0m
-  [91m |[0m Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+  [91m |[0m Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
   [91m |[0m Coercion failed because:
   [91m |[0m Mismatched argument types in subtype check
   [91m |[0m 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
index 69f2bb6f..55627db5 100644
--- a/test/typecheck/pass/Replicate/v1.sail
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index 62992f2c..c2c15c12 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -1,8 +1,8 @@
 Type error:
-[[96mReplicate/v2.sail[0m]:10:4-30
-10[96m |[0m    replicate_bits(x, 'N / 'M)
+[[96mReplicate/v2.sail[0m]:13:4-30
+13[96m |[0m    replicate_bits(x, 'N / 'M)
   [91m |[0m    [91m^------------------------^[0m
-  [91m |[0m Tried performing type coercion from {('ex80# : Int), true. vector(('M * 'ex80#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+  [91m |[0m Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
   [91m |[0m Coercion failed because:
   [91m |[0m Mismatched argument types in subtype check
   [91m |[0m 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
index e54b0af4..436ef24b 100644
--- a/test/typecheck/pass/Replicate/v2.sail
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -2,6 +2,9 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+overload operator % = {tmod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/anon_rec.sail b/test/typecheck/pass/anon_rec.sail
new file mode 100644
index 00000000..17dd1e07
--- /dev/null
+++ b/test/typecheck/pass/anon_rec.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+union Foo ('a : Type) = {
+  MkFoo : { field1 : 'a, field2 : int }
+}
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let _: Foo(unit) = MkFoo(struct { field1 = (), field2 = 22 });
+  print_endline("ok")
+}
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index af2cf65f..7bbd59ad 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26[96m |[0m  Some(Ctor1(a, x, c))
   [91m |[0m       [91m^------------^[0m
   [91m |[0m Could not resolve quantifiers for Ctor1
-  [91m |[0m [94m*[0m datasize('ex157#)
+  [91m |[0m [94m*[0m datasize('ex195#)
   [91m |[0m 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index e904aa61..24b927a5 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
   [91m |[0m                                                [91m^---------------^[0m
   [91m |[0m Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
   [91m |[0m Coercion failed because:
-  [91m |[0m (int(33), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))
+  [91m |[0m (int(33), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
   [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65
   [91m |[0m 17[96m |[0m    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
   [91m |[0m   [93m |[0m                                                [93m^---------------^[0m
-  [91m |[0m   [93m |[0m 'ex114# bound here
+  [91m |[0m   [93m |[0m 'ex152# bound here
   [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65
   [91m |[0m 17[96m |[0m    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
   [91m |[0m   [93m |[0m                                                [93m^---------------^[0m
-  [91m |[0m   [93m |[0m 'ex115# bound here
+  [91m |[0m   [93m |[0m 'ex153# bound here
   [91m |[0m [[96mexistential_ast3/v1.sail[0m]:17:48-65
   [91m |[0m 17[96m |[0m    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
   [91m |[0m   [93m |[0m                                                [93m^---------------^[0m
-  [91m |[0m   [93m |[0m 'ex119# bound here
+  [91m |[0m   [93m |[0m 'ex157# bound here
   [91m |[0m 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index fdd13607..a2c08583 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
   [91m |[0m                                                [91m^---------------^[0m
   [91m |[0m Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
   [91m |[0m Coercion failed because:
-  [91m |[0m (int(31), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))
+  [91m |[0m (int(31), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
   [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65
   [91m |[0m 17[96m |[0m    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
   [91m |[0m   [93m |[0m                                                [93m^---------------^[0m
-  [91m |[0m   [93m |[0m 'ex114# bound here
+  [91m |[0m   [93m |[0m 'ex152# bound here
   [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65
   [91m |[0m 17[96m |[0m    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
   [91m |[0m   [93m |[0m                                                [93m^---------------^[0m
-  [91m |[0m   [93m |[0m 'ex115# bound here
+  [91m |[0m   [93m |[0m 'ex153# bound here
   [91m |[0m [[96mexistential_ast3/v2.sail[0m]:17:48-65
   [91m |[0m 17[96m |[0m    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
   [91m |[0m   [93m |[0m                                                [93m^---------------^[0m
-  [91m |[0m   [93m |[0m 'ex119# bound here
+  [91m |[0m   [93m |[0m 'ex157# bound here
   [91m |[0m 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 2432e632..cf86b765 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25[96m |[0m    Some(Ctor(64, unsigned(0b0 @ b @ a)))
   [91m |[0m         [91m^-----------------------------^[0m
   [91m |[0m Could not resolve quantifiers for Ctor
-  [91m |[0m [94m*[0m (datasize(64) & (0 <= 'ex158# & ('ex158# + 1) <= 64))
+  [91m |[0m [94m*[0m (datasize(64) & (0 <= 'ex196# & ('ex196# + 1) <= 64))
   [91m |[0m 
diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail
index 4aac2bed..594130a8 100644
--- a/test/typecheck/pass/guards.sail
+++ b/test/typecheck/pass/guards.sail
@@ -1,8 +1,9 @@
 default Order dec
 
 $include <prelude.sail>
+$include <smt.sail>
 
-overload operator / = {quotient}
+overload operator / = {ediv_int}
 
 union T = {C1 : int, C2 : int}
 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index a63f28f1..80526204 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,8 @@ Type error:
   [91m |[0m No overloading for vector_access, tried:
   [91m |[0m [94m*[0m bitvector_access
   [91m |[0m    Could not resolve quantifiers for bitvector_access
-  [91m |[0m    [94m*[0m (0 <= 'ex76# & ('ex76# + 1) <= 3)
+  [91m |[0m    [94m*[0m (0 <= 'ex114# & ('ex114# + 1) <= 3)
   [91m |[0m [94m*[0m plain_vector_access
   [91m |[0m    Could not resolve quantifiers for plain_vector_access
-  [91m |[0m    [94m*[0m (0 <= 'ex79# & ('ex79# + 1) <= 3)
+  [91m |[0m    [94m*[0m (0 <= 'ex117# & ('ex117# + 1) <= 3)
   [91m |[0m 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index f37d215f..0b705b50 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,8 @@ Type error:
   [91m |[0m No overloading for vector_access, tried:
   [91m |[0m [94m*[0m bitvector_access
   [91m |[0m    Could not resolve quantifiers for bitvector_access
-  [91m |[0m    [94m*[0m (0 <= 'ex76# & ('ex76# + 1) <= 4)
+  [91m |[0m    [94m*[0m (0 <= 'ex114# & ('ex114# + 1) <= 4)
   [91m |[0m [94m*[0m plain_vector_access
   [91m |[0m    Could not resolve quantifiers for plain_vector_access
-  [91m |[0m    [94m*[0m (0 <= 'ex79# & ('ex79# + 1) <= 4)
+  [91m |[0m    [94m*[0m (0 <= 'ex117# & ('ex117# + 1) <= 4)
   [91m |[0m 
diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail
index 5ca85f53..cd3ca46c 100644
--- a/test/typecheck/pass/recursion.sail
+++ b/test/typecheck/pass/recursion.sail
@@ -2,6 +2,8 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+
 val log2 : int -> int
 
 function log2(n) =
diff --git a/test/typecheck/pass/shadow_let.sail b/test/typecheck/pass/shadow_let.sail
new file mode 100644
index 00000000..8a30744c
--- /dev/null
+++ b/test/typecheck/pass/shadow_let.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  foo(y);
+}
+\ No newline at end of file
diff --git a/test/typecheck/pass/shadow_let/v1.expect b/test/typecheck/pass/shadow_let/v1.expect
new file mode 100644
index 00000000..3cd21dc0
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.expect
@@ -0,0 +1,12 @@
+Type error:
+[[96mshadow_let/v1.sail[0m]:13:6-7
+13[96m |[0m  bar(y);
+  [91m |[0m      [91m^[0m
+  [91m |[0m Tried performing type coercion from int('_x#1) to int(2) on y
+  [91m |[0m Coercion failed because:
+  [91m |[0m int('_x#1) is not a subtype of int(2)
+  [91m |[0m [[96mshadow_let/v1.sail[0m]:9:6-8
+  [91m |[0m 9[96m |[0m  let 'x : {'z, 'z == 1. int('z)} = 1;
+  [91m |[0m  [93m |[0m      [93m^^[0m
+  [91m |[0m  [93m |[0m '_x#1 bound here
+  [91m |[0m 
diff --git a/test/typecheck/pass/shadow_let/v1.sail b/test/typecheck/pass/shadow_let/v1.sail
new file mode 100644
index 00000000..d7dc20a5
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  bar(y);
+}
+\ No newline at end of file