Merge branch 'sail2' into rmem_interpreter

30 files changed, 904 insertions, 426 deletions

diff --git a/src/Makefile b/src/Makefile
index e29a1ef0..abf49423 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -96,7 +96,7 @@ else
 	echo let dir=\"$(SHARE_DIR)\" >> manifest.ml
 	echo let commit=\"opam\" >> manifest.ml
 	echo let branch=\"sail2\" >> manifest.ml
-	echo let version=\"0.8\" >> manifest.ml
+	echo let version=\"$(shell grep '^version:' ../opam | grep -o -E '"[^"]+"')\" >> manifest.ml
 endif
 
 sail: ast.ml bytecode.ml manifest.ml
diff --git a/src/anf.ml b/src/anf.ml
index 38c77e0b..5db836e9 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -436,6 +436,8 @@ and pp_aval = function
 
 let ae_lit lit typ = AE_val (AV_lit (lit, typ))
 
+let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false
+
 (** GLOBAL: gensym_counter is used to generate fresh identifiers where
    needed. It should be safe to reset between top level
    definitions. **)
diff --git a/src/anf.mli b/src/anf.mli
index 5e162b7c..6b9c9b51 100644
--- a/src/anf.mli
+++ b/src/anf.mli
@@ -112,6 +112,8 @@ val apat_globals : 'a apat -> (id * 'a) list
 
 val apat_types : 'a apat -> 'a Bindings.t
 
+val is_dead_aexp : 'a aexp -> bool
+
 (* Compiling to ANF expressions *)
 
 val anf_pat : ?global:bool -> tannot pat -> typ apat
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 04b76a61..548cd15e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -116,7 +116,7 @@ let mk_qi_kopt kopt = QI_aux (QI_id kopt, Parse_ast.Unknown)
 
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
-  let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
+  let effect_opt = Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown) in
   let rec_opt = Rec_aux (Rec_nonrec, Parse_ast.Unknown) in
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
@@ -129,7 +129,7 @@ let mk_val_spec vs_aux =
 let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid
 let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k
 
-let is_nat_kopt = function
+let is_int_kopt = function
   | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true
   | _ -> false
 
@@ -417,11 +417,16 @@ let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
 let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
 let nc_lt n1 n2 = nc_lteq (nsum n1 (nint 1)) n2
 let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1))
-let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
 let nc_var kid = mk_nc (NC_var kid)
 let nc_true = mk_nc NC_true
 let nc_false = mk_nc NC_false
 
+let nc_or nc1 nc2 =
+  match nc1, nc2 with
+  | _, NC_aux (NC_false, _) -> nc1
+  | NC_aux (NC_false, _), _ -> nc2
+  | _, _ -> mk_nc (NC_or (nc1, nc2))
+
 let nc_and nc1 nc2 =
   match nc1, nc2 with
   | _, NC_aux (NC_true, _) -> nc1
@@ -439,7 +444,7 @@ let arg_kopt (KOpt_aux (KOpt_kind (K_aux (k, _), v), l)) =
   | K_order -> arg_order (Ord_aux (Ord_var v, l))
   | K_bool -> arg_bool (nc_var v)
   | K_type -> arg_typ (mk_typ (Typ_var v))
-           
+
 let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc]))
 
 let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
@@ -1355,6 +1360,7 @@ and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) =
   match typ_arg_aux with
   | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
   | A_typ typ -> [undefined_of_typ mwords l annot typ]
+  | A_bool nc -> [E_aux (E_constraint nc, (l, annot (atom_bool_typ nc)))]
   | A_order _ -> []
 
 let destruct_pexp (Pat_aux (pexp,ann)) =
@@ -1870,6 +1876,12 @@ let rec find_annot_exp sl (E_aux (aux, (l, annot)) as exp) =
          option_chain (find_annot_lexp sl lexp) (find_annot_exp sl exp)
       | E_var (lexp, exp1, exp2) ->
          option_chain (find_annot_lexp sl lexp) (option_mapm (find_annot_exp sl) [exp1; exp2])
+      | E_if (cond_exp, then_exp, else_exp) ->
+         option_mapm (find_annot_exp sl) [cond_exp; then_exp; else_exp]
+      | E_case (exp, cases) | E_try (exp, cases) ->
+         option_chain (find_annot_exp sl exp) (option_mapm (find_annot_pexp sl) cases)
+      | E_return exp | E_cast (_, exp) ->
+         find_annot_exp sl exp
       | _ -> None
     in
     match result with
@@ -1896,6 +1908,8 @@ and find_annot_lexp sl (LEXP_aux (aux, (l, annot))) =
 and find_annot_pat sl (P_aux (aux, (l, annot))) =
   if not (subloc sl l) then None else
     let result = match aux with
+      | P_vector_concat pats ->
+         option_mapm (find_annot_pat sl) pats
       | _ -> None
     in
     match result with
@@ -1906,32 +1920,43 @@ and find_annot_pexp sl (Pat_aux (aux, (l, annot))) =
   if not (subloc sl l) then None else
     match aux with
     | Pat_exp (pat, exp) ->
-       find_annot_exp sl exp
+       option_chain (find_annot_pat sl pat) (find_annot_exp sl exp)
     | Pat_when (pat, guard, exp) ->
-       None
+       option_chain (find_annot_pat sl pat) (option_mapm (find_annot_exp sl) [guard; exp])
 
 let find_annot_funcl sl (FCL_aux (FCL_Funcl (id, pexp), (l, annot))) =
-  if not (subloc sl l) then
-    None
-  else
+  if not (subloc sl l) then None else
     match find_annot_pexp sl pexp with
     | None -> Some (l, annot)
     | result -> result
 
 let find_annot_fundef sl (FD_aux (FD_function (_, _, _, funcls), (l, annot))) =
-  if not (subloc sl l) then
-    None
-  else
+  if not (subloc sl l) then None else
     match option_mapm (find_annot_funcl sl) funcls with
     | None -> Some (l, annot)
     | result -> result
 
+let find_annot_scattered sl (SD_aux (aux, (l, annot))) =
+  if not (subloc sl l) then None else
+    let result = match aux with
+      | SD_funcl fcl -> find_annot_funcl sl fcl
+      | _ -> None
+    in
+    match result with
+    | None -> Some (l, annot)
+    | _ -> result
+
 let rec find_annot_defs sl = function
   | DEF_fundef fdef :: defs ->
      begin match find_annot_fundef sl fdef with
      | None -> find_annot_defs sl defs
      | result -> result
      end
+  | DEF_scattered sdef :: defs ->
+     begin match find_annot_scattered sl sdef with
+     | None -> find_annot_defs sl defs
+     | result -> result
+     end
   | _ :: defs ->
      find_annot_defs sl defs
   | [] -> None
diff --git a/src/ast_util.mli b/src/ast_util.mli
index a2466326..ae63aca7 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -109,7 +109,7 @@ val dec_ord : order
 (* Utilites for working with kinded_ids *)
 val kopt_kid : kinded_id -> kid
 val kopt_kind : kinded_id -> kind
-val is_nat_kopt : kinded_id -> bool
+val is_int_kopt : kinded_id -> bool
 val is_order_kopt : kinded_id -> bool
 val is_typ_kopt : kinded_id -> bool
 val is_bool_kopt : kinded_id -> bool
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 3ced48b6..489bcc64 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -252,14 +252,14 @@ and string_of_fragment' ?zencode:(zencode=true) f =
 (* String representation of ctyps here is only for debugging and
    intermediate language pretty-printer. *)
 and string_of_ctyp = function
-  | CT_int -> "int"
+  | CT_lint -> "int"
   | CT_lbits true -> "lbits(dec)"
   | CT_lbits false -> "lbits(inc)"
   | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
   | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
   | CT_sbits true -> "sbits(dec)"
   | CT_sbits false -> "sbits(inc)"
-  | CT_int64 -> "int64"
+  | CT_fint n -> "int(" ^ string_of_int n ^ ")"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
@@ -276,14 +276,14 @@ and string_of_ctyp = function
 (** This function is like string_of_ctyp, but recursively prints all
    constructors in variants and structs. Used for debug output. *)
 and full_string_of_ctyp = function
-  | CT_int -> "int"
+  | CT_lint -> "int"
   | CT_lbits true -> "lbits(dec)"
   | CT_lbits false -> "lbits(inc)"
   | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
   | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
   | CT_sbits true -> "sbits(dec)"
   | CT_sbits false -> "sbits(inc)"
-  | CT_int64 -> "int64"
+  | CT_fint n -> "int(" ^ string_of_int n ^ ")"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
@@ -303,7 +303,7 @@ and full_string_of_ctyp = function
   | CT_poly -> "*"
 
 let rec map_ctyp f = function
-  | (CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _
+  | (CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _
      | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp
   | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps))
   | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp))
@@ -314,12 +314,12 @@ let rec map_ctyp f = function
 
 let rec ctyp_equal ctyp1 ctyp2 =
   match ctyp1, ctyp2 with
-  | CT_int, CT_int -> true
+  | CT_lint, CT_lint -> true
   | CT_lbits d1, CT_lbits d2 -> d1 = d2
   | CT_sbits d1, CT_sbits d2 -> d1 = d2
   | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2
   | CT_bit, CT_bit -> true
-  | CT_int64, CT_int64 -> true
+  | CT_fint n, CT_fint m -> n = m
   | CT_unit, CT_unit -> true
   | CT_bool, CT_bool -> true
   | CT_struct (id1, _), CT_struct (id2, _) -> Id.compare id1 id2 = 0
@@ -353,11 +353,11 @@ let rec ctyp_unify ctyp1 ctyp2 =
   | _, _ -> raise (Invalid_argument "ctyp_unify")
 
 let rec ctyp_suprema = function
-  | CT_int -> CT_int
+  | CT_lint -> CT_lint
   | CT_lbits d -> CT_lbits d
   | CT_fbits (_, d) -> CT_lbits d
   | CT_sbits d -> CT_lbits d
-  | CT_int64 -> CT_int
+  | CT_fint _ -> CT_lint
   | CT_unit -> CT_unit
   | CT_bool -> CT_bool
   | CT_real -> CT_real
@@ -382,7 +382,7 @@ let rec ctyp_ids = function
      IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
   | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
   | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
-  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
     | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
 
 let rec unpoly = function
@@ -394,7 +394,7 @@ let rec unpoly = function
   | f -> f
 
 let rec is_polymorphic = function
-  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
   | CT_tup ctyps -> List.exists is_polymorphic ctyps
   | CT_enum _ -> false
   | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
diff --git a/src/c_backend.ml b/src/c_backend.ml
index a1050972..aff2d49e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -110,7 +110,7 @@ type ctx =
     letbinds : int list;
     recursive_functions : IdSet.t;
     no_raw : bool;
-    optimize_z3 : bool;
+    optimize_smt : bool;
   }
 
 let initial_ctx env =
@@ -123,26 +123,28 @@ let initial_ctx env =
     letbinds = [];
     recursive_functions = IdSet.empty;
     no_raw = false;
-    optimize_z3 = true;
+    optimize_smt = true;
   }
 
 (** Convert a sail type into a C-type. This function can be quite
-   slow, because it uses ctx.local_env and Z3 to analyse the Sail
+   slow, because it uses ctx.local_env and SMT to analyse the Sail
    types and attempts to fit them into the smallest possible C
-   types, provided ctx.optimize_z3 is true (default) **)
+   types, provided ctx.optimize_smt is true (default) **)
 let rec ctyp_of_typ ctx typ =
   let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
   match typ_aux with
   | Typ_id id when string_of_id id = "bit"    -> CT_bit
   | Typ_id id when string_of_id id = "bool"   -> CT_bool
-  | Typ_id id when string_of_id id = "int"    -> CT_int
-  | Typ_id id when string_of_id id = "nat"    -> CT_int
+  | Typ_id id when string_of_id id = "int"    -> CT_lint
+  | Typ_id id when string_of_id id = "nat"    -> CT_lint
   | Typ_id id when string_of_id id = "unit"   -> CT_unit
   | Typ_id id when string_of_id id = "string" -> CT_string
   | Typ_id id when string_of_id id = "real"   -> CT_real
 
   | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
 
+  | Typ_app (id, args) when string_of_id id = "itself" ->
+     ctyp_of_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
   | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
      begin match destruct_range Env.empty typ with
      | None -> assert false (* Checked if range type in guard *)
@@ -150,13 +152,13 @@ let rec ctyp_of_typ ctx typ =
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
              when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
-           CT_int64
-        | n, m when ctx.optimize_z3 ->
+           CT_fint 64
+        | n, m when ctx.optimize_smt ->
            if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
-             CT_int64
+             CT_fint 64
            else
-             CT_int
-        | _ -> CT_int
+             CT_lint
+        | _ -> CT_lint
      end
 
   | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
@@ -173,7 +175,7 @@ let rec ctyp_of_typ ctx typ =
      let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
      begin match nexp_simp n with
      | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
-     | n when ctx.optimize_z3 && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
+     | n when ctx.optimize_smt && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
      | _ -> CT_lbits direction
      end
 
@@ -193,8 +195,8 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs)
 
-  | Typ_exist _ when ctx.optimize_z3 ->
-     (* Use Type_check.destruct_exist when optimising with z3, to
+  | Typ_exist _ when ctx.optimize_smt ->
+     (* Use Type_check.destruct_exist when optimising with SMT, to
         ensure that we don't cause any type variable clashes in
         local_env, and that we can optimize the existential based upon
         it's constraints. *)
@@ -212,8 +214,9 @@ let rec ctyp_of_typ ctx typ =
   | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
 
 let rec is_stack_ctyp ctyp = match ctyp with
-  | CT_fbits _ | CT_sbits _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
-  | CT_lbits _ | CT_int | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+  | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
+  | CT_fint n -> n <= 64
+  | CT_lbits _ | CT_lint | CT_real | CT_string | CT_list _ | CT_vector _ -> false
   | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
   | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *)
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -262,7 +265,7 @@ let hex_char =
 let literal_to_fragment (L_aux (l_aux, _) as lit) =
   match l_aux with
   | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
-     Some (F_lit (V_int n), CT_int64)
+     Some (F_lit (V_int n), CT_fint 64)
   | L_hex str when String.length str <= 16 ->
      let padding = 16 - String.length str in
      let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in
@@ -397,7 +400,7 @@ let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
        let aexp3 = analyze_functions ctx f aexp3 in
        let aexp4 = analyze_functions ctx f aexp4 in
        (* Currently we assume that loop indexes are always safe to put into an int64 *)
-       let ctx = { ctx with locals = Bindings.add id (Immutable, CT_int64) ctx.locals } in
+       let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in
        AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
 
     | AE_case (aval, cases, typ) ->
@@ -542,14 +545,14 @@ let analyze_primop' ctx id args typ =
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
                when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
-           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
+           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
         | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) ->
-           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
+           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
         | _ -> no_change
      end
 
   | "neg_int", [AV_C_fragment (frag, _, _)] ->
-     AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_int64))
+     AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_fint 64))
 
   | "replicate_bits", [AV_C_fragment (vec, vtyp, _); AV_C_fragment (times, _, _)] ->
      begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
@@ -736,15 +739,15 @@ let rec compile_aval l ctx = function
 
   | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
      let gs = gensym () in
-     [iinit CT_int gs (F_lit (V_int n), CT_int64)],
-     (F_id gs, CT_int),
-     [iclear CT_int gs]
+     [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
+     (F_id gs, CT_lint),
+     [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_num n, _), typ) ->
      let gs = gensym () in
-     [iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
-     (F_id gs, CT_int),
-     [iclear CT_int gs]
+     [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
+     (F_id gs, CT_lint),
+     [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), []
   | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), []
@@ -868,11 +871,11 @@ let rec compile_aval l ctx = function
        setup
        @ [iextern (CL_id (gs, vector_ctyp))
                   (mk_id "internal_vector_update")
-                  [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval]]
+                  [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]]
        @ cleanup
      in
      [idecl vector_ctyp gs;
-      iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)]]
+      iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]]
      @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)),
      (F_id gs, vector_ctyp),
      [iclear vector_ctyp gs]
@@ -1083,7 +1086,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
-         | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
+           | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
          | _ -> false
        in
        let case_label = label "case_" in
@@ -1103,7 +1106,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
        in
-       [iblock case_instrs; ilabel case_label]
+       if is_dead_aexp body then
+         [ilabel case_label]
+       else
+         [iblock case_instrs; ilabel case_label]
      in
      [icomment "begin match"]
      @ aval_setup @ [idecl ctyp case_return_id]
@@ -1159,18 +1165,23 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      []
 
   | AE_if (aval, then_aexp, else_aexp, if_typ) ->
-     let if_ctyp = ctyp_of_typ ctx if_typ in
-     let compile_branch aexp =
-       let setup, call, cleanup = compile_aexp ctx aexp in
-       fun clexp -> setup @ [call clexp] @ cleanup
-     in
-     let setup, cval, cleanup = compile_aval l ctx aval in
-     setup,
-     (fun clexp -> iif cval
-                       (compile_branch then_aexp clexp)
-                       (compile_branch else_aexp clexp)
-                       if_ctyp),
-     cleanup
+     if is_dead_aexp then_aexp then
+       compile_aexp ctx else_aexp
+     else if is_dead_aexp else_aexp then
+       compile_aexp ctx then_aexp
+     else
+       let if_ctyp = ctyp_of_typ ctx if_typ in
+       let compile_branch aexp =
+         let setup, call, cleanup = compile_aexp ctx aexp in
+         fun clexp -> setup @ [call clexp] @ cleanup
+       in
+       let setup, cval, cleanup = compile_aval l ctx aval in
+       setup,
+       (fun clexp -> iif cval
+                         (compile_branch then_aexp clexp)
+                         (compile_branch else_aexp clexp)
+                         if_ctyp),
+       cleanup
 
   (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *)
   | AE_record_update (aval, fields, typ) ->
@@ -1332,8 +1343,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      cleanup
 
   | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
-     (* We assume that all loop indices are safe to put in a CT_int64. *)
-     let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_int64) ctx.locals } in
+     (* We assume that all loop indices are safe to put in a CT_fint. *)
+     let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_fint 64) ctx.locals } in
 
      let is_inc = match ord with
        | Ord_inc -> true
@@ -1349,8 +1360,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in
      let step_gs = gensym () in
      let variable_init gs setup call cleanup =
-       [idecl CT_int64 gs;
-        iblock (setup @ [call (CL_id (gs, CT_int64))] @ cleanup)]
+       [idecl (CT_fint 64) gs;
+        iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)]
      in
 
      let loop_start_label = label "for_start_" in
@@ -1361,16 +1372,16 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      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_int64 loop_var;
-                 icopy l (CL_id (loop_var, CT_int64)) (F_id from_gs, CT_int64);
+     @ [iblock ([idecl (CT_fint 64) loop_var;
+                 icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64));
                  idecl CT_unit body_gs;
                  iblock ([ilabel loop_start_label]
                          @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label]
                          @ body_setup
                          @ [body_call (CL_id (body_gs, CT_unit))]
                          @ body_cleanup
-                         @ [icopy l (CL_id (loop_var, CT_int64))
-                                  (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)]
+                         @ [icopy l (CL_id (loop_var, (CT_fint 64)))
+                                  (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))]
                          @ [igoto loop_start_label]);
                  ilabel loop_end_label])],
      (fun clexp -> icopy l clexp unit_fragment),
@@ -1878,7 +1889,7 @@ let rec instrs_rename from_id to_id =
   | [] -> []
 
 let hoist_ctyp = function
-  | CT_int | CT_lbits _ | CT_struct _ -> true
+  | CT_lint | CT_lbits _ | CT_struct _ -> true
   | _ -> false
 
 let hoist_counter = ref 0
@@ -2410,8 +2421,8 @@ let rec sgen_ctyp = function
   | CT_bool -> "bool"
   | CT_fbits _ -> "fbits"
   | CT_sbits _ -> "sbits"
-  | CT_int64 -> "mach_int"
-  | CT_int -> "sail_int"
+  | CT_fint _ -> "mach_int"
+  | CT_lint -> "sail_int"
   | CT_lbits _ -> "lbits"
   | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
   | CT_struct (id, _) -> "struct " ^ sgen_id id
@@ -2430,8 +2441,8 @@ let rec sgen_ctyp_name = function
   | CT_bool -> "bool"
   | CT_fbits _ -> "fbits"
   | CT_sbits _ -> "sbits"
-  | CT_int64 -> "mach_int"
-  | CT_int -> "sail_int"
+  | CT_fint _ -> "mach_int"
+  | CT_lint -> "sail_int"
   | CT_lbits _ -> "lbits"
   | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
   | CT_struct (id, _) -> sgen_id id
@@ -2647,7 +2658,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        match ctyp with
        | CT_unit -> "UNIT", []
        | CT_bit -> "UINT64_C(0)", []
-       | CT_int64 -> "INT64_C(0xdeadc0de)", []
+       | CT_fint _ -> "INT64_C(0xdeadc0de)", []
        | CT_fbits _ -> "UINT64_C(0xdeadc0de)", []
        | CT_sbits _ -> "undefined_sbits()", []
        | CT_bool -> "false", []
@@ -3265,7 +3276,7 @@ let rec ctyp_dependencies = function
   | CT_ref ctyp -> ctyp_dependencies ctyp
   | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
   | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
-  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> []
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> []
 
 let codegen_ctg ctx = function
   | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp)
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 031493a4..2c46f38b 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -188,6 +188,8 @@ let rec rewrite_constant_function_calls' env ast =
     | E_app (id, args) when List.for_all is_constant args ->
        evaluate e_aux annot
 
+    | E_cast (typ, (E_aux (E_lit _, _) as lit)) -> ok (); lit
+
     | E_field (exp, id) when is_constant exp ->
        evaluate e_aux annot
 
diff --git a/src/constraint.ml b/src/constraint.ml
index b7fa50c3..5402f6f7 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -55,6 +55,76 @@ open Util
 
 let opt_smt_verbose = ref false
 
+type solver = {
+    command : string;
+    header : string;
+    footer : string;
+    negative_literals : bool;
+    uninterpret_power : bool
+  }
+
+let cvc4_solver = {
+    command = "cvc4 -L smtlib2 --tlimit=2000";
+    header = "(set-logic QF_UFNIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let mathsat_solver = {
+    command = "mathsat";
+    header = "(set-logic QF_UFLIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let z3_solver = {
+    command = "z3 -t:1000 -T:10";
+    (* Using push and pop is much faster, I believe because
+       incremental mode uses a different solver. *)
+    header = "(push)\n";
+    footer = "(pop)\n";
+    negative_literals = true;
+    uninterpret_power = false;
+  }
+
+let yices_solver = {
+    command = "yices-smt2 --timeout=2";
+    header = "(set-logic QF_UFLIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let vampire_solver = {
+    (* vampire sometimes likes to ignore its time limit *)
+    command = "timeout -s SIGKILL 3s vampire --time_limit 2s --input_syntax smtlib2 --mode smtcomp";
+    header = "";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let alt_ergo_solver ={
+    command = "alt-ergo";
+    header = "";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let opt_solver = ref z3_solver
+
+let set_solver = function
+  | "z3" -> opt_solver := z3_solver
+  | "alt-ergo" -> opt_solver := alt_ergo_solver
+  | "cvc4" -> opt_solver := cvc4_solver
+  | "mathsat" -> opt_solver := mathsat_solver
+  | "vampire" -> opt_solver := vampire_solver
+  | "yices" -> opt_solver := yices_solver
+  | unknown -> prerr_endline ("Unrecognised SMT solver " ^ unknown)
+
 (* SMTLIB v2.0 format is based on S-expressions so we have a
    lightweight representation of those here. *)
 type sexpr = List of (sexpr list) | Atom of string
@@ -101,6 +171,9 @@ let to_smt l vars constr =
     match aux with
     | Nexp_id id -> Atom (Util.zencode_string (string_of_id id))
     | Nexp_var v -> smt_var v
+    | Nexp_constant c
+         when Big_int.less_equal c (Big_int.of_int (-1)) && not !opt_solver.negative_literals ->
+       sfun "-" [Atom "0"; Atom (Big_int.to_string (Big_int.abs c))]
     | Nexp_constant c -> Atom (Big_int.to_string c)
     | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps)
     | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2]
@@ -108,6 +181,7 @@ let to_smt l vars constr =
     | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2]
     | Nexp_exp (Nexp_aux (Nexp_constant c, _)) when Big_int.greater c Big_int.zero ->
        Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c)))
+    | Nexp_exp nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp]
     | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
     | Nexp_neg nexp -> sfun "-" [smt_nexp nexp]
   in
@@ -137,12 +211,13 @@ let to_smt l vars constr =
 
 let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) =
   let variables, problem, var_map = to_smt l vars constr in
-  "(push)\n"
+  !opt_solver.header
   ^ variables ^ "\n"
+  ^ (if !opt_solver.uninterpret_power then "(declare-fun sailexp (Int) Int)\n" else "")
   ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem])
   ^ "\n(assert constraint)\n(check-sat)"
-  ^ (if get_model then "\n(get-model)" else "")
-  ^ "\n(pop)",
+  ^ (if get_model then "\n(get-model)\n" else "\n")
+  ^ !opt_solver.footer,
   var_map
 
 type smt_result = Unknown | Sat | Unsat
@@ -184,12 +259,12 @@ let save_digests () =
   DigestMap.iter output !known_problems;
   close_out out_chan
 
-let call_z3' l vars constraints : smt_result =
+let call_smt' l vars constraints : smt_result =
   let problems = [constraints] in
-  let z3_file, _ = smtlib_of_constraints l vars constraints in
+  let smt_file, _ = smtlib_of_constraints l vars constraints in
 
   if !opt_smt_verbose then
-    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file)
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file)
   else ();
 
   let rec input_lines chan = function
@@ -202,7 +277,7 @@ let call_z3' l vars constraints : smt_result =
        end
   in
 
-  let digest = Digest.string z3_file in
+  let digest = Digest.string smt_file in
   try
     let result = DigestMap.find digest !known_problems in
     result
@@ -210,45 +285,49 @@ let call_z3' l vars constraints : smt_result =
   | Not_found ->
     begin
       let (input_file, tmp_chan) =
-        try Filename.open_temp_file "constraint_" ".sat" with
-        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling Z3: " ^ msg))
+        try Filename.open_temp_file "constraint_" ".smt2" with
+        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling SMT: " ^ msg))
       in
-      output_string tmp_chan z3_file;
+      output_string tmp_chan smt_file;
       close_out tmp_chan;
-      let z3_output =
+      let smt_output =
         try
-          let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-          let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
-          let _ = Unix.close_process_in z3_chan in
-          z3_output
+          let smt_out, smt_in, smt_err = Unix.open_process_full (!opt_solver.command ^ " " ^ input_file) (Unix.environment ()) in
+          let smt_output =
+            try List.combine problems (input_lines smt_out (List.length problems)) with
+            | End_of_file -> List.combine problems ["unknown"]
+          in
+          let _ = Unix.close_process_full (smt_out, smt_in, smt_err) in
+          smt_output
         with
-        | exn -> raise (Reporting.err_general l ("Error when calling z3: " ^ Printexc.to_string exn))
+        | exn -> raise (Reporting.err_general l ("Error when calling smt: " ^ Printexc.to_string exn))
       in
       Sys.remove input_file;
       try
-        let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
+        let (problem, _) = List.find (fun (_, result) -> result = "unsat") smt_output in
         known_problems := DigestMap.add digest Unsat !known_problems;
         Unsat
       with
       | Not_found ->
-         let unsolved = List.filter (fun (_, result) -> result = "unknown") z3_output in
+         let unsolved = List.filter (fun (_, result) -> result = "unknown") smt_output in
          if unsolved == []
          then (known_problems := DigestMap.add digest Sat !known_problems; Sat)
          else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
     end
 
-let call_z3 l vars constraints =
-  let t = Profile.start_z3 () in
-  let result = call_z3' l vars constraints in
-  Profile.finish_z3 t;
+let call_smt l vars constraints =
+  let t = Profile.start_smt () in
+  let result = call_smt' l vars constraints in
+  Profile.finish_smt t;
   result
 
-let rec solve_z3 l vars constraints var =
-  let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
-  let z3_var = pp_sexpr (smt_var var) in
+let solve_smt l vars constraints var =
+  let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
+  let smt_var = pp_sexpr (smt_var var) in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file);
-     prerr_endline ("Solving for " ^ z3_var); *)
+  if !opt_smt_verbose then
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are (solve for %s): \n%s%!" smt_var smt_file)
+  else ();
 
   let rec input_all chan =
     try
@@ -259,27 +338,45 @@ let rec solve_z3 l vars constraints var =
       End_of_file -> []
   in
 
-  let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
-  output_string tmp_chan z3_file;
+  let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".smt2" in
+  output_string tmp_chan smt_file;
   close_out tmp_chan;
-  let z3_output =
+  let smt_output =
     try
-      let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-      let z3_output = String.concat " " (input_all z3_chan) in
-      let _ = Unix.close_process_in z3_chan in
-      z3_output
+      let smt_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+      let smt_output = String.concat " " (input_all smt_chan) in
+      let _ = Unix.close_process_in smt_chan in
+      smt_output
     with
     | exn ->
-       raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn))
+       raise (Reporting.err_general l ("Got error when calling smt: " ^ Printexc.to_string exn))
   in
   Sys.remove input_file;
-  let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in
+  let regexp = {|(define-fun |} ^ smt_var ^ {| () Int[ ]+\([0-9]+\))|} in
   try
-    let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in
-    let result = Big_int.of_string (Str.matched_group 1 z3_output) in
-    begin match call_z3 l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
-    | Unsat -> Some result
-    | _ -> None
-    end
+    let _ = Str.search_forward (Str.regexp regexp) smt_output 0 in
+    let result = Big_int.of_string (Str.matched_group 1 smt_output) in
+    Some result
   with
-    Not_found -> None
+  | Not_found -> None
+
+let solve_all_smt l vars constraints var =
+  let rec aux results =
+    let constraints = List.fold_left (fun ncs r -> (nc_and ncs (nc_neq (nconstant r) (nvar var)))) constraints results in
+    match solve_smt l vars constraints var with
+    | Some result -> aux (result :: results)
+    | None ->
+       match call_smt l vars constraints with
+       | Unsat -> Some results
+       | _ -> None
+  in
+  aux []
+
+let solve_unique_smt l vars constraints var =
+  match solve_smt l vars constraints var with
+  | Some result ->
+     begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
+     | Unsat -> Some result
+     | _ -> None
+     end
+  | None -> None
diff --git a/src/constraint.mli b/src/constraint.mli
index fa318c35..b5d6ff6b 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -54,11 +54,17 @@ open Ast_util
 
 val opt_smt_verbose : bool ref
 
+val set_solver : string -> unit
+
 type smt_result = Unknown | Sat | Unsat
 
 val load_digests : unit -> unit
 val save_digests : unit -> unit
 
-val call_z3 : l -> kind_aux KBindings.t -> n_constraint -> smt_result
+val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result
+
+val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
+
+val solve_all_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num list option
 
-val solve_z3 : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
+val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index c6fb0589..abe935b2 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -47,6 +47,10 @@ let opt_elf_threads = ref 1
 let opt_elf_entry = ref Big_int.zero
 let opt_elf_tohost = ref Big_int.zero
 
+(* the type of elf last loaded *)
+type elf_class = ELF_Class_64 | ELF_Class_32
+let opt_elf_class = ref ELF_Class_64 (* default *)
+
 type word8 = int
 
 let escape_char c =
@@ -66,14 +70,16 @@ let break n xs =
     | (_ :: _ as xs) -> helper ([Lem_list.take n xs] @ acc) (Lem_list.drop n xs)
   in helper [] xs
 
-let print_segment seg =
-  let bs = seg.Elf_interpreted_segment.elf64_segment_body in
+let print_segment bs =
   prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
   List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs))
 
+type elf_segs =
+  | ELF64 of Elf_interpreted_segment.elf64_interpreted_segment list
+  | ELF32 of Elf_interpreted_segment.elf32_interpreted_segment list
+
 let read name =
   let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
-
   prerr_endline "Elf read:";
   let (elf_file, elf_epi, symbol_map) =
     begin match info with
@@ -87,20 +93,18 @@ let read name =
        (elf_file, elf_epi, symbol_map)
     end
   in
-
   prerr_endline "\nElf segments:";
+
+  (* remove all the auto generated segments (they contain only 0s) *)
+  let prune_segments segs =
+    Lem_list.mapMaybe (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) segs in
   let (segments, e_entry, e_machine) =
     begin match elf_epi, elf_file with
-    | (Sail_interface.ELF_Class_32 _, _) -> failwith "cannot handle ELF_Class_32"
-    | (_, Elf_file.ELF_File_32 _)  -> failwith "cannot handle ELF_File_32"
-    | (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 f1) ->
-       (* remove all the auto generated segments (they contain only 0s) *)
-       let segments =
-         Lem_list.mapMaybe
-           (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None)
-           segments
-       in
-       (segments, e_entry, e_machine)
+    | (Sail_interface.ELF_Class_32 (segments, e_entry, e_machine), Elf_file.ELF_File_32 _) ->
+          (ELF32 (prune_segments segments), e_entry, e_machine)
+    | (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 _) ->
+          (ELF64 (prune_segments segments), e_entry, e_machine)
+    | (_, _) -> failwith "cannot handle ELF file"
     end
   in
   (segments, e_entry, symbol_map)
@@ -120,24 +124,20 @@ let write_file chan paddr i byte =
   output_string chan (Big_int.to_string (Big_int.add paddr (Big_int.of_int i)) ^ "\n");
   output_string chan (string_of_int byte ^ "\n")
 
-let load_segment ?writer:(writer=write_sail_lib) seg =
-  let open Elf_interpreted_segment in
-  let bs = seg.elf64_segment_body in
-  let paddr = seg.elf64_segment_paddr in
-  let base = seg.elf64_segment_base in
-  let offset = seg.elf64_segment_offset in
-  let size = seg.elf64_segment_size in
-  let memsz = seg.elf64_segment_memsz in
+let print_seg_info offset base paddr size memsz =
   prerr_endline "\nLoading Segment";
   prerr_endline ("Segment offset: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 offset)));
   prerr_endline ("Segment base address: " ^ (Big_int.to_string base));
   (* NB don't attempt to convert paddr to int64 because on MIPS it is quite likely to exceed signed
-     64-bit range e.g. addresses beginning 0x9.... Really need to_uint64 or to_string_hex but lem 
+     64-bit range e.g. addresses beginning 0x9.... Really need to_uint64 or to_string_hex but lem
      doesn't have them. *)
   prerr_endline ("Segment physical address: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 paddr)));
   prerr_endline ("Segment size: " ^  (Printf.sprintf "0x%Lx" (Big_int.to_int64 size)));
-  prerr_endline ("Segment memsz: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 memsz)));
-  print_segment seg;
+  prerr_endline ("Segment memsz: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 memsz)))
+
+let load_segment ?writer:(writer=write_sail_lib) bs paddr base offset size memsz =
+  print_seg_info offset base paddr size memsz;
+  print_segment bs;
   List.iteri (writer paddr) (List.rev_map int_of_char (List.rev (Byte_sequence.char_list_of_byte_sequence bs)));
   write_mem_zeros (Big_int.add paddr size) (Big_int.sub memsz size)
 
@@ -147,7 +147,32 @@ let load_elf ?writer:(writer=write_sail_lib) name =
   (if List.mem_assoc "tohost" symbol_map then
      let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
      opt_elf_tohost := tohost_addr);
-  List.iter (load_segment ~writer:writer) segments
+  (match segments with
+     | ELF64 segs ->
+           List.iter (fun seg ->
+                      let open Elf_interpreted_segment in
+                      let bs = seg.elf64_segment_body in
+                      let paddr = seg.elf64_segment_paddr in
+                      let base = seg.elf64_segment_base in
+                      let offset = seg.elf64_segment_offset in
+                      let size = seg.elf64_segment_size in
+                      let memsz = seg.elf64_segment_memsz in
+                      load_segment ~writer:writer bs paddr base offset size memsz)
+                     segs;
+           opt_elf_class := ELF_Class_64
+     | ELF32 segs ->
+           List.iter (fun seg ->
+                      let open Elf_interpreted_segment in
+                      let bs = seg.elf32_segment_body in
+                      let paddr = seg.elf32_segment_paddr in
+                      let base = seg.elf32_segment_base in
+                      let offset = seg.elf32_segment_offset in
+                      let size = seg.elf32_segment_size in
+                      let memsz = seg.elf32_segment_memsz in
+                      load_segment ~writer:writer bs paddr base offset size memsz)
+                     segs;
+           opt_elf_class := ELF_Class_32
+  )
 
 let load_binary ?writer:(writer=write_sail_lib) addr name =
   let f = open_in_bin name in
@@ -172,3 +197,5 @@ let load_binary ?writer:(writer=write_sail_lib) addr name =
 let elf_entry () = !opt_elf_entry
 (* Used by RISCV sail model test harness for exiting test *)
 let elf_tohost () = !opt_elf_tohost
+(* Used to check last loaded elf class. *)
+let elf_class () = !opt_elf_class
diff --git a/src/initial_check.ml b/src/initial_check.ml
index f728d92d..33844a72 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -595,7 +595,7 @@ let to_ast_typschm_opt ctx (P.TypSchm_opt_aux(aux,l)) : tannot_opt ctx_out =
 
 let to_ast_effects_opt (P.Effect_opt_aux(e,l)) : effect_opt =
   match e with
-  | P.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
+  | P.Effect_opt_none -> Effect_opt_aux(Effect_opt_none,l)
   | P.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects typ),l)
 
 let to_ast_funcl ctx (P.FCL_aux(fcl,l) : P.funcl) : (unit funcl) =
@@ -824,15 +824,15 @@ let val_spec_ids (Defs defs) =
   IdSet.of_list (vs_ids defs)
 
 let quant_item_param = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))]
   | _ -> []
 let quant_item_typ = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))]
   | _ -> []
 let quant_item_arg = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))]
   | _ -> []
 let undefined_typschm id typq =
diff --git a/src/isail.ml b/src/isail.ml
index e513e0ee..9a300673 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -294,7 +294,7 @@ let load_session upto file =
   | Some upto_file when Filename.basename upto_file = file -> None
   | Some upto_file ->
      let (_, ast, env) =
-       load_files ~generate:false !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
+       load_files ~check:true !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
      in
      Interactive.ast := append_ast !Interactive.ast ast;
      Interactive.env := env;
@@ -376,7 +376,7 @@ let handle_input' input =
         List.iter print_endline commands
      | ":poly" ->
         let is_kopt = match arg with
-          | "Int" -> is_nat_kopt
+          | "Int" -> is_int_kopt
           | "Type" -> is_typ_kopt
           | "Order" -> is_order_kopt
           | _ -> failwith "Invalid kind"
@@ -392,7 +392,7 @@ let handle_input' input =
           | Arg.Bad message | Arg.Help message -> print_endline message
         end;
      | ":spec" ->
-        let ast, env = Specialize.specialize !Interactive.ast !Interactive.env in
+        let ast, env = Specialize.(specialize' 1 int_specialization !Interactive.ast !Interactive.env) in
         Interactive.ast := ast;
         Interactive.env := env;
         interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
@@ -402,7 +402,7 @@ let handle_input' input =
         let open PPrint in
         let open C_backend in
         let ast = Process_file.rewrite_ast_c !Interactive.env !Interactive.ast in
-        let ast, env = Specialize.specialize ast !Interactive.env in
+        let ast, env = Specialize.(specialize typ_ord_specialization ast !Interactive.env) in
         let ctx = initial_ctx env in
         interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast
      | ":ir" ->
@@ -492,7 +492,7 @@ let handle_input' input =
            begin
              try
                load_into_session arg;
-               let (_, ast, env) = load_files !Interactive.env [arg] in
+               let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in
                Interactive.ast := append_ast !Interactive.ast ast;
                interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops;
                Interactive.env := env;
diff --git a/src/latex.ml b/src/latex.ml
index a0660daa..1806da47 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -71,20 +71,23 @@ type latex_state =
   { mutable noindent : bool;
     mutable this : id option;
     mutable norefs : StringSet.t;
-    mutable generated_names : string Bindings.t
+    mutable generated_names : string Bindings.t;
+    mutable commands : StringSet.t
   }
 
 let reset_state state =
   state.noindent <- false;
   state.this <- None;
   state.norefs <- StringSet.empty;
-  state.generated_names <- Bindings.empty
+  state.generated_names <- Bindings.empty;
+  state.commands <- StringSet.empty
 
 let state =
   { noindent = false;
     this = None;
     norefs = StringSet.empty;
-    generated_names = Bindings.empty
+    generated_names = Bindings.empty;
+    commands = StringSet.empty
   }
 
 let rec unique_postfix n =
@@ -285,24 +288,39 @@ let add_links str =
   in
   Str.global_substitute r subst str
 
+let rec skip_lines in_chan = function
+  | n when n <= 0 -> ()
+  | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1)
+
+let rec read_lines in_chan = function
+  | n when n <= 0 -> []
+  | n ->
+     let l = input_line in_chan in
+     let ls = read_lines in_chan (n - 1) in
+     l :: ls
+
 let latex_loc no_loc l =
-  match l with
-  | Parse_ast.Range (_, _) | Parse_ast.Documented (_, Parse_ast.Range (_, _)) ->
+  match simp_loc l with
+  | Some (p1, p2) ->
      begin
-       let using_color = !Util.opt_colors in
-       Util.opt_colors := false;
-       let code = Util.split_on_char '\n' (Reporting.loc_to_string l) in
-       let doc = match code with
-         | _ :: _ :: code -> string (add_links (String.concat "\n" code))
-         | _ -> empty
-       in
-       Util.opt_colors := using_color;
-       doc ^^ hardline
+       let open Lexing in
+       try
+         let in_chan = open_in p1.pos_fname in
+         try
+           skip_lines in_chan (p1.pos_lnum - 3);
+           let code = read_lines in_chan ((p2.pos_lnum - p1.pos_lnum) + 3) in
+           close_in in_chan;
+           let doc = match code with
+             | _ :: _ :: code -> string (add_links (String.concat "\n" code))
+             | _ -> empty
+           in
+           doc ^^ hardline
+         with
+         | _ -> close_in_noerr in_chan; docstring l ^^ no_loc
+       with
+       | _ -> docstring l ^^ no_loc
      end
-
-  | _ -> docstring l ^^ no_loc
-
-let commands = ref StringSet.empty
+  | None -> docstring l ^^ no_loc
 
 let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) =
   Pretty_print_sail.doc_id id ^^ space
@@ -322,10 +340,17 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
   let doc = if cat = Val then no_loc else latex_loc no_loc l in
   output_string chan (Pretty_print_sail.to_string doc);
   close_out chan;
+  let command = sprintf "\\%s%s%s" !opt_prefix (category_name cat) (latex_id id) in
+  if StringSet.mem command state.commands then
+    (Util.warn ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty)
+  else
+    begin
+      state.commands <- StringSet.add command state.commands;
 
-  ksprintf string "\\newcommand{\\%s%s%s}{\\phantomsection%s\\saildoc%s{" !opt_prefix (category_name cat) (latex_id id) labelling (category_name_simple cat)
-  ^^ docstring l ^^ string "}{"
-  ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file)
+      ksprintf string "\\newcommand{%s}{\\phantomsection%s\\saildoc%s{" command labelling (category_name_simple cat)
+      ^^ docstring l ^^ string "}{"
+      ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file)
+    end
 
 let latex_label str id =
   string (Printf.sprintf "\\label{%s:%s}" str (Util.zencode_string (string_of_id id)))
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 3167ad6b..c67b4fcb 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -201,7 +201,7 @@ let rec is_value (E_aux (e,(l,annot))) =
 
 let is_pure (Effect_opt_aux (e,_)) =
   match e with
-  | Effect_opt_pure -> true
+  | Effect_opt_none -> true
   | Effect_opt_effect (Effect_aux (Effect_set [],_)) -> true
   | _ -> false
 
@@ -2263,7 +2263,7 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
       prove __POS__ env (NC_aux (NC_equal (size,nexp), Parse_ast.Unknown))
     in
     if is_nexp_constant size then size else
-      match solve env size with
+      match solve_unique env size with
       | Some n -> nconstant n
       | None ->
          match List.find is_equal bound_nexps with
@@ -2930,7 +2930,7 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
   | _ -> None
 
 let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
-  match solve typ_env nexp with
+  match solve_unique typ_env nexp with
   | Some n -> nconstant n
   | None ->
      let is_equal kid =
@@ -3691,7 +3691,7 @@ let rec rewrite_app env typ (id,args) =
     let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
     match size with
     | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp)
-    | _ -> match solve env size with
+    | _ -> match solve_unique env size with
       | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp)
       | None -> e
   in
@@ -3711,7 +3711,7 @@ let rec rewrite_app env typ (id,args) =
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in begin
-         match solve env midsize with
+         match solve_unique env midsize with
          | Some c ->
             let midtyp = vector_typ (nconstant c) order bittyp in
             E_app (append,
@@ -3739,7 +3739,7 @@ let rec rewrite_app env typ (id,args) =
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in begin
-         match solve env midsize with
+         match solve_unique env midsize with
          | Some c ->
             let midtyp = vector_typ (nconstant c) order bittyp in
             E_app (append,
@@ -3797,7 +3797,7 @@ let rec rewrite_app env typ (id,args) =
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in begin
-         match solve env midsize with
+         match solve_unique env midsize with
          | Some c ->
             let midtyp = vector_typ (nconstant c) order bittyp in
             try_cast_to_typ
@@ -4000,7 +4000,7 @@ struct
 
 let simplify_size_nexp env quant_kids nexp =
   let rec aux (Nexp_aux (ne,l) as nexp) =
-    match solve env nexp with
+    match solve_unique env nexp with
     | Some n -> Some (nconstant n)
     | None ->
        let is_equal kid =
@@ -4191,7 +4191,7 @@ let fill_in_type env typ =
     | K_order
     | K_bool -> subst
     | K_int ->
-       (match solve env (nvar kid) with
+       (match solve_unique env (nvar kid) with
        | None -> subst
        | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in
   subst_src_typ subst typ
@@ -4300,7 +4300,7 @@ let add_bitvector_casts (Defs defs) =
   let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann)) =
     let fcl_env = env_of_annot fcl_ann in
     let (tq,typ) = Env.get_val_spec_orig id fcl_env in
-    let quant_kids = List.map kopt_kid (List.filter is_nat_kopt (quant_kopts tq)) in
+    let quant_kids = List.map kopt_kid (List.filter is_int_kopt (quant_kopts tq)) in
     let ret_typ =
       match typ with
       | Typ_aux (Typ_fn (_,ret,_),_) -> ret
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index ba21dd0a..f42a279b 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -716,13 +716,12 @@ let ocaml_pp_generators ctx defs orig_types required =
   and add_req_from_typarg required (A_aux (arg,_)) =
     match arg with
     | A_typ typ -> add_req_from_typ required typ
-    | A_nexp _
-    | A_order _
-      -> required
+    | A_nexp _ | A_order _ | A_bool _ -> required
   and add_req_from_td required (TD_aux (td,(l,_))) =
     match td with
     | TD_abbrev (_, _, A_aux (A_typ typ, _)) ->
        add_req_from_typ required typ
+    | TD_abbrev _ -> required
     | TD_record (_, _, fields, _) ->
        List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields
     | TD_variant (_, _, variants, _) ->
@@ -751,13 +750,13 @@ let ocaml_pp_generators ctx defs orig_types required =
     let gen_tyvars = List.map (fun k -> kopt_kid k |> zencode_kid)
                        (List.filter is_typ_kopt tquants) in
     let print_quant kindedid =
-      if is_nat_kopt kindedid then string "int" else
+      if is_int_kopt kindedid then string "int" else
       if is_order_kopt kindedid then string "bool" else
       parens (separate space [string "generators"; string "->"; zencode_kid (kopt_kid kindedid)])
     in
     let name = "gen_" ^ type_name id in
     let make_tyarg kindedid =
-      if is_nat_kopt kindedid
+      if is_int_kopt kindedid
       then mk_typ_arg (A_nexp (nvar (kopt_kid kindedid)))
       else if is_order_kopt kindedid
       then mk_typ_arg (A_order (mk_ord (Ord_var (kopt_kid kindedid))))
@@ -793,7 +792,7 @@ let ocaml_pp_generators ctx defs orig_types required =
                                        | _ -> space ^^ separate space args_pp
         in
         string ("g.gen_" ^ typ_str) ^^ args_pp
-      and typearg (A_aux (arg,_)) =
+      and typearg (A_aux (arg,l)) =
         match arg with
         | A_nexp (Nexp_aux (nexp,l) as full_nexp) ->
            (match nexp with
@@ -807,6 +806,7 @@ let ocaml_pp_generators ctx defs orig_types required =
             | Ord_inc -> string "true"
             | Ord_dec -> string "false")
         | A_typ typ -> parens (string "fun g -> " ^^ gen_type typ)
+        | A_bool nc -> raise (Reporting.err_todo l ("Unsupported constraint for generators: " ^ string_of_n_constraint nc))
       in
       let make_subgen (Typ_aux (typ,l) as full_typ) =
         let typ_str, args_pp =
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 5f0d7487..b86d4dd5 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -324,7 +324,7 @@ typschm_opt =
 
 type 
 effect_opt_aux =  (* Optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
+   Effect_opt_none (* sugar for empty effect set *)
  | Effect_opt_effect of atyp
 
 
diff --git a/src/parser.mly b/src/parser.mly
index 2cd0dbe1..9f7e2e0c 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,7 +133,7 @@ let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
 let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
 let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
-let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
+let mk_eannotn = Effect_opt_aux(Effect_opt_none,Unknown)
 
 let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
 
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 46d07cc3..adb00a77 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -370,6 +370,34 @@ let doc_nc_fn id =
   | "not" -> string "negb"
   | s -> string s
 
+type ex_atom_bool = ExBool_simple | ExBool_val of bool | ExBool_complex
+
+let non_trivial_ex_atom_bool l kopts nc atom_nc =
+  let vars = KOptSet.union (kopts_of_constraint nc) (kopts_of_constraint atom_nc) in
+  let exists = KOptSet.of_list kopts in
+  if KOptSet.subset vars exists then
+    let kenv = List.fold_left (fun kenv kopt -> KBindings.add (kopt_kid kopt) (unaux_kind (kopt_kind kopt)) kenv) KBindings.empty kopts in
+    match Constraint.call_smt l kenv (nc_and nc atom_nc),
+          Constraint.call_smt l kenv (nc_and nc (nc_not atom_nc)) with
+    | Sat, Sat -> ExBool_simple
+    | Sat, Unsat -> ExBool_val true
+    | Unsat, Sat -> ExBool_val false
+    | _ -> ExBool_complex
+  else ExBool_complex
+
+type ex_kind = ExNone | ExBool | ExGeneral
+
+let classify_ex_type (Typ_aux (t,l) as t0) =
+  match t with
+  | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin
+      match non_trivial_ex_atom_bool l kopts nc atom_nc with
+      | ExBool_simple -> ExNone, t1
+      | ExBool_val _ -> ExBool, t1
+      | ExBool_complex -> ExGeneral, t1
+    end
+  | Typ_exist (_,_,t1) -> ExGeneral,t1
+  | _ -> ExNone,t0
+
 (* When making changes here, check whether they affect coq_nvars_of_typ *)
 let rec doc_typ_fns ctx =
   (* following the structure of parser for precedence *)
@@ -476,13 +504,18 @@ let rec doc_typ_fns ctx =
                        [doc_var ctx var; colon; tpp;
                         ampersand;
                         doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc])
-          | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) ->
-             let var = mk_kid "_bool" in (* TODO collision avoid *)
-             let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
-             braces (separate space
-                       [doc_var ctx var; colon; string "bool";
-                        ampersand;
-                        doc_arithfact ctx ~exists:(List.map kopt_kid kopts) nc])
+          | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin
+             match non_trivial_ex_atom_bool l kopts nc atom_nc with
+             | ExBool_simple -> string "bool"
+             | ExBool_val t -> string "Bool(" ^^ if t then string "True)" else string "False)"
+             | ExBool_complex ->
+                let var = mk_kid "_bool" in (* TODO collision avoid *)
+                let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
+                braces (separate space
+                          [doc_var ctx var; colon; string "bool";
+                           ampersand;
+                           doc_arithfact ctx ~exists:(List.map kopt_kid kopts) nc])
+            end
           | _ ->
              raise (Reporting.err_todo l
                   ("Non-atom existential type not yet supported in Coq: " ^
@@ -1034,9 +1067,14 @@ let doc_exp, doc_let =
       let typ = expand_range_type typ in
       match destruct_exist_plain typ with
       | None -> epp
+      | Some (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l)) -> begin
+          match non_trivial_ex_atom_bool l kopts nc atom_nc with
+          | ExBool_simple -> epp
+          | ExBool_val t -> wrap_parens (string "build_Bool" ^/^ epp)
+          | ExBool_complex -> wrap_parens (string "build_ex" ^/^ epp)
+        end
       | Some _ ->
-         let epp = string "build_ex" ^/^ epp in
-         if aexp_needed then parens epp else epp
+         wrap_parens (string "build_ex" ^/^ epp)
     in
     let rec construct_dep_pairs env =
       let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) =
@@ -1049,8 +1087,14 @@ let doc_exp, doc_let =
            let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in
            let build_ex, out_typ =
              match destruct_exist_plain typ' with
-             | Some (_,_,t) -> true, t
-             | None -> false, typ'
+             | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin
+                 match non_trivial_ex_atom_bool l kopts nc atom_nc with
+                 | ExBool_simple -> None, t
+                 | ExBool_val _ -> Some "build_Bool", t
+                 | ExBool_complex -> Some "build_ex", t
+               end
+             | Some (_,_,t) -> Some "build_ex", t
+             | None -> None, typ'
            in
            let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in
            let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in
@@ -1063,16 +1107,17 @@ let doc_exp, doc_let =
                   not (similar_nexps ctxt (env_of exp) n1 n2)
                | _ -> false
            in
-           let exp_pp = expV (want_parens || autocast || build_ex) exp in
+           let exp_pp = expV (want_parens || autocast || Util.is_some build_ex) exp in
            let exp_pp =
              if autocast then
                let exp_pp = string "autocast" ^^ space ^^ exp_pp in
-               if want_parens || build_ex then parens exp_pp else exp_pp
+               if want_parens || Util.is_some build_ex then parens exp_pp else exp_pp
              else exp_pp
-           in if build_ex then
-                let exp_pp = string "build_ex" ^^ space ^^ exp_pp in
+           in match build_ex with
+              | Some s ->
+                let exp_pp = string s ^^ space ^^ exp_pp in
                 if want_parens then parens exp_pp else exp_pp
-              else exp_pp
+              | None -> exp_pp
       in aux
     in
     let liftR doc =
@@ -1162,7 +1207,7 @@ let doc_exp, doc_let =
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "None", _) as none -> doc_id_ctor none
-       | Id_aux (Id "foreach", _) ->
+       | Id_aux (Id "foreach#", _) ->
           begin
             match args with
             | [from_exp; to_exp; step_exp; ord_exp; vartuple; body] ->
@@ -1209,7 +1254,8 @@ let doc_exp, doc_let =
           | _ -> raise (Reporting.err_unreachable l __POS__
              "Unexpected number of arguments for loop combinator")
           end
-       | Id_aux (Id (("while" | "until") as combinator), _) ->
+       | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+          let combinator = String.sub combinator 0 (String.length combinator - 1) in
           begin
             match args with
             | [cond; varstuple; body] ->
@@ -1499,21 +1545,9 @@ let doc_exp, doc_let =
          debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ));
          debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ))
        in
-       let outer_ex,outer_typ' =
-         match outer_typ with
-         | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-         | t1 -> false,t1
-       in
-       let cast_ex,cast_typ' =
-         match cast_typ with
-         | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-         | t1 -> false,t1
-       in
-       let inner_ex,inner_typ' =
-         match inner_typ with
-         | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-         | t1 -> false,t1
-       in
+       let outer_ex,outer_typ' = classify_ex_type outer_typ in
+       let cast_ex,cast_typ' = classify_ex_type cast_typ in
+       let inner_ex,inner_typ' = classify_ex_type inner_typ in
        let autocast =
                 (* Avoid using helper functions which simplify the nexps *)
          is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
@@ -1526,30 +1560,34 @@ let doc_exp, doc_let =
        let effects = effectful (effect_of e) in
        let epp =
          if effects then
-           if inner_ex then
-             if cast_ex
-             (* If the types are the same use the cast as a hint to Coq,
-                otherwise derive the new type from the old one. *)
-             then if alpha_equivalent env inner_typ cast_typ
-                  then epp
-                  else string "derive_m" ^^ space ^^ epp
-             else string "projT1_m" ^^ space ^^ epp
-           else if cast_ex
-           then string "build_ex_m" ^^ space ^^ epp
-           else epp
-         else if cast_ex
-         then string "build_ex" ^^ space ^^ epp
-         else epp
+           match inner_ex, cast_ex with
+           | ExGeneral, ExGeneral ->
+              (* If the types are the same use the cast as a hint to Coq,
+                 otherwise derive the new type from the old one. *)
+              if alpha_equivalent env inner_typ cast_typ
+              then epp
+              else string "derive_m" ^^ space ^^ epp
+           | ExGeneral, ExNone ->
+              string "projT1_m" ^^ space ^^ epp
+           | ExNone, ExGeneral ->
+              string "build_ex_m" ^^ space ^^ epp
+           | ExNone, ExNone -> epp
+         else match cast_ex with
+              | ExGeneral -> string "build_ex" ^^ space ^^ epp
+              | ExBool -> string "build_Bool" ^^ space ^^ epp
+              | ExNone -> epp
        in
        let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in
        let epp =
          if effects then
-           if cast_ex && not outer_ex
-           then string "projT1_m" ^^ space ^^ parens epp
-           else epp
-         else if cast_ex
-         then string "projT1" ^^ space ^^ parens epp
-         else epp
+           match cast_ex, outer_ex with
+           | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp
+           | ExBool, ExNone -> string "projBool_m" ^^ space ^^ parens epp
+           | _ -> epp
+         else match cast_ex with
+              | ExGeneral -> string "projT1" ^^ space ^^ parens epp
+              | ExBool -> string "projBool" ^^ space ^^ parens epp
+              | ExNone -> epp
        in
        let epp =
          if autocast then
@@ -1718,10 +1756,10 @@ let doc_exp, doc_let =
                 | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_)
                     when not (is_enum (env_of e1) id) ->
                       let full_typ = (expand_range_type typ) in
-                      let binder = match destruct_exist_plain (Env.expand_synonyms (env_of e1) full_typ) with
-                        | Some _ ->
+                      let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with
+                        | ExGeneral, _ ->
                            squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
-                        | _ ->
+                        | (ExBool | ExNone), _ ->
                            parens (separate space [doc_id id; colon; doc_typ ctxt typ])
                       in separate space [string ">>= fun"; binder; bigarrow]
                 | _ ->
@@ -1775,6 +1813,10 @@ let doc_exp, doc_let =
       | E_aux (E_if (c', t', e'), _)
       | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) ->
          if_exp ctxt true c' t' e'
+      (* Special case to prevent current arm decoder becoming a staircase *)
+      (* TODO: replace with smarter pretty printing *)
+      | E_aux (E_internal_plet (pat,exp1,E_aux (E_cast (typ, (E_aux (E_if (_, _, _), _) as exp2)),_)),ann) when Typ.compare typ unit_typ == 0 ->
+         string "else" ^/^ top_exp ctxt false (E_aux (E_internal_plet (pat,exp1,exp2),ann))
       | _ -> prefix 2 1 (string "else") (top_exp ctxt false e)
     in
     (prefix 2 1
@@ -2200,9 +2242,10 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
   in
   let build_ex, ret_typ = replace_atom_return_type ret_typ in
-  let build_ex = match destruct_exist_plain (Env.expand_synonyms env (expand_range_type ret_typ)) with
-    | Some _ -> Some "build_ex"
-    | _ -> build_ex
+  let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with
+    | ExGeneral, _ -> Some "build_ex"
+    | ExBool, _ -> Some "build_Bool"
+    | ExNone, _ -> build_ex
   in
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
@@ -2469,7 +2512,7 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
      let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in
      let tqs = match tqs with
        | TypQ_aux (TypQ_tq qs,l) -> TypQ_aux (TypQ_tq (List.filter (function
-         | QI_aux (QI_id kopt,_) when is_nat_kopt kopt ->
+         | QI_aux (QI_id kopt,_) when is_int_kopt kopt ->
             let kid = kopt_kid kopt in
             KidSet.mem kid used && not (KidSet.mem kid args)
          | _ -> true) qs),l)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index aa03528f..6adcec46 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -316,7 +316,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
           * if we add a new Typ constructor *)
          let tpp = typ ty in
          if atyp_needed then parens tpp else tpp
-      | Typ_exist (kopts,_,ty) when List.for_all is_nat_kopt kopts -> begin
+      | Typ_exist (kopts,_,ty) when List.for_all is_int_kopt kopts -> begin
          let kids = List.map kopt_kid kopts in
          let tpp = typ ty in
          let visible_vars = lem_tyvars_of_typ ty in
@@ -359,7 +359,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp =
          Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       match Type_check.solve env size with
+       match Type_check.solve_unique env size with
        | Some n -> mk_typ (nconstant n)
        | None ->
           let is_equal nexp =
@@ -668,7 +668,7 @@ let doc_exp_lem, doc_let_lem =
           let call = doc_id_lem (append_id f "M") in
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
-       | Id_aux (Id "foreach", _) ->
+       | Id_aux (Id "foreach#", _) ->
           begin
             match args with
             | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
@@ -713,7 +713,8 @@ let doc_exp_lem, doc_let_lem =
           | _ -> raise (Reporting.err_unreachable l __POS__
             "Unexpected number of arguments for loop combinator")
           end
-       | Id_aux (Id (("while" | "until") as combinator), _) ->
+       | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+          let combinator = String.sub combinator 0 (String.length combinator - 1) in
           begin
             match args with
             | [cond; varstuple; body] ->
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 67f291bd..56026c81 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -66,7 +66,7 @@ let doc_id (Id_aux (id_aux, _)) =
 let doc_kid kid = string (Ast_util.string_of_kid kid)
 
 let doc_kopt = function
-  | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
+  | kopt when is_int_kopt kopt -> doc_kid (kopt_kid kopt)
   | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
   | kopt when is_order_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
   | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])
@@ -213,7 +213,7 @@ and doc_arg_typs = function
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
+    | QI_id kopt when is_int_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
     | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
     | QI_id kopt when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])]
     | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
@@ -234,7 +234,7 @@ let doc_quants quants =
 let doc_param_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
+    | QI_id kopt when is_int_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
     | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
     | QI_id kopt when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"]
     | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
@@ -619,8 +619,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | TD_variant (id, TypQ_aux (TypQ_tq qs, _), unions, _) ->
      separate space [string "union"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
-  | _ -> string "TYPEDEF"
-
+  | TD_bitfield _ -> string "BITFIELD" (* should be rewritten *)
 
 let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
   let doc_extern ext =
@@ -654,6 +653,12 @@ let rec doc_scattered (SD_aux (sd_aux, _)) =
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id
   | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) ->
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants
+  | SD_mapcl (id, mapcl) ->
+     separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl]
+  | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_none, _)) ->
+     separate space [string "scattered mapping"; doc_id id]
+  | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_some (_, typ), _)) ->
+     separate space [string "scattered mapping"; doc_id id; string ":"; doc_typ typ]
   | SD_unioncl (id, tu) ->
      separate space [string "union clause"; doc_id id; equals; doc_union tu]
 
diff --git a/src/process_file.ml b/src/process_file.ml
index d2a43b4a..3c2d4a22 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -159,7 +159,7 @@ let rec preprocess opts = function
      symbols := StringSet.add symbol !symbols;
      preprocess opts defs
 
-  | Parse_ast.DEF_pragma ("option", command, l) :: defs ->
+  | (Parse_ast.DEF_pragma ("option", command, l) as opt_pragma) :: defs ->
      begin
        try
          let args = Str.split (Str.regexp " +") command in
@@ -167,7 +167,7 @@ let rec preprocess opts = function
        with
        | Arg.Bad message | Arg.Help message -> raise (Reporting.err_general l message)
      end;
-     preprocess opts defs
+     opt_pragma :: preprocess opts defs
 
   | Parse_ast.DEF_pragma ("ifndef", symbol, l) :: defs ->
      let then_defs, else_defs, defs = cond_pragma l defs in
diff --git a/src/profile.ml b/src/profile.ml
index 1a8bd30b..f64bdfe0 100644
--- a/src/profile.ml
+++ b/src/profile.ml
@@ -51,13 +51,13 @@
 let opt_profile = ref false
 
 type profile = {
-    z3_calls : int;
-    z3_time : float
+    smt_calls : int;
+    smt_time : float
   }
 
 let new_profile = {
-    z3_calls = 0;
-    z3_time = 0.0
+    smt_calls = 0;
+    smt_time = 0.0
   }
 
 let profile_stack = ref []
@@ -68,12 +68,12 @@ let update_profile f =
   | (p :: ps) ->
      profile_stack := f p :: ps
 
-let start_z3 () =
-  update_profile (fun p -> { p with z3_calls = p.z3_calls + 1 });
+let start_smt () =
+  update_profile (fun p -> { p with smt_calls = p.smt_calls + 1 });
   Sys.time ()
 
-let finish_z3 t =
-  update_profile (fun p -> { p with z3_time = p.z3_time +. (Sys.time () -. t) })
+let finish_smt t =
+  update_profile (fun p -> { p with smt_time = p.smt_time +. (Sys.time () -. t) })
 
 let start () =
   profile_stack := new_profile :: !profile_stack;
@@ -84,7 +84,7 @@ let finish msg t =
     begin match !profile_stack with
     | p :: ps ->
        prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profiled" |> magenta |> clear) msg (Sys.time () -. t));
-       prerr_endline (Printf.sprintf "  Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time);
+       prerr_endline (Printf.sprintf "  SMT calls: %d, SMT time: %fs" p.smt_calls p.smt_time);
        profile_stack := ps
     | [] -> ()
     end
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 44d99537..d4601fa6 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1549,10 +1549,11 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex
        | None -> Pat_aux (Pat_exp (pat', body'), annot'))
      | Pat_aux (Pat_when (pat,guard,body),annot') ->
        let (pat',(guard',decls,_)) = remove_bitvector_pat pat in
+       let guard'' = rewrite_rec guard in
        let body' = decls (rewrite_rec body) in
        (match guard' with
-       | Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp (decls guard) guard', body'), annot')
-       | None -> Pat_aux (Pat_when (pat', (decls guard), body'), annot')) in
+       | Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp (decls guard'') guard', body'), annot')
+       | None -> Pat_aux (Pat_when (pat', (decls guard''), body'), annot')) in
     rewrap (E_case (e, List.map rewrite_pexp ps))
   | E_let (LB_aux (LB_val (pat,v),annot'),body) ->
      let (pat,(_,decls,_)) = remove_bitvector_pat pat in
@@ -3105,7 +3106,7 @@ let construct_toplevel_string_append_func env f_id pat =
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
   let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
-  let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+  let effect_none = (Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown)) in
   let s_id = fresh_stringappend_id () in
   let arg_pat = mk_pat (P_id s_id) in
   (* We can ignore guards here because we've already removed them *)
@@ -3210,7 +3211,7 @@ let construct_toplevel_string_append_func env f_id pat =
   in
   let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit])))) in
   let new_match = mk_exp (E_case (mk_exp (E_id s_id), [strip_pexp new_pexp; wildcard])) in
-  let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl f_id arg_pat new_match]), (unk,())) in
+  let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl f_id arg_pat new_match]), (unk,())) in
   let new_fun_def, env = Type_check.check_fundef env new_fun_def in
   List.flatten [new_val_spec; new_fun_def]
 
@@ -3525,7 +3526,11 @@ let rewrite_defs_mapping_patterns env =
        let mapping_in_typ = typ_of_annot p_annot in
 
        let x = Env.get_val_spec mapping_id env in
-       let (_, Typ_aux(Typ_bidir(typ1, typ2), _)) = x in
+
+       let typ1, typ2 = match x with
+         | (_, Typ_aux(Typ_bidir(typ1, typ2), _)) -> typ1, typ2
+         | (_, typ) -> raise (Reporting.err_unreachable (fst p_annot) __POS__ ("Must be bi-directional mapping: " ^ string_of_typ typ))
+       in
 
        let mapping_direction =
          if mapping_in_typ = typ1 then
@@ -3822,7 +3827,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        let v =
          fix_eff_exp (annot_exp (E_let (lb_lower,
            fix_eff_exp (annot_exp (E_let (lb_upper,
-             fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body]))
+             fix_eff_exp (annot_exp (E_app (mk_id "foreach#", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body]))
                el env (typ_of exp4))))
              el env (typ_of exp4))))
            el env (typ_of exp4)) in
@@ -3838,8 +3843,8 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
         let body = rewrite_var_updates (add_vars overwrite body vars) in
         let (E_aux (_,(_,bannot))) = body in
         let fname = match loop with
-          | While -> "while"
-          | Until -> "until" in
+          | While -> "while#"
+          | Until -> "until#" in
         let funcl = Id_aux (Id fname,gen_loc el) in
         let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]), (gen_loc el, bannot)) in
         Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
@@ -4140,9 +4145,9 @@ let rewrite_defs_remove_superfluous_returns env =
 
 let rewrite_defs_remove_e_assign env (Defs defs) =
   let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
-    [("foreach", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
-     ("while", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
-     ("until", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
+    [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
+     ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
+     ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
   let rewrite_exp _ e =
     replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
   rewrite_defs_base
@@ -4334,7 +4339,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
 
     let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
-    let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+    let effect_none = (Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown)) in
     (* We need to make sure we get the environment for the last mapping clause *)
     let env = match List.rev mapcls with
       | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot
@@ -4368,10 +4373,10 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let forwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
     let backwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
 
-    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
-    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
-    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
-    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
+    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
+    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
+    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
+    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
 
     typ_debug (lazy (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string)));
     typ_debug (lazy (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string)));
@@ -4390,7 +4395,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
               let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
-              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
+              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
               typ_debug (lazy (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string)));
               let forwards_prefix_fun, _ = Type_check.check_fundef env forwards_prefix_fun in
               forwards_prefix_spec @ forwards_prefix_fun
@@ -4400,7 +4405,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
                 let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
-                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
+                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
                 typ_debug (lazy (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string)));
                 let backwards_prefix_fun, _ = Type_check.check_fundef env backwards_prefix_fun in
                 backwards_prefix_spec @ backwards_prefix_fun
@@ -4642,8 +4647,11 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
         rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
   end
   | P_record _ ->
-     raise (Reporting.err_unreachable (fst ann) __POS__
-              "Record pattern not supported")
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Record pattern not supported")
+  | P_or _ ->
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Or pattern not supported")
+  | P_not _ ->
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Negated pattern not supported")
   | P_vector _
   | P_vector_concat _
   | P_string_append _ ->
@@ -4929,7 +4937,7 @@ let rewrite_explicit_measure env (Defs defs) =
         match Bindings.find id measures with
         | (measure_pat, measure_exp) ->
            let e = match e with
-             | Effect_opt_aux (Effect_opt_pure, _) ->
+             | Effect_opt_aux (Effect_opt_none, _) ->
                 Effect_opt_aux (Effect_opt_effect (mk_effect [BE_escape]), loc)
              | Effect_opt_aux (Effect_opt_effect eff,_) ->
                 Effect_opt_aux (Effect_opt_effect (add_escape eff), loc)
@@ -5164,10 +5172,21 @@ let rewrite_defs_ocaml = [
 
 let rewrite_defs_c = [
   ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
+
+  (* Remove bidirectional mappings *)
   ("realise_mappings", rewrite_defs_realise_mappings);
   ("toplevel_string_append", rewrite_defs_toplevel_string_append);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("mapping_builtins", rewrite_defs_mapping_patterns);
+
+  (* Monomorphisation *)
+  ("mono_rewrites", if_mono mono_rewrites);
+  ("recheck_defs", if_mono recheck_defs);
+  ("rewrite_toplevel_nexps", if_mono rewrite_toplevel_nexps);
+  ("monomorphise", if_mono monomorphise);
+  ("rewrite_atoms_to_singletons", if_mono (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
+  ("recheck_defs", if_mono recheck_defs);
+
   ("rewrite_undefined", rewrite_undefined_if_gen false);
   ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
   ("remove_not_pats", rewrite_defs_not_pats);
diff --git a/src/sail.ml b/src/sail.ml
index f481eb7b..edf1bda4 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -65,7 +65,7 @@ let opt_print_c = ref false
 let opt_print_latex = ref false
 let opt_print_coq = ref false
 let opt_print_cgen = ref false
-let opt_memo_z3 = ref true
+let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
 let opt_libs_lem = ref ([]:string list)
@@ -117,9 +117,15 @@ let options = Arg.align ([
   ( "-ocaml_generators",
     Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
     "<types> produce random generators for the given types");
+  ( "-smt_solver",
+    Arg.String (fun s -> Constraint.set_solver (String.trim s)),
+    "<solver> choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices.");
+  ( "-smt_linearize",
+    Arg.Set Type_check.opt_smt_linearize,
+    "(experimental) force linearization for constraints involving exponentials");
   ( "-latex",
-    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
-    " pretty print the input to latex");
+    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec],
+    " pretty print the input to LaTeX");
   ( "-latex_prefix",
     Arg.String (fun prefix -> Latex.opt_prefix := prefix),
     " set a custom prefix for generated LaTeX macro command (default sail)");
@@ -216,7 +222,7 @@ let options = Arg.align ([
     " memoize calls to z3, improving performance when typechecking repeatedly (default)");
   ( "-no_memo_z3",
     Arg.Clear opt_memo_z3,
-    " do not memoize calls to z3");
+    " do not memoize calls to z3 (default)");
   ( "-memo",
     Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache],
     " memoize calls to z3, and intermediate compilation results");
@@ -276,7 +282,7 @@ let options = Arg.align ([
     "<verbosity> (debug) verbose typechecker output: 0 is silent");
   ( "-dsmt_verbose",
     Arg.Set Constraint.opt_smt_verbose,
-    " (debug) print SMTLIB constraints sent to Z3");
+    " (debug) print SMTLIB constraints sent to SMT solver");
   ( "-dno_cast",
     Arg.Set opt_dno_cast,
     " (debug) typecheck without any implicit casting");
@@ -319,7 +325,7 @@ let _ =
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
-let load_files ?generate:(generate=true) type_envs files =
+let load_files ?check:(check=false) type_envs files =
   if !opt_memo_z3 then Constraint.load_digests () else ();
 
   let t = Profile.start () in
@@ -328,24 +334,27 @@ let load_files ?generate:(generate=true) type_envs files =
     List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
                      -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
   let ast = Process_file.preprocess_ast options ast in
-  let ast = Initial_check.process_ast ~generate:generate ast in
+  let ast = Initial_check.process_ast ~generate:(not check) ast in
   Profile.finish "parsing" t;
 
   let t = Profile.start () in
   let (ast, type_envs) = check_ast type_envs ast in
   Profile.finish "type checking" t;
 
-  let ast = Scattered.descatter ast in
-  let ast = rewrite_ast type_envs ast in
+  if !opt_memo_z3 then Constraint.save_digests () else ();
 
-  let out_name = match !opt_file_out with
-    | None when parsed = [] -> "out.sail"
-    | None -> fst (List.hd parsed)
-    | Some f -> f ^ ".sail" in
+  if check then
+    ("out.sail", ast, type_envs)
+  else
+    let ast = Scattered.descatter ast in
+    let ast = rewrite_ast type_envs ast in
 
-  if !opt_memo_z3 then Constraint.save_digests () else ();
+    let out_name = match !opt_file_out with
+      | None when parsed = [] -> "out.sail"
+      | None -> fst (List.hd parsed)
+      | Some f -> f ^ ".sail" in
 
-  (out_name, ast, type_envs)
+    (out_name, ast, type_envs)
 
 let main() =
   if !opt_print_version then
@@ -411,7 +420,8 @@ let main() =
       (if !(opt_print_c)
        then
          let ast_c = rewrite_ast_c type_envs ast in
-         let ast_c, type_envs = Specialize.specialize ast_c type_envs in
+         let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
+         (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization ast_c type_envs) in *)
          (* let ast_c = Spec_analysis.top_sort_defs ast_c in *)
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
diff --git a/src/scattered.ml b/src/scattered.ml
index de286e3f..92cb3561 100644
--- a/src/scattered.ml
+++ b/src/scattered.ml
@@ -66,8 +66,8 @@ let rec last_scattered_mapcl id = function
   | [] -> true
 
 (* Nothing cares about these and the AST should be changed *)
-let fake_effect_opt l = Effect_opt_aux (Effect_opt_pure, gen_loc l)
-let fake_rec_opt l = Rec_aux (Rec_rec, gen_loc l)
+let no_effect_opt l = Effect_opt_aux (Effect_opt_none, gen_loc l)
+let fake_rec_opt l = Rec_aux (Rec_nonrec, gen_loc l)
 
 let no_tannot_opt l = Typ_annot_opt_aux (Typ_annot_opt_none, gen_loc l)
 
@@ -95,7 +95,7 @@ let rec descatter' funcls mapcls = function
        | Some clauses -> List.rev (funcl :: clauses)
        | None -> [funcl]
      in
-     DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, fake_effect_opt l, clauses),
+     DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, no_effect_opt l, clauses),
                          (gen_loc l, Type_check.empty_tannot)))
      :: descatter' funcls mapcls defs
 
diff --git a/src/specialize.ml b/src/specialize.ml
index 00357557..591a415a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -52,11 +52,26 @@ open Ast
 open Ast_util
 open Rewriter
 
-let is_typ_ord_uvar = function
+let is_typ_ord_arg = function
   | A_aux (A_typ _, _) -> true
   | A_aux (A_order _, _) -> true
   | _ -> false
 
+type specialization = {
+    is_polymorphic : kinded_id -> bool;
+    instantiation_filter : kid -> typ_arg -> bool
+  }
+
+let typ_ord_specialization = {
+    is_polymorphic = (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt);
+    instantiation_filter = (fun _ -> is_typ_ord_arg)
+  }
+
+let int_specialization = {
+    is_polymorphic = is_int_kopt;
+    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false)
+  }
+
 let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
   let typ_aux = match typ_aux with
     | Typ_id v -> Typ_id v
@@ -81,34 +96,43 @@ and nexp_simp_typ_arg (A_aux (typ_arg_aux, l)) =
 
 (* We have to be careful about whether the typechecker has renamed anything returned by instantiation_of.
    This part of the typechecker API is a bit ugly. *)
-let fix_instantiation instantiation =
-  let instantiation = KBindings.bindings (KBindings.filter (fun _ arg -> is_typ_ord_uvar arg) instantiation) in
+let fix_instantiation spec instantiation =
+  let instantiation = KBindings.bindings (KBindings.filter spec.instantiation_filter instantiation) in
   let instantiation = List.map (fun (kid, arg) -> Type_check.orig_kid kid, nexp_simp_typ_arg arg) instantiation in
   List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty instantiation
 
+(* polymorphic_functions returns all functions that are polymorphic
+   for some set of kinded-identifiers, specified by the is_kopt
+   predicate. For example, polymorphic_functions is_int_kopt will
+   return all Int-polymorphic functions. *)
 let rec polymorphic_functions is_kopt (Defs defs) =
   match defs with
   | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, _, externs), _)) :: defs ->
-     let is_type_polymorphic = List.exists is_kopt (quant_kopts typq) in
-     if is_type_polymorphic then
+     let is_polymorphic = List.exists is_kopt (quant_kopts typq) in
+     if is_polymorphic then
        IdSet.add id (polymorphic_functions is_kopt (Defs defs))
      else
        polymorphic_functions is_kopt (Defs defs)
   | _ :: defs -> polymorphic_functions is_kopt (Defs defs)
   | [] -> IdSet.empty
 
+(* When we specialize a function, we need to generate new name. To do
+   this we take the instantiation that the new function is specialized
+   for and turn that into a string in such a way that alpha-equivalent
+   instantiations always get the same name. We then zencode that
+   string so it is a valid identifier name, and prepend it to the
+   previous function name. *)
 let string_of_instantiation instantiation =
   let open Type_check in
   let kid_names = ref KOptMap.empty in
   let kid_counter = ref 0 in
   let kid_name kid =
     try KOptMap.find kid !kid_names with
-    | Not_found -> begin
-        let n = string_of_int !kid_counter in
-        kid_names := KOptMap.add kid n !kid_names;
-        incr kid_counter;
-        n
-      end
+    | Not_found ->
+       let n = string_of_int !kid_counter in
+       kid_names := KOptMap.add kid n !kid_names;
+       incr kid_counter;
+       n
   in
 
   (* We need custom string_of functions to ensure that alpha-equivalent definitions get the same name *)
@@ -121,7 +145,7 @@ let string_of_instantiation instantiation =
     | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")"
     | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")"
     | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")"
-    | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")"
+    | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_nexp nexps ^ ")"
     | Nexp_exp n -> "2 ^ " ^ string_of_nexp n
     | Nexp_neg n -> "- " ^ string_of_nexp n
   in
@@ -132,7 +156,7 @@ let string_of_instantiation instantiation =
     | Typ_id id -> string_of_id id
     | Typ_var kid -> kid_name (mk_kopt K_type kid)
     | Typ_tup typs -> "(" ^ Util.string_of_list ", " string_of_typ typs ^ ")"
-    | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
+    | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_typ_arg args ^ ")"
     | Typ_fn (arg_typs, ret_typ, eff) ->
        "(" ^ Util.string_of_list ", " string_of_typ arg_typs ^ ") -> " ^ string_of_typ ret_typ ^ " effect " ^ string_of_effect eff
     | Typ_bidir (t1, t2) ->
@@ -160,9 +184,11 @@ let string_of_instantiation instantiation =
        kid_name (mk_kopt K_int kid) ^ " in {" ^ Util.string_of_list ", " Big_int.to_string ns ^ "}"
     | NC_aux (NC_true, _) -> "true"
     | NC_aux (NC_false, _) -> "false"
+    | NC_aux (NC_var kid, _) -> kid_name (mk_kopt K_bool kid)
+    | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_typ_arg args ^ ")"
   in
 
-  let string_of_binding (kid, arg) = string_of_kid kid ^ " => " ^ string_of_typ_arg arg in
+  let string_of_binding (kid, arg) = string_of_kid kid ^ "=>" ^ string_of_typ_arg arg in
   Util.zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation))
 
 let id_of_instantiation id instantiation =
@@ -179,12 +205,12 @@ let rec variant_generic_typ id (Defs defs) =
 (* Returns a list of all the instantiations of a function id in an
    ast. Also works with union constructors, and searches for them in
    patterns. *)
-let rec instantiations_of id ast =
+let rec instantiations_of spec id ast =
   let instantiations = ref [] in
 
   let inspect_exp = function
     | E_aux (E_app (id', _), _) as exp when Id.compare id id' = 0 ->
-       let instantiation = fix_instantiation (Type_check.instantiation_of exp) in
+       let instantiation = fix_instantiation spec (Type_check.instantiation_of exp) in
        instantiations := instantiation :: !instantiations;
        exp
     | exp -> exp
@@ -202,7 +228,7 @@ let rec instantiations_of id ast =
                                 (variant_generic_typ variant_id ast)
                                 typ
           in
-          instantiations := fix_instantiation instantiation :: !instantiations;
+          instantiations := fix_instantiation spec instantiation :: !instantiations;
           pat
        | Typ_aux (Typ_id variant_id, _) -> pat
        | _ -> failwith ("Union constructor " ^ string_of_pat pat ^ " has non-union type")
@@ -218,12 +244,12 @@ let rec instantiations_of id ast =
 
   !instantiations
 
-let rec rewrite_polymorphic_calls id ast =
+let rec rewrite_polymorphic_calls spec id ast =
   let vs_ids = Initial_check.val_spec_ids ast in
 
   let rewrite_e_aux = function
     | E_aux (E_app (id', args), annot) as exp when Id.compare id id' = 0 ->
-       let instantiation = fix_instantiation (Type_check.instantiation_of exp) in
+       let instantiation = fix_instantiation spec (Type_check.instantiation_of exp) in
        let spec_id = id_of_instantiation id instantiation in
        (* Make sure we only generate specialized calls when we've
           specialized the valspec. The valspec may not be generated if
@@ -278,13 +304,61 @@ and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
   | A_order ord -> KidSet.empty
   | A_bool _ -> KidSet.empty
 
-let specialize_id_valspec instantiations id ast =
+(* Implicit arguments have restrictions that won't hold
+   post-specialisation, but we can just remove them and turn them into
+   regular arguments. *)
+let rec remove_implicit (Typ_aux (aux, l) as t) =
+  match aux with
+  | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
+  | Typ_tup typs -> Typ_aux (Typ_tup (List.map remove_implicit typs), l)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map remove_implicit arg_typs, remove_implicit ret_typ, effs), l)
+  | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (remove_implicit typ1, remove_implicit typ2), l)
+  | Typ_app (Id_aux (Id "implicit", _), args) -> Typ_aux (Typ_app (mk_id "atom", List.map remove_implicit_arg args), l)
+  | Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map remove_implicit_arg args), l)
+  | Typ_id id -> Typ_aux (Typ_id id, l)
+  | Typ_exist (kopts, nc, typ) -> Typ_aux (Typ_exist (kopts, nc, remove_implicit typ), l)
+  | Typ_var v -> Typ_aux (Typ_var v, l)
+and remove_implicit_arg (A_aux (aux, l)) =
+  match aux with
+  | A_typ typ -> A_aux (A_typ (remove_implicit typ), l)
+  | arg -> A_aux (arg, l)
+
+let kopt_arg = function
+  | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> arg_nexp (nvar kid)
+  | KOpt_aux (KOpt_kind (K_aux (K_type,_), kid), _) -> arg_typ (mk_typ (Typ_var kid))
+  | _ -> failwith "oh no"
+
+(* For numeric type arguments we have to be careful not to run into a
+   situation where we have an instantiation like
+
+   'n => 'm, 'm => 8
+
+   and end up re-writing 'n to 8. This function turns an instantition
+   like the above into two,
+
+   'n => 'i#m, 'm => 8 and 'i#m => 'm
+
+   so we can do the substitution in two steps. *)
+let safe_instantiation instantiation =
+  let args =
+    List.map (fun (_, arg) -> kopts_of_typ_arg arg) (KBindings.bindings instantiation)
+    |> List.fold_left KOptSet.union KOptSet.empty
+    |> KOptSet.elements
+  in
+  List.fold_left (fun (i, r) v -> KBindings.map (fun arg -> subst_kid typ_arg_subst (kopt_kid v) (prepend_kid "i#" (kopt_kid v)) arg) i,
+                                  KBindings.add (prepend_kid "i#" (kopt_kid v)) (kopt_arg v) r)
+                 (instantiation, KBindings.empty) args
+
+let instantiate_constraints instantiation ncs =
+  List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) ncs
+
+let specialize_id_valspec spec instantiations id ast =
   match split_defs (is_valspec id) ast with
-  | None -> failwith ("Valspec " ^ string_of_id id ^ " does not exist!")
+  | None -> Reporting.unreachable (id_loc id) __POS__ ("Valspec " ^ string_of_id id ^ " does not exist!")
   | Some (pre_ast, vs, post_ast) ->
      let typschm, externs, is_cast, annot = match vs with
        | DEF_spec (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) -> typschm, externs, is_cast, annot
-       | _ -> assert false (* unreachable *)
+       | _ -> Reporting.unreachable (id_loc id) __POS__ "val-spec is not actually a val-spec"
      in
      let TypSchm_aux (TypSchm_ts (typq, typ), _) = typschm in
 
@@ -292,8 +366,9 @@ let specialize_id_valspec instantiations id ast =
      let spec_ids = ref IdSet.empty in
 
      let specialize_instance instantiation =
+       let safe_instantiation, reverse = safe_instantiation instantiation in
        (* Replace the polymorphic type variables in the type with their concrete instantiation. *)
-       let typ = Type_check.subst_unifiers instantiation typ in
+       let typ = remove_implicit (Type_check.subst_unifiers reverse (Type_check.subst_unifiers safe_instantiation typ)) in
 
        (* Collect any new type variables introduced by the instantiation *)
        let collect_kids kidsets = KidSet.elements (List.fold_left KidSet.union KidSet.empty kidsets) in
@@ -302,11 +377,17 @@ let specialize_id_valspec instantiations id ast =
 
        (* Remove type variables from the type quantifier. *)
        let kopts, constraints = quant_split typq in
-       let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt || is_order_kopt kopt)) kopts in
-       let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees
-                               @ List.map (mk_qi_id K_int) int_frees
-                               @ List.map mk_qi_kopt kopts
-                               @ List.map mk_qi_nc constraints) in
+       let constraints = instantiate_constraints safe_instantiation constraints in
+       let constraints = instantiate_constraints reverse constraints in
+       let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
+       let typq =
+         if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then
+           mk_typquant []
+         else
+           mk_typquant (List.map (mk_qi_id K_type) typ_frees
+                        @ List.map (mk_qi_id K_int) int_frees
+                        @ List.map mk_qi_kopt kopts
+                        @ List.map mk_qi_nc constraints) in
        let typschm = mk_typschm typq typ in
 
        let spec_id = id_of_instantiation id instantiation in
@@ -324,8 +405,9 @@ let specialize_id_valspec instantiations id ast =
 
 (* When we specialize a function definition we also need to specialize
    all the types that appear as annotations within the function
-   body. *)
-let specialize_annotations instantiation =
+   body. Also remove any type-annotation from the fundef itself,
+   because at this point we have that as a separate valspec.*)
+let specialize_annotations instantiation fdef =
   let open Type_check in
   let rw_pat = {
       id_pat_alg with
@@ -337,12 +419,21 @@ let specialize_annotations instantiation =
       lEXP_cast = (fun (typ, lexp) -> LEXP_cast (subst_unifiers instantiation typ, lexp));
       pat_alg = rw_pat
     } in
-  rewrite_fun {
-      rewriters_base with
-      rewrite_exp = (fun _ -> fold_exp rw_exp);
-      rewrite_pat = (fun _ -> fold_pat rw_pat)
-    }
-     
+  let fdef =
+    rewrite_fun {
+        rewriters_base with
+        rewrite_exp = (fun _ -> fold_exp rw_exp);
+        rewrite_pat = (fun _ -> fold_pat rw_pat)
+      } fdef
+  in
+  match fdef with
+  | FD_aux (FD_function (rec_opt, _, eff_opt, funcls), annot) ->
+     FD_aux (FD_function (rec_opt,
+                          Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown),
+                          eff_opt,
+                          funcls),
+             annot)
+
 let specialize_id_fundef instantiations id ast =
   match split_defs (is_fundef id) ast with
   | None -> ast
@@ -380,7 +471,15 @@ let specialize_id_overloads instantiations id (Defs defs) =
    valspecs are then re-specialized. This process is iterated until
    the whole spec is specialized. *)
 
-let initial_calls = (IdSet.of_list [mk_id "main"; mk_id "__SetConfig"; mk_id "__ListConfig"; mk_id "execute"; mk_id "decode"; mk_id "initialize_registers"; mk_id "append_64"])
+let initial_calls = IdSet.of_list
+  [ mk_id "main";
+    mk_id "__SetConfig";
+    mk_id "__ListConfig";
+    mk_id "execute";
+    mk_id "decode";
+    mk_id "initialize_registers";
+    mk_id "append_64" (* used to construct bitvector literals in C backend *)
+  ]
 
 let remove_unused_valspecs ?(initial_calls=initial_calls) env ast =
   let calls = ref initial_calls in
@@ -424,9 +523,9 @@ let slice_defs env (Defs defs) keep_ids =
   let defs = List.filter keep defs in
   remove_unused_valspecs env (Defs defs) ~initial_calls:keep_ids
 
-let specialize_id id ast =
-  let instantiations = instantiations_of id ast in
-  let ast = specialize_id_valspec instantiations id ast in
+let specialize_id spec id ast =
+  let instantiations = instantiations_of spec id ast in
+  let ast = specialize_id_valspec spec instantiations id ast in
   let ast = specialize_id_fundef instantiations id ast in
   specialize_id_overloads instantiations id ast
 
@@ -448,21 +547,26 @@ let reorder_typedefs (Defs defs) =
   let others = filter_typedefs defs in
   Defs (List.rev !tdefs @ others)
 
-let specialize_ids ids ast =
-  let ast = List.fold_left (fun ast id -> specialize_id id ast) ast (IdSet.elements ids) in
+let specialize_ids spec ids ast =
+  let ast = List.fold_left (fun ast id -> specialize_id spec id ast) ast (IdSet.elements ids) in
   let ast = reorder_typedefs ast in
   let ast, _ = Type_error.check Type_check.initial_env ast in
   let ast =
-    List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids)
+    List.fold_left (fun ast id -> rewrite_polymorphic_calls spec id ast) ast (IdSet.elements ids)
   in
   let ast, env = Type_error.check Type_check.initial_env ast in
   let ast = remove_unused_valspecs env ast in
   ast, env
 
-let rec specialize ast env =
-  let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in
-  if IdSet.is_empty ids then
+let rec specialize' n spec ast env =
+  if n = 0 then
     ast, env
   else
-    let ast, env = specialize_ids ids ast in
-    specialize ast env
+    let ids = polymorphic_functions spec.is_polymorphic ast in
+    if IdSet.is_empty ids then
+      ast, env
+    else
+      let ast, env = specialize_ids spec ids ast in
+      specialize' (n - 1) spec ast env
+
+let specialize = specialize' (-1)
diff --git a/src/specialize.mli b/src/specialize.mli
index 28029747..93dec239 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -54,10 +54,18 @@ open Ast
 open Ast_util
 open Type_check
 
+type specialization
+
+(** Only specialize Type- and Ord- kinded polymorphism. *)
+val typ_ord_specialization : specialization
+
+(** (experimental) specialise Int-kinded definitions *)
+val int_specialization : specialization
+
 (** Returns an IdSet with the function ids that have X-kinded
    parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first
    argument specifies what X should be - it should be one of:
-   [is_nat_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
+   [is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
    or some combination of those. *)
 val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
 
@@ -66,11 +74,15 @@ val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
    AST with [Type_check.initial_env]. The env parameter is the
    environment to return if there is no polymorphism to remove, in
    which case specialize returns the AST unmodified. *)
-val specialize : tannot defs -> Env.t -> tannot defs * Env.t
+val specialize : specialization -> tannot defs -> Env.t -> tannot defs * Env.t
+
+val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs * Env.t
 
-val instantiations_of : id -> tannot defs -> typ_arg KBindings.t list
+(** return all instantiations of a function id, with the
+   instantiations filtered according to the specialization. *)
+val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list
 
 val string_of_instantiation : typ_arg KBindings.t -> string
 
-(* Remove all function definitions except for the given set *)
+(** Remove all function definitions except for the given set *)
 val slice_defs : Env.t -> tannot defs -> IdSet.t -> tannot defs
diff --git a/src/type_check.ml b/src/type_check.ml
index b9f8f323..b43e17ed 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -72,6 +72,10 @@ let opt_no_lexp_bounds_check = ref false
    We prefer not to do it for latex output but it is otherwise a good idea. *)
 let opt_expand_valspec = ref true
 
+(* Linearize cases involving power where we would otherwise require
+   the SMT solver to use non-linear arithmetic. *)
+let opt_smt_linearize = ref false
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -246,6 +250,50 @@ and strip_kinded_id_aux = function
 and strip_kind = function
   | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown)
 
+let rec typ_nexps (Typ_aux (typ_aux, l)) =
+  match typ_aux with
+  | Typ_internal_unknown -> []
+  | Typ_id v -> []
+  | Typ_var kid -> []
+  | Typ_tup typs -> List.concat (List.map typ_nexps typs)
+  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
+  | Typ_exist (kids, nc, typ) -> typ_nexps typ
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
+  | Typ_bidir (typ1, typ2) ->
+     typ_nexps typ1 @ typ_nexps typ2
+and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
+  match typ_arg_aux with
+  | A_nexp n -> [n]
+  | A_typ typ -> typ_nexps typ
+  | A_bool nc -> constraint_nexps nc
+  | A_order ord -> []
+and constraint_nexps (NC_aux (nc_aux, l)) =
+  match nc_aux with
+  | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) ->
+     [n1; n2]
+  | NC_set _ | NC_true | NC_false | NC_var _ -> []
+  | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2
+  | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args)
+
+(* Return a KidSet containing all the type variables appearing in
+   nexp, where nexp occurs underneath a Nexp_exp, i.e. 2^nexp *)
+let rec nexp_power_variables (Nexp_aux (aux, _)) =
+  match aux with
+  | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) ->
+     KidSet.union (nexp_power_variables n1) (nexp_power_variables n2)
+  | Nexp_neg n ->
+     nexp_power_variables n
+  | Nexp_id _ | Nexp_var _ | Nexp_constant _ ->
+     KidSet.empty
+  | Nexp_app (_, ns) ->
+     List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables ns)
+  | Nexp_exp n ->
+     tyvars_of_nexp n
+
+let constraint_power_variables nc =
+  List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables (constraint_nexps nc))
+
 let rec name_pat (P_aux (aux, _)) =
   match aux with
   | P_id id | P_as (_, id) -> Some ("_" ^ string_of_id id)
@@ -261,7 +309,7 @@ let fresh_existential k =
 let named_existential k = function
   | Some n -> mk_kopt k (mk_kid n)
   | None -> fresh_existential k
- 
+
 let destruct_exist_plain ?name:(name=None) typ =
   match typ with
   | Typ_aux (Typ_exist ([kopt], nc, typ), _) ->
@@ -397,7 +445,7 @@ module Env : sig
   val wf_nexp : ?exs:KidSet.t -> t -> nexp -> unit
   val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit
 
-  (* Some of the code in the environment needs to use the Z3 prover,
+  (* Some of the code in the environment needs to use the smt solver,
      which is defined below. To break the circularity this would cause
      (as the prove code depends on the environment), we add a
      reference to the prover to the initial environment. *)
@@ -521,7 +569,7 @@ end = struct
     let kopts, ncs = quant_split typq in
     let rec subst_args kopts args =
       match kopts, args with
-      | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_nat_kopt kopt ->
+      | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt ->
          List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args)
       | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
          subst_args kopts args
@@ -543,6 +591,10 @@ end = struct
     match aux with
     | NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
     | NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
+    | NC_equal (n1, n2) -> NC_aux (NC_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
+    | NC_not_equal (n1, n2) -> NC_aux (NC_not_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
+    | NC_bounded_le (n1, n2) -> NC_aux (NC_bounded_le (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
+    | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
     | NC_app (id, args) ->
        (try
           begin match Bindings.find id env.typ_synonyms l env args with
@@ -550,7 +602,7 @@ end = struct
           | arg -> typ_error env l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
           end
         with Not_found -> NC_aux (NC_app (id, List.map (expand_synonyms_arg env) args), l))
-    | NC_true | NC_false | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _ | NC_var _ | NC_set _ -> nc
+    | NC_true | NC_false | NC_var _ | NC_set _ -> nc
 
   and expand_nexp_synonyms env (Nexp_aux (aux, l) as nexp) =
     typ_debug ~level:2 (lazy ("Expanding " ^ string_of_nexp nexp));
@@ -935,7 +987,7 @@ end = struct
         typ_print (lazy (adding ^ "record " ^ string_of_id id));
         let rec record_typ_args = function
           | [] -> []
-          | ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt ->
+          | ((QI_aux (QI_id kopt, _)) :: qis) when is_int_kopt kopt ->
              mk_typ_arg (A_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis
           | ((QI_aux (QI_id kopt, _)) :: qis) when is_typ_kopt kopt ->
              mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis
@@ -1068,7 +1120,7 @@ end = struct
   let add_typ_var l (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) env =
     if KBindings.mem v env.typ_vars then begin
         let n = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 in
-        let s_l, s_k = KBindings.find v env.typ_vars in 
+        let s_l, s_k = KBindings.find v env.typ_vars in
         let s_v = Kid_aux (Var (string_of_kid v ^ "#" ^ string_of_int n), l) in
         typ_print (lazy (Printf.sprintf "%stype variable (shadowing %s) %s : %s" adding (string_of_kid s_v) (string_of_kid v) (string_of_kind_aux k)));
         { env with
@@ -1087,11 +1139,34 @@ end = struct
   let add_constraint constr env =
     wf_constraint env constr;
     let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in
-    match nc_aux with
-    | NC_true -> env
-    | _ ->
-       typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
-       { env with constraints = constr :: env.constraints }
+    let power_vars = constraint_power_variables constr in
+    if KidSet.cardinal power_vars > 1 && !opt_smt_linearize then
+      typ_error env l ("Cannot add constraint " ^ string_of_n_constraint constr
+                       ^ " where more than two variables appear within an exponential")
+    else if KidSet.cardinal power_vars = 1 && !opt_smt_linearize then
+      let v = KidSet.choose power_vars in
+      let constrs = List.fold_left nc_and nc_true (get_constraints env) in
+      begin match Constraint.solve_all_smt l (get_typ_vars env) constrs v with
+      | Some solutions ->
+         typ_print (lazy (Util.("Linearizing " |> red |> clear) ^ string_of_n_constraint constr
+                          ^ " for " ^ string_of_kid v ^ " in " ^ Util.string_of_list ", " Big_int.to_string solutions));
+         let linearized =
+           List.fold_left
+             (fun c s -> nc_or c (nc_and (nc_eq (nvar v) (nconstant s)) (constraint_subst v (arg_nexp (nconstant s)) constr)))
+             nc_false solutions
+         in
+         typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint linearized));
+         { env with constraints = linearized :: env.constraints }
+      | None ->
+         typ_error env l ("Type variable " ^ string_of_kid v
+                          ^ " must have a finite number of solutions to add " ^ string_of_n_constraint constr)
+      end
+    else
+      match nc_aux with
+      | NC_true -> env
+      | _ ->
+         typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
+         { env with constraints = constr :: env.constraints }
 
   let get_ret_typ env = env.ret_typ
 
@@ -1282,7 +1357,7 @@ and simp_typ_aux = function
      would become {('s:Bool) ('r: Bool), nc('r). bool('s & 'r)},
      wherein all the redundant boolean variables have been combined
      into a single one. Making this simplification allows us to avoid
-     having to pass large numbers of pointless variables to Z3 if we
+     having to pass large numbers of pointless variables to SMT if we
      ever bind this existential. *)
   | Typ_exist (vars, nc, Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool b, _)]), _)) ->
      let kids = KidSet.of_list (List.map kopt_kid vars) in
@@ -1326,16 +1401,23 @@ this is equivalent to
 which is then a problem we can feed to the constraint solver expecting unsat.
  *)
 
-let prove_z3 env (NC_aux (_, l) as nc) =
+let prove_smt env (NC_aux (_, l) as nc) =
   let vars = Env.get_typ_vars env in
   let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
   let ncs = Env.get_constraints env in
-  match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs) with
+  match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs) with
   | Constraint.Unsat -> typ_debug (lazy "unsat"); true
   | Constraint.Sat -> typ_debug (lazy "sat"); false
-  | Constraint.Unknown -> typ_debug (lazy "unknown"); false
-
-let solve env (Nexp_aux (_, l) as nexp) =
+  | Constraint.Unknown ->
+     (* Work around versions of z3 that are confused by 2^n in
+        constraints, even when such constraints are irrelevant *)
+     let ncs' = List.concat (List.map constraint_conj ncs) in
+     let ncs' = List.filter (fun nc -> KidSet.is_empty (constraint_power_variables nc)) ncs' in
+     match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs') with
+     | Constraint.Unsat -> typ_debug (lazy "unsat"); true
+     | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false
+
+let solve_unique env (Nexp_aux (_, l) as nexp) =
   typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
                    ^ " |- " ^ string_of_nexp nexp ^ " = ?"));
   match nexp with
@@ -1345,7 +1427,7 @@ let solve env (Nexp_aux (_, l) as nexp) =
     let vars = Env.get_typ_vars env in
     let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
     let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
-    Constraint.solve_z3 l vars constr (mk_kid "solve#")
+    Constraint.solve_unique_smt l vars constr (mk_kid "solve#")
 
 let debug_pos (file, line, _, _) =
   "(" ^ file ^ "/" ^ string_of_int line ^ ") "
@@ -1358,7 +1440,7 @@ let prove pos env nc =
   else ();
   match nc_aux with
   | NC_true -> true
-  | _ -> prove_z3 env nc
+  | _ -> prove_smt env nc
 
 (**************************************************************************)
 (* 3. Unification                                                         *)
@@ -1376,32 +1458,6 @@ let rec nexp_frees ?exs:(exs=KidSet.empty) (Nexp_aux (nexp, l)) =
   | Nexp_exp n -> nexp_frees ~exs:exs n
   | Nexp_neg n -> nexp_frees ~exs:exs n
 
-let rec typ_nexps (Typ_aux (typ_aux, l)) =
-  match typ_aux with
-  | Typ_internal_unknown -> []
-  | Typ_id v -> []
-  | Typ_var kid -> []
-  | Typ_tup typs -> List.concat (List.map typ_nexps typs)
-  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
-  | Typ_exist (kids, nc, typ) -> typ_nexps typ
-  | Typ_fn (arg_typs, ret_typ, _) ->
-     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
-  | Typ_bidir (typ1, typ2) ->
-     typ_nexps typ1 @ typ_nexps typ2
-and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
-  match typ_arg_aux with
-  | A_nexp n -> [n]
-  | A_typ typ -> typ_nexps typ
-  | A_bool nc -> constraint_nexps nc
-  | A_order ord -> []
-and constraint_nexps (NC_aux (nc_aux, l)) =
-  match nc_aux with
-  | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) ->
-     [n1; n2]
-  | NC_set _ | NC_true | NC_false | NC_var _ -> []
-  | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2
-  | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args)
-
 let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
   match nexp1, nexp2 with
   | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0
@@ -1692,13 +1748,13 @@ let rec ambiguous_vars (Typ_aux (aux, _)) =
   match aux with
   | Typ_app (_, args) -> List.fold_left KidSet.union KidSet.empty (List.map ambiguous_arg_vars args)
   | _ -> KidSet.empty
-  
+
 and ambiguous_arg_vars (A_aux (aux, _)) =
   match aux with
   | A_bool nc -> ambiguous_nc_vars nc
   | A_nexp nexp -> ambiguous_nexp_vars nexp
   | _ -> KidSet.empty
-               
+
 and ambiguous_nc_vars (NC_aux (aux, _)) =
   match aux with
   | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2)
@@ -1903,9 +1959,17 @@ let rec subtyp l env typ1 typ2 =
      let env = add_typ_vars l (List.map (mk_kopt K_int) (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2)))) env in
      let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in
      if not (kids2 = []) then typ_error env l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else ();
-     let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
-     if prove __POS__ env nc2 then ()
-     else typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+     let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) (Env.get_typ_vars env) in
+     begin match Constraint.call_smt l vars (nc_eq nexp1 nexp2) with
+     | Constraint.Sat ->
+        let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
+        if prove __POS__ env nc2 then
+          ()
+        else
+          typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+     | _ ->
+        typ_error env l ("Constraint " ^ string_of_n_constraint (nc_eq nexp1 nexp2) ^ " is not satisfiable")
+     end
   | _, _ ->
   match typ_aux1, typ_aux2 with
   | _, Typ_internal_unknown when Env.allow_unknowns env -> ()
@@ -1966,11 +2030,24 @@ let subtype_check env typ1 typ2 =
 
 exception No_simple_rewrite;;
 
+let rec move_to_front p ys = function
+  | x :: xs when p x -> x :: (ys @ xs)
+  | x :: xs -> move_to_front p (x :: ys) xs
+  | [] -> ys
+
 let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) =
   let mk_exp exp = mk_exp ~loc:l exp in
   match aux with
   | Nexp_var v ->
+     (* Use a simple heuristic to find the most likely local we can
+        use, and move it to the front of the list. *)
+     let str = string_of_kid v in
+     let likely =
+       try let n = if str.[1] = '_' then 2 else 1 in String.sub str n (String.length str - n) with
+       | Invalid_argument _ -> str
+     in
      let locals = Env.get_locals env |> Bindings.bindings in
+     let locals = move_to_front (fun local -> likely = string_of_id (fst local)) [] locals in
      let same_size (local, (_, Typ_aux (aux, _))) =
        match aux with
        | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)])
@@ -4731,7 +4808,7 @@ let mk_synonym typq typ_arg =
   let kopts = List.map snd kopts in
   let rec subst_args env l kopts args =
     match kopts, args with
-    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_nat_kopt kopt ->
+    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
        let typ_arg, ncs = subst_args env l kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
        List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
diff --git a/src/type_check.mli b/src/type_check.mli
index 4ff52cd9..5ab986d0 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -71,6 +71,10 @@ val opt_no_lexp_bounds_check : bool ref
    We prefer not to do it for latex output but it is otherwise a good idea. *)
 val opt_expand_valspec : bool ref
 
+(** Linearize cases involving power where we would otherwise require
+   the SMT solver to use non-linear arithmetic. *)
+val opt_smt_linearize : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =
@@ -309,9 +313,15 @@ val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t
 
 val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t
 
+(** Attempt to prove a constraint using z3. Returns true if z3 can
+   prove that the constraint is true, returns false if z3 cannot prove
+   the constraint true. Note that this does not guarantee that the
+   constraint is actually false, as the constraint solver is somewhat
+   untrustworthy. *)
 val prove : (string * int * int * int) -> Env.t -> n_constraint -> bool
 
-val solve : Env.t -> nexp -> Big_int.num option
+(** Returns Some c if there is a unique c such that nexp = c *)
+val solve_unique : Env.t -> nexp -> Big_int.num option
 
 val canonicalize : Env.t -> typ -> typ