diff --git a/CHANGES.md b/CHANGES.md
index daa61f77..41778b1e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -24,8 +24,9 @@
 
   There is also a new `Round` class for types that can sensibly be
   rounded to integers.  This class has the methods `floor`, `ceiling`,
-  `trunc` and `round` for performing different kinds of
-  integer rounding.  Currently `Rational` is the only meber of `Round`.
+  `trunc`, `roundToEven`  and `roundAway` for performing different
+  kinds of integer rounding.  Currently `Rational` is the only member
+  of `Round`.
 
   The type of `(^^)` is modified to be
   `{a, e} (Ring a, Integral e) => a -> e -> a`. This makes it clear
@@ -35,6 +36,10 @@
   Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have
   had their types specialized so operate only on bitvectors.
 
+* Added an `Eq` class, and moved the equality operations
+  from `Cmp` into `Eq`. The `Z` type becomes a member of `Eq`
+  but not `Cmp`.
+
 * Added a base `Rational` type.  It is implemented as a pair of
   integers, quotiented in the usual way.  As such, it reduces to the
   theory of integers and requires no new solver support (beyond
@@ -45,6 +50,10 @@
 * The `generate` function (and thus `x @ i= e` definitions) has had
   its type specialized so the index type is always `Integer`.
 
+* The new typeclasses are arranged into a class hierarchy, and the
+  typechecker will use that information to infer superclass instances
+  from subclasses.
+
 ## New features
 
 * Document the behavior of lifted selectors.
@@ -57,10 +66,23 @@
 * More detailed information about the status of various symbols
   in the output of the `:browse` command (issue #688).
 
+* The `:safe` command will attempt to prove that a given Cryptol
+  term is safe; in other words, that it will not encounter a run-time
+  error for all inputs. Run-time errors arise from things like
+  division-by-zero, index-out-of-bounds situations and
+  explicit calls to `error` or `assert`.
+
+* The `:prove` and `:sat` commands now incorporate safety predicates
+  by default. In a `:sat` call, models will only be found that do not
+  cause run-time errors. For `:prove` calls, the safety conditions are
+  added as additional proof goals.  The prior behavior
+  (which ignored safety conditions) can be restored using
+  `:set ignore-safety = on`.
+
 ## Bug fixes
 
-* Closed issues #346, #444, #614, #617, #660, #662, #663, #664, #667, #670,
-  #711
+* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, #667, #670,
+  #702, #711, #712, #716, #723, #725, #731
 
 # 2.8.0 (September 4, 2019)
 
diff --git a/docs/Cryptol.pdf b/docs/Cryptol.pdf
index 648020b1..f4e88e79 100644
Binary files a/docs/Cryptol.pdf and b/docs/Cryptol.pdf differ
diff --git a/docs/CryptolPrims.md b/docs/CryptolPrims.md
index 50ece2cd..e25214b5 100644
--- a/docs/CryptolPrims.md
+++ b/docs/CryptolPrims.md
@@ -1,102 +1,59 @@
-Comparisons and Ordering
-------------------------
-
-    (==)   :  {a}   (Cmp a) => a -> a -> Bit
-    (!=)   :  {a}   (Cmp a) => a -> a -> Bit
-    (===)  :  {a,b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
-    (!==)  :  {a,b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
-
-    (<)    :  {a} (Cmp a) => a -> a -> Bit
-    (>)    :  {a} (Cmp a) => a -> a -> Bit
-    (<=)   :  {a} (Cmp a) => a -> a -> Bit
-    (>=)   :  {a} (Cmp a) => a -> a -> Bit
-
-    min    :  {a} (Cmp a) => a -> a -> a
-    max    :  {a} (Cmp a) => a -> a -> a
-
-    instance Cmp Bit
-    // No instance for functions.
-    instance (Cmp a, fin n) => Cmp [n]a
-    instance (Cmp a, Cmp b) => Cmp (a, b)
-    instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
-    instance                   Cmp Integer
-    instance (fin n, n>=1)  => Cmp (Z n)
-    instance                   Cmp Rational
-
-Signed Comparisons
+Typeclass Heriarchy
 ---------------------
 
-    (<$) : {a} (SignedCmp a) => a -> a -> Bit
-    (>$) : {a} (SignedCmp a) => a -> a -> Bit
-    (<=$) : {a} (SignedCmp a) => a -> a -> Bit
-    (>=$) : {a} (SignedCmp a) => a -> a -> Bit
+          Zero
+          /  \
+      Logic  Ring          Eq
+             /  \         /  \
+      Integral  Field   Cmp  SignedCmp
+                    \   /
+                    Round
+
+
+This diagram describes how the various typeclasses in
+Cryptol are related.  A type which is an instance of a
+subclass is also always a member of all of its superclasses.
+For example, any type which is a member of `Field` is also
+a member of `Ring` and `Zero`.
+
+
+Literals
+-----------------------
+    type Literal : # -> * -> Prop
+
+    number : {val, rep} Literal val rep => rep
+    length : {n, a, b} (fin n, Literal n b) => [n]a -> b
+
+    // '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'
+    fromTo : {first, last, a}
+               (fin last, last >= first,
+               Literal first a, Literal last a) =>
+               [1 + (last - first)]a
+
+    // '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'
+    fromThenTo : {first, next, last, a, len}
+                   ( fin first, fin next, fin last
+                   , Literal first a, Literal next a, Literal last a
+                   , first != next
+                   , lengthFromThenTo first next last == len) =>
+		   [len]a
 
-    // No instance for Bit
-    // No instance for functions.
-    instance (fin n, n >= 1)            => SignedCmp [n]
-    instance (SignedCmp a, fin n)       => SignedCmp [n]a
-            // (for [n]a, where a is other than Bit)
-    instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
-    instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
 
 Zero
 ----
 
+    type Zero  : * -> Prop
+
     zero       : {a} (Zero a) => a
 
 Every base and structured type in Cryptol is a member of class `Zero`.
 
 
-Arithmetic
-----------
-
-    (+)     : {a} (Ring a) => a -> a -> a
-    (-)     : {a} (Ring a) => a -> a -> a
-    (*)     : {a} (Ring a) => a -> a -> a
-    negate  : {a} (Ring a) => a -> a
-
-    (/)     : {a} (Integral a) => a -> a -> a
-    (%)     : {a} (Integral a) => a -> a -> a
-
-    (/.)    : {a} (Field a) => a -> a -> a
-    recip   : {a} (Field a) => a -> a
-
-    floor   : {a} (Round a) => a -> Integer
-    ceiling : {a} (Round a) => a -> Integer
-    trunc   : {a} (Round a) => a -> Integer
-    round   : {a} (Round a) => a -> Integer
-
-    (^^)    : {a, e} (Ring a, Integral e) => a -> e -> a
-
-    (/$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
-    (%$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
-    lg2     : {n} (fin n) => [n] -> [n]
-
-The prefix notation `- x` is syntactic sugar for `negate x`.
-
-    // No instance for `Bit`.
-    instance (fin n)          => Ring ([n]Bit)
-    instance (Ring a)         => Ring ([n]a)
-    instance (Ring b)         => Ring (a -> b)
-    instance (Ring a, Ring b) => Ring (a, b)
-    instance (Ring a, Ring b) => Ring { x : a, y : b }
-    instance                     Ring Integer
-    instance (fin n, n>=1)    => Ring (Z n)
-    instance                     Ring Rational
-
-Note that because there is no instance for `Ring Bit`
-the top two instances do not actually overlap.
-
-    instance                  Integral Integer 
-    instance (fin n)       => Integral ([n]Bit)
-
-    instance Field Rational
-
-    instance Round Rational
-
 Boolean
 -------
 
+    type Logic : * -> Prop
+
     False      : Bit
     True       : Bit
 
@@ -104,6 +61,8 @@ Boolean
     (||)       : {a} (Logic a) => a -> a -> a
     (^)        : {a} (Logic a) => a -> a -> a
     complement : {a} (Logic a) => a -> a
+      // The prefix notation '~ x' is syntactic
+      // sugar for 'complement x'.
 
     (==>)      : Bit -> Bit -> Bit
     (/\)       : Bit -> Bit -> Bit
@@ -118,17 +77,174 @@ Boolean
     // No instance for `Logic (Z n)`.
     // No instance for `Logic Rational`.
 
+
+Arithmetic
+----------
+
+    type Ring   : * -> Prop
+
+    fromInteger : {a} (Ring a) => Integer -> a
+    (+) : {a} (Ring a) => a -> a -> a
+    (-) : {a} (Ring a) => a -> a -> a
+    (*) : {a} (Ring a) => a -> a -> a
+    negate : {a} (Ring a) => a -> a
+      // The prefix notation `- x` is syntactic
+      // sugar for `negate x`.
+
+
+    type Integral : * -> Prop
+
+    (/) : {a} (Integral a) => a -> a -> a
+    (%) : {a} (Integral a) => a -> a -> a
+    toInteger : {a} (Integral a) => a -> Integer
+    infFrom : {a} (Integral a) => a -> [inf]a
+      // '[x...]' is syntactic sugar for 'infFrom x'
+    infFromThen : {a} (Integral a) => a -> a -> [inf]a
+      // [x,y...]' is syntactic sugar for 'infFromThen x y'
+
+
+    type Field : * -> Prop
+
+    (/.)  : {a} (Field a) => a -> a -> a
+    recip : {a} (Field a) => a -> a
+
+
+    type Round : * -> Prop
+
+    floor       : {a} (Round a) => a -> Integer
+    ceiling     : {a} (Round a) => a -> Integer
+    trunc       : {a} (Round a) => a -> Integer
+    roundAway   : {a} (Round a) => a -> Integer
+    roundToEven : {a} (Round a) => a -> Integer
+
+    (^^) : {a, e} (Ring a, Integral e) => a -> e -> a
+
+    // No instance for `Bit`.
+    instance (fin n)          => Ring ([n]Bit)
+    instance (Ring a)         => Ring ([n]a)
+    instance (Ring b)         => Ring (a -> b)
+    instance (Ring a, Ring b) => Ring (a, b)
+    instance (Ring a, Ring b) => Ring { x : a, y : b }
+    instance                     Ring Integer
+    instance (fin n, n>=1)    => Ring (Z n)
+    instance                     Ring Rational
+
+Note that because there is no instance for `Ring Bit`
+the top two instances do not actually overlap.
+
+    instance                  Integral Integer
+    instance (fin n)       => Integral ([n]Bit)
+
+    instance Field Rational
+
+    instance Round Rational
+
+
+Equality Comparisons
+------------------------
+
+    type Eq : * -> Prop
+
+    (==)  :  {a}   (Eq a) => a -> a -> Bit
+    (!=)  :  {a}   (Eq a) => a -> a -> Bit
+    (===) :  {a,b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
+    (!==) :  {a,b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
+
+    instance                  Eq Bit
+    instance (Eq a, fin n) => Eq [n]a
+    instance (Eq a, Eq b)  => Eq (a, b)
+    instance (Eq a, Eq b)  => Eq { x : a, y : b }
+    instance 	       	      Eq Integer
+    instance 		      Eq Rational
+    instance (fin n, n>=1) => Eq (Z n)
+    // No instance for functions.
+
+
+Comparisons and Ordering
+------------------------
+
+    type Cmp : * -> Prop
+
+    (<)  : {a} (Cmp a) => a -> a -> Bit
+    (>)  : {a} (Cmp a) => a -> a -> Bit
+    (<=) : {a} (Cmp a) => a -> a -> Bit
+    (>=) : {a} (Cmp a) => a -> a -> Bit
+
+    min  : {a} (Cmp a) => a -> a -> a
+    max  : {a} (Cmp a) => a -> a -> a
+
+    abs  : {a} (Cmp a, Ring a) => a -> a
+
+    instance                   Cmp Bit
+    instance (Cmp a, fin n) => Cmp [n]a
+    instance (Cmp a, Cmp b) => Cmp (a, b)
+    instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
+    instance                   Cmp Integer
+    instance                   Cmp Rational
+    // No instance for functions.
+
+
+Signed Comparisons
+---------------------
+
+    type SignedCmp : * -> Prop
+
+    (<$)  : {a} (SignedCmp a) => a -> a -> Bit
+    (>$)  : {a} (SignedCmp a) => a -> a -> Bit
+    (<=$) : {a} (SignedCmp a) => a -> a -> Bit
+    (>=$) : {a} (SignedCmp a) => a -> a -> Bit
+
+    // No instance for Bit
+    instance (fin n, n >= 1)            => SignedCmp [n]
+    instance (SignedCmp a, fin n)       => SignedCmp [n]a
+            // (for [n]a, where a is other than Bit)
+    instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
+    instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
+    // No instance for functions.
+
+
+Bitvectors
+-----------
+
+    (/$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
+    (%$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
+
+    carry   : {n} (fin n) => [n] -> [n] -> Bit
+    scarry  : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
+    sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
+
+    zext    : {m, n} (fin m, m >= n) => [n] -> [m]
+    sext    : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
+
+    lg2     : {n} (fin n) => [n] -> [n]
+
+    // Arithmetic shift only for bitvectors
+    (>>$)   : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
+
+
+Rationals
+---------
+
+    ratio : Integer -> Integer -> Rational
+
+
+Z(n)
+-----
+
+    fromZ : {n} (fin n, n >= 1) => Z n -> Integer
+
+
 Sequences
 ---------
 
-    join      : {parts,each,a} (fin each) => [parts][each]a -> [parts * each]a
-    split     : {parts,each,a} (fin each) => [parts * each]a -> [parts][each]a
+    join       : {parts,each,a} (fin each) => [parts][each]a -> [parts * each]a
+    split      : {parts,each,a} (fin each) => [parts * each]a -> [parts][each]a
 
-    (#)       : {front,back,a} (fin front) => [front]a -> [back]a -> [front + back]a
-    splitAt   : {front,back,a} (fin front) => [from + back] a -> ([front] a, [back] a)
+    (#)        : {front,back,a} (fin front) => [front]a -> [back]a -> [front + back]a
+    splitAt    : {front,back,a} (fin front) => [from + back] a -> ([front] a, [back] a)
 
-    reverse   : {n,a} (fin n) => [n]a -> [n]a
-    transpose : {n,m,a} [n][m]a -> [m][n]a
+    reverse    : {n,a} (fin n) => [n]a -> [n]a
+    transpose  : {n,m,a} [n][m]a -> [m][n]a
 
     (@)        : {n,a,ix}   (Integral ix) =>  [n]a -> ix    -> a
     (@@)       : {n,k,ix,a} (Integral ix) =>  [n]a -> [k]ix -> [k]a
@@ -145,6 +261,10 @@ Sequences
     tail       : {a, b} [1 + a]b -> [a]b
     last       : {a, b} [1 + a]b -> b
 
+    // Declarations of the form 'x @ i = e' are syntactic
+    // sugar for 'x = generate (\i -> e)'.
+    generate   : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a
+
     groupBy    : {each,parts,elem} (fin each) => [parts * each]elem -> [parts][each]elem
 
 Function `groupBy` is the same as `split` but with its type arguments
@@ -153,23 +273,60 @@ in a different order.
 Shift And Rotate
 ----------------
 
-    (<<)   : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
-    (>>)   : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
-    (<<<)  : {n,ix,a} (fin n, Integral ix)  => [n]a -> ix -> [n]a
-    (>>>)  : {n,ix,a} (fin n, Integral ix)  => [n]a -> ix -> [n]a
+    (<<)  : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
+    (>>)  : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
+    (<<<) : {n,ix,a} (fin n, Integral ix)  => [n]a -> ix -> [n]a
+    (>>>) : {n,ix,a} (fin n, Integral ix)  => [n]a -> ix -> [n]a
+
+
+GF(2) polynomials
+-----------------
+
+    pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
+    pdiv  : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
+    pmod  : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
 
-    // Arithmetic shift only for bitvectors
-    (>>$)  : {n,ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
 
 Random Values
 -------------
 
-    random    : {a} => [256] -> a
+    random : {a} => [256] -> a
+
+
+Errors and Assertions
+---------------------
+
+     undefined : {a} a
+     error     : {a,n} (fin n) => String n -> a
+     assert    : {a,n} (fin n) => Bit -> String n -> a -> a
+
 
 Debugging
 ---------
 
-     undefined   : {a} a
-     error       : {n a} [n][8] -> a
-     trace       : {n, a, b} (fin n) => [n][8] -> a -> b -> b
-     traceVal    : {n, a} (fin n) => [n][8] -> a -> a
+     trace     : {n, a, b} (fin n) => String n -> a -> b -> b
+     traceVal  : {n, a} (fin n) => String n -> a -> a
+
+
+Utility operations
+------------------
+
+    and   : {n} (fin n) => [n]Bit -> Bit
+    or    : {n} (fin n) => [n]Bit -> Bit
+    all   : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
+    any   : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
+    elem  : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
+
+    map   : {n, a, b} (a -> b) -> [n]a -> [n]b
+    foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
+    foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
+    scanl : {n, b, a}  (b -> a -> b) -> b -> [n]a -> [n+1]b
+    scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
+    sum   : {n, a} (fin n, Ring a) => [n]a -> a
+
+    iterate : {a} (a -> a) -> a -> [inf]a
+    repeat  : {n, a} a -> [n]a
+    zip     : {n, a, b} [n]a -> [n]b -> [n](a, b)
+    zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
+    uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
+    curry   : {a, b, c} ((a, b) -> c) -> a -> b -> c
diff --git a/docs/CryptolPrims.pdf b/docs/CryptolPrims.pdf
index a9e87d2e..0253ffef 100644
Binary files a/docs/CryptolPrims.pdf and b/docs/CryptolPrims.pdf differ
diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf
index 648020b1..f4e88e79 100644
Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ
diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
index 728a73d6..1c7685b1 100644
--- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
@@ -2667,10 +2667,11 @@ automatically, to get the answers:
 \begin{Exercise}\label{ex:recfun:4:1}
 Define a function {\tt elem} with the following signature:\indElem
 \begin{code}
-  elem : {n, t} (fin n, Cmp t) => (t, [n]t) -> Bit
+  elem : {n, t} (fin n, Eq t) => (t, [n]t) -> Bit
 \end{code}
 such that {\tt elem (x, xs)} returns {\tt True} if {\tt x} appears in
-{\tt xs}, and {\tt False} otherwise.
+{\tt xs}, and {\tt False} otherwise.\footnote{Note: this function
+  is already present in the Cryptol prelude.}
 \end{Exercise}
 \begin{Answer}\ansref{ex:recfun:4:1}
 Using a fold, it is easy to write {\tt elem}:
@@ -2922,7 +2923,7 @@ Type classes are a way of describing behaviors shared by multiple
 types.  As an example, consider the type of the function {\tt ==}:
 \begin{Verbatim}
     Cryptol> :t (==)
-    (==) : {a} (Cmp a) => a -> a -> Bit
+    (==) : {a} (Eq a) => a -> a -> Bit
 \end{Verbatim}
 
 This type signature may be read as, ``equality is an operator that
@@ -2930,7 +2931,7 @@ takes two objects of any single type that can be compared and returns
 a Bit.''
 
 Cryptol defines a collection of basic type classes: \texttt{Logic},
-\texttt{Zero}, \texttt{Cmp}, \texttt{SignedCmp}, \texttt{Ring},
+\texttt{Zero}, \texttt{Eq}, \texttt{Cmp}, \texttt{SignedCmp}, \texttt{Ring},
 \texttt{Integral}, \texttt{Field}, \texttt{Round}, and
 \texttt{Literal}. These appear in the type signature of operators and
 functions that require them. If a function you define calls, for
@@ -2952,15 +2953,17 @@ All of the built-in types of Cryptol are instances of class
 \texttt{Zero}.
 
 \item
-The \texttt{Cmp} typeclass includes the binary relation operators
-\texttt{<}, \texttt{>}, \texttt{<=}, \texttt{>=}, \texttt{==}, and
-\texttt{!=}, as well as the binary functions \texttt{min} and
-\texttt{max}. Note that equality and other comparisons are bundled
-into a single typeclass. Function types are not in class \texttt{Cmp}
+The \texttt{Eq} typeclass includes the equality testing operations
+\texttt{==} and \texttt{!=}. Function types are not in class \texttt{Eq}
 and cannot be compared with \texttt{==}, but Cryptol does provide a
 special pointwise comparison operator for functions, \texttt{(===) :
   \{a b\} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit}.
 
+\item
+The \texttt{Cmp} typeclass includes the binary relation operators
+\texttt{<}, \texttt{>}, \texttt{<=}, \texttt{>=}, as well as the
+binary functions \texttt{min} and \texttt{max}.
+
 \item
 The \texttt{SignedCmp} typeclass includes the binary relation
 operators \texttt{<\$}, \texttt{>\$}, \texttt{<=\$}, and
@@ -2996,9 +2999,9 @@ Currently, only type \texttt{Rational} is a member of this class.
 \item
  The \texttt{Round} typeclass contains types that can be
  rounded to integers.  It includes \texttt{floor}, \texttt{ceiling},
- \texttt{trunc} and \texttt{round} operations, which are all different
- ways of rounding values to integers.
-Currently, only type \texttt{Rational} is a member of this class.
+ \texttt{trunc}, \texttt{roundAway} and \texttt{roundToEven}
+ operations, which are all different ways of rounding values to
+ integers. Currently, only type \texttt{Rational} is a member of this class.
 
 \item
 The \texttt{Literal} typeclass includes numeric literals.
@@ -3008,7 +3011,7 @@ The \texttt{Literal} typeclass includes numeric literals.
   Without including an explicit type declaration, define a function
   that Cryptol infers has the following type:
 \begin{Verbatim}
-  cmpRing : {a,b} (Cmp a, Ring b) => a -> a -> b -> b
+  cmpRing : {a,b} (Eq a, Ring b) => a -> a -> b -> b
 \end{Verbatim}
 \end{Exercise}
 \begin{Answer}\ansref{ex:tvar:1}
@@ -3018,7 +3021,7 @@ This code:
 \end{code}
 yields the inferred type:
 \begin{Verbatim}
-  cmpRing : {a, b} (Cmp a, Ring b) => a -> a -> b -> b
+  cmpRing : {a, b} (Eq a, Ring b) => a -> a -> b -> b
 \end{Verbatim}
 \end{Answer}
 
diff --git a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
index 342a7eb4..fbbc7117 100644
--- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
+++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
@@ -213,7 +213,7 @@ a different value: a property we might expect to hold
 intuitively. Here is the type of {\tt flipNeverIdentity}:
 \begin{Verbatim}
   Cryptol> :t flipNeverIdentity
-  flipNeverIdentity : {a} (Cmp a, Logic a) => a -> Bit
+  flipNeverIdentity : {a} (Eq a, Logic a) => a -> Bit
 \end{Verbatim}
 So, the only requirement on \texttt{flipNeverIdentity} is that it
 receives some type that supports comparisons and logical operations.
diff --git a/docs/ProgrammingCryptol/prims/Primitives.tex b/docs/ProgrammingCryptol/prims/Primitives.tex
index f3f44097..5e4c1617 100644
--- a/docs/ProgrammingCryptol/prims/Primitives.tex
+++ b/docs/ProgrammingCryptol/prims/Primitives.tex
@@ -15,11 +15,11 @@ primsPlaceHolder=1;
 \end{Verbatim}
 \paragraph*{Comparisons}
 \begin{Verbatim}
-    ==, !=           : {a} (Cmp a) => a -> a -> Bit
+    ==, !=           : {a} (Eq a) => a -> a -> Bit
     <, >, <=, >=     : {a} (Cmp a) => a -> a -> Bit
     <$, >$, <=$, >=$ : {a} (SignedCmp a) => a -> a -> Bit
     min, max         : {a} (Cmp a) => a -> a -> a
-    ===, !==         : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
+    ===, !==         : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
 \end{Verbatim}
 \paragraph*{Arithmetic}
 \begin{Verbatim}
@@ -42,9 +42,10 @@ primsPlaceHolder=1;
     floor             : {a} (Round a) => a -> Integer
     ceiling           : {a} (Round a) => a -> Integer
     trunc             : {a} (Round a) => a -> Integer
-    round             : {a} (Round a) => a -> Integer
+    roundAway         : {a} (Round a) => a -> Integer
+    roundToEven       : {a} (Round a) => a -> Integer
 \end{Verbatim}
-\paragraph*{Polynomial arithmetic}
+\paragraph*{GF(2) polynomial arithmetic}
 \begin{Verbatim}
     pdiv  : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
     pmod  : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
@@ -97,6 +98,7 @@ primsPlaceHolder=1;
     all, any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
     curry    : {a, b, c} ((a, b) -> c) -> a -> b -> c
     uncurry  : {a, b, c} (a -> b -> c) -> (a, b) -> c
+    elem     : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
 \end{Verbatim}
 \paragraph*{Miscellaneous}
 \begin{Verbatim}
@@ -105,8 +107,9 @@ primsPlaceHolder=1;
 \end{Verbatim}
 \paragraph*{Representing exceptions}
 \begin{Verbatim}
-    error     : {a, len} (fin len) => [len][8] -> a
     undefined : {a} a
+    error     : {a, n} (fin n) => String n -> a
+    assert    : {a, n} (fin n) => Bit -> String n -> a -> a
     trace     : {n, a, b} [n][8] -> a -> b -> b
     traceVal  : {n, a} [n][8] -> a -> a
 \end{Verbatim}
diff --git a/docs/ProgrammingCryptol/technicalities/TechAppendix.tex b/docs/ProgrammingCryptol/technicalities/TechAppendix.tex
index f3a428f0..1004f85f 100644
--- a/docs/ProgrammingCryptol/technicalities/TechAppendix.tex
+++ b/docs/ProgrammingCryptol/technicalities/TechAppendix.tex
@@ -130,7 +130,7 @@ type of an infix operator (e.g., {\tt +}, {\tt ==}, etc.)  you will need
 to surround the operator with {\tt ()}, like this:
 \begin{Verbatim}
   Cryptol> :t (+)
-  (+) : {a} (Arith a) => a -> a -> a
+  (+) : {a} (Ring a) => a -> a -> a
 \end{Verbatim}
 
 \paragraph*{Browsing definitions}
@@ -158,14 +158,15 @@ have defined, along with their types.
     \hline
      \textbf{Option}     & \textbf{Default value} & \textbf{Meaning}  \\
     \hline
-     \texttt{ascii}           & \texttt{off}   & print sequences of bytes as a string  \\
+     \texttt{ascii}           & \texttt{off}   & print sequences of bytes as a string \\
      \texttt{base}            & \texttt{16}    & numeric base for printing words  \\
-     \texttt{debug}           & \texttt{off}   & whether to print verbose debugging information \\
+     \texttt{ignore-safety}   & \texttt{off}   & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
      \texttt{infLength}       & \texttt{5}     & number of elements to show from an infinite sequence \\
      \texttt{prover}          & \texttt{z3}    & which SMT solver to use for \texttt{:prove}  \\
      \texttt{satNum}          & \texttt{1}     & maximum number of solutions to show for \texttt{:sat} \\
+     \texttt{show-examples}   & \texttt{on}    & whether to print counterexamples and models \\
+     \texttt{smtfile}         & \texttt{-}     & file to write SMT problems when \texttt{prover = offline} \\
      \texttt{tests}           & \texttt{100}   & number of tests to run for \texttt{:check} \\
-     \texttt{warnDefaulting}  & \texttt{on}    & \todo[inline]{talk to Iavor} \\
     \hline
   \end{tabular*}
   \label{tab:set_options}
@@ -173,8 +174,9 @@ have defined, along with their types.
 \paragraph*{Environment options}
 A variety of environment options are set through the use of the
 \texttt{:set} command.  These options may change over time and some
-options may be available only on specific platforms.  The current
-options are summarized in~\autoref{tab:set_options}.
+options may be available only on specific platforms.  The most useful
+configuration options are summarized in~\autoref{tab:set_options}.
+Help information about all flags can found by typing {\tt :help :set flag}.
 
 \todo[inline]{Ensure index references exist for all commands.}
 
@@ -220,7 +222,7 @@ At the Cryptol prompt you can load a module by name with the {\tt
   :module} command.\indCmdLoadModule
 
 \paragraph*{}
-The next three commands all operate on \emph{properties}.  All take
+The next commands all operate on \emph{properties}.  All take
 either one or zero arguments.  If one argument is provided, then that
 property is the focus of the command; otherwise all properties in the
 current context are checked.  All three commands are covered in detail
@@ -231,16 +233,30 @@ The \texttt{:check} command performs random value testing on a
 property to increase one's confidence that the property is valid.
 See~\autoref{sec:quickcheck} for more detailed information.
 
+\paragraph*{Checking a property through exhaustive testing}
+The \texttt{:exhaust} command enumerates all the possible input values
+of a property to test that it is correct for every possible value.
+This is infeasible except for properties with quite small input
+domains!
+
 \paragraph*{Verifying a property through automated theorem proving}
 The \texttt{:prove} command uses an external SMT solver to attempt to
 automatically formally prove that a given property is valid.
 See~\autoref{sec:formal-proofs} for more detailed information.
 
 \paragraph*{Finding a satisfying assignment for a property}
-The \texttt{:sat} command uses an external SAT solver to attempt to
+The \texttt{:sat} command uses an external SMT solver to attempt to
 find a satisfying assignment to a property.  See~\autoref{sec:sat} for
 more detailed information.
 
+\paragraph*{Proving that a property is safe}
+The \texttt{:safe} command uses an external SMT solver to attempt to
+prove that the given term is safe for all inputs, which means it cannot
+encounter a run-time error.  Unlike the other commands in this section,
+\texttt{:safe} \emph{must} be given an argument and can be called on
+values that compute types other than \texttt{Bit}.  Most types, except
+infinite streams and functions, are allowed in the result type.
+
 % \paragraph*{Type specialization}
 % Discuss \texttt{:debug\_specialize}.  \todo[inline]{Dylan?}
 
diff --git a/docs/Semantics.pdf b/docs/Semantics.pdf
index 7774f768..7d1d14ed 100644
Binary files a/docs/Semantics.pdf and b/docs/Semantics.pdf differ
diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index cd02546d..e3f19403 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2013-2016 Galois, Inc.
+ * Copyright (c) 2013-2020 Galois, Inc.
  * Distributed under the terms of the BSD3 license (see LICENSE file)
  */
 
@@ -29,31 +29,33 @@ primitive type Bit : *
 /** The type of unbounded integers. */
 primitive type Integer : *
 
-/** 'Z n' is the type of integers, modulo 'n'.
-  *
-  * The values of `Z n` may be thought of as equivalance
-  * classes of integers according to the equivalence
-  * `x ~ y` iff `n` divides `x - y`.  `Z n` naturally
-  * forms a ring, but does not support integral division
-  * or indexing.
-  *
-  * However, you may use the `fromZ` operation
-  * to project values in `Z n` into the integers if such operations
-  * are required.  This will compute the reduced representative
-  * of the equivalance class. In other words, `fromZ` computes
-  * the (unique) integer value `i`  where `0 <= i < n` and
-  * `i` is in the given equivalance class.
-  */
+/**
+ * 'Z n' is the type of integers, modulo 'n'.
+ *
+ * The values of 'Z n' may be thought of as equivalance
+ * classes of integers according to the equivalence
+ * 'x ~ y' iff 'n' divides 'x - y'.  'Z n' naturally
+ * forms a ring, but does not support integral division
+ * or indexing.
+ *
+ * However, you may use the 'fromZ' operation
+ * to project values in 'Z n' into the integers if such operations
+ * are required.  This will compute the reduced representative
+ * of the equivalance class. In other words, 'fromZ' computes
+ * the (unique) integer value 'i'  where '0 <= i < n' and
+ * 'i' is in the given equivalance class.
+ */
 primitive type {n : #} (fin n, n >= 1) => Z n : *
 
-/** `Rational` is the type of rational numbers.
-  * Rational numbers form a Field (and thus a Ring).
-  *
-  * The `ratio` operation may be used to directly create
-  * rational values from as a ratio of integers, or
-  * the `fromInteger` method and the field operations
-  * can be used.
-  */
+/**
+ * 'Rational' is the type of rational numbers.
+ * Rational numbers form a Field (and thus a Ring).
+ *
+ * The 'ratio' operation may be used to directly create
+ * rational values from as a ratio of integers, or
+ * the 'fromInteger' method and the field operations
+ * can be used.
+ */
 primitive type Rational : *
 
 type Bool = Bit
@@ -255,13 +257,20 @@ primitive complement : {a} (Logic a) => a -> a
 
 // The Ring class -------------------------------------------------------
 
-/** Value types that support ring addition and multiplication. */
+/**
+ * Value types that support ring addition and multiplication.
+ *
+ * Floating-point values are only approximately a ring, but
+ * nonetheless inhabit this class.
+ */
 primitive type Ring : * -> Prop
 
 /**
  * Converts an unbounded integer to a value in a Ring. When converting
  * to the bitvector type [n], the value is reduced modulo 2^^n. Likewise,
- * when converting to Z n, the value is reduced modulo n.
+ * when converting to Z n, the value is reduced modulo n.  When converting
+ * to a floating-point value, the value is rounded to the nearest
+ * representable value.
  */
 primitive fromInteger : {a} (Ring a) => Integer -> a
 
@@ -302,10 +311,11 @@ primitive negate : {a} (Ring a) => a -> a
 
 // The Integral class -------------------------------------------------
 
-/** Value types that correspond to a segment of the
-  * integers. These types support integer division and
-  * modulus, indexing into sequences, and enumeration.
-  */
+/**
+ * Value types that correspond to a segment of the
+ * integers. These types support integer division and
+ * modulus, indexing into sequences, and enumeration.
+ */
 primitive type Integral : * -> Prop
 
 /**
@@ -332,8 +342,8 @@ primitive toInteger : {a} (Integral a) => a -> Integer
  * Compute the exponentiation of a value in a ring.
  *  * For type [n], the exponent is treated as unsigned.
  *  * It is an error to raise a value to a negative integer exponent.
- *  * Satisfies: `x ^^ 0 == fromInteger 1`
- *  * Satisfies: `x ^^ e == x * x ^^ (e-1)` when `e > 0`.
+ *  * Satisfies: 'x ^^ 0 == fromInteger 1'
+ *  * Satisfies: 'x ^^ e == x * x ^^ (e-1)' when 'e > 0'.
  */
 primitive (^^) : {a, e} (Ring a, Integral e) => a -> e -> a
 
@@ -352,21 +362,22 @@ primitive infFromThen : {a} (Integral a) => a -> a -> [inf]a
 
 // The Field class -------------------------------------------------
 
-/** Value types that correspond to a field; that is, a
-  * ring also posessing multiplicative inverses for
-  * non-zero elements.
-  *
-  * Floating-point values are only approximately a field,
-  * but nonetheless inhabit this class.
-  */
+/**
+ * Value types that correspond to a field; that is,
+ * a ring also posessing multiplicative inverses for
+ * non-zero elements.
+ *
+ * Floating-point values are only approximately a field,
+ * but nonetheless inhabit this class.
+ */
 primitive type Field : * -> Prop
 
 /**
-  * Reciprocal
-  *
-  * Compute the multiplicative inverse of an element of a field.
-  * The reciprocal of zero is undefined.
-  */
+ * Reciprocal
+ *
+ * Compute the multiplicative inverse of an element of a field.
+ * The reciprocal of 0 is undefined.
+ */
 primitive recip : {a} (Field a) => a -> a
 
 /**
@@ -581,11 +592,19 @@ a ==> b = if a then b else True
 
 /**
  * 2's complement signed division.  Division rounds toward 0.
+ *  Division by 0 is undefined.
+ *
+ *  * Satisfies 'x == x %$ y + (x /$ y) * y' for 'y != 0'.
  */
 primitive (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
 
 /**
  * 2's complement signed remainder.  Division rounds toward 0.
+ * Division by 0 is undefined.  Satisfies the following for 'y != 0'
+ *
+ *  * 'x %$ y == x - (x /$ y) * y'.
+ *  * 'x >=$ 0 ==> x %$ y >=$ 0'
+ *  * 'x <=$ 0 ==> x %$ y <=$ 0'
  */
 primitive (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
 
@@ -640,7 +659,7 @@ primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
  * Log base two.
  *
  * For words, computes the ceiling of log, base 2, of a number.
- *  We set `lg2 0 = 0`
+ *  We set 'lg2 0 = 0'
  */
 primitive lg2 : {n} (fin n) => [n] -> [n]
 
@@ -649,7 +668,9 @@ primitive lg2 : {n} (fin n) => [n] -> [n]
 
 /**
  * Compute the ratio of two integers as a rational.
- * ratio x y = (fromInteger x /. fromInteger y) : Rational
+ * Ratio is undefined if the denominator is 0.
+ *
+ * 'ratio x y = (fromInteger x /. fromInteger y) : Rational'
  */
 primitive ratio : Integer -> Integer -> Rational
 
@@ -704,17 +725,26 @@ primitive reverse : {n, a} (fin n) => [n]a -> [n]a
 primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
 
 
+/**
+ * Select the first (left-most) 'front' elements of a sequence.
+ */
 take : {front, back, a} (fin front) => [front + back]a -> [front]a
 take (x # _) = x
 
+/**
+ * Select all the elements after (to the right of) the 'front' elements of a sequence.
+ */
 drop : {front, back, a} (fin front) => [front + back]a -> [back]a
 drop ((_ : [front] _) # y) = y
 
+/**
+ * Drop the first (left-most) element of a sequence.
+ */
 tail : {n, a} [1 + n]a -> [n]a
 tail xs = drop`{1} xs
 
 /**
- * Return the left-most element of a sequence.
+ * Return the first (left-most) element of a sequence.
  */
 head : {n, a} [1 + n]a -> a
 head xs = xs @ 0
@@ -725,13 +755,18 @@ head xs = xs @ 0
 last : {n, a} (fin n) => [1 + n]a -> a
 last xs = xs ! 0
 
+/**
+ * Same as 'split', but with a different type argument order.
+ * Take a sequence of elements and break it into 'parts' sequences
+ * of 'each' elements.
+ */
 groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a
 groupBy = split`{parts=parts}
 
 /**
  * Left shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
-*/
+ */
 primitive (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
 
 /**
@@ -890,19 +925,27 @@ pmod x y = if y == 0 then 0/0 else last zs
 
 // Utility operations -----------------------------------------------------------------
 
-primitive error : {a, len} (fin len) => String len -> a
+/**
+ * Raise a run-time error with the given message.
+ * This function can be called at any type.
+ */
+primitive error : {a, n} (fin n) => String n -> a
 
+/**
+ * Raise a run-time error with a generic message.
+ * This function can be called at any type.
+ */
 undefined : {a} a
 undefined = error "undefined"
 
 /**
  * Assert that the given condition holds, and raise an error
- * with the given message if it does not.
+ * with the given message if it does not.  If the condition
+ * holds, return the third argument unchanged.
  */
-assert : {a, len} (fin len) => Bit -> String len -> a -> a
+assert : {a, n} (fin n) => Bit -> String n -> a -> a
 assert pred msg x = if pred then x else error msg
 
-
 /**
  * Generates random values from a seed.  When called with a function, currently
  * generates a function that always returns zero.
@@ -920,7 +963,7 @@ primitive random : {a} [256] -> a
  * which are unspecified.  Thus, the output produced by this
  * operation may be difficult to predict.
  */
-primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
+primitive trace : {n, a, b} (fin n) => String n -> a -> b -> b
 
 /**
  * Debugging function for tracing values.  The first argument is a string,
@@ -933,7 +976,7 @@ primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
  * which are unspecified.  Thus, the output produced by this
  * operation may be difficult to predict.
  */
-traceVal : {n, a} (fin n) => [n][8] -> a -> a
+traceVal : {n, a} (fin n) => String n -> a -> a
 traceVal msg x = trace msg x x
 
 
@@ -1016,7 +1059,7 @@ repeat x = [ x | _ <- zero : [n] ]
 /**
  * 'elem x xs' returns true if x is equal to a value in xs.
  */
-elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
+elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
 elem a xs = any (\x -> x == a) xs
 
 /**
diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout
index eb6ababa..071caa11 100644
--- a/tests/issues/issue226.icry.stdout
+++ b/tests/issues/issue226.icry.stdout
@@ -117,15 +117,15 @@ Symbols
     all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
     and : {n} (fin n) => [n] -> Bit
     any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
-    assert : {a, len} (fin len) => Bit -> String len -> a -> a
+    assert : {a, n} (fin n) => Bit -> String n -> a -> a
     carry : {n} (fin n) => [n] -> [n] -> Bit
     ceiling : {a} (Round a) => a -> Integer
     complement : {a} (Logic a) => a -> a
     curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
     demote : {val, rep} (Literal val rep) => rep
     drop : {front, back, a} (fin front) => [front + back]a -> [back]a
-    elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
-    error : {a, len} (fin len) => String len -> a
+    elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
+    error : {a, n} (fin n) => String n -> a
     False : Bit
     floor : {a} (Round a) => a -> Integer
     foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
@@ -186,8 +186,8 @@ Symbols
     tail : {n, a} [1 + n]a -> [n]a
     take : {front, back, a} (fin front) => [front + back]a -> [front]a
     toInteger : {a} (Integral a) => a -> Integer
-    trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
-    traceVal : {n, a} (fin n) => [n][8] -> a -> a
+    trace : {n, a, b} (fin n) => String n -> a -> b -> b
+    traceVal : {n, a} (fin n) => String n -> a -> a
     transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
     trunc : {a} (Round a) => a -> Integer
     uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
diff --git a/tests/regression/bvdiv.cry b/tests/regression/bvdiv.cry
new file mode 100644
index 00000000..717146d0
--- /dev/null
+++ b/tests/regression/bvdiv.cry
@@ -0,0 +1,70 @@
+// unsigned division properties
+
+bvdiv_euc : {n} (fin n) => [n] -> [n] -> Bit
+bvdiv_euc x y = y != 0 ==> (x/y)*y + x%y == x
+
+bvdiv_char : {n} (fin n) => [n] -> [n] -> Bit
+bvdiv_char x y = y != 0 ==> floor r == toInteger (x / y)
+  where
+    r = ratio (toInteger x) (toInteger y)
+
+bvdiv_mod : {n} (fin n) => [n] -> [n] -> Bit
+bvdiv_mod x y = y != 0 ==> (0 <= m /\ m < y)
+  where
+    m = x%y
+
+
+// some utility definitions
+
+sabs : {n} (fin n, n>=1) => [n] -> [n]
+sabs x = if x <=$ 0 then negate x else x
+
+toSignedInteger : {n} (fin n, n >=1 ) => [n] -> Integer
+toSignedInteger x = if x <=$ 0 then negate (toInteger (negate x)) else toInteger x
+
+minint : {n} (fin n, n >= 1) => [n]
+minint = 0b1 # zero
+
+maxint : {n} (fin n, n >= 1) => [n]
+maxint = ~minint
+
+
+// signed division properties
+
+bvsdiv_euc : {n} (fin n, n>=1) => [n] -> [n] -> Bit
+bvsdiv_euc x y = y != 0 ==> (x/$y)*y + x%$y == x
+
+bvsdiv_char : {n} (fin n, n>=1) => [n] -> [n] -> Bit
+bvsdiv_char x y = y != 0 ==> overflow \/ trunc r == toSignedInteger (x /$ y)
+  where
+    overflow = x == minint /\ y == (-1)
+    r = ratio (toSignedInteger x) (toSignedInteger y)
+
+bvsdiv_mod : {n} (fin n, n>=1) => [n] -> [n] -> Bit
+bvsdiv_mod x y = y != 0 ==> (0 <= m /\ m < sabs y)
+  where
+    m = sabs (x%$y)
+
+bvsdiv_mod_sign : {n} (fin n, n>=1) => [n] -> [n] -> Bit
+bvsdiv_mod_sign x y =
+  y != 0 ==>
+    if x >=$ 0 then x%$y >=$ 0 else x%$y <=$ 0
+
+bvsdiv_doc_properties : {n} (fin n, n>=1) => [n] -> [n] -> Bit
+bvsdiv_doc_properties x y =
+  y != 0 ==>
+    (x %$ y == x - (x /$ y) * y) /\
+    (x >=$ 0 ==> x%$y >=$ 0) /\
+    (x <=$ 0 ==> x%$y <=$ 0)
+
+// property instances to check
+
+property d1 = bvdiv_euc`{8}
+property c1 = bvdiv_char`{8}
+property m1 = bvdiv_mod`{8}
+
+property d2 = bvsdiv_euc`{8}
+property c2 = bvsdiv_char`{8}
+property m2 = bvsdiv_mod`{8}
+property m3 = bvsdiv_mod_sign`{8}
+property sdiv = bvsdiv_doc_properties`{8}
diff --git a/tests/regression/bvdiv.icry b/tests/regression/bvdiv.icry
new file mode 100644
index 00000000..d9ba6dfb
--- /dev/null
+++ b/tests/regression/bvdiv.icry
@@ -0,0 +1,2 @@
+:l bvdiv.cry
+:exhaust
diff --git a/tests/regression/bvdiv.icry.stdout b/tests/regression/bvdiv.icry.stdout
new file mode 100644
index 00000000..ae5c6a35
--- /dev/null
+++ b/tests/regression/bvdiv.icry.stdout
@@ -0,0 +1,27 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property d1 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property c1 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property m1 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property d2 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property c2 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property m2 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property m3 Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.
+property sdiv Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.