Backport fixes to SMT generation from poly_mapping branch

20 files changed, 787 insertions, 337 deletions

diff --git a/language/jib.ott b/language/jib.ott
index 1345ba64..6332c403 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -92,7 +92,6 @@ op :: '' ::=
 
 cval :: 'V_' ::=
   | name : ctyp                                       :: :: id
-  | '&' name : ctyp                                   :: :: ref
   | value : ctyp                                      :: :: lit
   | struct { uid0 = cval0 , ... , uidn = cvaln } ctyp :: :: struct
   | cval != kind id ( ctyp0 , ... , ctypn ) ctyp      :: :: ctor_kind
diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index c9892e4c..15daa545 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -38,6 +38,9 @@ let sign_extend bits len = exts_bits len bits
 val zeros : integer -> list bitU
 let zeros len = repeat [B0] len
 
+val ones : integer -> list bitU
+let ones len = repeat [B1] len
+
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index f657803f..69bf0852 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -423,6 +423,26 @@ let char_of_nibble = function
   | _ -> Nothing
   end
 
+let nibble_of_char = function
+  | #'0' -> Just (B0, B0, B0, B0)
+  | #'1' -> Just (B0, B0, B0, B1)
+  | #'2' -> Just (B0, B0, B1, B0)
+  | #'3' -> Just (B0, B0, B1, B1)
+  | #'4' -> Just (B0, B1, B0, B0)
+  | #'5' -> Just (B0, B1, B0, B1)
+  | #'6' -> Just (B0, B1, B1, B0)
+  | #'7' -> Just (B0, B1, B1, B1)
+  | #'8' -> Just (B1, B0, B0, B0)
+  | #'9' -> Just (B1, B0, B0, B1)
+  | #'A' -> Just (B1, B0, B1, B0)
+  | #'B' -> Just (B1, B0, B1, B1)
+  | #'C' -> Just (B1, B1, B0, B0)
+  | #'D' -> Just (B1, B1, B0, B1)
+  | #'E' -> Just (B1, B1, B1, B0)
+  | #'F' -> Just (B1, B1, B1, B1)
+  | _ -> Nothing
+  end
+
 let rec hexstring_of_bits bs = match bs with
   | b1 :: b2 :: b3 :: b4 :: bs ->
      let n = char_of_nibble (b1, b2, b3, b4) in
@@ -436,12 +456,14 @@ let rec hexstring_of_bits bs = match bs with
   end
 declare {isabelle; hol} termination_argument hexstring_of_bits = automatic
 
-let show_bitlist bs =
+let show_bitlist_prefix c bs =
   match hexstring_of_bits bs with
-  | Just s -> toString (#'0' :: #'x' :: s)
-  | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs)
+  | Just s -> toString (c :: #'x' :: s)
+  | Nothing -> toString (c :: #'b' :: map bitU_char bs)
   end
 
+let show_bitlist bs = show_bitlist_prefix #'0' bs
+
 (*** List operations *)
 
 let inline (^^) = append_list
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index c1f2d24c..ae6afc0c 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -100,7 +100,7 @@ let zencode_uid (id, ctyps) =
   match ctyps with
   | [] -> Util.zencode_string (string_of_id id)
   | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
-                              
+
 (**************************************************************************)
 (* 2. Converting sail types to C types                                    *)
 (**************************************************************************)
@@ -1094,24 +1094,28 @@ let sgen_mask n =
   else
     failwith "Tried to create a mask literal for a vector greater than 64 bits."
 
-let sgen_value = function
+let rec sgen_value = function
   | VL_bits ([], _) -> "UINT64_C(0)"
   | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
   | VL_int i -> Big_int.to_string i ^ "l"
   | VL_bool true -> "true"
   | VL_bool false -> "false"
-  | VL_null -> "NULL"
   | VL_unit -> "UNIT"
   | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
   | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
   | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
-  
+  | VL_matcher (n, uid) -> Printf.sprintf "matcher(%d, %d)" n uid
+  | VL_tuple values -> "(" ^ Util.string_of_list ", " string_of_value values ^ ")"
+  | VL_list [] -> "NULL"
+  | VL_list values -> "[|" ^ Util.string_of_list ", " string_of_value values ^ "|]"
+  | VL_enum element -> Util.zencode_string element
+  | VL_ref r -> "&" ^ Util.zencode_string r
+
 let rec sgen_cval = function
   | V_id (id, ctyp) -> sgen_name id
-  | V_ref (id, _) -> "&" ^ sgen_name id
   | V_lit (vl, ctyp) -> sgen_value vl
   | V_call (op, cvals) -> sgen_call op cvals
   | V_field (f, field) ->
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 0efac940..7cc1dd28 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -156,6 +156,7 @@ type ctx =
     locals : (mut * ctyp) Bindings.t;
     letbinds : int list;
     no_raw : bool;
+    unroll_loops : int option;
     convert_typ : ctx -> typ -> ctyp;
     optimize_anf : ctx -> typ aexp -> typ aexp;
     specialize_calls : bool;
@@ -174,6 +175,7 @@ let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
     locals = Bindings.empty;
     letbinds = [];
     no_raw = false;
+    unroll_loops = None;
     convert_typ = convert_typ;
     optimize_anf = optimize_anf;
     specialize_calls = false;
@@ -210,7 +212,7 @@ let rec compile_aval l ctx = function
      end
 
   | AV_ref (id, typ) ->
-     [], V_ref (name id, ctyp_of_typ ctx (lvar_typ typ)), []
+     [], V_lit (VL_ref (string_of_id id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), []
 
   | AV_lit (L_aux (L_string str, _), typ) ->
      [], V_lit ((VL_string (String.escaped str)), ctyp_of_typ ctx typ), []
@@ -581,12 +583,12 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
      | CT_list ctyp ->
         let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in
         let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in
-        [ijump (V_call (Eq, [cval; V_lit (VL_null, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
+        [ijump (V_call (Eq, [cval; V_lit (VL_list [], CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
      | _ ->
         raise (Reporting.err_general l "Tried to pattern match cons on non list type")
      end
 
-  | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_null, ctyp)])) case_label], [], ctx
+  | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_list [], ctyp)])) case_label], [], ctx
 
 let unit_cval = V_lit (VL_unit, CT_unit)
 
@@ -927,21 +929,29 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
 
      let loop_var = name loop_var in
 
+     let loop_body prefix continue =
+       prefix
+       @ [iblock ([ijump (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label]
+                  @ body_setup
+                  @ [body_call (CL_id (body_gs, CT_unit))]
+                  @ body_cleanup
+                  @ [icopy l (CL_id (loop_var, (CT_fint 64)))
+                       (V_call ((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)]))]
+                  @ continue ())]
+     in
+     (* We can either generate an actual loop body for C, or unroll the body for SMT *)
+     let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in
+     let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in
+     let body = match ctx.unroll_loops with Some times -> unroll times 0 | None -> actual in
+
      variable_init from_gs from_setup from_call from_cleanup
      @ variable_init to_gs to_setup to_call to_cleanup
      @ variable_init step_gs step_setup step_call step_cleanup
      @ [iblock ([idecl (CT_fint 64) loop_var;
                  icopy l (CL_id (loop_var, (CT_fint 64))) (V_id (from_gs, CT_fint 64));
-                 idecl CT_unit body_gs;
-                 iblock ([ilabel loop_start_label]
-                         @ [ijump (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label]
-                         @ body_setup
-                         @ [body_call (CL_id (body_gs, CT_unit))]
-                         @ body_cleanup
-                         @ [icopy l (CL_id (loop_var, (CT_fint 64)))
-                                  (V_call ((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)]))]
-                         @ [igoto loop_start_label]);
-                 ilabel loop_end_label])],
+                 idecl CT_unit body_gs]
+                @ body
+                @ [ilabel loop_end_label])],
      (fun clexp -> icopy l clexp unit_cval),
      []
 
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 273e9e03..4f9fecd8 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -78,6 +78,7 @@ type ctx =
     locals : (mut * ctyp) Bindings.t;
     letbinds : int list;
     no_raw : bool;
+    unroll_loops : int option;
     convert_typ : ctx -> typ -> ctyp;
     optimize_anf : ctx -> typ aexp -> typ aexp;
     (** If false (default), function arguments must match the function
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index 323f3cd0..a54ac4b3 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -162,7 +162,6 @@ let unique_per_function_ids cdefs =
 
 let rec cval_subst id subst = function
   | V_id (id', ctyp) -> if Name.compare id id' = 0 then subst else V_id (id', ctyp)
-  | V_ref (reg_id, ctyp) -> V_ref (reg_id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (op, cvals) -> V_call (op, List.map (cval_subst id subst) cvals)
   | V_field (cval, field) -> V_field (cval_subst id subst cval, field)
@@ -174,7 +173,6 @@ let rec cval_subst id subst = function
 
 let rec cval_map_id f = function
   | V_id (id, ctyp) -> V_id (f id, ctyp)
-  | V_ref (id, ctyp) -> V_ref (f id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (call, cvals) -> V_call (call, List.map (cval_map_id f) cvals)
   | V_field (cval, field) -> V_field (cval_map_id f cval, field)
@@ -433,7 +431,6 @@ let remove_tuples cdefs ctx =
   in
   let rec fix_cval = function
     | V_id (id, ctyp) -> V_id (id, ctyp)
-    | V_ref (id, ctyp) -> V_ref (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_ctor_kind (cval, id, unifiers, ctyp) ->
        V_ctor_kind (fix_cval cval, id, unifiers, ctyp)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index fbaf8d3f..df3be1b7 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -73,6 +73,8 @@ let opt_debug_graphs = ref false
 
 let opt_propagate_vars = ref false
 
+let opt_unroll_limit = ref 10
+
 module EventMap = Map.Make(Event)
 
 (* Note that we have to use x : ty ref rather than mutable x : ty, to
@@ -89,6 +91,8 @@ type ctx = {
     pragma_l : Ast.l;
     arg_stack : (int * string) Stack.t;
     ast : Type_check.tannot defs;
+    shared : ctyp Bindings.t;
+    preserved : IdSet.t;
     events : smt_exp Stack.t EventMap.t ref;
     node : int;
     pathcond : smt_exp Lazy.t;
@@ -114,6 +118,8 @@ let initial_ctx () = {
     pragma_l = Parse_ast.Unknown;
     arg_stack = Stack.create ();
     ast = Defs [];
+    shared = Bindings.empty;
+    preserved = IdSet.empty;
     events = ref EventMap.empty;
     node = -1;
     pathcond = lazy (Bool_lit true);
@@ -129,6 +135,19 @@ let event_stack ctx ev =
      ctx.events := EventMap.add ev stack !(ctx.events);
      stack
 
+let add_event ctx ev smt =
+  let stack = event_stack ctx ev in
+  Stack.push (Fn ("and", [Lazy.force ctx.pathcond; smt])) stack
+
+let add_pathcond_event ctx ev =
+  Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)
+
+let overflow_check ctx smt =
+  if not !opt_ignore_overflow then (
+    Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l "";
+    add_event ctx Overflow smt
+  )
+
 let lbits_size ctx = Util.power 2 ctx.lbits_index
 
 let vector_index = ref 5
@@ -188,21 +207,17 @@ let rec smt_ctyp ctx = function
    don't have a very good way to get the binary representation of
    either an ocaml integer or a big integer. *)
 let bvpint sz x =
+  let open Sail2_values in
   if Big_int.less_equal Big_int.zero x && Big_int.less_equal x (Big_int.of_int max_int) then (
-    let open Sail_lib in
     let x = Big_int.to_int x in
-    if sz mod 4 = 0 then
-      let hex = Printf.sprintf "%X" x in
-      let padding = String.make (sz / 4 - String.length hex) '0' in
-      Hex (padding ^ hex)
-    else
-      let bin = Printf.sprintf "%X" x |> list_of_string |> List.map hex_char |> List.concat in
-      let _, bin = Util.take_drop (function B0 -> true | B1 -> false) bin in
-      let bin = String.concat "" (List.map string_of_bit bin) in
-      let padding = String.make (sz - String.length bin) '0' in
-      Bin (padding ^ bin)
+    match Printf.sprintf "%X" x |> Util.string_to_list |> List.map nibble_of_char |> Util.option_all with
+    | Some nibbles ->
+       let bin = List.map (fun (a, b, c, d) -> [a; b; c; d]) nibbles |> List.concat in
+       let _, bin = Util.take_drop (function B0 -> true | _ -> false) bin in
+       let padding = List.init (sz - List.length bin) (fun _ -> B0) in
+       Bitvec_lit (padding @ bin)
+    | None -> assert false
   ) else if Big_int.greater x (Big_int.of_int max_int) then (
-    let open Sail_lib in
     let y = ref x in
     let bin = ref [] in
     while (not (Big_int.equal !y Big_int.zero)) do
@@ -210,14 +225,13 @@ let bvpint sz x =
       bin := (if Big_int.equal m Big_int.zero then B0 else B1) :: !bin;
       y := q
     done;
-    let bin = String.concat "" (List.map string_of_bit !bin) in
-    let padding_size = sz - String.length bin in
+    let padding_size = sz - List.length !bin in
     if padding_size < 0 then
       raise (Reporting.err_general Parse_ast.Unknown
                (Printf.sprintf "Could not create a %d-bit integer with value %s.\nTry increasing the maximum integer size"
                   sz (Big_int.to_string x)));
-    let padding = String.make (sz - String.length bin) '0' in
-    Bin (padding ^ bin)
+    let padding = List.init padding_size (fun _ -> B0) in
+    Bitvec_lit (padding @ !bin)
   ) else failwith "Invalid bvpint"
 
 let bvint sz x =
@@ -226,22 +240,68 @@ let bvint sz x =
   else
     bvpint sz x
 
+(** [force_size ctx n m exp] takes a smt expression assumed to be a
+   integer (signed bitvector) of length m and forces it to be length n
+   by either sign extending it or truncating it as required *)
+let force_size ?checked:(checked=true) ctx n m smt =
+  if n = m then
+    smt
+  else if n > m then
+    SignExtend (n - m, smt)
+  else
+    let check =
+      (* If the top bit of the truncated number is one *)
+      Ite (Fn ("=", [Extract (n - 1, n - 1, smt); Bitvec_lit [Sail2_values.B1]]),
+           (* Then we have an overflow, unless all bits we truncated were also one *)
+           Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvones (m - n)])]),
+           (* Otherwise, all the top bits must be zero *)
+           Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvzero (m - n)])]))
+    in
+    if checked then overflow_check ctx check else ();
+    Extract (n - 1, 0, smt)
+
+(** [unsigned_size ctx n m exp] is much like force_size, but it
+   assumes that the bitvector is unsigned *)
+let unsigned_size ?checked:(checked=true) ctx n m smt =
+  if n = m then
+    smt
+  else if n > m then
+    Fn ("concat", [bvzero (n - m); smt])
+  else
+    Extract (n - 1, 0, smt)
+
+let smt_conversion ctx from_ctyp to_ctyp x =
+  match from_ctyp, to_ctyp with
+  | _, _ when ctyp_equal from_ctyp to_ctyp -> x
+  | CT_constant c, CT_fint sz ->
+     bvint sz c
+  | CT_constant c, CT_lint ->
+     bvint ctx.lint_size c
+  | CT_fint sz, CT_lint ->
+     force_size ctx ctx.lint_size sz x
+  | CT_lint, CT_fint sz ->
+     force_size ctx sz ctx.lint_size x
+  | CT_lbits _, CT_fbits (n, _) ->
+     unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
+  | CT_fbits (n, _), CT_lbits _ ->
+     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); unsigned_size ctx (lbits_size ctx) n x])
+
+  | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))
+
 (* Translate Jib literals into SMT *)
-let smt_value ctx vl ctyp =
+let rec smt_value ctx vl ctyp =
   let open Value2 in
   match vl, ctyp with
-  | VL_bits (bs, true), CT_fbits (n, _) ->
-     (* FIXME: Output the correct number of bits in Jib_compile *)
-     begin match Sail2_values.hexstring_of_bits (List.rev (Util.take n (List.rev bs))) with
-     | Some s -> Hex (Xstring.implode s)
-     | None -> Bin (Xstring.implode (List.map Sail2_values.bitU_char (List.rev (Util.take n (List.rev bs)))))
-     end
+  | VL_bits (bv, true), CT_fbits (n, _) ->
+     unsigned_size ctx n (List.length bv) (Bitvec_lit bv)
+  | VL_bits (bv, true), CT_lbits _ ->
+     let sz = List.length bv in
+     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int sz); unsigned_size ctx (lbits_size ctx) sz (Bitvec_lit bv)])
   | VL_bool b, _ -> Bool_lit b
   | VL_int n, CT_constant m -> bvint (required_width n) n
   | VL_int n, CT_fint sz -> bvint sz n
   | VL_int n, CT_lint -> bvint ctx.lint_size n
-  | VL_bit Sail2_values.B0, CT_bit -> Bin "0"
-  | VL_bit Sail2_values.B1, CT_bit -> Bin "1"
+  | VL_bit b, CT_bit -> Bitvec_lit [b]
   | VL_unit, _ -> Enum "unit"
   | VL_string str, _ ->
      ctx.use_string := true;
@@ -252,7 +312,23 @@ let smt_value ctx vl ctyp =
        Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))])
      else
        Real_lit str
-  | vl, _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl)
+  | VL_enum str, _ -> Enum (Util.zencode_string str)
+  | VL_tuple vls, CT_tup ctyps when List.length vls = List.length ctyps ->
+     Fn ("tup" ^ string_of_int (List.length vls), List.map2 (smt_value ctx) vls ctyps)
+  | VL_ref reg_name, _ ->
+     let id = mk_id reg_name in
+     let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
+     assert (CTMap.cardinal rmap = 1);
+     begin match CTMap.min_binding_opt rmap with
+     | Some (ctyp, regs) ->
+        begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
+        | Some i ->
+           bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
+        | None -> assert false
+        end
+     | _ -> assert false
+     end
+  | _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl ^ " : " ^ string_of_ctyp ctyp)
 
 let rec smt_cval ctx cval =
   match cval_ctyp cval with
@@ -264,6 +340,7 @@ let rec smt_cval ctx cval =
      | V_id (Name (id, _) as ssa_id, _) ->
         begin match Type_check.Env.lookup_id id ctx.tc_env with
         | Enum _ -> Enum (zencode_id id)
+        | _ when Bindings.mem id ctx.shared -> Shared (zencode_id id)
         | _ -> Var (zencode_name ssa_id)
         end
      | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
@@ -272,7 +349,7 @@ let rec smt_cval ctx cval =
      | V_call (Bvor, [cval1; cval2]) ->
         Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
      | V_call (Bit_to_bool, [cval]) ->
-        Fn ("=", [smt_cval ctx cval; Bin "1"])
+        Fn ("=", [smt_cval ctx cval; Bitvec_lit [Sail2_values.B1]])
      | V_call (Eq, [cval1; cval2]) ->
         Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
      | V_call (Bnot, [cval]) ->
@@ -281,14 +358,18 @@ let rec smt_cval ctx cval =
         smt_conj (List.map (smt_cval ctx) cvals)
      | V_call (Bor, cvals) ->
         smt_disj (List.map (smt_cval ctx) cvals)
+     | V_call (Igt, [cval1; cval2]) ->
+        Fn ("bvsgt", [smt_cval ctx cval1; smt_cval ctx cval2])
+     | V_call (Iadd, [cval1; cval2]) ->
+        Fn ("bvadd", [smt_cval ctx cval1; smt_cval ctx cval2])
      | V_ctor_kind (union, ctor_id, unifiers, _) ->
         Fn ("not", [Tester (zencode_uid (ctor_id, unifiers), smt_cval ctx union)])
      | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
         Fn ("un" ^ zencode_uid (ctor_id, unifiers), [smt_cval ctx union])
-     | V_field (union, field) ->
-        begin match cval_ctyp union with
+     | V_field (record, field) ->
+        begin match cval_ctyp record with
         | CT_struct (struct_id, _) ->
-           Fn (zencode_upper_id struct_id ^ "_" ^ zencode_uid field, [smt_cval ctx union])
+           Field (zencode_upper_id struct_id ^ "_" ^ zencode_uid field, smt_cval ctx record)
         | _ -> failwith "Field for non-struct type"
         end
      | V_struct (fields, ctyp) ->
@@ -297,43 +378,18 @@ let rec smt_cval ctx cval =
            let set_field (field, cval) =
              match Util.assoc_compare_opt UId.compare field field_ctyps with
              | None -> failwith "Field type not found"
-             | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
-                smt_cval ctx cval
-             | _ -> failwith "Type mismatch when generating struct for SMT"
+             | Some ctyp ->
+                zencode_upper_id struct_id ^ "_" ^ zencode_uid field,
+                smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval)
            in
-           Fn (zencode_upper_id struct_id, List.map set_field fields)
+           Struct (zencode_upper_id struct_id, List.map set_field fields)
         | _ -> failwith "Struct does not have struct type"
         end
      | V_tuple_member (frag, len, n) ->
         ctx.tuple_sizes := IntSet.add len !(ctx.tuple_sizes);
         Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval ctx frag])
-     | V_ref (Name (id, _), _) ->
-        let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
-        assert (CTMap.cardinal rmap = 1);
-        begin match CTMap.min_binding_opt rmap with
-        | Some (ctyp, regs) ->
-           begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
-           | Some i ->
-              bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
-           | None -> assert false
-           end
-        | _ -> assert false
-        end
      | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)
 
-let add_event ctx ev smt =
-  let stack = event_stack ctx ev in
-  Stack.push (Fn ("=>", [Lazy.force ctx.pathcond; smt])) stack
-
-let add_pathcond_event ctx ev =
-  Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)
-
-let overflow_check ctx smt =
-  if not !opt_ignore_overflow then (
-    Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l "";
-    add_event ctx Overflow smt
-  )
-
 (**************************************************************************)
 (* 1. Generating SMT for Sail builtins                                    *)
 (**************************************************************************)
@@ -342,8 +398,8 @@ let builtin_type_error ctx fn cvals =
   let args = Util.string_of_list ", " (fun cval -> string_of_ctyp (cval_ctyp cval)) cvals in
   function
   | Some ret_ctyp ->
-     raise (Reporting.err_todo ctx.pragma_l
-       (Printf.sprintf "%s : (%s) -> %s" fn args (string_of_ctyp ret_ctyp)))
+     let message = Printf.sprintf "%s : (%s) -> %s" fn args (string_of_ctyp ret_ctyp) in
+     raise (Reporting.err_todo ctx.pragma_l message)
   | None ->
      raise (Reporting.err_todo ctx.pragma_l (Printf.sprintf "%s : (%s)" fn args))
 
@@ -385,36 +441,6 @@ let builtin_gteq = builtin_int_comparison "bvsge" Big_int.greater_equal
 
 (* ***** Arithmetic operations: lib/arith.sail ***** *)
 
-(** [force_size ctx n m exp] takes a smt expression assumed to be a
-   integer (signed bitvector) of length m and forces it to be length n
-   by either sign extending it or truncating it as required *)
-let force_size ?checked:(checked=true) ctx n m smt =
-  if n = m then
-    smt
-  else if n > m then
-    SignExtend (n - m, smt)
-  else
-    let check =
-      (* If the top bit of the truncated number is one *)
-      Ite (Fn ("=", [Extract (n - 1, n - 1, smt); Bin "1"]),
-           (* Then we have an overflow, unless all bits we truncated were also one *)
-           Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvones (m - n)])]),
-           (* Otherwise, all the top bits must be zero *)
-           Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvzero (m - n)])]))
-    in
-    if checked then overflow_check ctx check else ();
-    Extract (n - 1, 0, smt)
-
-(** [unsigned_size ctx n m exp] is much like force_size, but it
-   assumes that the bitvector is unsigned *)
-let unsigned_size ?checked:(checked=true) ctx n m smt =
-  if n = m then
-    smt
-  else if n > m then
-    Fn ("concat", [bvzero (n - m); smt])
-  else
-    Extract (n - 1, 0, smt)
-
 let int_size ctx = function
   | CT_constant n -> required_width n
   | CT_fint sz -> sz
@@ -457,8 +483,9 @@ let builtin_negate_int ctx v ret_ctyp =
   | CT_constant c, _ ->
      bvint (int_size ctx ret_ctyp) (Big_int.negate c)
   | ctyp, _ ->
+     let open Sail2_values in
      let smt = force_size ctx (int_size ctx ret_ctyp) (int_size ctx ctyp) (smt_cval ctx v) in
-     overflow_check ctx (Fn ("=", [smt; Bin ("1" ^ String.make (int_size ctx ret_ctyp - 1) '0')]));
+     overflow_check ctx (Fn ("=", [smt; Bitvec_lit (B1 :: List.init (int_size ctx ret_ctyp - 1) (fun _ -> B0))]));
      Fn ("bvneg", [smt])
 
 let builtin_shift_int fn big_int_fn ctx v1 v2 ret_ctyp =
@@ -494,7 +521,7 @@ let builtin_abs_int ctx v ret_ctyp =
   | ctyp, _ ->
      let sz = int_size ctx ctyp in
      let smt = smt_cval ctx v in
-     Ite (Fn ("=", [Extract (sz - 1, sz -1, smt); Bin "1"]),
+     Ite (Fn ("=", [Extract (sz - 1, sz -1, smt); Bitvec_lit [Sail2_values.B1]]),
           force_size ctx (int_size ctx ret_ctyp) sz (Fn ("bvneg", [smt])),
           force_size ctx (int_size ctx ret_ctyp) sz smt)
 
@@ -531,6 +558,25 @@ let builtin_min_int ctx v1 v2 ret_ctyp =
           smt1,
           smt2)
 
+let builtin_min_int ctx v1 v2 ret_ctyp =
+  match cval_ctyp v1, cval_ctyp v2 with
+  | CT_constant n, CT_constant m ->
+     bvint (int_size ctx ret_ctyp) (min n m)
+
+  | ctyp1, ctyp2 ->
+     let ret_sz = int_size ctx ret_ctyp in
+     let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in
+     let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in
+     Ite (Fn ("bvslt", [smt1; smt2]),
+          smt1,
+          smt2)
+
+let builtin_tdiv_int =
+  builtin_arith "bvudiv" (Sail2_values.tdiv_int) (fun x -> x)
+
+let builtin_tmod_int =
+  builtin_arith "bvurem" (Sail2_values.tmod_int) (fun x -> x)
+  
 let bvmask ctx len =
   let all_ones = bvones (lbits_size ctx) in
   let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
@@ -623,7 +669,7 @@ let builtin_sign_extend ctx vbits vlen ret_ctyp =
      smt_cval ctx vbits
   | CT_fbits (n, _), CT_fbits (m, _) ->
      let bv = smt_cval ctx vbits in
-     let top_bit_one = Fn ("=", [Extract (n - 1, n - 1, bv); Bin "1"]) in
+     let top_bit_one = Fn ("=", [Extract (n - 1, n - 1, bv); Bitvec_lit [Sail2_values.B1]]) in
      Ite (top_bit_one, Fn ("concat", [bvones (m - n); bv]), Fn ("concat", [bvzero (m - n); bv]))
 
   | _ -> builtin_type_error ctx "sign_extend" [vbits; vlen] (Some ret_ctyp)
@@ -658,14 +704,14 @@ let builtin_not_bits ctx v ret_ctyp =
   | _, _ -> builtin_type_error ctx "not_bits" [v] (Some ret_ctyp)
 
 let builtin_bitwise fn ctx v1 v2 ret_ctyp =
-  match cval_ctyp v1, cval_ctyp v2 with
-  | CT_fbits (n, _), CT_fbits (m, _) ->
-     assert (n = m);
+  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
+  | CT_fbits (n, _), CT_fbits (m, _), CT_fbits (o, _) ->
+     assert (n = m && m = o);
      let smt1 = smt_cval ctx v1 in
      let smt2 = smt_cval ctx v2 in
      Fn (fn, [smt1; smt2])
 
-  | CT_lbits _, CT_lbits _ ->
+  | CT_lbits _, CT_lbits _, CT_lbits _ ->
      let smt1 = smt_cval ctx v1 in
      let smt2 = smt_cval ctx v2 in
      Fn ("Bits", [Fn ("len", [smt1]); Fn (fn, [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])
@@ -674,6 +720,7 @@ let builtin_bitwise fn ctx v1 v2 ret_ctyp =
 
 let builtin_and_bits = builtin_bitwise "bvand"
 let builtin_or_bits = builtin_bitwise "bvor"
+let builtin_xor_bits = builtin_bitwise "bvxor"
 
 let builtin_append ctx v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
@@ -743,19 +790,29 @@ let builtin_length ctx v ret_ctyp =
   | _, _ -> builtin_type_error ctx "length" [v] (Some ret_ctyp)
 
 let builtin_vector_subrange ctx vec i j ret_ctyp =
-  match cval_ctyp vec, cval_ctyp i, cval_ctyp j with
-  | CT_fbits (n, _), CT_constant i, CT_constant j ->
+  match cval_ctyp vec, cval_ctyp i, cval_ctyp j, ret_ctyp with
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits _ ->
      Extract (Big_int.to_int i, Big_int.to_int j, smt_cval ctx vec)
 
-  | CT_lbits _, CT_constant i, CT_constant j ->
+  | CT_lbits _, CT_constant i, CT_constant j, CT_fbits _ ->
      Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec]))
 
+  | CT_fbits (n, _), i_ctyp, CT_constant j, CT_lbits _ when Big_int.equal j Big_int.zero ->
+     let len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
+     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx vec)])])
+
   | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp)
 
 let builtin_vector_access ctx vec i ret_ctyp =
   match cval_ctyp vec, cval_ctyp i, ret_ctyp with
   | CT_fbits (n, _), CT_constant i, CT_bit ->
      Extract (Big_int.to_int i, Big_int.to_int i, smt_cval ctx vec)
+  | CT_lbits _, CT_constant i, CT_bit ->
+     Extract (Big_int.to_int i, Big_int.to_int i, Fn ("contents", [smt_cval ctx vec]))
+
+  | CT_lbits _, i_ctyp, CT_bit ->
+     let shift = force_size ~checked:false ctx (lbits_size ctx) (int_size ctx i_ctyp) (smt_cval ctx i) in
+     Extract (0, 0, Fn ("bvlshr", [Fn ("contents", [smt_cval ctx vec]); shift]))
 
   | CT_vector _, CT_constant i, _ ->
      Fn ("select", [smt_cval ctx vec; bvint !vector_index i])
@@ -787,6 +844,21 @@ let builtin_vector_update ctx vec i x ret_ctyp =
 
   | _ -> builtin_type_error ctx "vector_update" [vec; i; x] (Some ret_ctyp)
 
+let builtin_vector_update_subrange ctx vec i j x ret_ctyp =
+  match cval_ctyp vec, cval_ctyp i, cval_ctyp j, cval_ctyp x, ret_ctyp with
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j >= 0 ->
+     assert (n = m);
+     let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
+     let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
+     Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])])
+
+  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j >= 0 ->
+     assert (n = m);
+     let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
+     Fn ("concat", [smt_cval ctx x; bot])
+
+  | _ -> builtin_type_error ctx "vector_update_subrange" [vec; i; j; x] (Some ret_ctyp)
+
 let builtin_unsigned ctx v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
   | CT_fbits (n, _), CT_fint m when m > n ->
@@ -800,6 +872,9 @@ let builtin_unsigned ctx v ret_ctyp =
        let smt = smt_cval ctx v in
        Fn ("concat", [bvzero (ctx.lint_size - n); smt])
 
+  | CT_lbits _, CT_lint ->
+     Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v]))
+
   | ctyp, _ -> builtin_type_error ctx "unsigned" [v] (Some ret_ctyp)
 
 let builtin_signed ctx v ret_ctyp =
@@ -810,6 +885,9 @@ let builtin_signed ctx v ret_ctyp =
   | CT_fbits (n, _), CT_lint ->
      SignExtend(ctx.lint_size - n, smt_cval ctx v)
 
+  | CT_lbits _, CT_lint ->
+     Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v]))
+    
   | ctyp, _ -> builtin_type_error ctx "signed" [v] (Some ret_ctyp)
 
 let builtin_add_bits ctx v1 v2 ret_ctyp =
@@ -818,6 +896,11 @@ let builtin_add_bits ctx v1 v2 ret_ctyp =
      assert (n = m && m = o);
      Fn ("bvadd", [smt_cval ctx v1; smt_cval ctx v2])
 
+  | CT_lbits _, CT_lbits _, CT_lbits _ ->
+     let smt1 = smt_cval ctx v1 in
+     let smt2 = smt_cval ctx v2 in
+     Fn ("Bits", [Fn ("len", [smt1]); Fn ("bvadd", [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])
+     
   | _ -> builtin_type_error ctx "add_bits" [v1; v2] (Some ret_ctyp)
 
 let builtin_sub_bits ctx v1 v2 ret_ctyp =
@@ -866,6 +949,13 @@ let builtin_replicate_bits ctx v1 v2 ret_ctyp =
      let c = m / n in
      Fn ("concat", List.init c (fun _ -> smt))
 
+  | CT_fbits (n, _), v2_ctyp, CT_lbits _ ->
+     let times = (lbits_size ctx / n) + 1 in
+     let len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx v2_ctyp) (smt_cval ctx v2) in
+     let smt1 = smt_cval ctx v1 in
+     let contents = Extract (lbits_size ctx - 1, 0, Fn ("concat", List.init times (fun _ -> smt1))) in
+     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])])
+
   | _ -> builtin_type_error ctx "replicate_bits" [v1; v2] (Some ret_ctyp)
 
 let builtin_sail_truncate ctx v1 v2 ret_ctyp =
@@ -928,13 +1018,18 @@ let builtin_get_slice_int ctx v1 v2 v3 ret_ctyp =
      in
      Extract ((start + len) - 1, start, smt)
 
+  | CT_lint, CT_lint, CT_constant start, CT_lbits _ when Big_int.equal start Big_int.zero ->
+     let len = Extract (ctx.lbits_index - 1, 0, smt_cval ctx v1) in
+     let contents = unsigned_size ~checked:false ctx (lbits_size ctx) ctx.lint_size (smt_cval ctx v2) in
+     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])])
+
   | _ -> builtin_type_error ctx "get_slice_int" [v1; v2; v3] (Some ret_ctyp)
 
 let builtin_count_leading_zeros ctx v ret_ctyp =
   let ret_sz = int_size ctx ret_ctyp in
   let rec lzcnt sz smt =
     if sz == 1 then
-      Ite (Fn ("=", [Extract (0, 0, smt); Bin "0"]),
+      Ite (Fn ("=", [Extract (0, 0, smt); Bitvec_lit [Sail2_values.B0]]),
            bvint ret_sz (Big_int.of_int 1),
            bvint ret_sz (Big_int.zero))
     else (
@@ -1050,6 +1145,8 @@ let smt_builtin ctx name args ret_ctyp =
   | "max_int", [v1; v2], _ -> builtin_max_int ctx v1 v2 ret_ctyp
   | "min_int", [v1; v2], _ -> builtin_min_int ctx v1 v2 ret_ctyp
 
+  | "ediv_int", [v1; v2], _ -> builtin_tdiv_int ctx v1 v2 ret_ctyp
+                            
   (* All signed and unsigned bitvector comparisons *)
   | "slt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvslt" ctx v1 v2 ret_ctyp
   | "ult_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvult" ctx v1 v2 ret_ctyp
@@ -1072,8 +1169,9 @@ let smt_builtin ctx name args ret_ctyp =
   | "sail_truncateLSB", [v1; v2], _ -> builtin_sail_truncateLSB ctx v1 v2 ret_ctyp
   | "shiftl", [v1; v2], _ -> builtin_shift "bvshl" ctx v1 v2 ret_ctyp
   | "shiftr", [v1; v2], _ -> builtin_shift "bvlshr" ctx v1 v2 ret_ctyp
-  | "or_bits", [v1; v2], _ -> builtin_or_bits ctx v1 v2 ret_ctyp
   | "and_bits", [v1; v2], _ -> builtin_and_bits ctx v1 v2 ret_ctyp
+  | "or_bits", [v1; v2], _ -> builtin_or_bits ctx v1 v2 ret_ctyp
+  | "xor_bits", [v1; v2], _ -> builtin_xor_bits ctx v1 v2 ret_ctyp
   | "not_bits", [v], _ -> builtin_not_bits ctx v ret_ctyp
   | "add_bits", [v1; v2], _ -> builtin_add_bits ctx v1 v2 ret_ctyp
   | "add_bits_int", [v1; v2], _ -> builtin_add_bits_int ctx v1 v2 ret_ctyp
@@ -1084,6 +1182,7 @@ let smt_builtin ctx name args ret_ctyp =
   | "vector_access", [v1; v2], ret_ctyp -> builtin_vector_access ctx v1 v2 ret_ctyp
   | "vector_subrange", [v1; v2; v3], ret_ctyp -> builtin_vector_subrange ctx v1 v2 v3 ret_ctyp
   | "vector_update", [v1; v2; v3], ret_ctyp -> builtin_vector_update ctx v1 v2 v3 ret_ctyp
+  | "vector_update_subrange", [v1; v2; v3; v4], ret_ctyp -> builtin_vector_update_subrange ctx v1 v2 v3 v4 ret_ctyp
   | "sail_unsigned", [v], ret_ctyp -> builtin_unsigned ctx v ret_ctyp
   | "sail_signed", [v], ret_ctyp -> builtin_signed ctx v ret_ctyp
   | "replicate_bits", [v1; v2], ret_ctyp -> builtin_replicate_bits ctx v1 v2 ret_ctyp
@@ -1110,16 +1209,30 @@ let smt_builtin ctx name args ret_ctyp =
   | "lteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<=", [smt_cval ctx v1; smt_cval ctx v2])
   | "gteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn (">=", [smt_cval ctx v1; smt_cval ctx v2])
 
-  | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
+  | _ ->
+     Reporting.unreachable ctx.pragma_l __POS__ ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
+
+let loc_doc = function
+  | Parse_ast.Documented (str, l) -> str
+  | _ -> "UNKNOWN"
 
 (* Memory reads and writes as defined in lib/regfp.sail *)
 let writes = ref (-1)
 
-let builtin_write_mem ctx wk addr_size addr data_size data =
+let builtin_write_mem l ctx wk addr_size addr data_size data =
   incr writes;
   let name = "W" ^ string_of_int !writes in
-  [Write_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
-              smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
+  [Write_mem {
+       name = name;
+       node = ctx.node;
+       active = Lazy.force ctx.pathcond;
+       kind = smt_cval ctx wk;
+       addr = smt_cval ctx addr;
+       addr_type = smt_ctyp ctx (cval_ctyp addr);
+       data = smt_cval ctx data;
+       data_type = smt_ctyp ctx (cval_ctyp data);
+       doc = loc_doc l
+  }],
   Var (name ^ "_ret")
 
 let ea_writes = ref (-1)
@@ -1133,11 +1246,19 @@ let builtin_write_mem_ea ctx wk addr_size addr data_size =
 
 let reads = ref (-1)
 
-let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
+let builtin_read_mem l ctx rk addr_size addr data_size ret_ctyp =
   incr reads;
   let name = "R" ^ string_of_int !reads in
-  [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk,
-             smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
+  [Read_mem {
+       name = name;
+       node = ctx.node;
+       active = Lazy.force ctx.pathcond;
+       ret_type = smt_ctyp ctx ret_ctyp;
+       kind = smt_cval ctx rk;
+       addr = smt_cval ctx addr;
+       addr_type = smt_ctyp ctx (cval_ctyp addr);
+       doc = loc_doc l
+  }],
   Read_res name
 
 let excl_results = ref (-1)
@@ -1150,26 +1271,51 @@ let builtin_excl_res ctx =
 
 let barriers = ref (-1)
 
-let builtin_barrier ctx bk =
+let builtin_barrier l ctx bk =
   incr barriers;
   let name = "B" ^ string_of_int !barriers in
-  [Barrier (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx bk)],
+  [Barrier {
+       name = name;
+       node = ctx.node;
+       active = Lazy.force ctx.pathcond;
+       kind = smt_cval ctx bk;
+       doc = loc_doc l
+  }],
   Enum "unit"
 
-let rec smt_conversion ctx from_ctyp to_ctyp x =
-  match from_ctyp, to_ctyp with
-  | _, _ when ctyp_equal from_ctyp to_ctyp -> x
-  | CT_constant c, CT_fint sz ->
-     bvint sz c
-  | CT_constant c, CT_lint ->
-     bvint ctx.lint_size c
-  | CT_fint sz, CT_lint ->
-     force_size ctx ctx.lint_size sz x
-  | CT_lbits _, CT_fbits (n, _) ->
-     unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
-  | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))
+let cache_maintenances = ref (-1)
+
+let builtin_cache_maintenance l ctx cmk addr_size addr =
+  incr cache_maintenances;
+  let name = "M" ^ string_of_int !cache_maintenances in
+  [Cache_maintenance {
+       name = name;
+       node = ctx.node;
+       active = Lazy.force ctx.pathcond;
+       kind = smt_cval ctx cmk;
+       addr = smt_cval ctx addr;
+       addr_type = smt_ctyp ctx (cval_ctyp addr);
+       doc = loc_doc l
+  }],
+  Enum "unit"
+
+let branch_announces = ref (-1)
+
+let builtin_branch_announce l ctx addr_size addr =
+  incr branch_announces;
+  let name = "C" ^ string_of_int !branch_announces in
+  [Branch_announce {
+       name = name;
+       node = ctx.node;
+       active = Lazy.force ctx.pathcond;
+       addr = smt_cval ctx addr;
+       addr_type = smt_ctyp ctx (cval_ctyp addr);
+       doc = loc_doc l
+  }],
+  Enum "unit"
 
 let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp)
+let preserve_const ctx id ctyp exp = Preserve_const (string_of_id id, smt_ctyp ctx ctyp, exp)
 let declare_const ctx id ctyp = Declare_const (zencode_name id, smt_ctyp ctx ctyp)
 
 let smt_ctype_def ctx = function
@@ -1339,7 +1485,10 @@ let c_literals ctx =
   in
   map_aval c_literal
 
-let unroll_foreach ctx = function
+(* If we know the loop variables exactly (especially after
+   specialization), we can unroll the exact number of times required,
+   and omit any comparisons. *)
+let unroll_static_foreach ctx = function
   | AE_aux (AE_for (id, from_aexp, to_aexp, by_aexp, order, body), env, l) as aexp ->
      begin match ctyp_of_typ ctx (aexp_typ from_aexp), ctyp_of_typ ctx (aexp_typ to_aexp), ctyp_of_typ ctx (aexp_typ by_aexp), order with
      | CT_constant f, CT_constant t, CT_constant b, Ord_aux (Ord_inc, _) ->
@@ -1414,7 +1563,7 @@ let smt_ssanode ctx cfg preds =
          pis ids None
      in
      match mux with
-     | None -> []
+     | None -> assert false
      | Some mux ->
         [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
 
@@ -1492,7 +1641,7 @@ let rec rmw_write = function
   | CL_id _ -> assert false
   | CL_tuple (clexp, _) -> rmw_write clexp
   | CL_field (clexp, _) -> rmw_write clexp
-  | clexp -> assert false
+  | clexp -> failwith "Could not understand l-expression"
 
 let rmw_read = function
   | CL_rmw (read, _, _) -> zencode_name read
@@ -1522,7 +1671,7 @@ let rmw_modify smt = function
           if UId.compare field field' = 0 then
             smt
           else
-            Fn (zencode_upper_id struct_id ^ "_" ^ zencode_uid field', [Var (rmw_read clexp)])
+            Field (zencode_upper_id struct_id ^ "_" ^ zencode_uid field', Var (rmw_read clexp))
         in
         Fn (zencode_upper_id struct_id, List.map set_field fields)
      | _ ->
@@ -1564,7 +1713,7 @@ let smt_instr ctx =
        else if name = "platform_write_mem" then
          begin match args with
          | [wk; addr_size; addr; data_size; data] ->
-            let mem_event, var = builtin_write_mem ctx wk addr_size addr data_size data in
+            let mem_event, var = builtin_write_mem l ctx wk addr_size addr data_size data in
             mem_event @ [define_const ctx id ret_ctyp var]
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for __write_mem"
@@ -1580,7 +1729,7 @@ let smt_instr ctx =
        else if name = "platform_read_mem" then
          begin match args with
          | [rk; addr_size; addr; data_size] ->
-            let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in
+            let mem_event, var = builtin_read_mem l ctx rk addr_size addr data_size ret_ctyp in
             mem_event @ [define_const ctx id ret_ctyp var]
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for __read_mem"
@@ -1588,7 +1737,23 @@ let smt_instr ctx =
        else if name = "platform_barrier" then
          begin match args with
          | [bk] ->
-            let mem_event, var = builtin_barrier ctx bk in
+            let mem_event, var = builtin_barrier l ctx bk in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __barrier"
+         end
+       else if name = "platform_cache_maintenance" then
+         begin match args with
+         | [cmk; addr_size; addr] ->
+            let mem_event, var = builtin_cache_maintenance l ctx cmk addr_size addr in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __barrier"
+         end
+       else if name = "platform_branch_announce" then
+         begin match args with
+         | [addr_size; addr] ->
+            let mem_event, var = builtin_branch_announce l ctx addr_size addr in
             mem_event @ [define_const ctx id ret_ctyp var]
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for __barrier"
@@ -1601,9 +1766,20 @@ let smt_instr ctx =
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for __excl_res"
          end
+       else if name = "sail_exit" then
+         (add_event ctx Assertion (Bool_lit false); [])
+       else if name = "sail_assert" then
+         begin match args with
+         | [assertion; _] ->
+            let smt = smt_cval ctx assertion in
+            add_event ctx Assertion (Fn ("not", [smt]));
+            []
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for assertion"
+         end
        else
          let value = smt_builtin ctx name args ret_ctyp in
-         [define_const ctx id ret_ctyp value]
+         [define_const ctx id ret_ctyp (Syntactic (value, List.map (smt_cval ctx) args))]
      else if extern && string_of_id (fst function_id) = "internal_vector_init" then
        [declare_const ctx id ret_ctyp]
      else if extern && string_of_id (fst function_id) = "internal_vector_update" then
@@ -1615,15 +1791,6 @@ let smt_instr ctx =
        | _ ->
           Reporting.unreachable l __POS__ "Bad arguments for internal_vector_update"
        end
-     else if string_of_id (fst function_id) = "sail_assert" then
-       begin match args with
-       | [assertion; _] ->
-          let smt = smt_cval ctx assertion in
-          add_event ctx Assertion smt;
-          []
-       | _ ->
-          Reporting.unreachable l __POS__ "Bad arguments for assertion"
-       end
      else if string_of_id (fst function_id) = "sail_assume" then
        begin match args with
        | [assumption] ->
@@ -1643,8 +1810,14 @@ let smt_instr ctx =
      Reporting.unreachable l __POS__ "Register reference write should be re-written by now"
 
   | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) ->
-     [define_const ctx id ctyp
-        (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
+     begin match id with
+     | Name (id, _) when IdSet.mem id ctx.preserved ->
+        [preserve_const ctx id ctyp
+           (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
+     | _ ->
+        [define_const ctx id ctyp
+           (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
+     end
 
   | I_aux (I_copy (clexp, cval), _) ->
      let smt = smt_cval ctx cval in
@@ -1721,13 +1894,19 @@ module Make_optimizer(S : Sequence) = struct
          | Some n -> Hashtbl.replace uses var (n + 1)
          | None -> Hashtbl.add uses var 1
          end
-      | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
+      | Syntactic (exp, _) -> uses_in_exp exp
+      | Shared _ | Enum _ | Read_res _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
       | Fn (_, exps) | Ctor (_, exps) ->
          List.iter uses_in_exp exps
+      | Field (_, exp) ->
+         uses_in_exp exp
+      | Struct (_, fields) ->
+         List.iter (fun (_, exp) -> uses_in_exp exp) fields
       | Ite (cond, t, e) ->
          uses_in_exp cond; uses_in_exp t; uses_in_exp e
       | Extract (_, _, exp) | Tester (_, exp) | SignExtend (_, exp) ->
          uses_in_exp exp
+      | Forall _ -> assert false
     in
 
     let remove_unused () = function
@@ -1737,6 +1916,11 @@ module Make_optimizer(S : Sequence) = struct
          | Some _ ->
             Stack.push def stack'
          end
+      | Declare_fun _ as def ->
+         Stack.push def stack'
+      | Preserve_const (_, _, exp) as def ->
+         uses_in_exp exp;
+         Stack.push def stack'
       | Define_const (var, _, exp) as def ->
          begin match Hashtbl.find_opt uses var with
          | None -> ()
@@ -1746,17 +1930,23 @@ module Make_optimizer(S : Sequence) = struct
          end
       | (Declare_datatypes _ | Declare_tuple _) as def ->
          Stack.push def stack'
-      | Write_mem (_, _, active, wk, addr, _, data, _) as def ->
-         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
+      | Write_mem w as def ->
+         uses_in_exp w.active; uses_in_exp w.kind; uses_in_exp w.addr; uses_in_exp w.data;
          Stack.push def stack'
       | Write_mem_ea (_, _, active, wk, addr, _, data_size, _) as def ->
          uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size;
          Stack.push def stack'
-      | Read_mem (_, _, active, _, rk, addr, _) as def ->
-         uses_in_exp active; uses_in_exp rk; uses_in_exp addr;
+      | Read_mem r as def ->
+         uses_in_exp r.active; uses_in_exp r.kind; uses_in_exp r.addr;
          Stack.push def stack'
-      | Barrier (_, _, active, bk) as def ->
-         uses_in_exp active; uses_in_exp bk;
+      | Barrier b as def ->
+         uses_in_exp b.active; uses_in_exp b.kind;
+         Stack.push def stack'
+      | Cache_maintenance m as def ->
+         uses_in_exp m.active; uses_in_exp m.kind; uses_in_exp m.addr;
+         Stack.push def stack'
+      | Branch_announce c as def ->
+         uses_in_exp c.active; uses_in_exp c.addr;
          Stack.push def stack'
       | Excl_res (_, _, active) as def ->
          uses_in_exp active;
@@ -1775,10 +1965,14 @@ module Make_optimizer(S : Sequence) = struct
     let constant_propagate = function
       | Declare_const _ as def ->
          S.add def seq
+      | Declare_fun _ as def ->
+         S.add def seq
+      | Preserve_const (var, typ, exp) ->
+         S.add (Preserve_const (var, typ, simp_smt_exp vars kinds exp)) seq
       | Define_const (var, typ, exp) ->
          let exp = simp_smt_exp vars kinds exp in
          begin match Hashtbl.find_opt uses var, simp_smt_exp vars kinds exp with
-         | _, (Bin _ | Bool_lit _) ->
+         | _, (Bitvec_lit _ | Bool_lit _) ->
             Hashtbl.add vars var exp
          | _, Var _ when !opt_propagate_vars ->
             Hashtbl.add vars var exp
@@ -1791,20 +1985,30 @@ module Make_optimizer(S : Sequence) = struct
             S.add (Define_const (var, typ, exp)) seq
          | None, _ -> assert false
          end
-      | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
-         S.add (Write_mem (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
-                           simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data, data_ty))
+      | Write_mem w ->
+         S.add (Write_mem { w with active = simp_smt_exp vars kinds w.active;
+                                   kind = simp_smt_exp vars kinds w.kind;
+                                   addr = simp_smt_exp vars kinds w.addr;
+                                   data = simp_smt_exp vars kinds w.data })
                seq
       | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
          S.add (Write_mem_ea (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
                               simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data_size, data_size_ty))
                seq
-      | Read_mem (name, node, active, typ, rk, addr, addr_typ) ->
-         S.add (Read_mem (name, node, simp_smt_exp vars kinds active, typ, simp_smt_exp vars kinds rk,
-                          simp_smt_exp vars kinds addr, addr_typ))
+      | Read_mem r ->
+         S.add (Read_mem { r with active = simp_smt_exp vars kinds r.active;
+                                  kind = simp_smt_exp vars kinds r.kind;
+                                  addr = simp_smt_exp vars kinds r.addr })
                seq
-      | Barrier (name, node, active, bk) ->
-         S.add (Barrier (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds bk)) seq
+      | Barrier b ->
+         S.add (Barrier { b with active = simp_smt_exp vars kinds b.active; kind = simp_smt_exp vars kinds b.kind }) seq
+      | Cache_maintenance m ->
+         S.add (Cache_maintenance { m with active = simp_smt_exp vars kinds m.active;
+                                           kind = simp_smt_exp vars kinds m.kind;
+                                           addr = simp_smt_exp vars kinds m.addr })
+               seq
+      | Branch_announce c ->
+         S.add (Branch_announce { c with active = simp_smt_exp vars kinds c.active; addr = simp_smt_exp vars kinds c.addr }) seq
       | Excl_res (name, node, active) ->
          S.add (Excl_res (name, node, simp_smt_exp vars kinds active)) seq
       | Assert exp ->
@@ -1843,6 +2047,26 @@ let smt_header ctx cdefs =
    register if it is. We also do a similar thing for *r = x
 *)
 let expand_reg_deref env register_map = function
+  | I_aux (I_funcall (CL_addr (CL_id (id, ctyp)), false, function_id, args), (_, l)) ->
+     begin match ctyp with
+     | CT_ref reg_ctyp ->
+        begin match CTMap.find_opt reg_ctyp register_map with
+        | Some regs ->
+           let end_label = label "end_reg_write_" in
+           let try_reg r =
+             let next_label = label "next_reg_write_" in
+             [ijump (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
+              ifuncall (CL_id (name r, reg_ctyp)) function_id args;
+              igoto end_label;
+              ilabel next_label]
+           in
+           iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])
+        | None ->
+           raise (Reporting.err_general l ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp))
+        end
+     | _ ->
+        raise (Reporting.err_general l "Register reference assignment must take a register reference as an argument")
+     end
   | I_aux (I_funcall (clexp, false, function_id, [reg_ref]), (_, l)) as instr ->
      let open Type_check in
      begin match (if Env.is_extern (fst function_id) env "smt" then Some (Env.get_extern (fst function_id) env "smt") else None) with
@@ -1855,7 +2079,7 @@ let expand_reg_deref env register_map = function
               let end_label = label "end_reg_deref_" in
               let try_reg r =
                 let next_label = label "next_reg_deref_" in
-                [ijump (V_call (Neq, [V_ref (name r, reg_ctyp); reg_ref])) next_label;
+                [ijump (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label;
                  icopy l clexp (V_id (name r, reg_ctyp));
                  igoto end_label;
                  ilabel next_label]
@@ -1877,7 +2101,7 @@ let expand_reg_deref env register_map = function
            let end_label = label "end_reg_write_" in
            let try_reg r =
              let next_label = label "next_reg_write_" in
-             [ijump (V_call (Neq, [V_ref (name r, reg_ctyp); V_id (id, ctyp)])) next_label;
+             [ijump (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
               icopy l (CL_id (name r, reg_ctyp)) cval;
               igoto end_label;
               ilabel next_label]
@@ -1927,7 +2151,7 @@ let smt_instr_list name ctx all_cdefs instrs =
     dump_graph name cfg;
 
   List.iter (fun n ->
-      begin match get_vertex cfg n with
+      match get_vertex cfg n with
       | None -> ()
       | Some ((ssa_elems, cfnode), preds, succs) ->
          let muxers =
@@ -1937,10 +2161,9 @@ let smt_instr_list name ctx all_cdefs instrs =
          let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in
          push_smt_defs stack muxers;
          push_smt_defs stack basic_block
-      end
     ) visit_order;
 
-  stack, cfg
+  stack, start, cfg
 
 let smt_cdef props lets name_file ctx all_cdefs = function
   | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
@@ -1967,7 +2190,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           |> remove_pointless_goto
         in
 
-        let stack, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
+        let stack, _, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
 
         let query = smt_query ctx pragma.query in
         push_smt_defs stack [Assert (Fn ("not", [query]))];
@@ -2038,25 +2261,30 @@ let rec build_register_map rmap = function
   | [] -> rmap
 
 let compile env ast =
-  let cdefs =
+  let cdefs, jib_ctx =
     let open Jib_compile in
-    let ctx =
-      initial_ctx
-        ~convert_typ:ctyp_of_typ
-        ~optimize_anf:(fun ctx aexp -> fold_aexp (unroll_foreach ctx) (c_literals ctx aexp))
-        env
+    let optimize_anf ctx aexp =
+      aexp
+      |> c_literals ctx
+      |> fold_aexp (unroll_static_foreach ctx)
     in
+    let ctx = initial_ctx ~convert_typ:ctyp_of_typ ~optimize_anf:optimize_anf env in
     let t = Profile.start () in
-    let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true; use_real = true } ast in
+    let cdefs, ctx =
+      compile_ast { ctx with specialize_calls = true;
+                             ignore_64 = true;
+                             unroll_loops = Some !opt_unroll_limit;
+                             struct_value = true;
+                             use_real = true } ast in
     Profile.finish "Compiling to Jib IR" t;
-    cdefs
+    cdefs, ctx
   in
   let cdefs = Jib_optimize.unique_per_function_ids cdefs in
   let rmap = build_register_map CTMap.empty cdefs in
-  cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap; ast = ast }
+  cdefs, jib_ctx, { (initial_ctx ()) with tc_env = jib_ctx.tc_env; register_map = rmap; ast = ast }
 
 let serialize_smt_model file env ast =
-  let cdefs, ctx = compile env ast in
+  let cdefs, _, ctx = compile env ast in
   let out_chan = open_out file in
   Marshal.to_channel out_chan cdefs [];
   Marshal.to_channel out_chan (Type_check.Env.set_prover None ctx.tc_env) [];
@@ -2073,7 +2301,7 @@ let deserialize_smt_model file =
 
 let generate_smt props name_file env ast =
   try
-    let cdefs, ctx = compile env ast in
+    let cdefs, _, ctx = compile env ast in
     smt_cdefs props [] name_file ctx cdefs cdefs
   with
   | Type_check.Type_error (_, l, err) ->
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index cdaf7e39..616877e4 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -73,44 +73,57 @@ val opt_default_lbits_index : int ref
 val opt_default_vector_index : int ref
 
 type ctx = {
-    (** Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
     lbits_index : int;
-    (** The size we use for integers where we don't know how large they are statically. *)
+    (** Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
     lint_size : int;
+    (** The size we use for integers where we don't know how large they are statically. *)
+    vector_index : int;
     (** A generic vector, vector('a) becomes Array (BitVec vector_index) 'a.
        We need to take care that vector_index is large enough for all generic vectors. *)
-    vector_index : int;
-    (** A map from each ctyp to a list of registers of that ctyp *)
     register_map : id list CTMap.t;
-    (** A set to keep track of all the tuple sizes we need to generate types for *)
+    (** A map from each ctyp to a list of registers of that ctyp *)
     tuple_sizes : IntSet.t ref;
-    (** tc_env is the global type-checking environment *)
+    (** A set to keep track of all the tuple sizes we need to generate types for *)
     tc_env : Type_check.Env.t;
+    (** tc_env is the global type-checking environment *)
+    pragma_l : Ast.l;
     (** A location, usually the $counterexample or $property we are
        generating the SMT for. Used for error messages. *)
-    pragma_l : Ast.l;
-    (** Used internally to keep track of function argument names *)
     arg_stack : (int * string) Stack.t;
-    (** The fully type-checked ast *)
+    (** Used internally to keep track of function argument names *)
     ast : Type_check.tannot defs;
+    (** The fully type-checked ast *)
+    shared : ctyp Bindings.t;
+    (** Shared variables. These variables do not get renamed by
+       Smtlib.suffix_variables_def, and their SSA number is
+       omitted. They should therefore only ever be read and never
+       written. Used by sail-axiomatic for symbolic values in the
+       initial litmus state. *)
+    preserved : IdSet.t;
+    (** icopy instructions to an id in preserved will generated a
+       define-const (by using Smtlib.Preserved_const) that will not be
+       simplified away or renamed. It will also not get a SSA
+       number. Such variables can therefore only ever be written to
+       once, and never read. They are used by sail-axiomatic to
+       extract information from the generated SMT. *)
+    events : smt_exp Stack.t EventMap.t ref;
     (** For every event type we have a stack of boolean SMT
        expressions for each occurance of that event. See
        src/property.ml for the event types *)
-    events : smt_exp Stack.t EventMap.t ref;
+    node : int;
+    pathcond : smt_exp Lazy.t;
     (** When generating SMT for an instruction pathcond will contain
        the global path conditional of the containing block/node in the
        control flow graph *)
-    node : int;
-    pathcond : smt_exp Lazy.t;
+    use_string : bool ref;
+    use_real : bool ref
     (** Set if we need to use strings or real numbers in the generated
        SMT, which then requires set-logic ALL or similar depending on
        the solver *)
-    use_string : bool ref;
-    use_real : bool ref
   }
 
 (** Compile an AST into Jib suitable for SMT generation, and initialise a context. *)
-val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx
+val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * Jib_compile.ctx * ctx
 
 (* TODO: Currently we internally use mutable stacks and queues to
    avoid any issues with stack overflows caused by some non
@@ -122,7 +135,7 @@ val smt_header : ctx -> cdef list -> smt_def list
 
 val smt_query : ctx -> Property.query -> smt_exp
 
-val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * (ssa_elem list * cf_node) Jib_ssa.array_graph
+val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * int * (ssa_elem list * cf_node) Jib_ssa.array_graph
 
 module type Sequence = sig
   type 'a t
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index 02e70e29..bf49a383 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -192,7 +192,7 @@ let fuzz_cdef ctx all_cdefs = function
                    @ [iend ()]
                  in
                  let smt_defs =
-                   try fst (smt_instr_list extern ctx all_cdefs jib) with
+                   try (fun (x, _, _) -> x) (smt_instr_list extern ctx all_cdefs jib) with
                    | _ ->
                       raise (Skip_iteration ("SMT error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
                  in
@@ -253,6 +253,6 @@ let fuzz_cdef ctx all_cdefs = function
 let fuzz seed env ast =
   Random.init seed;
 
-  let cdefs, ctx = compile env ast in
+  let cdefs, _, ctx = compile env ast in
 
   List.iter (fuzz_cdef ctx cdefs) cdefs
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9c405a48..b971c1fa 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -524,9 +524,6 @@ let rename_variables graph root children =
     | V_id (id, ctyp) ->
        let i = top_stack id in
        V_id (ssa_name i id, ctyp)
-    | V_ref (id, ctyp) ->
-       let i = top_stack id in
-       V_ref (ssa_name i id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_call (id, fs) -> V_call (id, List.map fold_cval fs)
     | V_field (f, field) -> V_field (fold_cval f, field)
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index bec4ce75..821cdabc 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -167,8 +167,6 @@ let name id = Name (id, -1)
 let rec cval_rename from_id to_id = function
   | V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp)
   | V_id (id, ctyp) -> V_id (id, ctyp)
-  | V_ref (id, ctyp) when Name.compare id from_id = 0 -> V_ref (to_id, ctyp)
-  | V_ref (id, ctyp) -> V_ref (id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (call, cvals) -> V_call (call, List.map (cval_rename from_id to_id) cvals)
   | V_field (f, field) -> V_field (cval_rename from_id to_id f, field)
@@ -351,24 +349,28 @@ and full_string_of_ctyp = function
   | CT_ref ctyp -> "ref(" ^ full_string_of_ctyp ctyp ^ ")"
   | ctyp -> string_of_ctyp ctyp
 
-let string_of_value = function
-  | VL_bits ([], _) -> "empty"
-  | VL_bits (bs, true) -> Sail2_values.show_bitlist bs
-  | VL_bits (bs, false) -> Sail2_values.show_bitlist (List.rev bs)
-  | VL_int i -> Big_int.to_string i
+let rec string_of_value = function
+  | VL_bits ([], _) -> "UINT64_C(0)"
+  | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
+  | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
+  | VL_int i -> Big_int.to_string i ^ "l"
   | VL_bool true -> "true"
   | VL_bool false -> "false"
-  | VL_null -> "NULL"
-  | VL_unit -> "()"
-  | VL_bit Sail2_values.B0 -> "bitzero"
-  | VL_bit Sail2_values.B1 -> "bitone"
-  | VL_bit Sail2_values.BU -> "bitundef"
+  | VL_unit -> "UNIT"
+  | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
+  | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
+  | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
+  | VL_matcher (n, uid) -> Printf.sprintf "matcher(%d, %d)" n uid
+  | VL_tuple values -> "(" ^ Util.string_of_list ", " string_of_value values ^ ")"
+  | VL_list [] -> "NULL"
+  | VL_list values -> "[|" ^ Util.string_of_list ", " string_of_value values ^ "|]"
+  | VL_enum element -> Util.zencode_string element
+  | VL_ref r -> "&" ^ Util.zencode_string r
 
 let rec string_of_cval = function
   | V_id (id, ctyp) -> string_of_name id
-  | V_ref (id, _) -> "&" ^ string_of_name id
   | V_lit (vl, ctyp) -> string_of_value vl
   | V_call (op, cvals) ->
      Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals)
@@ -585,7 +587,7 @@ let rec is_polymorphic = function
   | CT_poly -> true
 
 let rec cval_deps = function
-  | V_id (id, _) | V_ref (id, _) -> NameSet.singleton id
+  | V_id (id, _) -> NameSet.singleton id
   | V_lit _ -> NameSet.empty
   | V_field (cval, _) | V_poly (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval
   | V_call (_, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals)
@@ -659,7 +661,6 @@ let rec map_clexp_ctyp f = function
 
 let rec map_cval_ctyp f = function
   | V_id (id, ctyp) -> V_id (id, f ctyp)
-  | V_ref (id, ctyp) -> V_ref (id, f ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, f ctyp)
   | V_ctor_kind (cval, id, unifiers, ctyp) ->
      V_ctor_kind (map_cval_ctyp f cval, id, List.map f unifiers, f ctyp)
@@ -893,7 +894,6 @@ let rec infer_call op vs =
 
 and cval_ctyp = function
   | V_id (_, ctyp) -> ctyp
-  | V_ref (_, ctyp) -> CT_ref ctyp
   | V_lit (vl, ctyp) -> ctyp
   | V_ctor_kind _ -> CT_bool
   | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> ctyp
diff --git a/src/property.ml b/src/property.ml
index 955e755d..83594f4f 100644
--- a/src/property.ml
+++ b/src/property.ml
@@ -132,7 +132,7 @@ type query =
    | Q_or of query list
 
 let default_query =
-  Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow; Q_not (Q_all Assumption)]
+  Q_or [Q_and [Q_not (Q_exist Assertion); Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow; Q_not (Q_all Assumption)]
 
 module Event = struct
   type t = event
diff --git a/src/sail.ml b/src/sail.ml
index 0656aefa..c5b8e6ac 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -511,7 +511,7 @@ let target name out_name ast type_envs =
   | Some "smt" when !opt_smt_serialize ->
      let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
      let ast_smt, type_envs = Specialize.(specialize_passes 2 int_specialization_with_externs type_envs ast_smt) in
-     let jib, ctx = Jib_smt.compile type_envs ast_smt in
+     let jib, _, ctx = Jib_smt.compile type_envs ast_smt in
      let name_file =
        match !opt_file_out with
        | Some f -> f ^ ".smt_model"
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 06386f61..e12657c3 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -60,6 +60,30 @@ type smt_typ =
   | Tuple of smt_typ list
   | Array of smt_typ * smt_typ
 
+let rec smt_typ_compare t1 t2 =
+  match t1, t2 with
+  | Bitvec n, Bitvec m -> compare n m
+  | Bool, Bool -> 0
+  | String, String -> 0
+  | Real, Real -> 0
+  | Datatype (name1, _), Datatype (name2, _) -> String.compare name1 name2
+  | Tuple ts1, Tuple ts2 -> Util.lex_ord_list smt_typ_compare ts1 ts2
+  | Array (t11, t12), Array (t21, t22) ->
+     let c = smt_typ_compare t11 t21 in
+     if c = 0 then smt_typ_compare t12 t22 else c
+  | Bitvec _, _ -> 1
+  | _, Bitvec _ -> -1
+  | Bool, _ -> 1
+  | _, Bool -> -1
+  | String, _ -> 1
+  | _, String -> -1
+  | Real, _ -> 1
+  | _, Real -> -1
+  | Datatype _, _ -> 1
+  | _, Datatype _ -> -1
+  | Tuple _, _ -> 1
+  | _, Tuple _ -> -1
+
 let rec smt_typ_equal t1 t2 =
   match t1, t2 with
   | Bitvec n, Bitvec m -> n = m
@@ -89,11 +113,11 @@ let mk_variant name ctors =
 
 type smt_exp =
   | Bool_lit of bool
-  | Hex of string
-  | Bin of string
+  | Bitvec_lit of Sail2_values.bitU list
   | Real_lit of string
   | String_lit of string
   | Var of string
+  | Shared of string
   | Read_res of string
   | Enum of string
   | Fn of string * smt_exp list
@@ -102,6 +126,11 @@ type smt_exp =
   | SignExtend of int * smt_exp
   | Extract of int * int * smt_exp
   | Tester of string * smt_exp
+  | Syntactic of smt_exp * smt_exp list
+  | Struct of string * (string * smt_exp) list
+  | Field of string * smt_exp
+  (* Used by sail-axiomatic, should never be generated by sail -smt! *)
+  | Forall of (string * smt_typ) list * smt_exp
 
 let rec fold_smt_exp f = function
   | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args))
@@ -110,7 +139,11 @@ let rec fold_smt_exp f = function
   | SignExtend (n, exp) -> f (SignExtend (n, fold_smt_exp f exp))
   | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp))
   | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp))
-  | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Read_res _ | Enum _ as exp) -> f exp
+  | Forall (binders, exp) -> f (Forall (binders, fold_smt_exp f exp))
+  | Syntactic (exp, exps) -> f (Syntactic (fold_smt_exp f exp, List.map (fold_smt_exp f) exps))
+  | Field (name, exp) -> f (Field (name, fold_smt_exp f exp))
+  | Struct (name, fields) -> f (Struct (name, List.map (fun (field, exp) -> field, fold_smt_exp f exp) fields))
+  | (Bool_lit _ | Bitvec_lit  _ | Real_lit _ | String_lit _ | Var _ | Shared _ | Read_res _ | Enum _ as exp) -> f exp
 
 let smt_conj = function
   | [] -> Bool_lit true
@@ -136,21 +169,13 @@ let bvshl x y  = Fn ("bvshl", [x; y])
 let bvlshr x y = Fn ("bvlshr", [x; y])
 let bvult x y  = Fn ("bvult", [x; y])
 
-let bvzero n =
-  if n mod 4 = 0 then
-    Hex (String.concat "" (Util.list_init (n / 4) (fun _ -> "0")))
-  else
-    Bin (String.concat "" (Util.list_init n (fun _ -> "0")))
+let bvzero n = Bitvec_lit (Sail2_operators_bitlists.zeros (Big_int.of_int n))
 
-let bvones n =
-  if n mod 4 = 0 then
-    Hex (String.concat "" (Util.list_init (n / 4) (fun _ -> "F")))
-  else
-    Bin (String.concat "" (Util.list_init n (fun _ -> "1")))
+let bvones n = Bitvec_lit (Sail2_operators_bitlists.ones (Big_int.of_int n))
 
 let simp_equal x y =
   match x, y with
-  | Bin str1, Bin str2 -> Some (str1 = str2)
+  | Bitvec_lit bv1, Bitvec_lit bv2 -> Some (Sail2_operators_bitlists.eq_vec bv1 bv2)
   | _, _ -> None
 
 let simp_and xs =
@@ -175,6 +200,16 @@ let simp_or xs =
      else
        Fn ("or", xs)
 
+let rec all_bitvec_lit = function
+  | Bitvec_lit _ :: rest -> all_bitvec_lit rest
+  | [] -> true
+  | _ :: _ -> false
+
+let rec merge_bitvec_lit = function
+  | Bitvec_lit b :: rest -> b @ merge_bitvec_lit rest
+  | [] -> []
+  | _ :: _ -> assert false
+
 let simp_fn = function
   | Fn ("not", [Fn ("not", [exp])]) -> exp
   | Fn ("not", [Bool_lit b]) -> Bool_lit (not b)
@@ -184,6 +219,9 @@ let simp_fn = function
   | Fn ("and", xs) -> simp_and xs
   | Fn ("=>", [Bool_lit true; y]) -> y
   | Fn ("=>", [Bool_lit false; y]) -> Bool_lit true
+  | Fn ("bvsub", [Bitvec_lit bv1; Bitvec_lit bv2]) -> Bitvec_lit (Sail2_operators_bitlists.sub_vec bv1 bv2)
+  | Fn ("bvadd", [Bitvec_lit bv1; Bitvec_lit bv2]) -> Bitvec_lit (Sail2_operators_bitlists.add_vec bv1 bv2)
+  | Fn ("concat", xs) when all_bitvec_lit xs -> Bitvec_lit (merge_bitvec_lit xs)
   | Fn ("=", [x; y]) as exp ->
      begin match simp_equal x y with
      | Some b -> Bool_lit b
@@ -205,7 +243,16 @@ let rec simp_smt_exp vars kinds = function
      | Some exp -> simp_smt_exp vars kinds exp
      | None -> Var v
      end
-  | (Read_res _ | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | (Read_res _ | Shared _ | Enum _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | Field (field, exp) ->
+     let exp = simp_smt_exp vars kinds exp in
+     begin match exp with
+     | Struct (_, fields) ->
+        List.assoc field fields
+     | _ -> Field (field, exp)
+     end
+  | Struct (name, fields) ->
+     Struct (name, List.map (fun (field, exp) -> field, simp_smt_exp vars kinds exp) fields)
   | Fn (f, exps) ->
      let exps = List.map (simp_smt_exp vars kinds) exps in
      simp_fn (Fn (f, exps))
@@ -220,8 +267,8 @@ let rec simp_smt_exp vars kinds = function
   | Extract (i, j, exp) ->
      let exp = simp_smt_exp vars kinds exp in
      begin match exp with
-     | Bin str ->
-        Bin (String.sub str ((String.length str - 1) - i) ((i + 1) - j))
+     | Bitvec_lit bv ->
+        Bitvec_lit (Sail2_operators_bitlists.subrange_vec_dec bv (Big_int.of_int i) (Big_int.of_int j))
      | _ -> Extract (i, j, exp)
      end
   | Tester (str, exp) ->
@@ -235,48 +282,167 @@ let rec simp_smt_exp vars kinds = function
         end
      | _ -> Tester (str, exp)
      end
+  | Syntactic (exp, _) -> exp
   | SignExtend (i, exp) ->
      let exp = simp_smt_exp vars kinds exp in
-     SignExtend (i, exp)
+     begin match exp with
+     | Bitvec_lit bv ->
+        Bitvec_lit (Sail2_operators_bitlists.sign_extend bv (Big_int.of_int (i + List.length bv)))
+     | _ -> SignExtend (i, exp)
+     end
+  | Forall (binders, exp) -> Forall (binders, exp)
+
+type read_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    kind : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    ret_type : smt_typ;
+    doc : string
+  }
+
+type write_info = {
+    name : string;
+    node : int;
+    active  : smt_exp;
+    kind : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    data_type : smt_typ;
+    data : smt_exp;
+    doc : string
+  }
+
+type barrier_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    kind : smt_exp;
+    doc : string
+  }
+
+type branch_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    doc : string
+  }
+
+type cache_op_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    kind : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    doc : string
+  }
 
 type smt_def =
   | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
+  | Declare_fun of string * smt_typ list * smt_typ
   | Declare_const of string * smt_typ
   | Define_const of string * smt_typ * smt_exp
-  | Write_mem of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
+  (* Same as Define_const, but it'll never be removed by simplification *)
+  | Preserve_const of string * smt_typ * smt_exp
+  | Write_mem of write_info
   | Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
-  | Read_mem of string * int * smt_exp * smt_typ * smt_exp * smt_exp * smt_typ
-  | Barrier of string * int * smt_exp * smt_exp
+  | Read_mem of read_info
+  | Barrier of barrier_info
+  | Branch_announce of branch_info
+  | Cache_maintenance of cache_op_info
   | Excl_res of string * int * smt_exp
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
 
+let smt_def_map_exp f = function
+  | Define_fun (name, args, ty, exp) -> Define_fun (name, args, ty, f exp)
+  | Declare_fun (name, args, ty) -> Declare_fun (name, args, ty)
+  | Declare_const (name, ty) -> Declare_const (name, ty)
+  | Define_const (name, ty, exp) -> Define_const (name, ty, f exp)
+  | Preserve_const (name, ty, exp) -> Preserve_const (name, ty, f exp)
+  | Write_mem w -> Write_mem { w with active = f w.active; kind = f w.kind; addr = f w.addr; data = f w.data }
+  | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
+     Write_mem_ea (name, node, f active, f wk, f addr, addr_ty, f data_size, data_size_ty)
+  | Read_mem r -> Read_mem { r with active = f r.active; kind = f r.kind; addr = f r.addr }
+  | Barrier b -> Barrier { b with active = f b.active; kind = f b.kind }
+  | Cache_maintenance m -> Cache_maintenance { m with active = f m.active; kind = f m.kind ; addr = f m.addr }
+  | Branch_announce c -> Branch_announce { c with active = f c.active; addr = f c.addr }
+  | Excl_res (name, node, active) -> Excl_res (name, node, f active)
+  | Declare_datatypes (name, ctors) -> Declare_datatypes (name, ctors)
+  | Declare_tuple n -> Declare_tuple n
+  | Assert exp -> Assert (f exp)
+
+let smt_def_iter_exp f = function
+  | Define_fun (name, args, ty, exp) -> f exp
+  | Define_const (name, ty, exp) -> f exp
+  | Preserve_const (name, ty, exp) -> f exp
+  | Write_mem w -> f w.active; f w.kind; f w.addr; f w.data
+  | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
+     f active; f wk; f addr; f data_size
+  | Read_mem r -> f r.active; f r.kind; f r.addr
+  | Barrier b -> f b.active; f b.kind
+  | Cache_maintenance m -> f m.active; f m.kind; f m.addr
+  | Branch_announce c -> f c.active; f c.addr
+  | Excl_res (name, node, active) -> f active
+  | Assert exp -> f exp
+  | Declare_fun _ | Declare_const _ | Declare_tuple _ | Declare_datatypes _ -> ()
+
 let declare_datatypes = function
   | Datatype (name, ctors) -> Declare_datatypes (name, ctors)
   | _ -> assert false
 
+(** For generating SMT with multiple threads (i.e. for litmus tests),
+   we suffix all the variables in the generated SMT with a thread
+   identifier to avoid any name clashes between the two threads. *)
+
 let suffix_variables_exp sfx =
-  fold_smt_exp (function Var v -> Var (v ^ sfx) | exp -> exp)
+  fold_smt_exp (function Var v -> Var (v ^ sfx) | Read_res v -> Read_res (v ^ sfx) | exp -> exp)
+
+let suffix_variables_read_info sfx (r : read_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { r with name = r.name ^ sfx; active = suffix r.active; kind = suffix r.kind; addr = suffix r.addr }
+
+let suffix_variables_write_info sfx (w : write_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { w with name = w.name ^ sfx; active = suffix w.active; kind = suffix w.kind; addr = suffix w.addr; data = suffix w.data }
+
+let suffix_variables_barrier_info sfx (b : barrier_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { b with name = b.name ^ sfx; active = suffix b.active; kind = suffix b.kind }
+
+let suffix_variables_branch_info sfx (c : branch_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { c with name = c.name ^ sfx; active = suffix c.active; addr = suffix c.addr }
+
+let suffix_variables_cache_op_info sfx (m : cache_op_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { m with name = m.name ^ sfx; kind = suffix m.kind; active = suffix m.active; addr = suffix m.addr }
 
 let suffix_variables_def sfx = function
   | Define_fun (name, args, ty, exp) ->
      Define_fun (name ^ sfx, List.map (fun (arg, ty) -> sfx ^ arg, ty) args, ty, suffix_variables_exp sfx exp)
+  | Declare_fun (name, tys, ty) ->
+     Declare_fun (name ^ sfx, tys, ty)
   | Declare_const (name, ty) ->
      Declare_const (name ^ sfx, ty)
   | Define_const (name, ty, exp) ->
      Define_const (name ^ sfx, ty, suffix_variables_exp sfx exp)
-  | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
-     Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
-                suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty)
+  | Preserve_const (name, ty, exp) ->
+     Preserve_const (name, ty, suffix_variables_exp sfx exp)
+  | Write_mem w -> Write_mem (suffix_variables_write_info sfx w)
   | Write_mem_ea (name, node, active , wk, addr, addr_ty, data_size, data_size_ty) ->
-     Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
-                suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
-  | Read_mem (name, node, active, ty, rk, addr, addr_ty) ->
-     Read_mem (name ^ sfx, node, suffix_variables_exp sfx active, ty, suffix_variables_exp sfx rk,
-               suffix_variables_exp sfx addr, addr_ty)
-  | Barrier (name, node, active, bk) ->
-     Barrier (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx bk)
+     Write_mem_ea (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
+                   suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
+  | Read_mem r -> Read_mem (suffix_variables_read_info sfx r)
+  | Barrier b -> Barrier (suffix_variables_barrier_info sfx b)
+  | Cache_maintenance m -> Cache_maintenance (suffix_variables_cache_op_info sfx m)
+  | Branch_announce c -> Branch_announce (suffix_variables_branch_info sfx c)
   | Excl_res (name, node, active) ->
      Excl_res (name ^ sfx, node, suffix_variables_exp sfx active)
   | Declare_datatypes (name, ctors) ->
@@ -286,54 +452,37 @@ let suffix_variables_def sfx = function
   | Assert exp ->
      Assert (suffix_variables_exp sfx exp)
 
-let merge_datatypes defs1 defs2 =
-  let module StringSet = Set.Make(String) in
-  let datatype_name = function
-    | Declare_datatypes (name, _) -> name
-    | _ -> assert false
-  in
-  let names = List.fold_left (fun set def -> StringSet.add (datatype_name def) set) StringSet.empty defs1 in
-  defs1 @ List.filter (fun def -> not (StringSet.mem (datatype_name def) names)) defs2
-
-let merge_tuples defs1 defs2 =
-  let tuple_size = function
-    | Declare_tuple size -> size
-    | _ -> assert false
-  in
-  let names = List.fold_left (fun set def -> Util.IntSet.add (tuple_size def) set) Util.IntSet.empty defs1 in
-  defs1 @ List.filter (fun def -> not (Util.IntSet.mem (tuple_size def) names)) defs2
-
-let merge_smt_defs defs1 defs2 =
-  let is_tuple = function
-    | Declare_datatypes _ | Declare_tuple _ -> true
-    | _ -> false
-  in
-  let is_datatype = function
-    | Declare_datatypes _ | Declare_tuple _ -> true
-    | _ -> false
-  in
-  let datatypes1, body1 = List.partition is_datatype defs1 in
-  let datatypes2, body2 = List.partition is_datatype defs2 in
-  let tuples1, datatypes1 = List.partition is_tuple datatypes1 in
-  let tuples2, datatypes2 = List.partition is_tuple datatypes2 in
-  merge_tuples tuples1 tuples2 @ merge_datatypes datatypes1 datatypes2 @ body1 @ body2
-
 let pp_sfun str docs =
   let open PPrint in
   parens (separate space (string str :: docs))
 
+let rec pp_smt_typ =
+  let open PPrint in
+  function
+  | Bool -> string "Bool"
+  | String -> string "String"
+  | Real -> string "Real"
+  | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n)
+  | Datatype (name, _) -> string name
+  | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys)
+  | Array (ty1, ty2) -> pp_sfun "Array" [pp_smt_typ ty1; pp_smt_typ ty2]
+
+let pp_str_smt_typ (str, ty) = let open PPrint in parens (string str ^^ space ^^ pp_smt_typ ty)
+
 let rec pp_smt_exp =
   let open PPrint in
   function
   | Bool_lit b -> string (string_of_bool b)
   | Real_lit str -> string str
   | String_lit str -> string ("\"" ^ str ^ "\"")
-  | Hex str -> string ("#x" ^ str)
-  | Bin str -> string ("#b" ^ str)
+  | Bitvec_lit bv -> string (Sail2_values.show_bitlist_prefix '#' bv)
   | Var str -> string str
+  | Shared str -> string str
   | Read_res str -> string (str ^ "_ret")
   | Enum str -> string str
   | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
+  | Field (str, exp) -> parens (string str ^^ space ^^ pp_smt_exp exp)
+  | Struct (str, fields) -> parens (string str ^^ space ^^ separate_map space (fun (_, exp) -> pp_smt_exp exp) fields)
   | Ctor (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
   | Ite (cond, then_exp, else_exp) ->
      parens (separate space [string "ite"; pp_smt_exp cond; pp_smt_exp then_exp; pp_smt_exp else_exp])
@@ -343,19 +492,9 @@ let rec pp_smt_exp =
      parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp exp)
   | SignExtend (i, exp) ->
      parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp exp)
-
-let rec pp_smt_typ =
-  let open PPrint in
-  function
-  | Bool -> string "Bool"
-  | String -> string "String"
-  | Real -> string "Real"
-  | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n)
-  | Datatype (name, _) -> string name
-  | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys)
-  | Array (ty1, ty2) -> pp_sfun "Array" [pp_smt_typ ty1; pp_smt_typ ty2]
-
-let pp_str_smt_typ (str, ty) = let open PPrint in string str ^^ space ^^ pp_smt_typ ty
+  | Syntactic (exp, _) -> pp_smt_exp exp
+  | Forall (binders, exp) ->
+     parens (string "forall" ^^ space ^^ parens (separate_map space pp_str_smt_typ binders) ^^ space ^^ pp_smt_exp exp)
 
 let pp_smt_def =
   let open PPrint in
@@ -367,18 +506,23 @@ let pp_smt_def =
              ^^ space ^^ pp_smt_typ ty
              ^//^ pp_smt_exp exp)
 
+  | Declare_fun (name, args, ty) ->
+     parens (string "declare-fun" ^^ space ^^ string name
+             ^^ space ^^ parens (separate_map space pp_smt_typ args)
+             ^^ space ^^ pp_smt_typ ty)
+
   | Declare_const (name, ty) ->
      pp_sfun "declare-const" [string name; pp_smt_typ ty]
 
-  | Define_const (name, ty, exp) ->
+  | Define_const (name, ty, exp) | Preserve_const (name, ty, exp) ->
      pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
 
-  | Write_mem (name, _, active, wk, addr, addr_ty, data, data_ty) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_data"); pp_smt_typ data_ty; pp_smt_exp data] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
-     ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ Bool]
+  | Write_mem w ->
+     pp_sfun "define-const" [string (w.name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp w.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (w.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp w.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (w.name ^ "_data"); pp_smt_typ w.data_type; pp_smt_exp w.data] ^^ hardline
+     ^^ pp_sfun "define-const" [string (w.name ^ "_addr"); pp_smt_typ w.addr_type; pp_smt_exp w.addr] ^^ hardline
+     ^^ pp_sfun "declare-const" [string (w.name ^ "_ret"); pp_smt_typ Bool]
 
   | Write_mem_ea (name, _, active, wk, addr, addr_ty, data_size, data_size_ty) ->
      pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
@@ -386,15 +530,24 @@ let pp_smt_def =
      ^^ pp_sfun "define-const" [string (name ^ "_size"); pp_smt_typ data_size_ty; pp_smt_exp data_size] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr]
 
-  | Read_mem (name, _, active, ty, rk, addr, addr_ty) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zread_kind"; pp_smt_exp rk] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
-     ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ ty]
+  | Read_mem r ->
+     pp_sfun "define-const" [string (r.name ^ "_kind"); string "Zread_kind"; pp_smt_exp r.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (r.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp r.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (r.name ^ "_addr"); pp_smt_typ r.addr_type; pp_smt_exp r.addr] ^^ hardline
+     ^^ pp_sfun "declare-const" [string (r.name ^ "_ret"); pp_smt_typ r.ret_type]
 
-  | Barrier (name, _, active, bk) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active]
+  | Barrier b ->
+     pp_sfun "define-const" [string (b.name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp b.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (b.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp b.active]
+
+  | Cache_maintenance m ->
+     pp_sfun "define-const" [string (m.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp m.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (m.name ^ "_kind"); string "Zcache_op_kind"; pp_smt_exp m.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (m.name ^ "_addr"); pp_smt_typ m.addr_type; pp_smt_exp m.addr]
+
+  | Branch_announce c ->
+     pp_sfun "define-const" [string (c.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp c.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (c.name ^ "_addr"); pp_smt_typ c.addr_type; pp_smt_exp c.addr]
 
   | Excl_res (name, _, active) ->
      pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool] ^^ hardline
@@ -404,7 +557,7 @@ let pp_smt_def =
      let pp_ctor (ctor_name, fields) =
        match fields with
        | [] -> parens (string ctor_name)
-       | _ -> pp_sfun ctor_name (List.map (fun field -> parens (pp_str_smt_typ field)) fields)
+       | _ -> pp_sfun ctor_name (List.map pp_str_smt_typ fields)
      in
      pp_sfun "declare-datatypes"
        [Printf.ksprintf string "((%s 0))" name;
diff --git a/src/util.ml b/src/util.ml
index 02a5468a..99f1111f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -143,6 +143,22 @@ let remove_dups compare eq l =
   in
   aux [] l'
 
+let lex_ord_list comparison xs ys =
+  let rec lex_lists xs ys =
+    match xs, ys with
+    | x :: xs, y :: ys ->
+       let c = comparison x y in
+       if c = 0 then lex_lists xs ys else c
+    | [], [] -> 0
+    | _, _ -> assert false
+  in
+  if List.length xs = List.length ys then
+    lex_lists xs ys
+  else if List.length xs < List.length ys then
+    -1
+  else
+    1
+
 let rec power i tothe =
   if tothe <= 0
   then 1
@@ -228,7 +244,7 @@ let option_bind f = function
   | None -> None
   | Some(o) -> f o
 
-let rec option_binop f x y = match x, y with
+let option_binop f x y = match x, y with
   | Some x, Some y -> Some (f x y)
   | _ -> None
 
diff --git a/src/util.mli b/src/util.mli
index a29bdba2..3d83a1a4 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -73,6 +73,9 @@ val remove_duplicates : 'a list -> 'a list
 (** [remove_dups compare eq l] as remove_duplicates but with parameterised comparison and equality *)
 val remove_dups : ('a -> 'a -> int) -> ('a -> 'a -> bool) -> 'a list -> 'a list
 
+(** Lift a comparison order to the lexical order on lists *)
+val lex_ord_list : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+
 (** [assoc_equal_opt] and [assoc_compare_opt] are like List.assoc_opt
    but take equality/comparison functions as arguments, rather than
    relying on OCaml's built in equality *)
diff --git a/src/value2.lem b/src/value2.lem
index 0afaa2d1..a334ac58 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -60,4 +60,8 @@ type vl =
   | VL_int of integer
   | VL_string of string
   | VL_real of string
-  | VL_null (* Used for unitialized values and null pointers in C compilation *)
+  | VL_tuple of list vl
+  | VL_matcher of int * int
+  | VL_list of list vl
+  | VL_enum of string
+  | VL_ref of string
diff --git a/test/smt/revrev_endianness.sail b/test/smt/revrev_endianness.unsat.sail
index f792871f..f792871f 100644
--- a/test/smt/revrev_endianness.sail
+++ b/test/smt/revrev_endianness.unsat.sail
diff --git a/test/smt/revrev_endianness2.sail b/test/smt/revrev_endianness2.unsat.sail
index 33ba93a2..33ba93a2 100644
--- a/test/smt/revrev_endianness2.sail
+++ b/test/smt/revrev_endianness2.unsat.sail