Merge branch 'sail2' into separate_bv

79 files changed, 2053 insertions, 710 deletions

diff --git a/.gitignore b/.gitignore
index 2ee1ce5d..3bd2cdd5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -38,6 +38,9 @@ lib/hol/sail-heap
 /src/sail.docdir
 /src/ast.lem
 /src/ast.ml
+/src/jib.lem
+/src/jib.ml
+/src/manifest.ml
 
 /test/typecheck/rtpass*/
 /test/typecheck/tests.xml
diff --git a/INSTALL.md b/INSTALL.md
index 23e46cec..d3476af5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,112 +1,70 @@
-Installing Sail on Ubuntu and macOS
-=========================
+These are instructions for installing Sail via opam, the ocaml package manager.
+The most up-to-date version of this document can be found on the Sail wiki
 
-This note lists the commands needed to get Sail and all dependencies
-working on a new Ubuntu install or macOS. We have recently (2018-02-17) tested these
-on Xubuntu 16.04 LTS in a virtual machine and on macOS Sierra 10.12.6, so they should
-work. Hopefully this will be useful as a reference.
+https://github.com/rems-project/sail/wiki/OPAMInstall
 
-Basics
-------
+To build everything from source, instructions can be found here:
 
-First we need some basic packages if they're not already installed.
+https://github.com/rems-project/sail/wiki/Building-from-Source
 
-For Ubuntu:
+# How to install Sail from opam
+
+Install opam if you haven't already: https://opam.ocaml.org/doc/Install.html
+
+Use opam to install a version of ocaml we know works for us:
 ```
-sudo apt-get install build-essential git
+opam switch 4.06.1
 ```
-
-For macOS: compilers and supporting utilities are called Xcode instead of build-essential. First, download Xcode from the Mac App Store, and then run the following in the terminal:
+OR, if you are using opam >=2.0, the syntax of the switch command changed slightly:
 ```
-xcode-select --install
+opam switch create ocaml-base-compiler.4.06.1
 ```
-git can be installed using ```brew install git```
 
-OCaml and sail expect some packages. m4 is for OPAM, libgmp-dev is for
-zarith which most of our tools rely on. Sail uses Z3 as a constraint
-solver.
+Then set up the environment for the ocaml we just installed:
 ```
-sudo apt-get install m4 libgmp-dev z3
+eval `opam config env` 
 ```
-For macOS: ```brew install m4 gmp z3``` 
-
-OCaml and OPAM
---------------
-
-Install OPAM. Either directly from [https://opam.ocaml.org] or from
-the package manager - both should work, but we used the install script
-from the website. This should install OCaml 4.05. Don't forget to run
-```opam init``` after installing OPAM.
-
-We now need the following packages from OPAM.
+Add our local opam repo:
 ```
-opam install ocamlbuild
-opam install num
-opam install zarith
-opam install menhir
-opam install omd
+opam repository add rems https://github.com/rems-project/opam-repository.git
 ```
-
-Ott
----
-
-Before cloning the repositories you may need to set up ssh keys with
-github or use https. Create a directory to install the various REMS
-tools and cd into it.
+Install system dependencies, on Ubuntu:
 ```
-git clone git@github.com:ott-lang/ott.git
-cd ott
-make
-cd ..
+sudo apt-get install build-essential libgmp-dev z3
 ```
-Sail depends on ott, so add the ott executable (``` path-to-ott/bin```) in the $PATH.
-
-
-Lem
----
-
-If you are using OCaml 4.06, you'll need to run `opam install num` before building lem.
-
+or homebrew:
 ```
-git clone git@github.com:rems-project/lem.git
-cd lem
-make
-cd ocaml-lib
-make install
-cd ../..
+brew install gmp z3
 ```
-
-Linksem
--------
-
-Before installing linksem, we are required to set the LEMLIB environment variable and to put the lem executable in $PATH. LEMLIB should be the library directory within the checked-out lem directory (i.e. ```path-to-lem/library/```). Next, install linksem as
-
+Install sail and its dependencies:
 ```
-git clone git@github.com:rems-project/linksem.git
-cd linksem
-make && make install
+opam install sail
 ```
+If all goes well then you'll have sail in your path:
+```
+which sail
+sail --help
+```
+Some source files that sail uses are found in at ``opam config var sail:share`` (e.g. for ``$include <foo.sail>``) but sail should find those when it needs them.
 
-Sail
-----
-
-Sail depends on lem and ott, so make sure lem and ott executables
-exist in $PATH.
+### Installing development versions of Sail
+Released Sail packages lag behind the latest development in the repository. If you find you need a recently added feature or bug fix you can use opam pin to install the latest version of Sail from the repository. Assuming you have previously followed the above instructions (required to install dependencies):
 ```
-git clone git@github.com:rems-project/sail.git
+git clone https://github.com/rems-project/sail.git
 cd sail
-make
+opam pin add sail .
 ```
-To build Sail with interactive support we need two more commands
+will install from a local checkout of the Sail sources.
+
+You can update with new changes as they are committed by pulling and reinstalling:
 ```
-opam install linenoise
-make isail
+git pull
+opam reinstall sail
 ```
-To test Sail is installed correctly, execute the following from the
-root directory of the sail repository. You may also need to set
-$LEM_DIR to the root of the lem repository for the lem tests. Some of
-the C backend tests will fail if valgrind isn't installed.
+
+To remove the pin and revert to the latest released opam package type:
 ```
-export SAIL_DIR=$PWD
-test/run_tests.sh
+opam pin remove sail
 ```
+
+Alternatively you could follow the instructions to [build Sail manually](https://github.com/rems-project/sail/wiki/Building-from-Source), optionally skipping the steps to install ott, lem and linksem if they were already installed via opam.
diff --git a/doc/internals.md b/doc/internals.md
new file mode 100644
index 00000000..6ba60fa6
--- /dev/null
+++ b/doc/internals.md
@@ -0,0 +1,454 @@
+# Sail Internals
+
+## Abstract Syntax Tree
+
+The Sail abstract syntax tree (AST) is defined by an ott grammar in
+[sail.ott](https://github.com/rems-project/sail/blob/sail2/language/sail.ott). This
+generates a OCaml (and lem) version of the ast in `src/ast.ml` and
+`src/ast.lem`. Technically the OCaml version of the AST is generated
+by [Lem](https://github.com/rems-project/lem), which allows the Sail
+OCaml source to seamlessly interoperate with parts written in
+Lem. Although we do not make much use of this, in principle it allows
+us to implement parts of Sail in Lem, which would enable them to be
+verified in Isabelle or HOL.
+
+The Sail AST looks something like:
+
+```OCaml
+and 'a exp =
+ | E_aux of ( 'a exp_aux) * 'a annot
+
+and 'a exp_aux =  (* expression *)
+ | E_block of ( 'a exp) list (* sequential block *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of typ * ( 'a exp) (* cast *)
+ | E_app of id * ( 'a exp) list (* function application *)
+ | E_tuple of ( 'a exp) list (* tuple *)
+ | E_if of ( 'a exp) * ( 'a exp) * ( 'a exp) (* conditional *)
+ ...
+```
+
+Each constructor is prefixed by a unique code (in this case `E` for
+expressions), and is additionally wrapped by an *aux* constructor
+which attaches an annotation to each node in the AST, consisting of an
+arbitrary type that parameterises the AST, and a location identifying
+the position of the AST node in the source code:
+
+```
+type 'a annot = l * 'a
+```
+
+There are various types of locations:
+
+```
+type l =
+  | Unknown
+  | Unique of int * l
+  | Generated of l
+  | Range of Lexing.position * Lexing.position
+  | Documented of string * l
+```
+
+`Range` defines a range of positions given by the parser, the
+`Documented` constructor attaches doc-comments to
+locations. `Generated` is used to signify that code is generated based
+on code from some other location. `Unique` is used internally to tag
+locations with unique integers so they can be referred to
+later. `Unknown` is used for Sail that has no obvious corresponding
+location, although this should be avoided as much possible as it leads
+to poor error messages. Ast nodes programatically generated initially
+have `Unknown` locations, but `Ast_util.locate` can be used to
+recursively attach `Generated` locations for error purposes.
+
+A convention in the Sail source is that a single variable `l` is
+always a location, usually the closest location.
+
+### AST utilities
+
+There are various functions for manipulating the AST defined in
+[ast_util](https://github.com/rems-project/sail/blob/sail2/src/ast_util.mli). These
+include constructor functions like `mk_exp` for generating untyped
+expressions and various functions for destructuring AST nodes. It also
+defines various useful Sets and Maps, e.g. sets of identifiers, type
+variables etc. Note that type variables in Sail are often internally
+referred to as *kids*, I think this is because type variables are
+defined as having a specific *kind*, i.e. `'n : Int` is a type
+variable with kind `Int`. (Although `kinded_id` is technically a
+separate type which is a type variable * kind pair).
+
+### Parse AST
+
+There is a separate AST
+[parse_ast.ml](https://github.com/rems-project/sail/blob/sail2/src/parse_ast.ml)
+which the parser generates. It is very similar to the main AST except
+it contains some additional syntactic sugar. The parse ast is
+desugared by the
+[initial_check](https://github.com/rems-project/sail/blob/sail2/src/initial_check.mli)
+file, which performs some basic checks in addition from mapping the
+parse AST to the main AST.
+
+## Overall Structure
+
+The main entry point for Sail is the file
+[sail.ml](https://github.com/rems-project/sail/blob/sail2/src/sail.ml). Each
+backend option e.g. `-c`, `-lem`, `-ocaml` etc, is referred to as a
+*target*, and the `set_target` function is used to set the
+`opt_target` variable, for example
+
+```OCaml
+  ( "-c",
+    Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen],
+    " output a C translated version of the input");
+```
+
+defines the `-c` option. Each Sail option is configured via via `opt_`
+variables defined at the top of each relevant file. In this case we
+tell Sail that when we generate C, we also want to generated
+`undefined_X` functions for each type `X`. In general such `opt_`
+variables should be set when we start Sail and remain immutable
+thereafter.
+
+The first function called by `main` is `Sail.load_files`. This
+function parses all the files passed to Sail, and then concatenates
+their ASTs. The pre-processor is then run, which evaluates `$directive`
+statements in Sail, such as
+
+```
+$include <prelude.sail>
+```
+
+Unlike the C pre-processor the Sail pre-processor operates over actual
+Sail ASTs rather than strings. This can recursively include other
+files into the AST, as well as add/remove parts of the AST with
+`$ifdef` etc. Directives that are used are preserved in the AST, so
+they also function as a useful way to pass auxiliary information to
+the various Sail backends.
+
+The initial check mentioned above is then run to desugar the AST, and
+then the type-checker is run which produces a fully type-checked
+AST. Type annotations are attached to every node (for which an
+annotation makes sense) using the aux constructors. The type-checker
+is discussed in more details later.
+
+After type-checking the Sail scattered definitions are de-scattered
+into single functions.
+
+All the above is shared by each target and performed by the
+`load_files` function.
+
+The next step is to apply various target-specific rewrites to the AST
+before passing it to the backend for each target.
+
+The file
+[rewrites.ml](https://github.com/rems-project/sail/blob/sail2/src/rewrites.ml) defines a list of rewrites:
+
+```OCaml
+let all_rewrites = [
+    ("pat_string_append", Basic_rewriter rewrite_defs_pat_string_append);
+    ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns);
+    ("mono_rewrites", Basic_rewriter mono_rewrites);
+    ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps);
+    ("monomorphise", Basic_rewriter monomorphise);
+    ...
+```
+
+and each target specifies a list of rewrites to apply like so:
+
+```OCaml
+let rewrites_interpreter = [
+    ("no_effect_check", []);
+    ("realise_mappings", []);
+    ("toplevel_string_append", []);
+    ("pat_string_append", []);
+    ("mapping_builtins", []);
+    ("undefined", [Bool_arg false]);
+    ("vector_concat_assignments", []);
+    ("tuple_assignments", []);
+    ("simple_assignments", [])
+  ]
+```
+
+Once these rewrites have occurred the `Sail.target` function is called
+which invokes the backend for each target, e.g. for OCaml:
+
+```OCaml
+  | Some "ocaml" ->
+     let ocaml_generator_info =
+       match !opt_ocaml_generators with
+       | [] -> None
+       | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators)
+     in
+     let out = match !opt_file_out with None -> "out" | Some s -> s in
+     Ocaml_backend.ocaml_compile out ast ocaml_generator_info
+```
+
+There is also a `Sail.prover_regstate` function that allows the
+register state to be Set up in a prover-agnostic way for each of the
+theorem-prover targets.
+
+## Type Checker
+
+The Sail type-checker is contained within
+[src/type_check.ml](https://github.com/rems-project/sail/blob/sail2/src/type_check.ml). This
+file is long, but is structured as follows:
+
+1. The type checking environment is defined. The functions that
+   operate on the typing environment are contained with a separate
+   `Env` module. The purpose of this module is to hide the internal
+   representation of the typing environment and ensure that the main
+   type-checker code can only interact with it using the functions
+   defined in this module, which can be set up to guarantee any
+   invariant we need. Code outside the type-checker itself can only
+   interact with an even more restricted subset of these functions
+   exported via the mli interface file.
+
+2. Helper definitions for subtyping and constraint solving are set
+   up. The code that actually talks to an external SMT solver is
+   contained within a separate file
+   [src/constraint.ml](https://github.com/rems-project/sail/blob/sail2/src/constraint.ml),
+   whereas the code here sets up the interface between the typing
+   environment and the solver.
+
+3. Next comes the definitions for unification and instantiation of
+   types. There is some additional code (3.5) to handle subtyping with
+   existential types, which can use unification to instantiate
+   existentially quantified type variables.
+
+4. Sail allows some type-level constructs to appear in term-level
+   variables, but these are then eliminated during type-checking in a
+   process called *sizeof*-rewriting, after the (somewhat-awkwardly)
+   named *sizeof* keyword.
+
+5. Finally all the typing rules are given. Sail has a bi-directional
+   type-checking approach. So there are checking rules like
+   `check_exp`, `check_pat`, etc., as well as inference rules like
+   `infer_exp`, `infer_pat`, etc.
+
+6. Effects added by the previous typing rules are now propagated
+   upwards through the AST
+
+7. Finally we have rules for checking and processing toplevel
+   definitions of functions and datatypes.
+
+The interface by which the rest of Sail can interact with the
+type-checker and type annotations is strictly controlled by it's [mli
+interface](https://github.com/rems-project/sail/blob/sail2/src/type_check.mli)
+file. We try to keep much of the type-checking internals as abstract
+as possible.
+
+## Rewriter
+
+The rewriting framework used by the various rewrites mentioned
+previously is defined in
+[src/rewriter.ml](https://github.com/rems-project/sail/blob/sail2/src/rewriter.ml). It
+contains various large structs with functions for every single AST
+node, and allows data to be threaded through each re-write in various
+ways. Most of the re-writes are defined in
+[src/rewrites.ml](https://github.com/rems-project/sail/blob/sail2/src/rewrites.ml),
+although the re-writer is used for other rewrite like passes such as
+e.g. constant folding in
+[src/constant_fold.ml](https://github.com/rems-project/sail/blob/sail2/src/constant_fold.ml)
+which combines the rewriter with the Sail interpreter.
+
+The rewriter also acts as the interface to the Sail monomorphisation
+code, in
+[src/monomorphise.ml](https://github.com/rems-project/sail/blob/sail2/src/monomorphise.ml).
+
+## Jib
+
+The C and SMT backends for Sail use a custom intermediate
+representation (IR) called *Jib* (it's a type of Sail). Like the full
+AST this is defined as an ott grammar in
+[language/jib.ott](https://github.com/rems-project/sail/blob/sail2/language/jib.ott). The
+sail "-ir" target allows Sail to be converted into this IR without any further processing.
+
+The Jib related files are contained within a sub-directory
+`src/jib/`. First we convert Sail to A-normal form (ANF) in
+[src/jib/anf.ml](https://github.com/rems-project/sail/blob/sail2/src/jib/anf.ml),
+then
+[src/jib/jib_compile.ml](https://github.com/rems-project/sail/blob/sail2/src/jib/jib_compile.ml)
+converts this into Jib.
+
+The Jib representation has the advantage of being much simpler than
+the full Sail AST, and it removes a lot of the typing complexity, as
+types are replaced with simpler ones (`ctyp`). Note that many
+Jib-related types are prefixed by `c` as it was originally only used
+when generating C.
+
+The key optimisation we do when generating Jib is we analyse the Sail
+types using SMT to try to fit arbitrary-precision types into smaller
+fixed-precision machine-word types that exist within Jib. To aid in
+this we have a
+[specialisation pass](https://github.com/rems-project/sail/blob/sail2/src/specialize.ml)
+that removes polymorphism by creating specialised copies of functions
+based on how their type-quantifiers are instantiated. This can be used
+in addition to the Sail monomorphisation above.
+
+Once we have generated Jib, the code generator from Jib into C is
+fairly straightforward.
+
+## Jib to SMT translation
+
+Starting with some Sail such as:
+```
+default order dec
+
+$include <prelude.sail>
+
+register r : bits(32)
+
+$property
+function property(xs: bits(32)) -> bool = {
+  ys : bits(32) = 0x1234_5678;
+  if (r[0] == bitzero) then {
+    ys = 0xffff_ffff
+  } else {
+    ys = 0x0000_0000
+  };
+  (ys == sail_zeros(32) | ys == sail_ones(32))
+}
+```
+
+We first compile to Jib, then inline all functions and flatten the
+resulting code into a list of instructions as below. The Sail->Jib
+step can be parameterised in a few ways so it differs slightly to when
+we compile Sail to C. First, a specialisation pass specialises
+integer-polymorphic functions and builtins, which is reflected in the
+name mangling scheme so, e.g.
+```
+zz7mzJzK0zCz0z7nzJzK32#bitvector_access
+```
+is a specialised version of bitvector access for 'n => 32 & 'm => 0.
+This lets us generate optimal SMT operations for monomorphic code, as
+the SMTLIB operations like ZeroExtend and Extract are only defined for
+natural number constants and bitvectors of known lengths. We also have
+to treat zero-length bitvectors differently to C, as SMT does not
+allow zero-length bitvectors, and unlike when we compile to C, we can
+have fixed-precision bitvectors of greater that 64-bits in the
+generated Jib.
+
+```
+var ys#u12_l#9 : fbits(32, dec)
+ys#u12_l#9 : fbits(32, dec) = UINT64_C(0x12345678)
+var gs#2#u12_l#15 : bool
+var gs#1#u12_l#17 : bit
+gs#1#u12_l#17 : bit = zz7mzJzK0zCz0z7nzJzK32#bitvector_access(R, 0l)
+gs#2#u12_l#15 : bool = eq_bit(gs#1#u12_l#17, UINT64_C(0))
+kill gs#1#u12_l#17 : bit
+var gs#6#u12_l#16 : unit
+jump gs#2#u12_l#15 then_13
+ys#u12_l#9 : fbits(32, dec) = UINT64_C(0x00000000)
+gs#6#u12_l#16 : unit = UNIT
+goto endif_14
+then_13:
+ys#u12_l#9 : fbits(32, dec) = UINT64_C(0xFFFFFFFF)
+gs#6#u12_l#16 : unit = UNIT
+endif_14:
+kill gs#2#u12_l#15 : bool
+var gs#5#u12_l#10 : bool
+var gs#3#u12_l#14 : fbits(32, dec)
+gs#3#u12_l#14 : fbits(32, dec) = zz7nzJzK32#sail_zeros(32l)
+gs#5#u12_l#10 : bool = zz7nzJzK32#eq_bits(ys#u12_l#9, gs#3#u12_l#14)
+kill gs#3#u12_l#14 : fbits(32, dec)
+var gs#7#u12_l#11 : bool
+jump gs#5#u12_l#10 then_11
+var gs#4#u12_l#12 : fbits(32, dec)
+var gs#0#u9_l#13 : fbits(32, dec)
+gs#0#u9_l#13 : fbits(32, dec) = zz7nzJzK32#sail_zeros(32l)
+gs#4#u12_l#12 : fbits(32, dec) = zz7nzJzK32#not_vec(gs#0#u9_l#13)
+kill gs#0#u9_l#13 : fbits(32, dec)
+goto end_inline_10
+end_inline_10:
+gs#7#u12_l#11 : bool = zz7nzJzK32#eq_bits(ys#u12_l#9, gs#4#u12_l#12)
+kill gs#4#u12_l#12 : fbits(32, dec)
+goto endif_12
+then_11:
+gs#7#u12_l#11 : bool = true
+endif_12:
+return : bool = gs#7#u12_l#11
+kill gs#5#u12_l#10 : bool
+kill ys#u12_l#9 : fbits(32, dec)
+end
+undefined bool
+```
+
+The above Jib is then turned into a control-flow-graph in SSA
+form.
+
+![SSA graph](https://github.com/rems-project/sail/blob/sail2/doc/sail-smt.png)
+
+The conditionals that affect control-flow are put into separate nodes
+(in yellow), so we can easily compute the global path conditional for
+each block (stored in a function pi(cond0, ... , condn) by using the
+yellow conditional nodes between each node and the start node.
+
+From this form the conversion to SMT is as follows:
+
+A variable declaration such as
+```
+var x : fbits(32, dec)
+```
+would become
+```
+(declare-const x (BitVec 32))
+```
+
+A call to a builtin
+```
+x : T = f(y0, ... , yn)
+```
+would become
+```
+(define-const x T' exp)
+```
+where exp encodes the builtin f using SMT bitvector operations
+
+Phi functions are mapped to muxers as follows - for a function
+`phi(x0,...,xn)` we turn that into an if-then-else statement which
+selects `x0` to `xn` based on the global path conditionals of the
+parent blocks corresponding to each argument. Each phi function in a
+block always has the same number of arguments as the number of parent
+nodes, and the arguments are in the same order as the node index for
+each parent.
+
+The above scheme generates a lot of declare-const and define-const
+statements that may not be needed so we do some simple dead-code
+elimination and constant propagation, which results in the following
+SMT:
+```
+(set-logic QF_AUFBVDT)
+(declare-const zR/0 (_ BitVec 32))
+(define-const zysz3u12_lz30/5 (_ BitVec 32) (ite (not (= ((_ extract 0 0) zR/0) #b0)) #x00000000 #xFFFFFFFF))
+(assert (and (not (ite (not (= zysz3u12_lz30/5 #x00000000)) (= zysz3u12_lz30/5 (bvnot #x00000000)) true))))
+(check-sat)
+```
+
+For monomorphic-bitvector manipulating code we can generate very
+compact SMT. Both specialisation and monomorphisation can be used to
+help monomorphise bitvectors. For variable-length bitvectors we can
+represent them as length-bitvector pairs, up to a certain bounded max
+length (default 256). This is less efficient but unavoidable in
+certain places. Integers are currently mapped to either 128 bit
+bitvectors (or any configurable max length) or 64 bit bitvectors.
+
+The one slightly tricky thing to support is register references, e.g.
+```
+(*r) : T = 0xFFFF_FFFF
+```
+where `r` is a register reference. For this we look for all registers
+with type T (as a Jib type, where type-equality is trivial), and
+convert the above to
+```
+if r = ref R1 then
+  R1 = 0xFFFF_FFFF
+else if r = ref R2 then
+  R2 = 0xFFFF_FFFF
+else ...
+```
+if we did some smarter constant folding (e.g. propagating the GPRs
+letbinding in some of our specs) this could potentially generate SMT
+that is just as good as a manual if-then-else implementation of the
+register read/write functions. This step is done before converting to
+SSA so each register in the if-then-else cascade gets the correct
+indices.
diff --git a/doc/sail-smt.png b/doc/sail-smt.png
new file mode 100644
index 00000000..146a8c9f
--- /dev/null
+++ b/doc/sail-smt.png
diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index e65d9428..0d70b51e 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -45,7 +45,8 @@
 
 (defconst sail2-special
   '("_prove" "_not_prove" "create" "kill" "convert" "undefined"
-    "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" "$latex" "$property" "$counterexample"))
+    "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize"
+    "$latex" "$property" "$counterexample" "$suppress_warnings"))
 
 (defconst sail2-font-lock-keywords
   `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face)
diff --git a/language/sail.ott b/language/sail.ott
index a49a2adc..8ef2babf 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -532,133 +532,69 @@ internal_loop_measure :: 'Measure_' ::=
 
 exp :: 'E_' ::=
   {{ com expression }}
-  {{ aux _ annot }} {{ auxparam 'a }}  
-
-  | { exp1 ; ... ; expn }                               :: :: block {{ com sequential block }}
-% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)
-
-  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com nondeterministic block }}
-
+  {{ aux _ annot }} {{ auxparam 'a }}
+  | { exp1 ; ... ; expn }                               :: :: block
+    {{ com sequential block }}
   | id                                                  :: :: id
     {{ com identifier }}
-
   | lit                                                 :: :: lit
     {{ com literal constant }}
-
   | ( typ ) exp                                         :: :: cast
     {{ com cast }}
-
-  | id ( exp1 , .. , expn )                                   :: :: app
+  | id ( exp1 , .. , expn )                             :: :: app
     {{ com function application }}
-  | id exp                                               :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} 
-   {{ com funtion application to tuple }}
-
-% Note: fully applied function application only
-
   | exp1 id exp2                                        :: :: app_infix
     {{ com infix function application }}
- 
   | ( exp1 , .... , expn )                              :: :: tuple
     {{ com tuple }}
-
   | if exp1 then exp2 else exp3                         :: :: if
     {{ com conditional }}
-
   | if exp1 then exp2                                   :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
   | loop internal_loop_measure exp1 exp2                    :: :: loop
   | while internal_loop_measure exp1 do exp2                :: S :: while {{ ichlo [[ loop internal_loop_measure while exp1 exp2 ]] }}
   | repeat internal_loop_measure exp1 until exp2            :: S :: until {{ ichlo [[ loop internal_loop_measure until exp2 exp1 ]] }}
   | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for   {{ com loop }}
 
-% vectors
+  % vectors
   | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
-% order comes from global command-line option???
-% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn 
-% the expi and the result are both of type vector of 'a 
-
-% we pick [ ] not { } for vector literals for consistency with their
-% array-like access syntax, in contrast to the C which has funny
-% syntax for array literals.  We don't have to preserve [ ] for lists
-% as we don't expect to use lists very much. 
-
-  | exp [ exp' ]                                      :: :: vector_access
-  {{ com vector access }}
-
-  | exp [ exp1 '..' exp2 ]                               :: :: vector_subrange
-  {{ com subvector extraction }}
-  % do we want to allow a comma-separated list of such thingies?  
-
-  | [ exp with exp1 = exp2 ]                          :: :: vector_update 
-  {{ com vector functional update }}
-
-  | [ exp with exp1 : exp2 = exp3 ]                   :: :: vector_update_subrange
-  {{ com vector subrange update, with vector}}
-  % do we want a functional update form with a comma-separated list of such?
-
-  | exp : exp2                                        :: :: vector_append
-  {{ com vector concatenation }}
-
-% lists 
-  | [|| exp1 , ..  , expn ||]                           :: :: list
-  {{ com list }}
-  | exp1 '::' exp2                                    :: :: cons
-    {{ com cons }}
-
-
-% const unions
-
-% const structs
-
-% TODO
-
-  | { fexp0 , ... , fexpn }                    :: :: record
-    {{ com struct }}
-  | { exp with fexp0 , ... , fexpn }           :: :: record_update
-    {{ com functional update of struct }}
-  | exp . id                                   :: :: field
-    {{ com field projection from struct  }}
-
-%Expressions for creating and accessing vectors
-
+  | exp [ exp' ]                                      :: :: vector_access {{ com vector access }}
+  | exp [ exp1 '..' exp2 ]                            :: :: vector_subrange {{ com subvector extraction }}
+  | [ exp with exp1 = exp2 ]                          :: :: vector_update {{ com vector functional update }}
+  | [ exp with exp1 '..' exp2 = exp3 ]                :: :: vector_update_subrange {{ com vector subrange update, with vector}}
+  | exp1 @ exp2                                       :: :: vector_append {{ com vector concatenation }}
 
+  % lists
+  | [| exp1 , ..  , expn |]                           :: :: list {{ com list }}
+  | exp1 '::' exp2                                    :: :: cons {{ com cons }}
 
-%  map : forall 'x 'y ''N.  ('x -> 'y) -> vector ''N 'x -> vector ''N 'y
-%  zip : forall 'x 'y ''N.  vector ''N 'x  -> vector ''N 'y -> vector ''N ('x*'y) 
-%  foldl : forall 'x 'y ''N. ('x 'y -> 'y) -> vector ''N 'x -> 'y -> 'y
-% foldr : forall 'x 'y ''N. ('x 'y -> 'y) -> 'y -> vector ''N 'x -> 'y
-% foldmap : forall 'x 'y 'z ''N. ((x,y) -> (x,z)) -> x -> vector ''N y -> vector ''N z
-%(or unzip)
+  % structs
+  | struct { fexp0 , ... , fexpn }                    :: :: record {{ com struct }}
+  | { exp with fexp0 , ... , fexpn }                  :: :: record_update {{ com functional update of struct }}
+  | exp . id                                          :: :: field {{ com field projection from struct  }}
 
-%  and maybe with nice syntax
+  | match exp { pexp1 , ... , pexpn }                 :: :: case {{ com pattern matching }}
 
-  | match exp { pexp1 '|'  ... '|' pexpn } :: :: case
-    {{ com pattern matching }}
-%  | ( typ ) exp                                      :: :: Typed
-%    {{ com Type-annotated expressions }}
-  | letbind in exp                                  :: :: let
+  | letbind in exp                                    :: :: let
     {{ com let expression }}
 
-  | lexp := exp                                      :: :: assign
+  | lexp = exp                                        :: :: assign
     {{ com imperative assignment }}
 
-  | sizeof nexp                                         :: :: sizeof
-  {{ com the value of $[[nexp]]$ at run time }}
+  | sizeof nexp                                       :: :: sizeof
+    {{ com the value of $[[nexp]]$ at run time }}
 
-  | return exp                                       :: :: return {{ com  return $[[exp]]$ from current function }}
-% this can be used to break out of for loops
-  | exit exp						:: :: exit
+  | return exp                                        :: :: return {{ com  return $[[exp]]$ from current function }}
+  | exit exp                                          :: :: exit
     {{ com halt all current execution }}
-  | ref id                                     :: :: ref
-  | throw exp                                  :: :: throw
-  | try exp catch pexp1 .. pexpn             :: :: try
-%, potentially calling a system, trap, or interrupt handler with exp
-  | assert ( exp , exp' )                            :: :: assert
-    {{ com halt with error $[[exp']]$ when not $[[exp]]$ }}
-% exp' is optional?
-  | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
-  | var lexp = exp in exp'    :: I :: var {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
-  | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }}
-  | return_int ( exp )                                          ::  :: internal_return {{ com For internal use to embed into monad definition }}
+  | ref id                                            :: :: ref
+  | throw exp                                         :: :: throw
+  | try exp catch { pexp1 , ... , pexpn }             :: :: try
+  | assert ( exp , exp' )                             :: :: assert
+    {{ com halt with error message $[[exp']]$ when not $[[exp]]$. exp' is optional. }}
+  | ( exp )                                           :: S :: paren {{ ichlo [[exp]] }}
+  | var lexp = exp in exp'  :: I :: var {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
+  | let pat = exp in exp'   :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }}
+  | return_int ( exp )      ::  :: internal_return {{ com For internal use to embed into monad definition }}
   | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
   | constraint n_constraint :: :: constraint
 
diff --git a/lib/arith.sail b/lib/arith.sail
index 1950080a..d04c7988 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -70,7 +70,7 @@ val _shl_int = "shl_int" : (int, int) -> int
 
 overload shl_int = {_shl8, _shl32, _shl_int}
 
-val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
+val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
 
 val _shr_int = "shr_int" : (int, int) -> int
 
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 5a5f130c..9b5888c7 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -291,6 +291,9 @@ rewrite <- Z.lt_le_pred.
 auto.
 Defined.
 
+Definition sint0 {a} `{ArithFact (a >= 0)} (x : mword a) : Z :=
+  if sumbool_of_bool (Z.eqb a 0) then 0 else projT1 (sint x).
+
 Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0.
 unfold length_list.
 auto with zarith.
@@ -393,9 +396,9 @@ val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val rotl         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
 (* TODO: check/redefine behaviour on out-of-range n *)
-Definition shiftl       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift w (Z.to_nat n)) v.
-Definition shiftr       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift w (Z.to_nat n)) v.
-Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta w (Z.to_nat n)) v.
+Definition shiftl       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift' w (Z.to_nat n)) v.
+Definition shiftr       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift' w (Z.to_nat n)) v.
+Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta' w (Z.to_nat n)) v.
 (*
 Definition rotl         := rotl_bv
 Definition rotr         := rotr_bv
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 5ab93cbc..68d097fb 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -181,6 +181,37 @@ Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
+Fixpoint pick_bit_list {rv e} (n:nat) : monad rv (list bool) e :=
+  match n with
+  | O => returnm []
+  | S m => choose_bool "pick_bit_list" >>= fun b =>
+           pick_bit_list m >>= fun t =>
+           returnm (b::t)
+  end%list.
+
+Definition internal_pick {rv a e} (xs : list a) : monad rv a e :=
+  let n := length xs in
+  match xs with
+  | h::_ =>
+    pick_bit_list (2 + n) >>= fun bs =>
+    let i := (Word.wordToNat (wordFromBitlist bs) mod n)%nat in
+    returnm (List.nth i xs h)
+  | [] => Fail "internal_pick called on empty list"
+  end.
+
+Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e :=
+  match n with
+  | O => returnm Word.WO
+  | S m =>
+    choose_bool "undefined_word_nat" >>= fun b =>
+    undefined_word_nat m >>= fun t =>
+    returnm (Word.WS b t)
+  end.
+
+Definition undefined_bitvector {rv e} n `{ArithFact (n >= 0)} : monad rv (mword n) e :=
+  undefined_word_nat (Z.to_nat n) >>= fun w =>
+  returnm (word_to_mword w).
+
 (* If we need to build an existential after a monadic operation, assume that
    we can do it entirely from the type. *)
 
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index f95e4b6c..b26a2ff3 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -113,6 +113,8 @@ Definition choose_bool {rv E} descr : monad rv bool E := Choose descr returnm.
 (*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
 Definition undefined_bool {rv e} (_:unit) : monad rv bool e := choose_bool "undefined_bool".
 
+Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
+
 (*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
 Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
  if exp then Done tt else Fail msg.
diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v
index e4e4316e..494e36d4 100644
--- a/lib/coq/Sail2_real.v
+++ b/lib/coq/Sail2_real.v
@@ -9,16 +9,28 @@ Instance Decidable_eq_real : forall (x y : R), Decidable (x = y) :=
 
 Definition realFromFrac (num denom : Z) : R := Rdiv (IZR num) (IZR denom).
 
+Definition neg_real := Ropp.
+Definition mult_real := Rmult.
+Definition sub_real := Rminus.
+Definition add_real := Rplus.
+Definition div_real := Rdiv.
+Definition sqrt_real := sqrt.
+Definition abs_real := Rabs.
+
+(* Use flocq definitions, but without making the whole library a dependency. *)
+Definition round_down (x : R) := (up x - 1)%Z.
+Definition round_up (x : R) := (- round_down (- x))%Z.
+
+Definition to_real := IZR.
+
+Definition eq_real := Reqb.
 Definition gteq_real (x y : R) : bool := if Rge_dec x y then true else false.
 Definition lteq_real (x y : R) : bool := if Rle_dec x y then true else false.
 Definition gt_real (x y : R) : bool := if Rgt_dec x y then true else false.
 Definition lt_real (x y : R) : bool := if Rlt_dec x y then true else false.
 
 (* Export select definitions from outside of Rbase *)
-Definition powerRZ := powerRZ.
-Definition Rabs := Rabs.
-Definition sqrt := sqrt.
+Definition pow_real := powerRZ.
 
-(* Use flocq definitions, but without making the whole library a dependency. *)
-Definition Zfloor (x : R) := (up x - 1)%Z.
-Definition Zceil (x : R) := (- Zfloor (- x))%Z.
+Definition print_real (_ : string) (_ : R) : unit := tt.
+Definition prerr_real (_ : string) (_ : R) : unit := tt.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 1ddc3f22..17d79830 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -156,6 +156,16 @@ apply Zmult_ge_compat; auto with zarith.
 * apply Z_div_ge0; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith.
 Qed.
 
+Lemma ZEuclid_pos_div : forall x y, y > 0 -> ZEuclid.div x y >= 0 -> x >= 0.
+intros x y GT.
+  specialize (ZEuclid.div_mod x y);
+  specialize (ZEuclid.mod_always_pos x y);
+  generalize (ZEuclid.modulo x y);
+  generalize (ZEuclid.div x y);
+  intros.
+nia.
+Qed.
+
 Lemma ZEuclid_div_ge : forall x y, y > 0 -> x >= 0 -> x - ZEuclid.div x y >= 0.
 intros.
 unfold ZEuclid.div.
@@ -185,7 +195,7 @@ apply ZEuclid.div_mod.
 assumption.
 Qed.
 
-Hint Resolve ZEuclid_div_pos ZEuclid_div_ge ZEuclid_div_mod0 : sail.
+Hint Resolve ZEuclid_div_pos ZEuclid_pos_div ZEuclid_div_ge ZEuclid_div_mod0 : sail.
 
 
 (*
@@ -873,6 +883,9 @@ Program Definition to_word {n} : n >= 0 -> word (Z.to_nat n) -> mword n :=
   | Zpos _ => fun _ w => w
   end.
 
+Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >= 0)} : mword n :=
+  to_word (match H with Build_ArithFact _ H' => H' end) w.
+
 (*val length_mword : forall a. mword a -> Z*)
 Definition length_mword {n} (w : mword n) := n.
 
@@ -904,7 +917,7 @@ Parameter undefined_bit : bool.
 Definition getBit {n} :=
 match n with
 | O => fun (w : word O) i => undefined_bit
-| S n => fun (w : word (S n)) i => wlsb (wrshift w i)
+| S n => fun (w : word (S n)) i => wlsb (wrshift' w i)
 end.
 
 Definition access_mword_dec {m} (w : mword m) n := bitU_of_bool (getBit (get_word w) (Z.to_nat n)).
@@ -922,7 +935,7 @@ Definition setBit {n} :=
 match n with
 | O => fun (w : word O) i b => w
 | S n => fun (w : word (S n)) i (b : bool) =>
-  let bit : word (S n) := wlshift (natToWord _ 1) i in
+  let bit : word (S n) := wlshift' (natToWord _ 1) i in
   let mask : word (S n) := wnot bit in
   let masked := wand mask w in
   if b then masked else wor masked bit
@@ -1051,9 +1064,9 @@ end.
 (* Definitions in the context that involve proof for other constraints can
    break some of the constraint solving tactics, so prune definition bodies
    down to integer types. *)
-Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end.
-Ltac clear_non_Z_defns := 
-  repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end.
+Ltac not_Z_bool ty := match ty with Z => fail 1 | bool => fail 1 | _ => idtac end.
+Ltac clear_non_Z_bool_defns := 
+  repeat match goal with H := _ : ?X |- _ => not_Z_bool X; clearbody H end.
 Ltac clear_irrelevant_defns :=
 repeat match goal with X := _ |- _ =>
   match goal with |- context[X] => idtac end ||
@@ -1119,11 +1132,11 @@ Ltac unbool_comparisons_goal :=
 (* Split up dependent pairs to get at proofs of properties *)
 Ltac extract_properties :=
   (* Properties of local definitions *)
-  repeat match goal with H := (projT1 ?X) |- _ =>
+  repeat match goal with H := context[projT1 ?X] |- _ =>
     let x := fresh "x" in
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
-    change (projT1 (existT _ x Hx)) with x in *; unfold H in * end;
+    change (projT1 (existT _ x Hx)) with x in * end;
   (* Properties in the goal *)
   repeat match goal with |- context [projT1 ?X] =>
     let x := fresh "x" in
@@ -1240,7 +1253,9 @@ Ltac filter_disjunctions :=
   | H1:context [?t = true \/ ?P], H2: ?t = false |- _ => is_var t; rewrite H2 in H1
   | H1:context [?t = false \/ ?P], H2: ?t = true |- _ => is_var t; rewrite H2 in H1
   end;
-  repeat rewrite truefalse, falsetrue, or_False_l, or_False_r in *.
+  rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *;
+  (* We may have uncovered more conjunctions *)
+  repeat match goal with H:and _ _ |- _ => destruct H end.
 
 (* Turn x := if _ then ... into x = ... \/ x = ... *)
 
@@ -1296,10 +1311,51 @@ Ltac clear_irrelevant_bindings :=
       end
     end.
 
+(* Currently, the ASL to Sail translation produces some constraints of the form
+   P \/ x = true, P \/ x = false, which are simplified by the tactic below.  In
+   future the translation is likely to be cleverer, and this won't be
+   necessary. *)
+(* TODO: remove duplication with filter_disjunctions *)
+Lemma remove_unnecessary_casesplit {P:Prop} {x} :
+  P \/ x = true -> P \/ x = false -> P.
+  intuition congruence.
+Qed.
+Lemma remove_eq_false_true {P:Prop} {x} :
+  x = true -> P \/ x = false -> P.
+intros H1 [H|H]; congruence.
+Qed.
+Lemma remove_eq_true_false {P:Prop} {x} :
+  x = false -> P \/ x = true -> P.
+intros H1 [H|H]; congruence.
+Qed.
+Ltac remove_unnecessary_casesplit :=
+repeat match goal with
+| H1 : ?P \/ ?v = true, H2 : ?v = true |- _ => clear H1
+| H1 : ?P \/ ?v = true, H2 : ?v = false |- _ => apply (remove_eq_true_false H2) in H1
+| H1 : ?P \/ ?v = false, H2 : ?v = false |- _ => clear H1
+| H1 : ?P \/ ?v = false, H2 : ?v = true |- _ => apply (remove_eq_false_true H2) in H1
+| H1 : ?P \/ ?v1 = true, H2 : ?P \/ ?v2 = false |- _ =>
+  constr_eq v1 v2;
+  is_var v1;
+  apply (remove_unnecessary_casesplit H1) in H2;
+  clear H1
+  (* There are worse cases where the hypotheses are different, so we actually
+     do the casesplit *)
+| H1 : _ \/ ?v = true, H2 : _ \/ ?v = false |- _ =>
+  is_var v;
+  destruct v;
+  [ clear H1; destruct H2; [ | congruence ]
+  | clear H2; destruct H1; [ | congruence ]
+  ]
+end;
+(* We may have uncovered more conjunctions *)
+repeat match goal with H:and _ _ |- _ => destruct H end.
+
+
 Ltac prepare_for_solver :=
 (*dump_context;*)
  clear_irrelevant_defns;
- clear_non_Z_defns;
+ clear_non_Z_bool_defns;
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  split_cases;
  extract_properties;
@@ -1309,6 +1365,7 @@ Ltac prepare_for_solver :=
  unbool_comparisons;
  unbool_comparisons_goal;
  repeat match goal with H:and _ _ |- _ => destruct H end;
+ remove_unnecessary_casesplit;
  unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
  reduce_pow;
@@ -1357,7 +1414,14 @@ tauto.
 Qed.
 
 Ltac solve_euclid :=
-repeat match goal with |- context [ZEuclid.modulo ?x ?y] =>
+repeat match goal with
+| |- context [ZEuclid.modulo ?x ?y] =>
+  specialize (ZEuclid.div_mod x y);
+  specialize (ZEuclid.mod_always_pos x y);
+  generalize (ZEuclid.modulo x y);
+  generalize (ZEuclid.div x y);
+  intros
+| |- context [ZEuclid.div ?x ?y] =>
   specialize (ZEuclid.div_mod x y);
   specialize (ZEuclid.mod_always_pos x y);
   generalize (ZEuclid.modulo x y);
@@ -1420,14 +1484,136 @@ Ltac simple_ex_iff :=
     solve [apply iff_refl | eassumption]
   end.
 
+(* Another attempt at similar goals, this time allowing for conjuncts to move
+  around, and filling in integer existentials and redundant boolean ones.
+   TODO: generalise / combine with simple_ex_iff. *)
+
+Ltac ex_iff_construct_bool_witness :=
+let rec search x y :=
+  lazymatch y with
+  | x => constr:(true)
+  | ?y1 /\ ?y2 =>
+    let b1 := search x y1 in
+    let b2 := search x y2 in
+    constr:(orb b1 b2)
+  | _ => constr:(false)
+  end
+in
+let rec make_clause x :=
+  lazymatch x with
+  | ?l = true => l
+  | ?l = false => constr:(negb l)
+  | @eq Z ?l ?n => constr:(Z.eqb l n)
+  | ?p \/ ?q =>
+    let p' := make_clause p in
+    let q' := make_clause q in
+    constr:(orb p' q')
+  | _ => fail
+  end in
+let add_clause x xs :=
+  let l := make_clause x in
+  match xs with
+  | true => l
+  | _ => constr:(andb l xs)
+  end
+in
+let rec construct_ex l r x :=
+  lazymatch l with
+  | ?l1 /\ ?l2 =>
+    let y := construct_ex l1 r x in
+    construct_ex l2 r y
+  | _ =>
+   let present := search l r in
+   lazymatch eval compute in present with true => x | _ => add_clause l x end
+  end
+in
+let witness := match goal with
+| |- ?l <-> ?r => construct_ex l r constr:(true)
+end in
+instantiate (1 := witness).
+
+Ltac ex_iff_fill_in_ints :=
+  let rec search l r y :=
+    match y with
+    | l = r => idtac
+    | ?v = r => is_evar v; unify v l
+    | ?y1 /\ ?y2 => first [search l r y1 | search l r y2]
+    | _ => fail
+    end
+  in
+  match goal with
+  | |- ?l <-> ?r =>
+    let rec traverse l :=
+    lazymatch l with
+    | ?l1 /\ ?l2 =>
+      traverse l1; traverse l2
+    | @eq Z ?x ?y => search x y r
+    | _ => idtac
+    end
+    in traverse l
+  end.
+
+Ltac ex_iff_fill_in_bools :=
+  let rec traverse t :=
+    lazymatch t with
+    | ?v = ?t => try (is_evar v; unify v t)
+    | ?p /\ ?q => traverse p; traverse q
+    | _ => idtac
+    end
+  in match goal with
+  | |- _ <-> ?r => traverse r
+  end.
+
+Ltac conjuncts_iff_solve :=
+  ex_iff_fill_in_ints;
+  ex_iff_construct_bool_witness;
+  ex_iff_fill_in_bools;
+  unbool_comparisons_goal;
+  clear;
+  intuition.
+
+Ltac ex_iff_solve :=
+  match goal with
+  | |- @ex _ _ => eexists; ex_iff_solve
+  (* Range constraints are attached to the right *)
+  | |- _ /\ _ => split; [ex_iff_solve | omega]
+  | |- _ <-> _ => conjuncts_iff_solve
+  end.
+
+
 Lemma iff_false_left {P Q R : Prop} : (false = true) <-> Q -> (false = true) /\ P <-> Q /\ R.
 intuition.
 Qed.
 
+(* Very simple proofs for trivial arithmetic.  Preferable to running omega/lia because
+   they can get bogged down if they see large definitions; should also guarantee small
+   proof terms. *)
+Lemma Z_compare_lt_eq : Lt = Eq -> False. congruence. Qed.
+Lemma Z_compare_lt_gt : Lt = Gt -> False. congruence. Qed.
+Lemma Z_compare_eq_lt : Eq = Lt -> False. congruence. Qed.
+Lemma Z_compare_eq_gt : Eq = Gt -> False. congruence. Qed.
+Lemma Z_compare_gt_lt : Gt = Lt -> False. congruence. Qed.
+Lemma Z_compare_gt_eq : Gt = Eq -> False. congruence. Qed.
+Ltac z_comparisons :=
+  solve [
+    exact eq_refl
+  | exact Z_compare_lt_eq
+  | exact Z_compare_lt_gt
+  | exact Z_compare_eq_lt
+  | exact Z_compare_eq_gt
+  | exact Z_compare_gt_lt
+  | exact Z_compare_gt_eq
+  ].
+
+
+(* Redefine this to add extra solver tactics *)
+Ltac sail_extra_tactic := fail.
+
 Ltac main_solver :=
  solve
  [ match goal with |- (?x ?y) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) y) end
  | apply ArithFact_mword; assumption
+ | z_comparisons
  | omega with Z
    (* Try sail hints before dropping the existential *)
  | subst; eauto 3 with zarith sail
@@ -1439,8 +1625,22 @@ Ltac main_solver :=
                         | |- context [ZEuclid.modulo] => solve_euclid
    end
  | match goal with |- context [Z.mul] => nia end
+ (* If we have a disjunction from a set constraint on a variable we can often
+    solve a goal by trying them (admittedly this is quite heavy handed...) *)
+ | subst;
+   let aux x :=
+    is_var x;
+    intuition (subst;auto)
+   in
+   match goal with
+   | _:(@eq Z _ ?x) \/ (@eq Z _ ?x) \/ _ |- context[?x] => aux x
+   | _:(@eq Z ?x _) \/ (@eq Z ?x _) \/ _ |- context[?x] => aux x
+   | _:(@eq Z _ ?x) \/ (@eq Z _ ?x) \/ _, _:@eq Z ?y (ZEuclid.div ?x _) |- context[?y] => is_var x; aux y
+   | _:(@eq Z ?x _) \/ (@eq Z ?x _) \/ _, _:@eq Z ?y (ZEuclid.div ?x _) |- context[?y] => is_var x; aux y
+   end
  (* Booleans - and_boolMP *)
  | simple_ex_iff
+ | ex_iff_solve
  | drop_bool_exists; solve [eauto using iff_refl, or_iff_cong, and_iff_cong | intuition]
  | match goal with |- (forall l r:bool, _ -> _ -> exists _ : bool, _) =>
      let r := fresh "r" in
@@ -1479,9 +1679,18 @@ Ltac main_solver :=
      (* Don't use auto for the fallback to keep runtime down *)
      firstorder fail
    end*)
+ | sail_extra_tactic
  | idtac "Unable to solve constraint"; dump_context; fail
  ].
 
+(* Omega can get upset by local definitions that are projections from value/proof pairs.
+   Complex goals can use prepare_for_solver to extract facts; this tactic can be used
+   for simpler proofs without using prepare_for_solver. *)
+Ltac simple_omega :=
+  repeat match goal with
+  H := projT1 _ |- _ => clearbody H
+  end; omega.
+
 Ltac solve_arithfact :=
 (* Attempt a simple proof first to avoid lengthy preparation steps (especially
    as the large proof terms can upset subsequent proofs). *)
@@ -1492,7 +1701,8 @@ try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end
 (* Trying reflexivity will fill in more complex metavariable examples than
    fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
 try (constructor; reflexivity);
-try (constructor; omega);
+try (constructor; repeat match goal with |- and _ _ => split end; z_comparisons);
+try (constructor; simple_omega);
 prepare_for_solver;
 (*dump_context;*)
 constructor;
@@ -2145,6 +2355,23 @@ subst; compute;
 auto using Build_ArithFact.
 Defined.
 
+Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <= x <= 31)} `{HR:ArithFact (y = 1)}: {z : Z & ArithFact (0 <= z <= 15)}.
+refine (existT _ (shr_int x y) _).
+destruct HE as [HE].
+destruct HR as [HR];
+subst.
+unfold shr_int.
+rewrite <- Z.div2_spec.
+constructor.
+rewrite Z.div2_div.
+specialize (Z.div_mod x 2).
+specialize (Z.mod_pos_bound x 2).
+generalize (Z.div x 2).
+generalize (x mod 2).
+intros.
+nia.
+Defined.
+
 Lemma shl_8_ge_0 {n} : shl_int 8 n >= 0.
 unfold shl_int.
 apply Z.le_ge.  
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 4e4a099f..965b236e 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -61,6 +61,7 @@ THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits.
  */
 val truncateLSB = {
   ocaml: "vector_truncateLSB",
+  interpreter: "vector_truncateLSB",
   lem: "vector_truncateLSB",
   coq: "vector_truncateLSB",
   c: "sail_truncateLSB"
@@ -205,7 +206,7 @@ val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bit
 val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
 function slice_mask(n,i,l) =
   if l >= n then {
-    sail_ones(n)
+    sail_shiftleft(sail_ones(n), i)
   } else {
     let one : bits('n) = sail_mask(n, 0b1 : bits(1)) in
     sail_shiftleft(sub_bits(sail_shiftleft(one, l), one), i)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 014d50d0..b061600f 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -197,7 +197,7 @@ module Nexp = struct
        let lex2 = List.length args1 - List.length args2 in
        let lex3 =
          if lex2 = 0 then
-           List.fold_left2 (fun l n1 n2 -> if compare n1 n2 = 0 then 0 else compare n1 n2) 0 args1 args2
+           List.fold_left2 (fun l n1 n2 -> lex_ord (l, compare n1 n2)) 0 args1 args2
          else 0
        in
        lex_ord (lex1, lex_ord (lex2, lex3))
@@ -515,7 +515,6 @@ let unaux_constraint (NC_aux (nc, _)) = nc
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
-  | E_nondet xs -> E_nondet (List.map (map_exp_annot f) xs)
   | E_id id -> E_id id
   | E_ref id -> E_ref id
   | E_lit lit -> E_lit lit
@@ -942,7 +941,6 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_var (lexp, binding, exp) -> "var " ^ string_of_lexp lexp ^ " = " ^ string_of_exp binding ^ " in " ^ string_of_exp exp
   | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
   | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
-  | E_nondet _ -> "NONDET"
   | E_internal_value v -> "INTERNAL_VALUE(" ^ Value.string_of_value v ^ ")"
 
 and string_of_measure (Measure_aux (m,_)) =
@@ -1537,7 +1535,6 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
   let wrap e_aux = E_aux (e_aux, annot) in
   let e_aux = match e_aux with
     | E_block exps -> E_block (List.map (subst id value) exps)
-    | E_nondet exps -> E_nondet (List.map (subst id value) exps)
     | E_id id' -> if Id.compare id id' = 0 then unaux_exp value else E_id id'
     | E_lit lit -> E_lit lit
     | E_cast (typ, exp) -> E_cast (typ, subst id value exp)
@@ -1759,7 +1756,6 @@ and locate_fpat : 'a. (l -> l) -> 'a fpat -> 'a fpat = fun f (FP_aux (FP_Fpat (i
 let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, annot))) ->
   let e_aux = match e_aux with
     | E_block exps -> E_block (List.map (locate f) exps)
-    | E_nondet exps -> E_nondet (List.map (locate f) exps)
     | E_id id -> E_id (locate_id f id)
     | E_lit lit -> E_lit (locate_lit f lit)
     | E_cast (typ, exp) -> E_cast (locate_typ f typ, locate f exp)
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 4c26b641..abedcf35 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -201,9 +201,10 @@ let rw_exp ok not_ok istate =
         try (ok (); Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)) with
         | Type_error (env, l, err) ->
            (* A type error here would be unexpected, so don't ignore it! *)
-           Util.warn ("Type error when folding constants in "
-                      ^ string_of_exp (E_aux (e_aux, annot))
-                      ^ "\n" ^ Type_error.string_of_type_error err);
+           Reporting.warn "" l
+             ("Type error when folding constants in "
+              ^ string_of_exp (E_aux (e_aux, annot))
+              ^ "\n" ^ Type_error.string_of_type_error err);
            not_ok ();
            E_aux (e_aux, annot)
       end
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 89a4ba82..201e43e7 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -387,9 +387,6 @@ let const_props defs ref_vars =
     | E_block es ->
        let es',assigns = threaded_map (const_prop_exp substs) assigns es in
        re (E_block es') assigns
-    | E_nondet es ->
-       let es',assigns = non_det_exp_list es in
-       re (E_nondet es') assigns
     | E_id id ->
        let env = Type_check.env_of_annot (l, annot) in
        (try
diff --git a/src/graph.ml b/src/graph.ml
index 703deba9..62da3292 100644
--- a/src/graph.ml
+++ b/src/graph.ml
@@ -69,15 +69,6 @@ module type S =
     val add_edge : node -> node -> graph -> graph
     val add_edges : node -> node list -> graph -> graph
 
-    (** Add edges to the graph, but may leave the internal structure
-       of the graph in a non-normalized state. Fix leaves repairs any
-       such issue in the graph. These additional functions are much
-       faster than those above, but it is important to call fix_leaves
-       before calling reachable, prune, or any other function. *)
-    val add_edge' : node -> node -> graph -> graph
-    val add_edges' : node -> node list -> graph -> graph
-    val fix_leaves : graph -> graph
-
     val children : graph -> node -> node list
 
     (** Return the set of nodes that are reachable from the first set
@@ -125,25 +116,26 @@ module Make(Ord: OrderedType) = struct
     with
     | Not_found -> []
 
-  let fix_leaves cg =
-    NS.fold (fun leaf cg -> if NM.mem leaf cg then cg else NM.add leaf NS.empty cg) (leaves cg) cg
+  let fix_some_leaves cg nodes =
+    NS.fold (fun leaf cg -> if NM.mem leaf cg then cg else NM.add leaf NS.empty cg) nodes cg
+
+  let fix_leaves cg = fix_some_leaves cg (leaves cg)
 
-  let add_edge' caller callee cg =
+  let add_edge caller callee cg =
+    let cg = fix_some_leaves cg (NS.singleton callee) in
     try
       NM.add caller (NS.add callee (NM.find caller cg)) cg
     with
     | Not_found -> NM.add caller (NS.singleton callee) cg
 
-  let add_edges' caller callees cg =
+  let add_edges caller callees cg =
     let callees = List.fold_left (fun s c -> NS.add c s) NS.empty callees in
+    let cg = fix_some_leaves cg callees in
     try
       NM.add caller (NS.union callees (NM.find caller cg)) cg
     with
     | Not_found -> NM.add caller callees cg
 
-  let add_edge caller callee cg = fix_leaves (add_edge' caller callee cg)
-  let add_edges caller callees cg = fix_leaves (add_edges' caller callees cg)
-
   let reachable roots cuts cg =
     let visited = ref NS.empty in
 
diff --git a/src/graph.mli b/src/graph.mli
index 02480a9d..09b78304 100644
--- a/src/graph.mli
+++ b/src/graph.mli
@@ -71,15 +71,6 @@ module type S =
     val add_edge : node -> node -> graph -> graph
     val add_edges : node -> node list -> graph -> graph
 
-    (** Add edges to the graph, but may leave the internal structure
-       of the graph in a non-normalized state. Fix leaves repairs any
-       such issue in the graph. These additional functions are much
-       faster than those above, but it is important to call fix_leaves
-       before calling reachable, prune, or any other function. *)
-    val add_edge' : node -> node -> graph -> graph
-    val add_edges' : node -> node list -> graph -> graph
-    val fix_leaves : graph -> graph
-
     val children : graph -> node -> node list
 
     (** Return the set of nodes that are reachable from the first set
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 1f15d054..b2e3dc79 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -365,7 +365,6 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
       (match to_ast_fexps false ctx exps with
       | Some(fexps) -> E_record(fexps)
       | None -> E_block(List.map (to_ast_exp ctx) exps))
-    | P.E_nondet(exps) -> E_nondet(List.map (to_ast_exp ctx) exps)
     | P.E_id(id) -> E_id(to_ast_id id)
     | P.E_ref(id) -> E_ref(to_ast_id id)
     | P.E_lit(lit) -> E_lit(to_ast_lit lit)
diff --git a/src/interpreter.ml b/src/interpreter.ml
index db4f45f6..def0963f 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -549,7 +549,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      wrap (E_block (E_aux (E_assign (lexp, exp), annot) :: body))
   | E_var (lexp, exp, body) ->
      wrap (E_block [E_aux (E_assign (lexp, exp), annot); body])
-     
+
   | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp'))
   | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp]))
   | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
diff --git a/src/isail.ml b/src/isail.ml
index 094ad3df..9e9b6236 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -266,6 +266,10 @@ let help =
   | ":compile" ->
      sprintf ":compile %s - Compile AST to a specified target, valid targets are lem, coq, ocaml, c, and ir (intermediate representation)"
              (color yellow "<target>")
+  | ":slice" ->
+     ":slice - Slice AST to the definitions which the functions given by :slice_roots depend on, up to the functions given by :slice_cuts"
+  | ":thin_slice" ->
+     ":thin_slice - Slice AST to the function definitions given with :slice_roots"
   | "" ->
      sprintf "Type %s for a list of commands, and %s %s for information about a specific command"
              (color green ":commands") (color green ":help") (color yellow "<command>")
@@ -425,7 +429,7 @@ let handle_input' input =
           | Arg.Bad message | Arg.Help message -> print_endline message
         end;
      | ":spec" ->
-        let ast, env = Specialize.(specialize' 1 int_specialization !Interactive.ast !Interactive.env) in
+        let ast, env = Specialize.(specialize_passes 1 int_specialization !Interactive.env !Interactive.ast) in
         Interactive.ast := ast;
         Interactive.env := env;
         interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops
@@ -540,7 +544,22 @@ let handle_input' input =
            let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
            let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
            let g = G.prune roots cuts g in
-           Interactive.ast := Slice.filter_ast !slice_cuts g !Interactive.ast
+           Interactive.ast := Slice.filter_ast cuts g !Interactive.ast
+        | ":thin_slice" ->
+           let open Slice in
+           let module SliceNodeSet = Set.Make(Slice.Node) in
+           let module SliceNodeMap = Map.Make(Slice.Node) in
+           let module G = Graph.Make(Slice.Node) in
+           let g = Slice.graph_of_ast !Interactive.ast in
+           let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in
+           let keep = function
+             | (Function id,_) when IdSet.mem id (!slice_roots) -> None
+             | (Function id,_) -> Some (Function id)
+             | _ -> None
+           in
+           let cuts = SliceNodeMap.bindings g |> Util.map_filter keep |> SliceNodeSet.of_list in
+           let g = G.prune roots cuts g in
+           Interactive.ast := Slice.filter_ast cuts g !Interactive.ast
         | ":list_rewrites" ->
            let print_rewrite (name, rw) =
              print_endline (name ^ " " ^ Util.(String.concat " " (describe_rewrite rw) |> yellow |> clear))
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index bd4813ed..5165904d 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -556,8 +556,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
   | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
 
   | E_block [] ->
-     Util.warn (Reporting.loc_to_string l
-                ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)");
+     Reporting.warn "" l
+       "Translating empty block (possibly assigning to an uninitialized variable at the end of a block?)";
      mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp))
   | E_block exps ->
      let exps, last = split_block l exps in
@@ -752,9 +752,5 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      (* Sizeof nodes removed by sizeof rewriting pass *)
      raise (Reporting.err_unreachable l __POS__ "encountered E_constraint node when converting to ANF")
 
-  | E_nondet _ ->
-     (* We don't compile E_nondet nodes *)
-     raise (Reporting.err_unreachable l __POS__ "encountered E_nondet node when converting to ANF")
-
   | E_internal_return _ | E_internal_plet _ ->
      raise (Reporting.err_unreachable l __POS__ "encountered unexpected internal node when converting to ANF")
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 90c0022d..0518b9c5 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -1184,6 +1184,89 @@ let fix_early_return ret instrs =
 
 let letdef_count = ref 0
 
+let compile_funcl ctx id pat guard exp =
+  (* Find the function's type. *)
+  let quant, Typ_aux (fn_typ, _) =
+    try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env
+  in
+  let arg_typs, ret_typ = match fn_typ with
+    | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
+    | _ -> assert false
+  in
+
+  (* Handle the argument pattern. *)
+  let fundef_label = label "fundef_fail_" in
+  let orig_ctx = ctx in
+  (* The context must be updated before we call ctyp_of_typ on the argument types. *)
+  let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in
+
+  let arg_ctyps =  List.map (ctyp_of_typ ctx) arg_typs in
+  let ret_ctyp = ctyp_of_typ ctx ret_typ in
+
+  (* Compile the function arguments as patterns. *)
+  let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in
+  let ctx =
+    (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *)
+    List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps
+  in
+
+  let guard_instrs = match guard with
+    | Some guard ->
+       let guard_aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in
+       let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in
+       let guard_label = label "guard_" in
+       let gs = ngensym () in
+       [iblock (
+            [idecl CT_bool gs]
+            @ guard_setup
+            @ [guard_call (CL_id (gs, CT_bool))]
+            @ guard_cleanup
+            @ [ijump (V_id (gs, CT_bool)) guard_label;
+               imatch_failure ();
+               ilabel guard_label]
+       )]
+    | None -> []
+  in
+
+  (* Optimize and compile the expression to ANF. *)
+  let aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in
+
+  let setup, call, cleanup = compile_aexp ctx aexp in
+  let destructure, destructure_cleanup =
+    compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label
+  in
+
+  let instrs = arg_setup @ destructure @ guard_instrs @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in
+  let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in
+  let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
+
+  if Id.compare (mk_id !opt_debug_function) id = 0 then
+    let header =
+      Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id)
+                     (Util.string_of_list ", " string_of_id (List.map fst compiled_args))
+                     (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps)
+                     Util.(string_of_ctyp ret_ctyp |> yellow |> clear)
+    in
+    prerr_endline (Util.header header (List.length arg_ctyps + 2));
+    prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs))
+  else ();
+
+  if !opt_debug_flow_graphs then
+    begin
+      let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
+      let root, _, cfg = Jib_ssa.control_flow_graph instrs in
+      let idom = Jib_ssa.immediate_dominators cfg root in
+      let _, cfg = Jib_ssa.ssa instrs in
+      let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
+      Jib_ssa.make_dot out_chan cfg;
+      close_out out_chan;
+      let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in
+      Jib_ssa.make_dominators_dot out_chan idom cfg;
+      close_out out_chan;
+    end;
+
+  [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
+
 (** Compile a Sail toplevel definition into an IR definition **)
 let rec compile_def n total ctx def =
   match def with
@@ -1243,76 +1326,16 @@ and compile_def' n total ctx = function
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
      Util.progress "Compiling " (string_of_id id) n total;
+     compile_funcl ctx id pat None exp
 
-     (* Find the function's type. *)
-     let quant, Typ_aux (fn_typ, _) =
-       try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env
-     in
-     let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
-       | _ -> assert false
-     in
-
-     (* Handle the argument pattern. *)
-     let fundef_label = label "fundef_fail_" in
-     let orig_ctx = ctx in
-     (* The context must be updated before we call ctyp_of_typ on the argument types. *)
-     let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in
-
-     let arg_ctyps =  List.map (ctyp_of_typ ctx) arg_typs in
-     let ret_ctyp = ctyp_of_typ ctx ret_typ in
-
-     (* Compile the function arguments as patterns. *)
-     let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in
-     let ctx =
-       (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *)
-       List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps
-     in
-
-     (* Optimize and compile the expression to ANF. *)
-     let aexp = no_shadow (pat_ids pat) (anf exp) in
-     let aexp = ctx.optimize_anf ctx aexp in
-
-     let setup, call, cleanup = compile_aexp ctx aexp in
-     let destructure, destructure_cleanup =
-       compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label
-     in
-
-     let instrs = arg_setup @ destructure @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in
-     let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in
-     let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
-
-     if Id.compare (mk_id !opt_debug_function) id = 0 then
-       let header =
-         Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id)
-                        (Util.string_of_list ", " string_of_id (List.map fst compiled_args))
-                        (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps)
-                        Util.(string_of_ctyp ret_ctyp |> yellow |> clear)
-       in
-       prerr_endline (Util.header header (List.length arg_ctyps + 2));
-       prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs))
-     else ();
-
-     if !opt_debug_flow_graphs then
-       begin
-         let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
-         let root, _, cfg = Jib_ssa.control_flow_graph instrs in
-         let idom = Jib_ssa.immediate_dominators cfg root in
-         let _, cfg = Jib_ssa.ssa instrs in
-         let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
-         Jib_ssa.make_dot out_chan cfg;
-         close_out out_chan;
-         let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in
-         Jib_ssa.make_dominators_dot out_chan idom cfg;
-         close_out out_chan;
-       end;
-
-     [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
+  | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_when (pat, guard, exp), _)), _)]), _)) ->
+     Util.progress "Compiling " (string_of_id id) n total;
+     compile_funcl ctx id pat (Some guard) exp
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) ->
      raise (Reporting.err_general l "Encountered function with no clauses")
 
-  | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) ->
+  | DEF_fundef (FD_aux (FD_function (_, _, _, _ :: _ :: _), (l, _))) ->
      raise (Reporting.err_general l "Encountered function with multiple clauses")
 
   (* All abbreviations should expanded by the typechecker, so we don't
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 0d70695b..07cab66b 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -88,6 +88,7 @@ type ctx = {
     arg_stack : (int * string) Stack.t;
     ast : Type_check.tannot defs;
     events : smt_exp Stack.t EventMap.t ref;
+    node : int;
     pathcond : smt_exp Lazy.t;
     use_string : bool ref;
     use_real : bool ref
@@ -112,6 +113,7 @@ let initial_ctx () = {
     arg_stack = Stack.create ();
     ast = Defs [];
     events = ref EventMap.empty;
+    node = -1;
     pathcond = lazy (Bool_lit true);
     use_string = ref false;
     use_real = ref false;
@@ -210,7 +212,7 @@ let bvpint sz x =
     let padding_size = sz - String.length bin in
     if padding_size < 0 then
       raise (Reporting.err_general Parse_ast.Unknown
-               (Printf.sprintf "Count not create a %d-bit integer with value %s.\nTry increasing the maximum integer size"
+               (Printf.sprintf "Could not create a %d-bit integer with value %s.\nTry increasing the maximum integer size"
                   sz (Big_int.to_string x)));
     let padding = String.make (sz - String.length bin) '0' in
     Bin (padding ^ bin)
@@ -258,65 +260,71 @@ let zencode_ctor ctor_id unifiers =
      Util.zencode_string (string_of_id ctor_id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
 
 let rec smt_cval ctx cval =
-  match cval with
-  | V_lit (vl, ctyp) -> smt_value ctx vl ctyp
-  | V_id (Name (id, _) as ssa_id, _) ->
-     begin match Type_check.Env.lookup_id id ctx.tc_env with
-     | Enum _ -> Enum (zencode_id id)
-     | _ -> Var (zencode_name ssa_id)
-     end
-  | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
-  | V_call (Neq, [cval1; cval2]) ->
-     Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
-  | V_call (Bvor, [cval1; cval2]) ->
-     Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
-  | V_call (Bit_to_bool, [cval]) ->
-     Fn ("=", [smt_cval ctx cval; Bin "1"])
-  | V_call (Bnot, [cval]) ->
-     Fn ("not", [smt_cval ctx cval])
-  | V_call (Band, cvals) ->
-     smt_conj (List.map (smt_cval ctx) cvals)
-  | V_call (Bor, cvals) ->
-     smt_disj (List.map (smt_cval ctx) cvals)
-  | V_ctor_kind (union, ctor_id, unifiers, _) ->
-     Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
-  | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
-     Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_cval ctx union])
-  | V_field (union, field) ->
-     begin match cval_ctyp union with
-     | CT_struct (struct_id, _) ->
-        Fn (zencode_upper_id struct_id ^ "_" ^ field, [smt_cval ctx union])
-     | _ -> failwith "Field for non-struct type"
-     end
-  | V_struct (fields, ctyp) ->
-     begin match ctyp with
-     | CT_struct (struct_id, field_ctyps) ->
-        let set_field (field, cval) =
-          match Util.assoc_compare_opt Id.compare field field_ctyps with
-          | None -> failwith "Field type not found"
-          | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
-             smt_cval ctx cval
-          | _ -> failwith "Type mismatch when generating struct for SMT"
-        in
-        Fn (zencode_upper_id struct_id, List.map set_field fields)
-     | _ -> failwith "Struct does not have struct type"
-     end
-  | V_tuple_member (frag, len, n) ->
-     ctx.tuple_sizes := IntSet.add len !(ctx.tuple_sizes);
-     Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval ctx frag])
-  | V_ref (Name (id, _), _) ->
-     let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
-     assert (CTMap.cardinal rmap = 1);
-     begin match CTMap.min_binding_opt rmap with
-     | Some (ctyp, regs) ->
-        begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
-        | Some i ->
-           bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
-        | None -> assert false
+  match cval_ctyp cval with
+  | CT_constant n ->
+     bvint (required_width n) n
+  | _ ->
+     match cval with
+     | V_lit (vl, ctyp) -> smt_value ctx vl ctyp
+     | V_id (Name (id, _) as ssa_id, _) ->
+        begin match Type_check.Env.lookup_id id ctx.tc_env with
+        | Enum _ -> Enum (zencode_id id)
+        | _ -> Var (zencode_name ssa_id)
         end
-     | _ -> assert false
-     end
-  | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)
+     | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
+     | V_call (Neq, [cval1; cval2]) ->
+        Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
+     | V_call (Bvor, [cval1; cval2]) ->
+        Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
+     | V_call (Bit_to_bool, [cval]) ->
+        Fn ("=", [smt_cval ctx cval; Bin "1"])
+     | V_call (Eq, [cval1; cval2]) ->
+        Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
+     | V_call (Bnot, [cval]) ->
+        Fn ("not", [smt_cval ctx cval])
+     | V_call (Band, cvals) ->
+        smt_conj (List.map (smt_cval ctx) cvals)
+     | V_call (Bor, cvals) ->
+        smt_disj (List.map (smt_cval ctx) cvals)
+     | V_ctor_kind (union, ctor_id, unifiers, _) ->
+        Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
+     | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
+        Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_cval ctx union])
+     | V_field (union, field) ->
+        begin match cval_ctyp union with
+        | CT_struct (struct_id, _) ->
+           Fn (zencode_upper_id struct_id ^ "_" ^ field, [smt_cval ctx union])
+        | _ -> failwith "Field for non-struct type"
+        end
+     | V_struct (fields, ctyp) ->
+        begin match ctyp with
+        | CT_struct (struct_id, field_ctyps) ->
+           let set_field (field, cval) =
+             match Util.assoc_compare_opt Id.compare field field_ctyps with
+             | None -> failwith "Field type not found"
+             | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
+                smt_cval ctx cval
+             | _ -> failwith "Type mismatch when generating struct for SMT"
+           in
+           Fn (zencode_upper_id struct_id, List.map set_field fields)
+        | _ -> failwith "Struct does not have struct type"
+        end
+     | V_tuple_member (frag, len, n) ->
+        ctx.tuple_sizes := IntSet.add len !(ctx.tuple_sizes);
+        Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval ctx frag])
+     | V_ref (Name (id, _), _) ->
+        let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
+        assert (CTMap.cardinal rmap = 1);
+        begin match CTMap.min_binding_opt rmap with
+        | Some (ctyp, regs) ->
+           begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
+           | Some i ->
+              bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
+           | None -> assert false
+           end
+        | _ -> assert false
+        end
+     | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)
 
 let add_event ctx ev smt =
   let stack = event_stack ctx ev in
@@ -327,7 +335,7 @@ let add_pathcond_event ctx ev =
 
 let overflow_check ctx smt =
   if not !opt_ignore_overflow then (
-    Util.warn "Adding overflow check in generated SMT";
+    Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l "";
     add_event ctx Overflow smt
   )
 
@@ -382,7 +390,7 @@ let builtin_gteq = builtin_int_comparison "bvsge" Big_int.greater_equal
 
 (* ***** Arithmetic operations: lib/arith.sail ***** *)
 
-(** [force_size n m exp] takes a smt expression assumed to be a
+(** [force_size ctx n m exp] takes a smt expression assumed to be a
    integer (signed bitvector) of length m and forces it to be length n
    by either sign extending it or truncating it as required *)
 let force_size ?checked:(checked=true) ctx n m smt =
@@ -402,6 +410,16 @@ let force_size ?checked:(checked=true) ctx n m smt =
     if checked then overflow_check ctx check else ();
     Extract (n - 1, 0, smt)
 
+(** [unsigned_size ctx n m exp] is much like force_size, but it
+   assumes that the bitvector is unsigned *)
+let unsigned_size ?checked:(checked=true) ctx n m smt =
+  if n = m then
+    smt
+  else if n > m then
+    Fn ("concat", [bvzero (n - m); smt])
+  else
+    failwith "bad arguments to unsigned_size"
+
 let int_size ctx = function
   | CT_constant n -> required_width n
   | CT_fint sz -> sz
@@ -420,13 +438,6 @@ let builtin_arith fn big_int_fn padding ctx v1 v2 ret_ctyp =
   | CT_constant c1, CT_constant c2, _ ->
      bvint (int_size ctx ret_ctyp) (big_int_fn c1 c2)
 
-  | ctyp, CT_constant c, _ ->
-     let n = int_size ctx ctyp in
-     force_size ctx (int_size ctx ret_ctyp) n (Fn (fn, [smt_cval ctx v1; bvint n c]))
-  | CT_constant c, ctyp, _ ->
-     let n = int_size ctx ctyp in
-     force_size ctx (int_size ctx ret_ctyp) n (Fn (fn, [bvint n c; smt_cval ctx v2]))
-
   | ctyp1, ctyp2, _ ->
      let ret_sz = int_size ctx ret_ctyp in
      let smt1 = smt_cval ctx v1 in
@@ -438,6 +449,12 @@ let builtin_add_int = builtin_arith "bvadd" Big_int.add (fun x -> x + 1)
 let builtin_sub_int = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1)
 let builtin_mult_int = builtin_arith "bvmul" Big_int.mul (fun x -> x * 2)
 
+let builtin_sub_nat ctx v1 v2 ret_ctyp =
+  let result = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1) ctx v1 v2 ret_ctyp in
+  Ite (Fn ("bvslt", [result; bvint (int_size ctx ret_ctyp) Big_int.zero]),
+       bvint (int_size ctx ret_ctyp) Big_int.zero,
+       result)
+
 let builtin_negate_int ctx v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
   | _, CT_constant c ->
@@ -493,6 +510,53 @@ let builtin_pow2 ctx v ret_ctyp =
 
   | _ -> builtin_type_error ctx "pow2" [v] (Some ret_ctyp)
 
+let builtin_max_int ctx v1 v2 ret_ctyp =
+  match cval_ctyp v1, cval_ctyp v2 with
+  | CT_constant n, CT_constant m ->
+     bvint (int_size ctx ret_ctyp) (max n m)
+
+  | ctyp1, ctyp2 ->
+     let ret_sz = int_size ctx ret_ctyp in
+     let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in
+     let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in
+     Ite (Fn ("bvslt", [smt1; smt2]),
+          smt2,
+          smt1)
+
+let builtin_min_int ctx v1 v2 ret_ctyp =
+  match cval_ctyp v1, cval_ctyp v2 with
+  | CT_constant n, CT_constant m ->
+     bvint (int_size ctx ret_ctyp) (min n m)
+
+  | ctyp1, ctyp2 ->
+     let ret_sz = int_size ctx ret_ctyp in
+     let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in
+     let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in
+     Ite (Fn ("bvslt", [smt1; smt2]),
+          smt1,
+          smt2)
+
+let builtin_eq_bits ctx v1 v2 =
+  match cval_ctyp v1, cval_ctyp v2 with
+  | CT_fbits (n, _), CT_fbits (m, _) ->
+     let o = max n m in
+     let smt1 = unsigned_size ctx o n (smt_cval ctx v1) in
+     let smt2 = unsigned_size ctx o n (smt_cval ctx v2) in
+     Fn ("=", [smt1; smt2])
+
+  | CT_lbits _, CT_lbits _ ->
+     Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+
+  | CT_lbits _, CT_fbits (n, _) ->
+     let smt2 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v2) in
+     Fn ("=", [Fn ("contents", [smt_cval ctx v1]); smt2])
+
+  | CT_fbits (n, _), CT_lbits _ ->
+     let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in
+     Fn ("=", [smt1; Fn ("contents", [smt_cval ctx v2])])
+
+  | _ -> builtin_type_error ctx "eq_bits" [v1; v2] None
+
 let builtin_zeros ctx v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
   | _, CT_fbits (n, _) -> bvzero n
@@ -514,7 +578,7 @@ let builtin_ones ctx cval = function
      Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; bvones (lbits_size ctx)])]);
   | ret_ctyp -> builtin_type_error ctx "ones" [cval] (Some ret_ctyp)
 
-(* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval
+(* [bvzeint ctx esz cval] (BitVector Zero Extend INTeger), takes a cval
    which must be an integer type (either CT_fint, or CT_lint), and
    produces a bitvector which is either zero extended or truncated to
    exactly esz bits. *)
@@ -773,11 +837,10 @@ let builtin_replicate_bits ctx v1 v2 ret_ctyp =
      let smt = smt_cval ctx v1 in
      Fn ("concat", List.init (Big_int.to_int c) (fun _ -> smt))
 
-  (*| CT_fbits (n, _), ctyp2, CT_lbits _ ->
-     let len = Fn ("bvmul", [bvint ctx.lbits_index (Big_int.of_int n);
-                             Extract (ctx.lbits_index - 1, 0, smt_cval ctx v2)])
-     in
-     assert false*)
+  | CT_fbits (n, _), _, CT_fbits (m, _) ->
+     let smt = smt_cval ctx v1 in
+     let c = m / n in
+     Fn ("concat", List.init c (fun _ -> smt))
 
   | _ -> builtin_type_error ctx "replicate_bits" [v1; v2] (Some ret_ctyp)
 
@@ -791,7 +854,12 @@ let builtin_sail_truncate ctx v1 v2 ret_ctyp =
      assert (Big_int.to_int c = m && m < lbits_size ctx);
      Extract (Big_int.to_int c - 1, 0, Fn ("contents", [smt_cval ctx v1]))
 
-  | _ -> builtin_type_error ctx "sail_truncate" [v2; v2] (Some ret_ctyp)
+  | CT_fbits (n, _), _, CT_lbits _ ->
+     let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in
+     let smt2 = bvzeint ctx ctx.lbits_index v2 in
+     Fn ("Bits", [smt2; Fn ("bvand", [bvmask ctx smt2; smt1])])
+
+  | _ -> builtin_type_error ctx "sail_truncate" [v1; v2] (Some ret_ctyp)
 
 let builtin_sail_truncateLSB ctx v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
@@ -927,7 +995,6 @@ let builtin_sqrt_real ctx root v =
 
 let smt_builtin ctx name args ret_ctyp =
   match name, args, ret_ctyp with
-  | "eq_bits", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
   | "eq_anything", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
 
   (* lib/flow.sail *)
@@ -946,6 +1013,7 @@ let smt_builtin ctx name args ret_ctyp =
   (* lib/arith.sail *)
   | "add_int", [v1; v2], _ -> builtin_add_int ctx v1 v2 ret_ctyp
   | "sub_int", [v1; v2], _ -> builtin_sub_int ctx v1 v2 ret_ctyp
+  | "sub_nat", [v1; v2], _ -> builtin_sub_nat ctx v1 v2 ret_ctyp
   | "mult_int", [v1; v2], _ -> builtin_mult_int ctx v1 v2 ret_ctyp
   | "neg_int", [v], _ -> builtin_negate_int ctx v ret_ctyp
   | "shl_int", [v1; v2], _ -> builtin_shl_int ctx v1 v2 ret_ctyp
@@ -955,6 +1023,9 @@ let smt_builtin ctx name args ret_ctyp =
   | "abs_int", [v], _ -> builtin_abs_int ctx v ret_ctyp
   | "pow2", [v], _ -> builtin_pow2 ctx v ret_ctyp
 
+  | "max_int", [v1; v2], _ -> builtin_max_int ctx v1 v2 ret_ctyp
+  | "min_int", [v1; v2], _ -> builtin_min_int ctx v1 v2 ret_ctyp
+
   (* All signed and unsigned bitvector comparisons *)
   | "slt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvslt" ctx v1 v2 ret_ctyp
   | "ult_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvult" ctx v1 v2 ret_ctyp
@@ -966,6 +1037,7 @@ let smt_builtin ctx name args ret_ctyp =
   | "ugteq_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvuge" ctx v1 v2 ret_ctyp
 
   (* lib/vector_dec.sail *)
+  | "eq_bits", [v1; v2], CT_bool -> builtin_eq_bits ctx v1 v2
   | "zeros", [v], _ -> builtin_zeros ctx v ret_ctyp
   | "sail_zeros", [v], _ -> builtin_zeros ctx v ret_ctyp
   | "ones", [v], _ -> builtin_ones ctx v ret_ctyp
@@ -1022,7 +1094,8 @@ let writes = ref (-1)
 let builtin_write_mem ctx wk addr_size addr data_size data =
   incr writes;
   let name = "W" ^ string_of_int !writes in
-  [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
+  [Write_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
+              smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
   Var (name ^ "_ret")
 
 let ea_writes = ref (-1)
@@ -1030,7 +1103,8 @@ let ea_writes = ref (-1)
 let builtin_write_mem_ea ctx wk addr_size addr data_size =
   incr ea_writes;
   let name = "A" ^ string_of_int !ea_writes in
-  [Write_mem_ea (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))],
+  [Write_mem_ea (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
+                 smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))],
   Enum "unit"
 
 let reads = ref (-1)
@@ -1038,15 +1112,16 @@ let reads = ref (-1)
 let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
   incr reads;
   let name = "R" ^ string_of_int !reads in
-  [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
-  Var (name ^ "_ret")
+  [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk,
+             smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
+  Read_res name
 
 let excl_results = ref (-1)
 
 let builtin_excl_res ctx =
   incr excl_results;
   let name = "E" ^ string_of_int !excl_results in
-  [Excl_res name],
+  [Excl_res (name, ctx.node, Lazy.force ctx.pathcond)],
   Var (name ^ "_ret")
 
 let barriers = ref (-1)
@@ -1054,7 +1129,7 @@ let barriers = ref (-1)
 let builtin_barrier ctx bk =
   incr barriers;
   let name = "B" ^ string_of_int !barriers in
-  [Barrier (name, smt_cval ctx bk)],
+  [Barrier (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx bk)],
   Enum "unit"
 
 let rec smt_conversion ctx from_ctyp to_ctyp x =
@@ -1064,6 +1139,8 @@ let rec smt_conversion ctx from_ctyp to_ctyp x =
      bvint sz c
   | CT_constant c, CT_lint ->
      bvint ctx.lint_size c
+  | CT_fint sz, CT_lint ->
+     force_size ctx ctx.lint_size sz x
   | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))
 
 let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp)
@@ -1295,8 +1372,8 @@ let smt_ssanode ctx cfg preds =
   | Phi (id, ctyp, ids) ->
      let get_pi n =
        match get_vertex cfg n with
-       | Some ((ssanodes, _), _, _) ->
-          List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
+       | Some ((ssa_elems, _), _, _) ->
+          List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems)
        | None -> failwith "Predecessor node does not exist"
      in
      let pis = List.map get_pi (IntSet.elements preds) in
@@ -1360,8 +1437,8 @@ let rec get_pathcond n cfg ctx =
   let open Jib_ssa in
   let get_pi m =
     match get_vertex cfg m with
-    | Some ((ssanodes, _), _, _) ->
-       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes))
+    | Some ((ssa_elems, _), _, _) ->
+       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems))
     | None -> failwith "Node does not exist"
   in
   match get_vertex cfg n with
@@ -1533,7 +1610,7 @@ let smt_instr ctx =
        end
      else if not extern then
        let smt_args = List.map (smt_cval ctx) args in
-       [define_const ctx id ret_ctyp (Fn (zencode_id function_id, smt_args))]
+       [define_const ctx id ret_ctyp (Ctor (zencode_id function_id, smt_args))]
      else
        failwith ("Unrecognised function " ^ string_of_id function_id)
 
@@ -1569,7 +1646,7 @@ let smt_instr ctx =
   | instr ->
      failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr))
 
-let smt_cfnode all_cdefs ctx ssanodes =
+let smt_cfnode all_cdefs ctx ssa_elems =
   let open Jib_ssa in
   function
   | CF_start inits ->
@@ -1619,8 +1696,8 @@ module Make_optimizer(S : Sequence) = struct
          | Some n -> Hashtbl.replace uses var (n + 1)
          | None -> Hashtbl.add uses var 1
          end
-      | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
-      | Fn (f, exps) ->
+      | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
+      | Fn (_, exps) | Ctor (_, exps) ->
          List.iter uses_in_exp exps
       | Ite (cond, t, e) ->
          uses_in_exp cond; uses_in_exp t; uses_in_exp e
@@ -1644,19 +1721,20 @@ module Make_optimizer(S : Sequence) = struct
          end
       | (Declare_datatypes _ | Declare_tuple _) as def ->
          Stack.push def stack'
-      | Write_mem (_, wk, addr, _, data, _) as def ->
-         uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
+      | Write_mem (_, _, active, wk, addr, _, data, _) as def ->
+         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
          Stack.push def stack'
-      | Write_mem_ea (_, wk, addr, _, data_size, _) as def ->
-         uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size;
+      | Write_mem_ea (_, _, active, wk, addr, _, data_size, _) as def ->
+         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size;
          Stack.push def stack'
-      | Read_mem (_, _, rk, addr, _) as def ->
-         uses_in_exp rk; uses_in_exp addr;
+      | Read_mem (_, _, active, _, rk, addr, _) as def ->
+         uses_in_exp active; uses_in_exp rk; uses_in_exp addr;
          Stack.push def stack'
-      | Barrier (_, bk) as def ->
-         uses_in_exp bk;
+      | Barrier (_, _, active, bk) as def ->
+         uses_in_exp active; uses_in_exp bk;
          Stack.push def stack'
-      | Excl_res _ as def ->
+      | Excl_res (_, _, active) as def ->
+         uses_in_exp active;
          Stack.push def stack'
       | Assert exp as def ->
          uses_in_exp exp;
@@ -1666,35 +1744,46 @@ module Make_optimizer(S : Sequence) = struct
     Stack.fold remove_unused () stack;
 
     let vars = Hashtbl.create (Stack.length stack') in
+    let kinds = Hashtbl.create (Stack.length stack') in
     let seq = S.create () in
 
     let constant_propagate = function
       | Declare_const _ as def ->
          S.add def seq
       | Define_const (var, typ, exp) ->
-         begin match Hashtbl.find_opt uses var, simp_smt_exp vars exp with
+         let exp = simp_smt_exp vars kinds exp in
+         begin match Hashtbl.find_opt uses var, simp_smt_exp vars kinds exp with
          | _, (Bin _ | Bool_lit _) ->
             Hashtbl.add vars var exp
          | _, Var _ when !opt_propagate_vars ->
             Hashtbl.add vars var exp
+         | _, (Ctor (str, _)) ->
+            Hashtbl.add kinds var str;
+            S.add (Define_const (var, typ, exp)) seq
          | Some 1, _ ->
             Hashtbl.add vars var exp
          | Some _, exp ->
             S.add (Define_const (var, typ, exp)) seq
          | None, _ -> assert false
          end
-      | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
-         S.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data, data_ty)) seq
-      | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) ->
-         S.add (Write_mem_ea (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data_size, data_size_ty)) seq
-      | Read_mem (name, typ, rk, addr, addr_typ) ->
-         S.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr, addr_typ)) seq
-      | Barrier (name, bk) ->
-         S.add (Barrier (name, simp_smt_exp vars bk)) seq
-      | Excl_res name ->
-         S.add (Excl_res name) seq
+      | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
+         S.add (Write_mem (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
+                           simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data, data_ty))
+               seq
+      | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
+         S.add (Write_mem_ea (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
+                              simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data_size, data_size_ty))
+               seq
+      | Read_mem (name, node, active, typ, rk, addr, addr_typ) ->
+         S.add (Read_mem (name, node, simp_smt_exp vars kinds active, typ, simp_smt_exp vars kinds rk,
+                          simp_smt_exp vars kinds addr, addr_typ))
+               seq
+      | Barrier (name, node, active, bk) ->
+         S.add (Barrier (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds bk)) seq
+      | Excl_res (name, node, active) ->
+         S.add (Excl_res (name, node, simp_smt_exp vars kinds active)) seq
       | Assert exp ->
-         S.add (Assert (simp_smt_exp vars exp)) seq
+         S.add (Assert (simp_smt_exp vars kinds exp)) seq
       | (Declare_datatypes _ | Declare_tuple _) as def ->
          S.add def seq
       | Define_fun _ -> assert false
@@ -1815,18 +1904,18 @@ let smt_instr_list name ctx all_cdefs instrs =
   List.iter (fun n ->
       begin match get_vertex cfg n with
       | None -> ()
-      | Some ((ssanodes, cfnode), preds, succs) ->
+      | Some ((ssa_elems, cfnode), preds, succs) ->
          let muxers =
-           ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
+           ssa_elems |> List.map (smt_ssanode ctx cfg preds) |> List.concat
          in
-         let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in
-         let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in
+         let ctx = { ctx with node = n; pathcond = lazy (get_pathcond n cfg ctx) } in
+         let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in
          push_smt_defs stack muxers;
-         push_smt_defs stack basic_block;
+         push_smt_defs stack basic_block
       end
     ) visit_order;
 
-  stack
+  stack, cfg
 
 let smt_cdef props lets name_file ctx all_cdefs = function
   | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
@@ -1853,7 +1942,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           |> remove_pointless_goto
         in
 
-        let stack = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
+        let stack, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
 
         let query = smt_query ctx pragma.query in
         push_smt_defs stack [Assert (Fn ("not", [query]))];
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index f6198a37..2680f937 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -52,6 +52,7 @@ open Ast
 open Ast_util
 open Jib
 open Jib_util
+open Jib_ssa
 open Smtlib
 
 val opt_ignore_overflow : bool ref
@@ -59,6 +60,8 @@ val opt_auto : bool ref
 val opt_debug_graphs : bool ref
 val opt_propagate_vars : bool ref
 
+val zencode_name : name -> string
+
 module IntSet : Set.S with type elt = int
 module EventMap : Map.S with type key = Property.event
 
@@ -95,8 +98,9 @@ type ctx = {
        src/property.ml for the event types *)
     events : smt_exp Stack.t EventMap.t ref;
     (** When generating SMT for an instruction pathcond will contain
-       the global path conditional of the containing block in the
+       the global path conditional of the containing block/node in the
        control flow graph *)
+    node : int;
     pathcond : smt_exp Lazy.t;
     (** Set if we need to use strings or real numbers in the generated
        SMT, which then requires set-logic ALL or similar depending on
@@ -116,7 +120,9 @@ val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx
 
 val smt_header : ctx -> cdef list -> smt_def list
 
-val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t
+val smt_query : ctx -> Property.query -> smt_exp
+
+val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * (ssa_elem list * cf_node) Jib_ssa.array_graph
 
 module type Sequence = sig
   type 'a t
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
new file mode 100644
index 00000000..37ae753f
--- /dev/null
+++ b/src/jib/jib_smt_fuzz.ml
@@ -0,0 +1,255 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Jib
+open Jib_smt
+open Jib_util
+open Smtlib
+
+let gen_value (Typ_aux (aux, _) as typ) =
+  match aux with
+  | Typ_id id when string_of_id id = "bit" ->
+     Some (
+         if Random.bool () then
+           mk_lit_exp L_zero, V_lit (VL_bit Sail2_values.B0, CT_bit)
+         else
+           mk_lit_exp L_one, V_lit (VL_bit Sail2_values.B1, CT_bit)
+       )
+
+  | Typ_app (id, _) when string_of_id id = "atom_bool" ->
+     Some (
+         if Random.bool () then
+           mk_lit_exp L_true, V_lit (VL_bool true, CT_bool)
+         else
+           mk_lit_exp L_false, V_lit (VL_bool false, CT_bool)
+       )
+
+  | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_constant n, _)), _)]) when string_of_id id = "atom" ->
+     Some (
+         if Random.bool () then
+           mk_lit_exp (L_num n), V_lit (VL_int n, CT_constant n)
+         else
+           let n = Big_int.of_int (Random.int 32) in
+           let n = if Random.bool () then n else Big_int.negate n in
+           match Random.int 3 with
+           | 0 ->
+              mk_lit_exp (L_num n), V_lit (VL_int n, CT_fint 64)
+           | 1 ->
+              mk_lit_exp (L_num n), V_lit (VL_int n, CT_lint)
+           | _ ->
+              mk_lit_exp (L_num n), V_lit (VL_int n, CT_constant n)
+       )
+
+  | Typ_app (id, _) when string_of_id id = "atom" ->
+     Some (
+         let n = Big_int.of_int (Random.int 32) in
+         let n = if Random.bool () then n else Big_int.negate n in
+         match Random.int 3 with
+         | 0 ->
+            mk_lit_exp (L_num n), V_lit (VL_int n, CT_fint 64)
+         | 1 ->
+            mk_lit_exp (L_num n), V_lit (VL_int n, CT_lint)
+         | _ ->
+            mk_lit_exp (L_num n), V_lit (VL_int n, CT_constant n)
+       )
+
+  | _ ->
+     None
+
+let rec gen_ret_ctyp (Typ_aux (aux, _)) =
+  match aux with
+  | Typ_id id when string_of_id id = "bool" ->
+     Some CT_bool
+  | Typ_app (id, _) when string_of_id id = "atom" ->
+     if Random.bool () then Some (CT_fint 64) else Some CT_lint
+  | Typ_app (id, _) when string_of_id id = "atom_bool" ->
+     Some CT_bool
+  | Typ_id id when string_of_id id = "nat" ->
+     Some CT_lint
+  | Typ_id id when string_of_id id = "int" ->
+     Some CT_lint
+  | Typ_exist (_, _, typ) ->
+     gen_ret_ctyp typ
+  | _ -> None
+
+let gen_assertion ctyp value id =
+  let open Smtlib in
+  let open Value in
+  match ctyp, value with
+  | CT_bool, V_bool b ->
+     [icopy Parse_ast.Unknown (CL_id (Return (-1), CT_bool)) (V_call (Eq, [V_id (id, ctyp); V_lit (VL_bool b, ctyp)]))]
+  | CT_lint, V_int n ->
+     [icopy Parse_ast.Unknown (CL_id (Return (-1), CT_bool)) (V_call (Eq, [V_id (id, ctyp); V_lit (VL_int n, ctyp)]))]
+  | CT_fint 64, V_int n ->
+     [icopy Parse_ast.Unknown (CL_id (Return (-1), CT_bool)) (V_call (Eq, [V_id (id, ctyp); V_lit (VL_int n, ctyp)]))]
+  | _ ->
+     assert false
+
+let rec run frame =
+  match frame with
+  | Interpreter.Done (state, v) -> Some v
+  | Interpreter.Step (lazy_str, _, _, _) ->
+     run (Interpreter.eval_frame frame)
+  | Interpreter.Break frame ->
+     run (Interpreter.eval_frame frame)
+  | Interpreter.Fail (_, _, _, _, msg) ->
+     None
+  | Interpreter.Effect_request (out, state, stack, eff) ->
+     run (Interpreter.default_effect_interp state eff)
+
+exception Skip_iteration of string;;
+
+let fuzz_cdef ctx all_cdefs = function
+  | CDEF_spec (id, arg_ctyps, ret_ctyp) when not (string_of_id id = "and_bool" || string_of_id id = "or_bool") ->
+     let open Type_check in
+     let open Interpreter in
+     if Env.is_extern id ctx.tc_env "smt" then (
+       let extern = Env.get_extern id ctx.tc_env "smt" in
+       let typq, (Typ_aux (aux, _) as typ) = Env.get_val_spec id ctx.tc_env in
+       let istate = initial_state ctx.ast ctx.tc_env Value.primops in
+       let header = smt_header ctx all_cdefs in
+       prerr_endline (Util.("Fuzz: " |> cyan |> clear) ^ string_of_id id ^ " = \"" ^ extern ^ "\" : " ^ string_of_typ typ);
+
+       match aux with
+       | Typ_fn (arg_typs, ret_typ, _) ->
+          let iterations = ref 0 in
+          let max_iterations = 100 in
+          let continue = ref true in
+          let skipped = ref 0 in
+
+          while !iterations < max_iterations && !continue do
+            begin try
+              begin match List.map gen_value arg_typs |> Util.option_all, gen_ret_ctyp ret_typ with
+              | Some values, Some ret_ctyp ->
+                 let ctx = { ctx with events = ref EventMap.empty; pragma_l = id_loc id; arg_stack = Stack.create () } in
+                 let call =
+                   try mk_exp (E_app (id, List.map fst values)) |> infer_exp ctx.tc_env with
+                   | Type_error _ -> raise (Skip_iteration ("Type error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
+                 in
+                 let result =
+                   match run (Step (lazy "", istate, return call, [])) with
+                   | Some v -> v
+                   | None ->
+                      raise (Skip_iteration ("Interpreter error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
+                 in
+
+                 let jib =
+                   let gs = Jib_compile.ngensym () in
+                   [ifuncall (CL_id (gs, ret_ctyp)) id (List.map snd values)]
+                   @ gen_assertion ret_ctyp result gs
+                   @ [iend ()]
+                 in
+                 let smt_defs =
+                   try fst (smt_instr_list extern ctx all_cdefs jib) with
+                   | _ ->
+                      raise (Skip_iteration ("SMT error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
+                 in
+                 let smt_defs = Stack.fold (fun xs x -> x :: xs) [] smt_defs in
+                 let query = Assert (Fn ("not", [smt_query ctx Property.default_query])) in
+
+                 let fname, out_chan = Filename.open_temp_file (Util.zencode_string (string_of_id id)) ".smt2" in
+                 if !(ctx.use_string) || !(ctx.use_real) then
+                   output_string out_chan "(set-logic ALL)\n"
+                 else
+                   output_string out_chan "(set-logic QF_AUFBVDT)\n";
+                 List.iter (fun smt -> output_string out_chan (string_of_smt_def smt ^ "\n")) (header @ smt_defs @ [query]);
+                 output_string out_chan "(check-sat)\n";
+                 close_out out_chan;
+
+                 let in_chan = Printf.ksprintf Unix.open_process_in "cvc4 --lang=smt2.6 %s" fname in
+                 let lines = ref [] in
+                 begin
+                   try
+                     while true do
+                       lines := input_line in_chan :: !lines
+                     done
+                   with
+                   | End_of_file -> ()
+                 end;
+                 let _ = Unix.close_process_in in_chan in
+                 let solver_output = List.rev !lines |> String.concat "\n" |> parse_sexps in
+                 begin match solver_output with
+                 | [Atom "unsat"] -> ()
+                 | _ ->
+                    prerr_endline (Util.("SMT check failed:" |> red |> clear)
+                                   ^ "\n" ^ Util.string_of_list ", " string_of_exp (List.map fst values)
+                                   ^ " : " ^ Util.string_of_list ", " string_of_ctyp (List.map (fun v -> cval_ctyp (snd v)) values)
+                                   ^ " -> " ^ string_of_ctyp ret_ctyp
+                                   ^ " = " ^ Value.string_of_value result
+                                   ^ "\nFilename: " ^ fname);
+                    continue := false
+                 end
+              | _, _ ->
+                 prerr_endline Util.("Could not generate values for function types" |> yellow |> clear);
+                 continue := false
+              end
+            with
+            | Skip_iteration str ->
+               incr skipped
+            end;
+            incr iterations
+          done;
+          if !continue then
+            prerr_endline (Util.("ok" |> green |> clear) ^ Printf.sprintf " (%d/%d skipped)" !skipped max_iterations)
+
+       | _ ->
+          raise (Reporting.err_general (id_loc id) "Function prototype must have a function type")
+     ) else ()
+
+  | _ -> ()
+
+let fuzz seed env ast =
+  Random.init seed;
+
+  let cdefs, ctx = compile env ast in
+
+  List.iter (fuzz_cdef ctx cdefs) cdefs
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index dadb20fd..3357bc11 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -61,7 +61,7 @@ val make : initial_size:int -> unit -> 'a array_graph
 module IntSet : Set.S with type elt = int
 
 val get_cond : 'a array_graph -> int -> Jib.cval
-     
+
 val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
 
 val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit
diff --git a/src/latex.ml b/src/latex.ml
index aa786b83..9f5979c1 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -342,7 +342,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
   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)
+    (Reporting.warn "" l ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty)
   else
     begin
       state.commands <- StringSet.add command state.commands;
@@ -417,7 +417,7 @@ let process_pragma l command =
      Some (ksprintf string "\\newcommand{\\%s}{%s}" name body)
 
   | _ ->
-     Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l));
+     Reporting.warn "Bad latex pragma at" l "";
      None
 
 let tdef_id = function
diff --git a/src/libsail.mllib b/src/libsail.mllib
index b9d91834..fb3d1264 100644
--- a/src/libsail.mllib
+++ b/src/libsail.mllib
@@ -5,6 +5,8 @@ Bitfield
 C_backend
 Cgen_backend
 Constant_fold
+Constant_propagation
+Constant_propagation_mutrec
 Constraint
 Elf_loader
 Error_format
@@ -17,6 +19,7 @@ Jib
 Jib_compile
 Jib_optimize
 Jib_ssa
+Jib_smt
 Jib_util
 Latex
 Lexer
@@ -27,6 +30,7 @@ Ocaml_backend
 Optimize
 Parse_ast
 Parser
+Parser_combinators
 Pattern_completeness
 PPrint
 PPrintCombinators
@@ -40,6 +44,7 @@ Pretty_print_lem
 Pretty_print_sail
 Process_file
 Profile
+Property
 Reporting
 Rewriter
 Rewrites
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 1e52d708..93579420 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -545,11 +545,6 @@ let stop_at_false_assertions e =
              then E_aux (E_block es,ann), stop
              else E_aux (E_block (es@[dummy_value_of_typ typ']),ann), Some typ'
        end
-    | E_nondet es ->
-       let es,stops = List.split (List.map exp es) in
-       let stop = List.exists (function Some _ -> true | _ -> false) stops in
-       let stop = if stop then Some (typ_of_annot ann) else None in
-       E_aux (E_nondet es,ann), stop
     | E_cast (typ,e) -> let e,stop = exp e in
                         let stop = match stop with Some _ -> Some typ | None -> None in
                         E_aux (E_cast (typ,e),ann),stop
@@ -980,7 +975,6 @@ let split_defs all_errors splits env defs =
         let re e = E_aux (e,annot) in
         match e with
         | E_block es -> re (E_block (List.map map_exp es))
-        | E_nondet es -> re (E_nondet (List.map map_exp es))
         | E_id _
         | E_lit _
         | E_sizeof _
@@ -2048,9 +2042,6 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
             d, assigns, merge r r'
        in
        aux env assigns es
-    | E_nondet es ->
-       let _, assigns, r = non_det es in
-       (dempty, assigns, r)
     | E_id id ->
        begin 
          match Bindings.find id env.var_deps with
@@ -2536,8 +2527,7 @@ let rec sets_from_assert e =
    above. *)
 let rec find_set_assertions (E_aux (e,_)) =
   match e with
-  | E_block es
-  | E_nondet es ->
+  | E_block es ->
      List.fold_left merge_set_asserts_by_kid KBindings.empty (List.map find_set_assertions es)
   | E_cast (_,e) -> find_set_assertions e
   | E_let (LB_aux (LB_val (p,e1),_),e2) ->
@@ -3686,10 +3676,10 @@ type options = {
 }
 
 let recheck defs =
-  let w = !Util.opt_warnings in
-  let () = Util.opt_warnings := false in
+  let w = !Reporting.opt_warnings in
+  let () = Reporting.opt_warnings := false in
   let r = Type_error.check (Type_check.Env.no_casts Type_check.initial_env) defs in
-  let () = Util.opt_warnings := w in
+  let () = Reporting.opt_warnings := w in
   r
 
 let mono_rewrites = MonoRewrites.mono_rewrite
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index ba2e5e69..28ce43d3 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -473,10 +473,17 @@ let ocaml_funcls ctx =
           explicit type signatures with universal quantification. *)
        let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
        let pat_sym = gensym () in
-       let pat, exp =
+       let pat, guard, exp =
          match pexp with
-         | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp
-         | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported"
+         | Pat_aux (Pat_exp (pat, exp),_) -> pat, None, exp
+         | Pat_aux (Pat_when (pat, guard, exp),_) -> pat, Some guard, exp
+       in
+       let ocaml_guarded_exp ctx exp = function
+         | Some guard ->
+            separate space [string "if"; ocaml_exp ctx guard;
+                            string "then"; parens (ocaml_exp ctx exp);
+                            string "else"; Printf.ksprintf string "failwith \"Pattern match failure in %s\"" (string_of_id id)]
+         | None -> ocaml_exp ctx exp
        in
        let annot_pat =
          let pat =
@@ -496,7 +503,7 @@ let ocaml_funcls ctx =
            separate space [call_header; zencode ctx id;
                            annot_pat; colon; ocaml_typ ctx ret_typ; equals;
                            sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
-           ^//^ ocaml_exp ctx exp
+           ^//^ ocaml_guarded_exp ctx exp guard
            ^^ rparen
          else
            separate space [call_header; zencode ctx id; colon;
@@ -504,7 +511,7 @@ let ocaml_funcls ctx =
                            ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
                            string "fun"; annot_pat; string "->";
                            sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
-           ^//^ ocaml_exp ctx exp
+           ^//^ ocaml_guarded_exp ctx exp guard
            ^^ rparen
        in
        ocaml_funcl call string_of_arg string_of_ret
diff --git a/src/optimize.ml b/src/optimize.ml
index a372abf4..1fc2fbe8 100644
--- a/src/optimize.ml
+++ b/src/optimize.ml
@@ -87,7 +87,7 @@ let recheck (Defs defs) =
           !specs @ !bodies @ find_optimizations defs
 
        | _ ->
-          Util.warn ("Unrecognised optimize pragma in this context: " ^ pragma);
+          Reporting.warn "Unrecognised optimize pragma at" p_l "";
           def1 :: def2 :: find_optimizations defs
        end
 
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 5c3a5382..1d2c3534 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -247,7 +247,6 @@ and measure =
 and
 exp_aux =  (* Expression *)
    E_block of (exp) list (* block (parsing conflict with structs?) *)
- | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
  | E_id of id (* identifier *)
  | E_ref of id
  | E_deref of exp
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 79fc93ee..3e26502d 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -106,7 +106,7 @@ let rec generalize ctx (P_aux (p_aux, (l, _)) as pat) =
        | Unbound -> GP_wild
        | Local (Immutable, _) -> GP_wild
        | Register _ | Local (Mutable, _) ->
-          Util.warn ("Matching on register or mutable variable at " ^ Reporting.loc_to_string l); GP_wild
+          Reporting.warn "Matching on register or mutable variable at " l ""; GP_wild
        | Enum _ -> GP_app (Bindings.singleton id GP_wild)
      end
   | P_var (pat, _) -> generalize ctx pat
@@ -164,7 +164,7 @@ let join_bits bits1 bits2 =
 
 (* The join_lit function takes two patterns and produces a pattern
    that matches both literals *)
-let rec join_lit (L_aux (l_aux1, _) as lit1) (L_aux (l_aux2, _) as lit2) =
+let rec join_lit (L_aux (l_aux1, l) as lit1) (L_aux (l_aux2, _) as lit2) =
   match l_aux1, l_aux2 with
   (* The only literal with type unit is the unit literal *)
   | L_unit, _ -> GP_lit lit1
@@ -207,7 +207,7 @@ let rec join_lit (L_aux (l_aux1, _) as lit1) (L_aux (l_aux2, _) as lit2) =
        Printf.sprintf "Have two differently typed pattern literals %s and %s matching the same thing"
                       (string_of_lit lit1) (string_of_lit lit2)
      in
-     Util.warn message;
+     Reporting.warn "" l message;
      GP_wild
 
 let rec join ctx gpat1 gpat2 =
@@ -270,7 +270,7 @@ let combine ctx gpat (l, pat) =
      (* This warning liable to false positives as join returns a
         pattern that overapproximates what can match, so we only
         report when the second match is a constructor. *)
-     Util.warn (Printf.sprintf "Possible redundant pattern match at %s\n" (Reporting.loc_to_string l));
+     Reporting.warn "Possible redundant pattern match at" l "";
      GP_wild
   | _, gpat' -> join ctx gpat gpat'
 
@@ -288,15 +288,11 @@ let shrink_loc = function
 
 let check l ctx cases =
   match cases_to_pats cases with
-  | [] -> Util.warn (Printf.sprintf "No non-guarded patterns at %s\n" (Reporting.loc_to_string (shrink_loc l)))
+  | [] -> Reporting.warn "No non-guarded patterns at" (shrink_loc l) ""
   | (_, pat) :: pats ->
      let top_pat = List.fold_left (combine ctx) (generalize ctx pat) pats in
      if is_wild top_pat then
        ()
      else
-       let message =
-         Printf.sprintf "Possible incomplete pattern match at %s\n\nMost general matched pattern is %s\n"
-                        (Reporting.loc_to_string (shrink_loc l))
-                        (string_of_gpat top_pat |> Util.cyan |> Util.clear)
-       in
-       Util.warn message
+       Reporting.warn "Possible incomplete pattern match at" (shrink_loc l)
+         (Printf.sprintf "Most general matched pattern is %s" (string_of_gpat top_pat |> Util.cyan |> Util.clear))
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 37e99662..f0947315 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1459,6 +1459,42 @@ let doc_exp, doc_let =
        let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in
        if aexp_needed then parens epp else epp
     | E_app(f,args) ->
+       let env = env_of full_exp in
+       let doc_loop_var (E_aux (e,(l,_)) as exp) =
+         match e with
+         | E_id id ->
+            let id_pp = doc_id id in
+            let typ = general_typ_of exp in
+            if Util.is_some (is_auto_decomposed_exist ctxt env typ)
+            then string "build_ex" ^^ space ^^ id_pp ^/^
+                   colon ^^ space ^^ doc_typ ctxt env typ,
+                 separate space [string "existT"; underscore; id_pp; underscore],
+                 true
+            else id_pp, id_pp, false
+         | E_lit (L_aux (L_unit,_)) -> string "tt", underscore, false
+         | _ -> raise (Reporting.err_unreachable l __POS__
+                         ("Bad expression for variable in loop: " ^ string_of_exp exp))
+       in
+       let make_loop_vars extra_binders varstuple =
+         match varstuple with
+         | E_aux (E_tuple vs, _) ->
+            let vs = List.map doc_loop_var vs in
+            let mkpp f vs = separate (string ", ") (List.map f vs) in
+            let tup_pp = mkpp (fun (pp,_,_) -> pp) vs in
+            let match_pp = mkpp (fun (_,pp,_) -> pp) vs in
+            parens tup_pp,
+            separate space (string "fun" :: extra_binders @
+                              [squote ^^ parens match_pp; bigarrow])
+         | _ ->
+            let exp_pp,match_pp,decompose = doc_loop_var varstuple in
+            let vpp = if decompose
+                      then squote ^^ parens match_pp
+                      else match_pp
+            in
+            let exp_pp = if decompose then parens exp_pp else exp_pp in
+            exp_pp,
+            separate space (string "fun" :: extra_binders @ [vpp; bigarrow])
+       in
        begin match f with
        | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
          when effectful (effect_of full_exp) ->
@@ -1498,30 +1534,21 @@ let doc_exp, doc_let =
                  | E_aux (E_lit (L_aux (L_true, _)), _) -> "_up"
                  | _ -> raise (Reporting.err_unreachable l __POS__ ("Unexpected loop direction " ^ string_of_exp ord_exp))
                in
-               let combinator = if effectful (effect_of body) then "foreach_ZM" else "foreach_Z" in
+               let effects = effectful (effect_of body) in
+               let combinator = if effects then "foreach_ZM" else "foreach_Z" in
                let combinator = combinator ^ dir in
                let body_ctxt = add_single_kid_id_rename ctxt loopvar (mk_kid ("loop_" ^ string_of_id loopvar)) in
-               let used_vars_body = find_e_ids body in
-               let body_lambda =
-                 (* Work around indentation issues in Lem when translating
-                    tuple or literal unit patterns to Isabelle *)
-                 match fst (uncast_exp vartuple) with
-                   | E_aux (E_tuple _, _)
-                     when not (IdSet.mem (mk_id "varstup") used_vars_body)->
-                      separate space [string "fun"; doc_id loopvar; string "_"; string "varstup"; bigarrow]
-                      ^^ break 1 ^^
-                      separate space [string "let"; squote ^^ expY vartuple; string ":= varstup in"]
-                   | E_aux (E_lit (L_aux (L_unit, _)), _)
-                     when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
-                      separate space [string "fun"; doc_id loopvar; string "_"; string "unit_var"; bigarrow]
-                   | _ ->
-                      separate space [string "fun"; doc_id loopvar; string "_"; expY vartuple; bigarrow]
+               let from_exp_pp, to_exp_pp, step_exp_pp =
+                 expY from_exp, expY to_exp, expY step_exp
+               in
+               let vartuple_pp, body_lambda =
+                 make_loop_vars [doc_id loopvar; underscore] vartuple
                in
                parens (
                    (prefix 2 1)
                      ((separate space) [string combinator;
-                                        expY from_exp; expY to_exp; expY step_exp;
-                                        expY vartuple])
+                                        from_exp_pp; to_exp_pp; step_exp_pp;
+                                        vartuple_pp])
                      (parens
                         (prefix 2 1 (group body_lambda) (top_exp body_ctxt false body))
                      )
@@ -1572,23 +1599,13 @@ let doc_exp, doc_let =
               | Some exp -> "T", [expY exp]
             in
             let used_vars_body = find_e_ids body in
-            let lambda =
-              (* Work around indentation issues in Lem when translating
-                 tuple or literal unit patterns to Isabelle *)
-              match fst (uncast_exp varstuple) with
-              | E_aux (E_tuple _, _)
-                   when not (IdSet.mem (mk_id "varstup") used_vars_body)->
-                 separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^
-                   separate space [string "let"; squote ^^ expY varstuple; string ":= varstup in"]
-              | E_aux (E_lit (L_aux (L_unit, _)), _)
-                   when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
-                 separate space [string "fun unit_var"; bigarrow]
-              | _ ->
-                 separate space [string "fun"; expY varstuple; bigarrow]
+            let varstuple_pp, lambda =
+              make_loop_vars [] varstuple
             in
             parens (
                 (prefix 2 1)
-                  ((separate space) (string (combinator ^ csuffix ^ msuffix)::measure_pp@[expY varstuple]))
+                  ((separate space) (string (combinator ^ csuffix ^ msuffix)::
+                                       measure_pp@[varstuple_pp]))
                   ((prefix 0 1)
                      (parens (prefix 2 1 (group lambda) (expN cond)))
                      (parens (prefix 2 1 (group lambda) (expN body))))
@@ -1604,16 +1621,11 @@ let doc_exp, doc_let =
                  | None -> expY exp
                in
                let epp = separate space [string "early_return"; exp_pp] in
-               let aexp_needed, tepp =
-                 if contains_t_pp_var ctxt (typ_of exp) ||
-                    contains_t_pp_var ctxt (typ_of full_exp) then
-                   aexp_needed, epp
-                 else
-                   let tannot = separate space [string "MR";
-                     doc_atomic_typ ctxt (env_of full_exp) false (typ_of full_exp);
-                     doc_atomic_typ ctxt (env_of exp) false (typ_of exp)] in
-                   true, doc_op colon epp tannot in
-               if aexp_needed then parens tepp else tepp
+               let tannot = separate space [string "MR";
+                 doc_atomic_typ ctxt (env_of full_exp) false (typ_of full_exp);
+                 doc_atomic_typ ctxt (env_of exp) false (typ_of exp)]
+               in
+               parens (doc_op colon epp tannot)
             | _ -> raise (Reporting.err_unreachable l __POS__
                "Unexpected number of arguments for early_return builtin")
           end
@@ -1705,9 +1717,8 @@ let doc_exp, doc_let =
               let ekids = Env.get_typ_vars env in
               KidSet.for_all (fun kid -> KBindings.mem kid ekids) (nexp_frees n)
             in
-            match typ_of_arg, typ_from_fn with
-            | Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n1,_)]),_),
-              Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n2,_)]),_)
+            match destruct_atom_nexp env typ_of_arg, destruct_atom_nexp env typ_from_fn with
+            | Some n1, Some n2
                  when vars_in_env n2 && not (similar_nexps ctxt env n1 n2) ->
                underscore
             | _ ->
@@ -1814,7 +1825,6 @@ let doc_exp, doc_let =
            raise (report l __POS__ "E_field expression with no register or record type"))
     | E_block [] -> string "tt"
     | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.")
-    | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.")
     | E_id id | E_ref id ->
        let env = env_of full_exp in
        let typ = typ_of full_exp in
@@ -1833,11 +1843,24 @@ let doc_exp, doc_let =
             let exp_typ = expand_range_type (Env.expand_synonyms env typ) in
             let ann_typ = general_typ_of full_exp in
             let ann_typ = expand_range_type (Env.expand_synonyms env ann_typ) in
+            let autocast =
+              (* Avoid using helper functions which simplify the nexps *)
+              is_bitvector_typ exp_typ && is_bitvector_typ ann_typ &&
+                match exp_typ, ann_typ with
+                | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
+                  Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
+                   not (similar_nexps ctxt env n1 n2)
+                | _ -> false
+            in
             let () =
               debug ctxt (lazy ("Variable " ^ string_of_id id ^ " with type " ^ string_of_typ typ));
-              debug ctxt (lazy (" expected type " ^ string_of_typ ann_typ))
+              debug ctxt (lazy (" expected type " ^ string_of_typ ann_typ));
+              debug ctxt (lazy (" autocast " ^ string_of_bool autocast))
             in
-            doc_id id
+            if autocast then
+              wrap_parens (string "autocast" ^/^ doc_id id)
+            else
+              doc_id id
          | _ -> doc_id id
        end
     | E_lit lit -> doc_lit lit
@@ -1846,7 +1869,7 @@ let doc_exp, doc_let =
        let outer_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in
        let outer_typ = expand_range_type outer_typ in
        let cast_typ = expand_range_type (Env.expand_synonyms env typ) in
-       let inner_typ = Env.expand_synonyms env (general_typ_of e) in
+       let inner_typ = Env.expand_synonyms env (typ_of e) in
        let inner_typ = expand_range_type inner_typ in
        let () =
          debug ctxt (lazy ("Cast of type " ^ string_of_typ cast_typ));
@@ -1857,8 +1880,8 @@ let doc_exp, doc_let =
        let outer_ex,_,outer_typ' = classify_ex_type ctxt env outer_typ in
        let cast_ex,_,cast_typ' = classify_ex_type ctxt env ~rawbools:true cast_typ in
        let inner_ex,_,inner_typ' = classify_ex_type ctxt env inner_typ in
-       let autocast =
-                (* Avoid using helper functions which simplify the nexps *)
+       let autocast_out =
+         (* Avoid using helper functions which simplify the nexps *)
          is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
            match outer_typ', cast_typ' with
            | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
@@ -1866,18 +1889,37 @@ let doc_exp, doc_let =
               not (similar_nexps ctxt env n1 n2)
            | _ -> false
        in
+       let autocast_in =
+         (* Avoid using helper functions which simplify the nexps *)
+         is_bitvector_typ inner_typ' && is_bitvector_typ cast_typ' &&
+           match inner_typ', cast_typ' with
+           | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
+         Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
+              not (similar_nexps ctxt env n1 n2)
+           | _ -> false
+       in
        let effects = effectful (effect_of e) in
-       let autocast =
-         (* We don't currently have a version of autocast under existentials,
-            but they're rare and may be unnecessary *)
-         if effects && outer_ex = ExGeneral then false else autocast
+       (* We don't currently have a version of autocast under existentials,
+          but they're rare and may be unnecessary *)
+       let autocast_out =
+         if effects && outer_ex = ExGeneral then false else autocast_out
+       in
+       let autocast_in =
+         if effects && inner_ex = ExGeneral then false else autocast_in
        in
        let () =
          debug ctxt (lazy (" effectful: " ^ string_of_bool effects ^
                            " outer_ex: " ^ string_of_ex_kind outer_ex ^
                            " cast_ex: " ^ string_of_ex_kind cast_ex ^
                            " inner_ex: " ^ string_of_ex_kind inner_ex ^
-                           " autocast: " ^ string_of_bool autocast))
+                           " autocast_in: " ^ string_of_bool autocast_in ^
+                           " autocast_out: " ^ string_of_bool autocast_out))
+       in
+       let epp =
+         if autocast_in then
+           string "autocast" ^/^ parens epp
+         else
+           epp
        in
        let epp =
          if effects then
@@ -1908,7 +1950,7 @@ let doc_exp, doc_let =
               | ExNone -> epp
        in
        let epp =
-         if autocast then
+         if autocast_out then
            string (if effects then "autocast_m" else "autocast") ^^ space ^^ parens epp
          else epp
        in
@@ -2039,6 +2081,31 @@ let doc_exp, doc_let =
              let epp = liftR (separate space [string assert_fn; expY assert_e1; expY assert_e2]) in
              let epp = infix 0 1 (string mid) epp (top_exp new_ctxt false e2) in
              if aexp_needed then parens (align epp) else align epp
+         | _,
+           (E_aux (E_if (if_cond,
+                         (  E_aux (E_throw _,_)
+                          | E_aux (E_block [E_aux (E_throw _,_)],_) as throw_exp),
+                   else_exp),_)), _
+              when condition_produces_constraint ctxt if_cond ->
+            let cond_pp = expY if_cond in
+            let throw_pp = expN throw_exp in
+            (* Push non-trivial else branches below *)
+            let e2 =
+              match else_exp with
+              | E_aux (E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)),_)
+              | E_aux (E_internal_return
+                         (E_aux (E_cast (_, E_aux (E_lit (L_aux (L_unit,_)),_)),_)),_)
+                -> e2
+              | _ -> E_aux (E_internal_plet (pat,else_exp,e2),(l,annot))
+            in
+            (* TODO: capture avoid *)
+            let hyp = string "_non_throw_hyp" in
+            group (parens (string "match sumbool_of_bool " ^^ space ^^ cond_pp ^^ space ^^ string "with" ^/^
+                      group (string "| left _ =>" ^/^ throw_pp) ^/^
+                        group (string "| right " ^^ hyp ^^ string " =>" ^/^
+                          string "returnm " ^^ hyp) ^/^ string "end")) ^/^
+              string " >>= fun _ => " ^/^
+                top_exp new_ctxt false e2
          | _ ->
             let epp =
               let middle =
@@ -2079,6 +2146,8 @@ let doc_exp, doc_let =
                        end
                      | _ -> plain_binder
                    in separate space [string ">>= fun"; binder; bigarrow]
+                | P_aux (P_typ (typ, pat'),_) ->
+                   separate space [string ">>= fun"; squote ^^ parens (doc_pat ctxt true true (pat, typ_of e1) ^/^ colon ^^ space ^^ doc_typ ctxt outer_env typ); bigarrow]
                 | _ ->
                    separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow]
               in
@@ -2151,17 +2220,22 @@ let doc_exp, doc_let =
     (* Prefer simple lets over patterns, because I've found Coq can struggle to
        work out return types otherwise *)
     | LB_val(P_aux (P_id id,_),e)
-      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) (typ_of e)) &&
-           not (is_enum (env_of e) id) ->
+      when not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; coloneq])
               (top_exp ctxt false e)
     | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
-      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) typ) &&
+      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) ~rawbools:true typ) &&
            not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; colon; doc_typ ctxt (env_of e) typ; coloneq])
               (top_exp ctxt false e)
+    | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
+      when (* is auto decomposed *)
+           not (is_enum (env_of e) id) ->
+       prefix 2 1
+              (separate space [string "let"; doc_id id; coloneq])
+              (top_exp ctxt false e)
     | LB_val(P_aux (P_typ (typ,pat),_),(E_aux (_,e_ann) as e)) ->
        prefix 2 1
               (separate space [string "let"; squote ^^ doc_pat ctxt true false (pat, typ); coloneq])
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 83b6901a..5cea9ba9 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -250,7 +250,9 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) =
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 and lem_nexps_of_typ_arg (A_aux (ta,_)) =
   match ta with
-  | A_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
+  | A_nexp nexp ->
+      let nexp = nexp_simp (orig_nexp nexp) in
+      if is_nexp_constant nexp then NexpSet.empty else NexpSet.singleton nexp
   | A_typ typ -> lem_nexps_of_typ typ
   | A_order _ -> NexpSet.empty
   | A_bool _ -> NexpSet.empty
@@ -433,24 +435,11 @@ let doc_lit_lem (L_aux(lit,l)) =
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
-(* typ_doc is the doc for the type being quantified *)
-let doc_quant_item vars_included (QI_aux (qi, _)) = match qi with
-| QI_id (KOpt_aux (KOpt_kind (_, kid), _)) ->
-   (match vars_included with
-     None -> doc_var kid
-   | Some set -> (*when KidSet.mem kid set -> doc_var kid*)
-      let nexps = NexpSet.filter (fun nexp -> KidSet.mem (orig_kid kid) (nexp_frees nexp)) set in
-      separate_map space doc_nexp_lem (NexpSet.elements nexps))
-| _ -> empty
-
-let doc_typquant_items_lem vars_included (TypQ_aux(tq,_)) = match tq with
-| TypQ_tq qs -> separate_map space (doc_quant_item vars_included) qs
-| _ -> empty
-
-let doc_typquant_lem (TypQ_aux(tq,_)) vars_included typ = match tq with
-| TypQ_tq ((_ :: _) as qs) ->
-  string "forall " ^^ separate_map space (doc_quant_item vars_included) qs ^^ string ". " ^^ typ
-| _ -> typ
+let kid_nexps_of_typquant tq =
+  quant_kopts tq |> List.filter (fun k -> is_int_kopt k || is_typ_kopt k) |> List.map kopt_kid |> List.map nvar
+
+let doc_typquant_items_lem quant_nexps =
+  separate_map space doc_nexp_lem quant_nexps
 
 (* Produce Size type constraints for bitvector sizes when using
    machine words.  Often these will be unnecessary, but this simple
@@ -497,7 +486,7 @@ let doc_typschm_lem env quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
     let nexps_to_include = NexpSet.union nexps_used nexps_sizes in
     if NexpSet.is_empty nexps_to_include
     then pt
-    else doc_typquant_lem tq (Some nexps_to_include) (ptyc ^^ pt)
+    else string "forall " ^^ doc_typquant_items_lem (NexpSet.elements nexps_to_include) ^^ string ". " ^^ ptyc ^^ pt
   else pt
 
 let is_ctor env id = match Env.lookup_id id env with
@@ -831,7 +820,6 @@ let doc_exp_lem, doc_let_lem =
            raise (report l __POS__ "E_field expression with no register or record type"))
     | E_block [] -> string "()"
     | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.")
-    | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.")
     | E_id id | E_ref id ->
        let env = env_of full_exp in
        let typ = typ_of full_exp in
@@ -1063,7 +1051,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
   | TD_abbrev(id,typq,A_aux (A_typ typ, _)) ->
      let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in
      doc_op equals
-       (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
+       (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem (kid_nexps_of_typquant typq)])
        (doc_typschm_lem env false typschm)
   | TD_abbrev _ -> empty
   | TD_record(id,typq,fs,_) ->
@@ -1115,7 +1103,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
           doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *)
     let sorts_pp = doc_typquant_sorts (doc_id_lem_type id) typq in
     doc_op equals
-           (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
+           (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem (kid_nexps_of_typquant typq)])
            ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^ sorts_pp
     (* if !opt_sequential && string_of_id id = "regstate" then empty
     else separate_map hardline doc_field fs *)
@@ -1134,7 +1122,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
          let ar_doc = group (separate_map (break 1) (doc_type_union_lem env) ar) in
          let typ_pp =
            (doc_op equals)
-             (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem None typq])
+             (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem (kid_nexps_of_typquant typq)])
              ((*doc_typquant_lem typq*) ar_doc) in
          let make_id pat id =
            separate space [string "SIA.Id_aux";
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index da44645c..ae1f467c 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -387,7 +387,6 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_block [] -> string "()"
   | E_block exps ->
      group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace)
-  | E_nondet exps -> assert false
   (* This is mostly for the -convert option *)
   | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
      separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y]
diff --git a/src/process_file.ml b/src/process_file.ml
index 1672663b..7da3c130 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -145,6 +145,7 @@ let all_pragmas =
       "latex";
       "property";
       "counterexample";
+      "suppress_warnings";
     ]
 
 let rec preprocess opts = function
@@ -180,7 +181,7 @@ let rec preprocess opts = function
   | Parse_ast.DEF_pragma ("include", file, l) :: defs ->
      let len = String.length file in
      if len = 0 then
-       (Util.warn "Skipping bad $include. No file argument."; preprocess opts defs)
+       (Reporting.warn "" l "Skipping bad $include. No file argument."; preprocess opts defs)
      else if file.[0] = '"' && file.[len - 1] = '"' then
        let relative = match l with
          | Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname))
@@ -207,11 +208,18 @@ let rec preprocess opts = function
        include_defs @ preprocess opts defs
      else
        let help = "Make sure the filename is surrounded by quotes or angle brackets" in
-       (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs)
+       (Reporting.warn "" l ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs)
+
+  | Parse_ast.DEF_pragma ("suppress_warnings", _, l) :: defs ->
+     begin match Reporting.simp_loc l with
+     | None -> () (* This shouldn't happen, but if it does just continue *)
+     | Some (p, _) -> Reporting.suppress_warnings_for_file p.pos_fname
+     end;
+     preprocess opts defs
 
   | Parse_ast.DEF_pragma (p, arg, l) :: defs ->
      if not (StringSet.mem p all_pragmas) then
-       Util.warn (Reporting.loc_to_string l ^ "Unrecognised directive: " ^ p);
+       Reporting.warn "" l ("Unrecognised directive: " ^ p);
      Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs
 
   | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs ->
diff --git a/src/property.mli b/src/property.mli
index 8005f91a..66a732b9 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -104,6 +104,8 @@ type query =
    | Q_and of query list
    | Q_or of query list
 
+val default_query : query
+
 type pragma = {
     query : query;
     litmus : string list;
diff --git a/src/reporting.ml b/src/reporting.ml
index 9387ee6b..0b727836 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -95,6 +95,8 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+let opt_warnings = ref true
+
 type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
 
 let print_err_internal p_l m1 m2 =
@@ -143,7 +145,7 @@ let dest_err = function
   | Err_general (l, m) -> ("Error", Loc l, m)
   | Err_unreachable (l, (file, line, _, _), m) ->
      (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
-  | Err_todo (l, m) -> ("Todo" ^ m, Loc l, "")
+  | Err_todo (l, m) -> ("Todo", Loc l, m)
   | Err_syntax (p, m) -> ("Syntax error", Pos p, m)
   | Err_syntax_loc (l, m) -> ("Syntax error", Loc l, m)
   | Err_lex (p, s) -> ("Lexical error", Pos p, s)
@@ -164,3 +166,24 @@ let unreachable l pos msg =
 let print_error e =
   let (m1, pos_l, m2) = dest_err e in
   print_err_internal pos_l m1 m2
+
+(* Warnings *)
+
+module StringSet = Set.Make(String)
+
+let ignored_files = ref StringSet.empty
+
+let suppress_warnings_for_file f =
+  ignored_files := StringSet.add f !ignored_files
+
+let warn str1 l str2 =
+  if !opt_warnings then
+    match simp_loc l with
+    | None ->
+       prerr_endline (Util.("Warning" |> yellow |> clear) ^ ": " ^ str1 ^ "\n" ^ str2)
+    | Some (p1, p2) when not (StringSet.mem p1.pos_fname !ignored_files) ->
+       prerr_endline (Util.("Warning" |> yellow |> clear) ^ ": "
+                      ^ str1 ^ (if str1 <> "" then " " else "") ^ loc_to_string l ^ str2)
+    | Some _ -> ()
+  else
+    ()
diff --git a/src/reporting.mli b/src/reporting.mli
index 28f2a799..0bdff5ca 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -50,16 +50,18 @@
 
 (** Basic error reporting
 
-  [Reporting] contains functions to report errors and warnings. 
+  [Reporting] contains functions to report errors and warnings.
   It contains functions to print locations ([Parse_ast.l] and [Ast.l]) and lexing positions.
 
   The main functionality is reporting errors. This is done by raising a
-  [Fatal_error] exception. This is caught internally and reported via [report_error]. 
+  [Fatal_error] exception. This is caught internally and reported via [report_error].
   There are several predefined types of errors which all cause different error
-  messages. If none of these fit, [Err_general] can be used.       
+  messages. If none of these fit, [Err_general] can be used.
 
 *)
 
+val opt_warnings : bool ref
+
 (** {2 Auxiliary Functions } *)
 
 (** [loc_to_string] includes code from file if code optional argument is true (default) *)
@@ -70,7 +72,7 @@ val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
 
 (** [short_loc_to_string] prints the location as a single line in a simple format *)
 val short_loc_to_string : Parse_ast.l -> string
-  
+
 (** [print_err fatal print_loc_source l head mes] prints an error / warning message to
     std-err. It starts with printing location information stored in [l]
     It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.
@@ -113,7 +115,15 @@ val err_typ : Parse_ast.l -> string -> exn
 
 (** [err_syntax_loc] is an abbreviation for [Fatal_error (Err_syntax_loc (l, m))] *)
 val err_syntax_loc : Parse_ast.l -> string -> exn
-  
+
 val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
 
 val print_error : error -> unit
+
+(** Print a warning message. The first string is printed before the
+   location, the second after. *)
+val warn : string -> Parse_ast.l -> string -> unit
+
+(** Will suppress all warnings for a given file. Used by
+   $suppress_warnings directive in process_file.ml *)
+val suppress_warnings_for_file : string -> unit
diff --git a/src/return_analysis.ml b/src/return_analysis.ml
index 256f97cf..789df2c5 100644
--- a/src/return_analysis.ml
+++ b/src/return_analysis.ml
@@ -69,8 +69,6 @@ let analyze_exp_returns exp =
           analyze last exp
        end
 
-    | E_nondet exps -> List.iter (analyze last) exps
-
     | E_id id ->
        if last then
          add_return annot
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 2573a135..24261861 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -140,7 +140,6 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot)
 | Some (env, typ, eff) ->
   let effsum = match e with
     | E_block es -> union_eff_exps es
-    | E_nondet es -> union_eff_exps es
     | E_id _ | E_ref _
     | E_lit _ -> eff
     | E_cast (_,e) -> effect_of e
@@ -271,7 +270,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   let rewrite = rewriters.rewrite_exp rewriters in
   match exp with
   | E_block exps -> rewrap (E_block (List.map rewrite exps))
-  | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
   | E_id _ | E_lit _  -> rewrap exp
   | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp))
   | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps))
@@ -534,7 +532,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
   { e_block                  : 'exp list -> 'exp_aux
-  ; e_nondet                 : 'exp list -> 'exp_aux
   ; e_id                     : id -> 'exp_aux
   ; e_ref                    : id -> 'exp_aux
   ; e_lit                    : lit -> 'exp_aux
@@ -596,7 +593,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
 
 let rec fold_exp_aux alg = function
   | E_block es -> alg.e_block (List.map (fold_exp alg) es)
-  | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es)
   | E_id id -> alg.e_id id
   | E_ref id -> alg.e_ref id
   | E_lit lit -> alg.e_lit lit
@@ -680,7 +676,6 @@ let fold_function alg (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, fun
 
 let id_exp_alg =
   { e_block = (fun es -> E_block es)
-  ; e_nondet = (fun es -> E_nondet es)
   ; e_id = (fun id -> E_id id)
   ; e_ref = (fun id -> E_ref id)
   ; e_lit = (fun lit -> (E_lit lit))
@@ -776,7 +771,6 @@ let compute_exp_alg bot join =
   let join_list vs = List.fold_left join bot vs in
   let split_join f es = let (vs,es) = List.split es in (join_list vs, f es) in
   { e_block = split_join (fun es -> E_block es)
-  ; e_nondet = split_join (fun es -> E_nondet es)
   ; e_id = (fun id -> (bot, E_id id))
   ; e_ref = (fun id -> (bot, E_ref id))
   ; e_lit = (fun lit -> (bot, E_lit lit))
@@ -883,7 +877,6 @@ let pure_pat_alg bot join =
 let pure_exp_alg bot join =
   let join_list vs = List.fold_left join bot vs in
   { e_block = join_list
-  ; e_nondet = join_list
   ; e_id = (fun id -> bot)
   ; e_ref = (fun id -> bot)
   ; e_lit = (fun lit -> bot)
@@ -1004,10 +997,6 @@ let default_fold_exp f x (E_aux (e,ann) as exp) =
      let x,es = List.fold_left (fun (x,es) e ->
                     let x,e' = f x e in x,e'::es) (x,[]) es in
      x, re (E_block (List.rev es))
-  | E_nondet es ->
-     let x,es = List.fold_left (fun (x,es) e ->
-                    let x,e' = f x e in x,e'::es) (x,[]) es in
-     x, re (E_nondet (List.rev es))
   | E_id _
   | E_ref _
   | E_lit _ -> x, exp
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 878e0d15..77974f86 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -118,7 +118,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = 
  { e_block                  : 'exp list -> 'exp_aux
- ; e_nondet                 : 'exp list -> 'exp_aux
  ; e_id                     : id -> 'exp_aux
  ; e_ref                    : id -> 'exp_aux
  ; e_lit                    : lit -> 'exp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 6c38c689..b1fb0cdd 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2335,7 +2335,6 @@ let rewrite_defs_letbind_effects env =
 
     match exp_aux with
     | E_block es -> failwith "E_block should have been removed till now"
-    | E_nondet _ -> failwith "E_nondet not supported"
     | E_id id -> k exp
     | E_ref id -> k exp
     | E_lit _ -> k exp
@@ -4340,12 +4339,18 @@ let funcl_loc (FCL_aux (_,(l,_))) = l
 
 let rewrite_case (e,ann) =
   match e with
-  | E_case (e1,cases) ->
+  | E_case (e1,cases)
+  | E_try (e1,cases) ->
      begin
      let env = env_of_annot ann in
      let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in
+     let rebuild cases = match e with
+       | E_case _ -> E_case (e1,cases)
+       | E_try _ -> E_try (e1,cases)
+       | _ -> assert false
+     in
      match rps with
-     | [] -> E_aux (E_case (e1,cases),ann)
+     | [] -> E_aux (rebuild cases,ann)
      | (example::_) ->
 
         let _ =
@@ -4358,7 +4363,7 @@ let rewrite_case (e,ann) =
         let ann' = mk_tannot env (typ_of_annot ann) (mk_effect [BE_escape]) in
         (* TODO: use an expression that specifically indicates a failed pattern match *)
         let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in
-        E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann)
+        E_aux (rebuild (cases@[Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann)
      end
   | E_let (LB_aux (LB_val (pat,e1),lb_ann),e2) ->
      begin
@@ -5020,6 +5025,7 @@ let rewrites_target tgt =
   | "c" -> rewrites_c
   | "ir" -> rewrites_c @ [("properties", [])]
   | "smt" -> rewrites_c @ [("properties", [])]
+  | "smtfuzz" -> rewrites_c @ [("properties", [])]
   | "sail" -> []
   | "latex" -> []
   | "interpreter" -> rewrites_interpreter
diff --git a/src/sail.ml b/src/sail.ml
index c4991fe5..eae7c4cf 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -87,7 +87,7 @@ let options = Arg.align ([
     Arg.Set Interactive.opt_emacs_mode,
     " run sail interactively as an emacs mode child process");
   ( "-no_warn",
-    Arg.Clear Util.opt_warnings,
+    Arg.Clear Reporting.opt_warnings,
     " do not print warnings");
   ( "-tofrominterp",
     set_target "tofrominterp",
@@ -348,6 +348,9 @@ let options = Arg.align ([
   ( "-dprofile",
     Arg.Set Profile.opt_profile,
     " (debug) provide basic profiling information for rewriting passes within Sail");
+  ( "-dsmtfuzz",
+    set_target "smtfuzz",
+    " (debug) fuzz sail SMT builtins");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
@@ -450,28 +453,28 @@ let target name out_name ast type_envs =
      close_out f
 
   | Some "c" ->
-     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
+     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
      let ast_c, type_envs =
        if !opt_specialize_c then
-         Specialize.(specialize' 2 int_specialization ast_c type_envs)
+         Specialize.(specialize_passes 2 int_specialization type_envs ast_c)
        else
          ast_c, type_envs
      in
      let close, output_chan = match !opt_file_out with Some f -> true, open_out (f ^ ".c") | None -> false, stdout in
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c;
      flush output_chan;
      if close then close_out output_chan else ()
 
   | Some "ir" ->
-     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
+     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
      (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *)
      let close, output_chan =
        match !opt_file_out with
        | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".ir.sail"))
        | None -> false, stdout
      in
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in
      (* let cdefs = List.map Jib_optimize.flatten_cdef cdefs in *)
      let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in
@@ -479,18 +482,21 @@ let target name out_name ast type_envs =
      flush output_chan;
      if close then close_out output_chan else ()
 
+  | Some "smtfuzz" ->
+     Jib_smt_fuzz.fuzz 0 type_envs ast
+
   | Some "smt" ->
      let open Ast_util in
      let props = Property.find_properties ast in
      Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls;
-     let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
-     let ast_smt, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_smt type_envs) in
+     let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
+     let ast_smt, type_envs = Specialize.(specialize_passes 2 int_specialization_with_externs type_envs ast_smt) in
      let name_file =
        match !opt_file_out with
        | Some f -> fun str -> f ^ "_" ^ str ^ ".smt2"
        | None -> fun str -> str ^ ".smt2"
      in
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      Jib_smt.generate_smt props name_file type_envs ast_smt;
 
   | Some "lem" ->
@@ -500,7 +506,7 @@ let target name out_name ast type_envs =
      output "" (Coq_out (!opt_libs_coq)) [(out_name, type_envs, ast)]
 
   | Some "latex" ->
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in
      begin
        try
@@ -524,7 +530,7 @@ let main () =
   else
     begin
       let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
-      Util.opt_warnings := false; (* Don't show warnings during re-writing for now *)
+      Reporting.opt_warnings := false; (* Don't show warnings during re-writing for now *)
 
       begin match !opt_process_elf, !opt_file_out with
       | Some elf, Some out ->
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 40f5cecf..3812e4f7 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -733,6 +733,7 @@ let sign_extend (vec, n) =
   | B1 :: _ as vec -> replicate_bits ([B1], Big_int.of_int (m - List.length vec)) @ vec
 
 let zeros n = replicate_bits ([B0], n)
+let ones  n = replicate_bits ([B1], n)
 
 let shift_bits_right_arith (x, y) =
   let ybi = uint(y) in
diff --git a/src/slice.ml b/src/slice.ml
index 78009059..9dee4761 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -157,9 +157,9 @@ let add_def_to_graph graph def =
     let env = env_of_annot annot in
     begin match p_aux with
     | P_app (id, _) ->
-       graph := G.add_edge' self (Constructor id) !graph
+       graph := G.add_edge self (Constructor id) !graph
     | P_typ (typ, _) ->
-       IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ)
+       IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
     | _ -> ()
     end;
     P_aux (p_aux, annot)
@@ -170,9 +170,9 @@ let add_def_to_graph graph def =
     let env = env_of_annot annot in
     begin match lexp_aux with
     | LEXP_cast (typ, _) ->
-       IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ)
+       IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
     | LEXP_memory (id, _) ->
-       graph := G.add_edge' self (Function id) !graph
+       graph := G.add_edge self (Function id) !graph
     | _ -> ()
     end;
     LEXP_aux (lexp_aux, annot)
@@ -183,22 +183,22 @@ let add_def_to_graph graph def =
     begin match e_aux with
     | E_id id ->
        begin match Env.lookup_id id env with
-       | Register _ -> graph := G.add_edge' self (Register id) !graph
-       | Enum _ -> graph := G.add_edge' self (Constructor id) !graph
+       | Register _ -> graph := G.add_edge self (Register id) !graph
+       | Enum _ -> graph := G.add_edge self (Constructor id) !graph
        | _ ->
           if IdSet.mem id (Env.get_toplevel_lets env) then
-            graph := G.add_edge' self (Letbind id) !graph
+            graph := G.add_edge self (Letbind id) !graph
           else ()
        end
     | E_app (id, _) ->
        if Env.is_union_constructor id env then
-         graph := G.add_edge' self (Constructor id) !graph
+         graph := G.add_edge self (Constructor id) !graph
        else
-         graph := G.add_edge' self (Function id) !graph
+         graph := G.add_edge self (Function id) !graph
     | E_ref id ->
-       graph := G.add_edge' self (Register id) !graph
+       graph := G.add_edge self (Register id) !graph
     | E_cast (typ, _) ->
-       IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ)
+       IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
     | _ -> ()
     end;
     E_aux (e_aux, annot)
@@ -218,7 +218,7 @@ let add_def_to_graph graph def =
     match aux with
     | QI_id _ -> ()
     | QI_constraint nc ->
-       IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (constraint_ids nc)
+       IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (constraint_ids nc)
   in
 
   let scan_typquant self (TypQ_aux (aux, _)) =
@@ -230,7 +230,7 @@ let add_def_to_graph graph def =
   let add_type_def_to_graph (TD_aux (aux, (l, _))) =
     match aux with
     | TD_abbrev (id, typq, arg) ->
-       graph := G.add_edges' (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_arg_ids arg))) !graph;
+       graph := G.add_edges (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_arg_ids arg))) !graph;
        scan_typquant (Type id) typq
     | TD_record (id, typq, fields, _) ->
        let field_nodes =
@@ -239,44 +239,44 @@ let add_def_to_graph graph def =
          |> IdSet.elements
          |> List.map (fun id -> Type id)
        in
-       graph := G.add_edges' (Type id) field_nodes !graph;
+       graph := G.add_edges (Type id) field_nodes !graph;
        scan_typquant (Type id) typq
     | TD_variant (id, typq, ctors, _) ->
        let ctor_nodes =
          List.map (fun (Tu_aux (Tu_ty_id (typ, id), _)) -> (typ_ids typ, id)) ctors
          |> List.fold_left (fun (ids, ctors) (ids', ctor) -> (IdSet.union ids ids', IdSet.add ctor ctors)) (IdSet.empty, IdSet.empty)
        in
-       IdSet.iter (fun ctor_id -> graph := G.add_edge' (Constructor ctor_id) (Type id) !graph) (snd ctor_nodes);
-       IdSet.iter (fun typ_id -> graph := G.add_edge' (Type id) (Type typ_id) !graph) (fst ctor_nodes);
+       IdSet.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) (snd ctor_nodes);
+       IdSet.iter (fun typ_id -> graph := G.add_edge (Type id) (Type typ_id) !graph) (fst ctor_nodes);
        scan_typquant (Type id) typq
     | TD_enum (id, ctors, _) ->
-       List.iter (fun ctor_id -> graph := G.add_edge' (Constructor ctor_id) (Type id) !graph) ctors
+       List.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) ctors
     | TD_bitfield _ ->
        Reporting.unreachable l __POS__ "Bitfield should be re-written"
   in
 
   begin match def with
   | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) ->
-     graph := G.add_edges' (Function id) [] !graph;
-     IdSet.iter (fun typ_id -> graph := G.add_edge' (Function id) (Type typ_id) !graph) (typ_ids typ)
+     graph := G.add_edges (Function id) [] !graph;
+     IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ)
   | DEF_fundef fdef ->
      let id = id_of_fundef fdef in
-     graph := G.add_edges' (Function id) [] !graph;
+     graph := G.add_edges (Function id) [] !graph;
      ignore (rewrite_fun (rewriters (Function id)) fdef)
   | DEF_val (LB_aux (LB_val (pat, exp), _) as lb) ->
      let ids = pat_ids pat in
-     IdSet.iter (fun id -> graph := G.add_edges' (Letbind id) [] !graph) ids;
+     IdSet.iter (fun id -> graph := G.add_edges (Letbind id) [] !graph) ids;
      IdSet.iter (fun id -> ignore (rewrite_let (rewriters (Letbind id)) lb)) ids
   | DEF_type tdef ->
      add_type_def_to_graph tdef
   | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
-     IdSet.iter (fun typ_id -> graph := G.add_edge' (Register id) (Type typ_id) !graph) (typ_ids typ)
+     IdSet.iter (fun typ_id -> graph := G.add_edge (Register id) (Type typ_id) !graph) (typ_ids typ)
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
      ignore (rewrite_exp  (rewriters (Register id)) exp);
-     IdSet.iter (fun typ_id -> graph := G.add_edge' (Register id) (Type typ_id) !graph) (typ_ids typ)
+     IdSet.iter (fun typ_id -> graph := G.add_edge (Register id) (Type typ_id) !graph) (typ_ids typ)
   | _ -> ()
   end;
-  G.fix_leaves !graph
+  !graph
 
 let rec graph_of_ast (Defs defs) =
   let module G = Graph.Make(Node) in
@@ -305,9 +305,10 @@ let id_of_reg_dec (DEC_aux (aux, _)) =
 
 let filter_ast cuts g (Defs defs) =
   let rec filter_ast' g =
+    let module NS = Set.Make(Node) in
     let module NM = Map.Make(Node) in
     function
-    | DEF_fundef fdef :: defs when IdSet.mem (id_of_fundef fdef) cuts -> filter_ast' g defs
+    | DEF_fundef fdef :: defs when NS.mem (Function (id_of_fundef fdef)) cuts -> filter_ast' g defs
     | DEF_fundef fdef :: defs when NM.mem (Function (id_of_fundef fdef)) g -> DEF_fundef fdef :: filter_ast' g defs
     | DEF_fundef _ :: defs -> filter_ast' g defs
 
@@ -327,6 +328,10 @@ let filter_ast cuts g (Defs defs) =
     | DEF_type tdef :: defs when NM.mem (Type (id_of_typedef tdef)) g -> DEF_type tdef :: filter_ast' g defs
     | DEF_type _ :: defs -> filter_ast' g defs
 
+    | DEF_measure (id,_,_) :: defs when NS.mem (Function id) cuts -> filter_ast' g defs
+    | (DEF_measure (id,_,_) as def) :: defs when NM.mem (Function id) g -> def :: filter_ast' g defs
+    | DEF_measure _ :: defs -> filter_ast' g defs
+
     | def :: defs -> def :: filter_ast' g defs
 
     | [] -> []
diff --git a/src/slice.mli b/src/slice.mli
index 04f140fe..0c15defb 100644
--- a/src/slice.mli
+++ b/src/slice.mli
@@ -68,4 +68,4 @@ val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph
 
 val dot_of_ast : out_channel -> Type_check.tannot defs -> unit
 
-val filter_ast : IdSet.t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs
+val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 5a2fcd44..b90f33a7 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -94,8 +94,10 @@ type smt_exp =
   | Real_lit of string
   | String_lit of string
   | Var of string
+  | Read_res of string
   | Enum of string
   | Fn of string * smt_exp list
+  | Ctor of string * smt_exp list
   | Ite of smt_exp * smt_exp * smt_exp
   | SignExtend of int * smt_exp
   | Extract of int * int * smt_exp
@@ -103,11 +105,12 @@ type smt_exp =
 
 let rec fold_smt_exp f = function
   | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args))
+  | Ctor (name, args) -> f (Ctor (name, List.map (fold_smt_exp f) args))
   | Ite (cond, t, e) -> f (Ite (fold_smt_exp f cond, fold_smt_exp f t, fold_smt_exp f e))
   | SignExtend (n, exp) -> f (SignExtend (n, fold_smt_exp f exp))
   | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp))
   | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp))
-  | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Enum _ as exp) -> f exp
+  | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Read_res _ | Enum _ as exp) -> f exp
 
 let smt_conj = function
   | [] -> Bool_lit true
@@ -196,44 +199,55 @@ let simp_ite = function
   | Ite (Bool_lit false, _, else_exp) -> else_exp
   | exp -> exp
 
-let rec simp_smt_exp vars = function
+let rec simp_smt_exp vars kinds = function
   | Var v ->
      begin match Hashtbl.find_opt vars v with
-     | Some exp -> simp_smt_exp vars exp
+     | Some exp -> simp_smt_exp vars kinds exp
      | None -> Var v
      end
-  | (Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | (Read_res _ | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
   | Fn (f, exps) ->
-     let exps = List.map (simp_smt_exp vars) exps in
+     let exps = List.map (simp_smt_exp vars kinds) exps in
      simp_fn (Fn (f, exps))
+  | Ctor (f, exps) ->
+     let exps = List.map (simp_smt_exp vars kinds) exps in
+     simp_fn (Ctor (f, exps))
   | Ite (cond, t, e) ->
-     let cond = simp_smt_exp vars cond in
-     let t = simp_smt_exp vars t in
-     let e = simp_smt_exp vars e in
+     let cond = simp_smt_exp vars kinds cond in
+     let t = simp_smt_exp vars kinds t in
+     let e = simp_smt_exp vars kinds e in
      simp_ite (Ite (cond, t, e))
   | Extract (i, j, exp) ->
-     let exp = simp_smt_exp vars exp in
+     let exp = simp_smt_exp vars kinds exp in
      begin match exp with
      | Bin str ->
         Bin (String.sub str ((String.length str - 1) - i) ((i + 1) - j))
      | _ -> Extract (i, j, exp)
      end
   | Tester (str, exp) ->
-     let exp = simp_smt_exp vars exp in
-     Tester (str, exp)
+     let exp = simp_smt_exp vars kinds exp in
+     begin match exp with
+     | Var v ->
+        begin match Hashtbl.find_opt kinds v with
+        | Some str' when str = str' -> Bool_lit true
+        | Some str' -> Bool_lit false
+        | None -> Tester (str, exp)
+        end
+     | _ -> Tester (str, exp)
+     end
   | SignExtend (i, exp) ->
-     let exp = simp_smt_exp vars exp in
+     let exp = simp_smt_exp vars kinds exp in
      SignExtend (i, exp)
 
 type smt_def =
   | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
   | Declare_const of string * smt_typ
   | Define_const of string * smt_typ * smt_exp
-  | Write_mem of string * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
-  | Write_mem_ea of string * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
-  | Read_mem of string * smt_typ * smt_exp * smt_exp * smt_typ
-  | Barrier of string * smt_exp
-  | Excl_res of string
+  | Write_mem of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
+  | Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
+  | Read_mem of string * int * smt_exp * smt_typ * smt_exp * smt_exp * smt_typ
+  | Barrier of string * int * smt_exp * smt_exp
+  | Excl_res of string * int * smt_exp
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
@@ -252,16 +266,19 @@ let suffix_variables_def sfx = function
      Declare_const (name ^ sfx, ty)
   | Define_const (name, ty, exp) ->
      Define_const (name ^ sfx, ty, suffix_variables_exp sfx exp)
-  | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
-     Write_mem (name ^ sfx, suffix_variables_exp sfx wk, suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty)
-  | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) ->
-     Write_mem (name ^ sfx, suffix_variables_exp sfx wk, suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
-  | Read_mem (name, ty, rk, addr, addr_ty) ->
-     Read_mem (name ^ sfx, ty, suffix_variables_exp sfx rk, suffix_variables_exp sfx addr, addr_ty)
-  | Barrier (name, bk) ->
-     Barrier (name ^ sfx, bk)
-  | Excl_res name ->
-     Excl_res (name ^ sfx)
+  | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
+     Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
+                suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty)
+  | Write_mem_ea (name, node, active , wk, addr, addr_ty, data_size, data_size_ty) ->
+     Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
+                suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
+  | Read_mem (name, node, active, ty, rk, addr, addr_ty) ->
+     Read_mem (name ^ sfx, node, suffix_variables_exp sfx active, ty, suffix_variables_exp sfx rk,
+               suffix_variables_exp sfx addr, addr_ty)
+  | Barrier (name, node, active, bk) ->
+     Barrier (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx bk)
+  | Excl_res (name, node, active) ->
+     Excl_res (name ^ sfx, node, suffix_variables_exp sfx active)
   | Declare_datatypes (name, ctors) ->
      Declare_datatypes (name, ctors)
   | Declare_tuple n ->
@@ -314,8 +331,10 @@ let rec pp_smt_exp =
   | Hex str -> string ("#x" ^ str)
   | Bin str -> string ("#b" ^ str)
   | Var str -> string str
+  | Read_res str -> string (str ^ "_ret")
   | Enum str -> string str
   | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
+  | Ctor (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
   | Ite (cond, then_exp, else_exp) ->
      parens (separate space [string "ite"; pp_smt_exp cond; pp_smt_exp then_exp; pp_smt_exp else_exp])
   | Extract (i, j, exp) ->
@@ -354,27 +373,32 @@ let pp_smt_def =
   | Define_const (name, ty, exp) ->
      pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
 
-  | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
+  | Write_mem (name, _, active, wk, addr, addr_ty, data, data_ty) ->
      pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
+     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_data"); pp_smt_typ data_ty; pp_smt_exp data] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
      ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ Bool]
 
-  | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) ->
+  | Write_mem_ea (name, _, active, wk, addr, addr_ty, data_size, data_size_ty) ->
      pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
+     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_size"); pp_smt_typ data_size_ty; pp_smt_exp data_size] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr]
 
-  | Read_mem (name, ty, rk, addr, addr_ty) ->
+  | Read_mem (name, _, active, ty, rk, addr, addr_ty) ->
      pp_sfun "define-const" [string (name ^ "_kind"); string "Zread_kind"; pp_smt_exp rk] ^^ hardline
+     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
      ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ ty]
 
-  | Barrier (name, bk) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk]
+  | Barrier (name, _, active, bk) ->
+     pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk] ^^ hardline
+     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active]
 
-  | Excl_res name ->
-     pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool]
+  | Excl_res (name, _, active) ->
+     pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool] ^^ hardline
+     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active]
 
   | Declare_datatypes (name, ctors) ->
      let pp_ctor (ctor_name, fields) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 8afc985d..907c62a5 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -184,7 +184,7 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
 let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.t * Nameset.t * Nameset.t) =
   let list_fv b n s es = List.fold_right (fun e (b,n,s) -> fv_of_exp consider_var b n s e) es (b,n,s) in
   match e with
-  | E_block es | Ast.E_nondet es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es ->
+  | E_block es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es ->
     list_fv bound used set es
   | E_id id ->
      let used = conditional_add_exp bound used id in
@@ -808,7 +808,6 @@ let nexp_subst_fns substs =
     let re e = E_aux (e,(l,s_tannot annot)) in
       match e with
       | E_block es -> re (E_block (List.map s_exp es))
-      | E_nondet es -> re (E_nondet (List.map s_exp es))
       | E_id _
       | E_ref _
       | E_lit _
diff --git a/src/specialize.ml b/src/specialize.ml
index a601974e..815514d1 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -586,7 +586,7 @@ let specialize_ids spec ids ast =
   Profile.finish "specialization pass" t;
   ast, env
 
-let rec specialize' n spec ast env =
+let rec specialize_passes n spec env ast =
   if n = 0 then
     ast, env
   else
@@ -595,6 +595,6 @@ let rec specialize' n spec ast env =
       ast, env
     else
       let ast, env = specialize_ids spec ids ast in
-      specialize' (n - 1) spec ast env
+      specialize_passes (n - 1) spec env ast
 
-let specialize = specialize' (-1)
+let specialize = specialize_passes (-1)
diff --git a/src/specialize.mli b/src/specialize.mli
index 0a64112c..ddfb0c67 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -81,11 +81,11 @@ val add_initial_calls : IdSet.t -> unit
    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 : specialization -> tannot defs -> Env.t -> tannot defs * Env.t
+val specialize : specialization -> Env.t -> tannot defs -> tannot defs * Env.t
 
 (** specialize' n performs at most n specialization passes. Useful for
    int_specialization which is not guaranteed to terminate. *)
-val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs * Env.t
+val specialize_passes : int -> specialization -> Env.t -> tannot defs -> tannot defs * Env.t
 
 (** return all instantiations of a function id, with the
    instantiations filtered according to the specialization. *)
diff --git a/src/type_check.ml b/src/type_check.ml
index fabcd7b4..1dd806f0 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3129,9 +3129,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        (* If the identifier we're matching on is also a constructor of
           a union, that's probably a mistake, so warn about it. *)
        if Env.is_union_constructor v env then
-         Util.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at %s\n"
-                                   (string_of_id v)
-                                   (Reporting.loc_to_string l))
+         Reporting.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at"
+                                        (string_of_id v))
+                        l ""
        else ();
        match Env.lookup_id v env with
        | Local _ | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
@@ -3696,8 +3696,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let rec last_typ = function [exp] -> typ_of exp | _ :: exps -> last_typ exps | [] -> unit_typ in
      let inferred_block = check_block l env exps None in
      annot_exp (E_block inferred_block) (last_typ inferred_block)
-  | E_nondet exps ->
-     annot_exp (E_nondet (List.map (fun exp -> crule check_exp env exp unit_typ) exps)) unit_typ
   | E_id v ->
      begin
        match Env.lookup_id v env with
@@ -4087,9 +4085,9 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
        (* If the identifier we're matching on is also a constructor of
           a union, that's probably a mistake, so warn about it. *)
        if Env.is_union_constructor v env then
-         Util.warn (Printf.sprintf "Identifier %s found in mapping-pattern is also a union constructor at %s\n"
-                                   (string_of_id v)
-                                   (Reporting.loc_to_string l))
+         Reporting.warn (Printf.sprintf "Identifier %s found in mapping-pattern is also a union constructor at"
+                                        (string_of_id v))
+                        l ""
        else ();
        match Env.lookup_id v env with
        | Local (Immutable, _) | Unbound -> annot_mpat (MP_id v) typ, Env.add_local v (Immutable, typ) env, []
@@ -4411,9 +4409,6 @@ and propagate_exp_effect_aux = function
   | E_block xs ->
      let p_xs = List.map propagate_exp_effect xs in
      E_block p_xs, collect_effects p_xs
-  | E_nondet xs ->
-     let p_xs = List.map propagate_exp_effect xs in
-     E_nondet p_xs, collect_effects p_xs
   | E_id id -> E_id id, no_effect
   | E_ref id -> E_ref id, no_effect
   | E_lit lit -> E_lit lit, no_effect
diff --git a/src/util.ml b/src/util.ml
index 6a2fb9bb..2745631c 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -94,7 +94,6 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-let opt_warnings = ref true
 let opt_colors = ref true
 let opt_verbosity = ref 0
 
@@ -110,7 +109,7 @@ let rec butlast = function
 
 module Duplicate(S : Set.S) = struct
 
-type dups = 
+type dups =
   | No_dups of S.t
   | Has_dups of S.elt
 
@@ -129,7 +128,7 @@ end
 let remove_duplicates l =
   let l' = List.sort Pervasives.compare l in
   let rec aux acc l = match (acc, l) with
-      (_, []) -> List.rev acc 
+      (_, []) -> List.rev acc
     | ([], x :: xs) -> aux [x] xs
     | (y::ys, x :: xs) -> if (x = y) then aux (y::ys) xs else aux (x::y::ys) xs
   in
@@ -138,7 +137,7 @@ let remove_duplicates l =
 let remove_dups compare eq l =
   let l' = List.sort compare l in
   let rec aux acc l = match (acc, l) with
-      (_, []) -> List.rev acc 
+      (_, []) -> List.rev acc
     | ([], x :: xs) -> aux [x] xs
     | (y::ys, x :: xs) -> if (eq x y) then aux (y::ys) xs else aux (x::y::ys) xs
   in
@@ -159,7 +158,7 @@ let rec assoc_compare_opt cmp k l =
     | [] -> None
     | (k',v)::l -> if cmp k k' = 0 then Some v else assoc_compare_opt cmp k l
 
-let rec compare_list f l1 l2 = 
+let rec compare_list f l1 l2 =
   match (l1,l2) with
     | ([],[]) -> 0
     | (_,[]) -> 1
@@ -199,7 +198,7 @@ let rec map_filter (f : 'a -> 'b option) (l : 'a list) : 'b list =
   match l with [] -> []
     | x :: xs ->
       let xs' = map_filter f xs in
-      match (f x) with None -> xs' 
+      match (f x) with None -> xs'
         | Some x' -> x' :: xs'
 
 let list_index p l =
@@ -317,13 +316,13 @@ let string_to_list s =
     else aux (i-1) (s.[i] :: acc)
   in aux (String.length s - 1) []
 
-module IntSet = Set.Make( 
+module IntSet = Set.Make(
   struct
     let compare = Pervasives.compare
     type t = int
   end )
 
-module IntIntSet = Set.Make( 
+module IntIntSet = Set.Make(
   struct
     let compare = Pervasives.compare
     type t = int * int
@@ -456,11 +455,6 @@ let file_encode_string str =
   let md5 = Digest.to_hex (Digest.string zstr) in
   String.lowercase_ascii zstr ^ String.lowercase_ascii md5
 
-let warn str =
-  if !opt_warnings then
-    prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str)
-  else ()
-
 let log_line str line msg =
   "\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg
 
diff --git a/src/util.mli b/src/util.mli
index ddc5347f..9c57e360 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -50,13 +50,12 @@
 
 (** Various non Sail specific utility functions *)
 
-(* Last element of a list *)
-val last : 'a list -> 'a
-
-val opt_warnings : bool ref
 val opt_colors : bool ref
 val opt_verbosity : int ref
 
+(* Last element of a list *)
+val last : 'a list -> 'a
+
 val butlast : 'a list -> 'a list
 
 (** Mixed useful things *)
@@ -270,5 +269,3 @@ val log_line : string -> int -> string -> string
 val header : string -> int -> string
 
 val progress : string -> string -> int -> int -> unit
-
-val warn : string -> unit
diff --git a/src/value.ml b/src/value.ml
index 6c2e0839..c509c81f 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -433,6 +433,10 @@ let value_zeros = function
   | [v] -> mk_vector (Sail_lib.zeros (coerce_int v))
   | _ -> failwith "value zeros"
 
+let value_ones = function
+  | [v] -> mk_vector (Sail_lib.ones (coerce_int v))
+  | _ -> failwith "value ones"
+
 let value_shiftl = function
   | [v1; v2] -> mk_vector (Sail_lib.shiftl (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value shiftl"
@@ -670,6 +674,7 @@ let primops =
       ("zero_extend", value_zero_extend);
       ("sign_extend", value_sign_extend);
       ("zeros", value_zeros);
+      ("ones", value_ones);
       ("shiftr", value_shiftr);
       ("shiftl", value_shiftl);
       ("shift_bits_left", value_shift_bits_left);
@@ -724,6 +729,7 @@ let primops =
       ("undefined_unit", fun _ -> V_unit);
       ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
       ("undefined_int", fun _ -> V_int Big_int.zero);
+      ("undefined_nat", fun _ -> V_int Big_int.zero);
       ("undefined_bool", fun _ -> V_bool false);
       ("undefined_vector", value_undefined_vector);
       ("undefined_string", fun _ -> V_string "");
diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh
index cc6f223e..dc2bdde4 100755
--- a/test/aarch64_small/run_tests.sh
+++ b/test/aarch64_small/run_tests.sh
@@ -45,7 +45,7 @@ function finish_suite {
 
 printf "<testsuites>\n" >> $DIR/tests.xml
 
-if make -B -C ../../aarch64_small SAIL="$SAILDIR/sail"
+if make -B -C ../../aarch64_small armV8.lem SAIL="$SAILDIR/sail"
 then
     green "built aarch64_small to lem" "ok"
 else
diff --git a/test/builtins/slice_mask.sail b/test/builtins/slice_mask.sail
new file mode 100644
index 00000000..e694f029
--- /dev/null
+++ b/test/builtins/slice_mask.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <exception_basic.sail>
+$include <flow.sail>
+$include <vector_dec.sail>
+
+function main (() : unit) -> unit = {
+  assert(slice_mask(32, 8, 4)   == 0x00000F00);
+  assert(slice_mask(32, 16, 8)  == 0x00FF0000);
+  assert(slice_mask(32, 15, 3)  == 0x00038000);
+  assert(slice_mask(32, 16, 32) == 0xFFFF0000);
+}
diff --git a/test/c/single_guard.expect b/test/c/single_guard.expect
new file mode 100644
index 00000000..070cdc2c
--- /dev/null
+++ b/test/c/single_guard.expect
@@ -0,0 +1,2 @@
+In main
+In test
diff --git a/test/c/single_guard.sail b/test/c/single_guard.sail
new file mode 100644
index 00000000..017ed8a5
--- /dev/null
+++ b/test/c/single_guard.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+val test : unit -> unit
+
+function test(_ if true) = {
+  print_endline("In test")
+}
+
+function main() -> unit = {
+  print_endline("In main");
+  test()
+}
\ No newline at end of file
diff --git a/test/coq/pass/non_exh_exc.sail b/test/coq/pass/non_exh_exc.sail
new file mode 100644
index 00000000..8ce99163
--- /dev/null
+++ b/test/coq/pass/non_exh_exc.sail
@@ -0,0 +1,18 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+  Error_foo : unit,
+  Error_bar : int
+}
+
+val f : int -> int effect {escape}
+
+function f(n) = {
+  try {
+    let m : int = if n > 5 then n - 3 else throw(Error_bar(n)) in
+    m + 1
+  } catch {
+    Error_bar(n) => n
+  }
+}
diff --git a/test/coq/pass/throw_fact.sail b/test/coq/pass/throw_fact.sail
new file mode 100644
index 00000000..e40267b1
--- /dev/null
+++ b/test/coq/pass/throw_fact.sail
@@ -0,0 +1,25 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+  BadInput : int
+}
+
+val test1 : int -> nat effect {escape}
+
+function test1(n) = {
+  if (n < 0) then {
+    throw (BadInput(n))
+  };
+  n
+}
+
+val test2 : int -> nat effect {escape}
+
+function test2(n) = {
+  m : nat = 0;
+  if (n < 0) then {
+    throw (BadInput(n))
+  } else { m = 1 };
+  n+m
+}
diff --git a/test/coq/pass/var_type_autocast.sail b/test/coq/pass/var_type_autocast.sail
new file mode 100644
index 00000000..6c65b978
--- /dev/null
+++ b/test/coq/pass/var_type_autocast.sail
@@ -0,0 +1,13 @@
+default Order dec
+$include <prelude.sail>
+$include <smt.sail>
+
+val load_bytes : forall 'n, 'n >= 0. int('n) -> bits(8 * 'n)
+
+val foo : forall 'n, 'n in {8,16}. (int('n),bool) -> bits('n)
+
+function foo(n,b) = {
+  let 'bytes = ediv_int(n,8);
+  let data = load_bytes(bytes);
+  if b then data else sail_zeros(n)
+}
diff --git a/test/smt/arith_LC32L.unsat.sail b/test/smt/arith_LC32L.unsat.sail
index 547a5cb1..82184bf8 100644
--- a/test/smt/arith_LC32L.unsat.sail
+++ b/test/smt/arith_LC32L.unsat.sail
@@ -2,26 +2,11 @@ default Order dec
 
 $include <prelude.sail>
 
-$option -smt_ignore_overflow
-
 $property
 function prop(x: int, y: int(32), z: int) -> bool = {
   let add_comm  = x + y == y + x;
   let add_assoc = (x + y) + z == x + (y + z);
   let add_id  = x + 0 == x;
 
-  let mul_comm = x * y == y * x;
-  let mul_assoc = (x * y) * z == x * (y * z);
-  let mul_zero = x * 0 == 0;
-
-  let add_mul_distrib = x * (y + z) == (x * y) + (x * z);
-
-  let add_neg_zero = x + negate(x) == 0;
-  let add_neg_sub  = x + negate(y) == x - y;
-  let neg_neg = negate(negate(x)) == x;
-
   add_comm & add_assoc & add_id
-  & mul_comm & mul_assoc & mul_zero
-  & add_mul_distrib
-  & add_neg_zero & add_neg_sub & neg_neg
-}
\ No newline at end of file
+}
diff --git a/test/smt/arith_LC32L_1.unsat.sail b/test/smt/arith_LC32L_1.unsat.sail
new file mode 100644
index 00000000..82184bf8
--- /dev/null
+++ b/test/smt/arith_LC32L_1.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  let add_comm  = x + y == y + x;
+  let add_assoc = (x + y) + z == x + (y + z);
+  let add_id  = x + 0 == x;
+
+  add_comm & add_assoc & add_id
+}
diff --git a/test/smt/arith_LC32L_2.unsat.sail b/test/smt/arith_LC32L_2.unsat.sail
new file mode 100644
index 00000000..9a29fe13
--- /dev/null
+++ b/test/smt/arith_LC32L_2.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  let mul_comm = x * y == y * x;
+  let mul_zero1 = x * 0 == 0;
+  let mul_zero2 = y * 0 == 0;
+
+  mul_comm & mul_zero1 & mul_zero2
+}
\ No newline at end of file
diff --git a/test/smt/arith_LC32L_3.unsat.sail b/test/smt/arith_LC32L_3.unsat.sail
new file mode 100644
index 00000000..7d97a76b
--- /dev/null
+++ b/test/smt/arith_LC32L_3.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  if  -10000 <= x & x <= 10000 & -10000 <= z & z <= 10000 then
+    (x * y) * z == x * (y * z)
+  else true
+}
diff --git a/test/smt/arith_LC32L_4.unsat.sail b/test/smt/arith_LC32L_4.unsat.sail
new file mode 100644
index 00000000..e94ab2c3
--- /dev/null
+++ b/test/smt/arith_LC32L_4.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32)) -> bool = {
+  let add_neg_zero = x + negate(x) == 0;
+  let add_neg_sub  = x + negate(y) == x - y;
+  let neg_neg = negate(negate(x)) == x;
+
+  add_neg_zero & add_neg_sub & neg_neg
+}
diff --git a/test/smt/load_store_dep.sat.sail b/test/smt/load_store_dep.sat.sail
new file mode 100644
index 00000000..bb35c6f7
--- /dev/null
+++ b/test/smt/load_store_dep.sat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+$include "test/arch.sail"
+
+/* Default memory model is as weak as possible, so this is not true */
+$counterexample
+function prop() -> bool = {
+  let _ = arch_load(0b00, 0b01);
+  let _ = arch_store(0b10, 0b00);
+  X(0b01) == X(0b10)
+}
diff --git a/test/smt/minmax.unsat.sail b/test/smt/minmax.unsat.sail
new file mode 100644
index 00000000..f1bdf55a
--- /dev/null
+++ b/test/smt/minmax.unsat.sail
@@ -0,0 +1,20 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$property
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(3, 2) == 3);
+  assert(min_int(3, 2) == 2);
+  assert(max_int(-132542345, 3) == 3);
+
+  assert(max_int(a, b) == max_int(b, a));
+  assert(min_int(a, b) == min_int(b, a));
+
+  assert(max_int(0, 0) == 0);
+
+  true
+}
diff --git a/test/smt/minmax_1.sat.sail b/test/smt/minmax_1.sat.sail
new file mode 100644
index 00000000..09119db0
--- /dev/null
+++ b/test/smt/minmax_1.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, a) == max_int(b, a));
+  true
+}
diff --git a/test/smt/minmax_2.sat.sail b/test/smt/minmax_2.sat.sail
new file mode 100644
index 00000000..dd773058
--- /dev/null
+++ b/test/smt/minmax_2.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, b) == min_int(a, b));
+  true
+}
diff --git a/test/smt/sail_mask.unsat.sail b/test/smt/sail_mask.unsat.sail
new file mode 100644
index 00000000..4afbab90
--- /dev/null
+++ b/test/smt/sail_mask.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 0 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0b0);
+  assert(x == sail_zeros(n));
+  true
+}
diff --git a/test/smt/sail_mask_2.unsat.sail b/test/smt/sail_mask_2.unsat.sail
new file mode 100644
index 00000000..8904bbe9
--- /dev/null
+++ b/test/smt/sail_mask_2.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 1 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0b1);
+  assert(x == sail_zero_extend(0b1, n));
+  true
+}
diff --git a/test/smt/sail_mask_3.unsat.sail b/test/smt/sail_mask_3.unsat.sail
new file mode 100644
index 00000000..5f4b5fe4
--- /dev/null
+++ b/test/smt/sail_mask_3.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 32 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  assert(x == sail_zero_extend(0xdeadbeef, n));
+  true
+}
diff --git a/test/smt/sail_mask_4.unsat.sail b/test/smt/sail_mask_4.unsat.sail
new file mode 100644
index 00000000..368a3f2d
--- /dev/null
+++ b/test/smt/sail_mask_4.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 31 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  if n >= 32 then
+     assert(x == sail_zero_extend(0xdeadbeef, n))
+  else
+     assert(x == 0b1011110101011011011111011101111);
+  true
+}
diff --git a/test/smt/sail_mask_5.unsat.sail b/test/smt/sail_mask_5.unsat.sail
new file mode 100644
index 00000000..452c7f6c
--- /dev/null
+++ b/test/smt/sail_mask_5.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 31 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  if n >= 32 then
+     assert(x == sail_zero_extend(0xdeadbeef, n))
+  else
+     assert(0b1011110101011011011111011101111 == x);
+  true
+}
diff --git a/test/typecheck/pass/constant_nexp/v2.expect b/test/typecheck/pass/constant_nexp/v2.expect
index 3c4dcc16..7c0e8093 100644
--- a/test/typecheck/pass/constant_nexp/v2.expect
+++ b/test/typecheck/pass/constant_nexp/v2.expect
@@ -3,6 +3,6 @@ Type error:
 12 |  let _ = czeros(sizeof('n - 10) + 20);
    |          ^--------------------------^
    | Could not resolve quantifiers for czeros
-   | * is_constant(('fv47#n : Int))
+   | * is_constant(('fv50#n : Int))
    | * (('n - 10) + 20) >= 0
    |