diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@
 a partial answer to one of its main issue which is scalability.
 
 *copilot-theorem* is a Copilot library aimed at checking automatically some safety
-properties on Copilot programs. It includes :
+properties on Copilot programs. It includes:
 
 * A general interface for *provers* and a *proof scheme* mechanism aimed at
   splitting the task of proving a complex property into checking a sequence of
@@ -26,12 +26,12 @@
 
 ### Installation instructions
 
-*copilot-theorem* needs the following dependencies to be installed :
+*copilot-theorem* needs the following dependencies to be installed:
 
 * The *copilot-core* and *copilot-language* Haskell libraries
-* The *Yices2* SMT-solver : `yices-smt2` must be in your `$PATH`
-* The *Z3* SMT-solver : `z3` must be in your `$PATH`
-* The *Kind2* model checker : `kind2` must be in your `$PATH`
+* The *Yices2* SMT-solver: `yices-smt2` must be in your `$PATH`
+* The *Z3* SMT-solver: `z3` must be in your `$PATH`
+* The *Kind2* model checker: `kind2` must be in your `$PATH`
 
 To build it, just clone this repository and use `cabal install`. You will find
 some examples in the `examples` folder, which can be built with `cabal install`
@@ -53,7 +53,7 @@
 boolean stream to a property name with the `prop` construct in the
 specification.
 
-For instance, here is a straightforward specification declaring one property :
+For instance, here is a straightforward specification declaring one property:
 
 ```haskell
 spec :: Spec
@@ -65,7 +65,7 @@
 
 Let's say we want to check that `gt0` holds. For this, we use the `prove ::
 Prover -> ProofScheme -> Spec -> IO ()` function exported by `Copilot.Theorem`.
-This function takes three arguments :
+This function takes three arguments:
 
 * The prover we want to use. For now, two provers are available, exported by
   the `Copilot.Theorem.Light` and `Copilot.Theorem.Kind2` module.
@@ -86,7 +86,7 @@
 
 The `Copilot.Theorem.Prover` defines a general interface for provers. Therefore,
 it is really easy to add a new prover by creating a new object of type
-`Prover`. The latter is defined like this :
+`Prover`. The latter is defined like this:
 
 ```haskell
 data Cex = Cex
@@ -120,13 +120,13 @@
 
 and checks if the assumptions logically entail the conclusion.
 
-Two provers are provided by default : `Light` and `Kind2`.
+Two provers are provided by default: `Light` and `Kind2`.
 
 #### The light prover
 
 The *light prover* is a really simple prover which uses the Yices SMT solver
 with the `QF_UFLIA` theory and is limited to prove *k-inductive* properties,
-that is properties such that there exists some *k* such that :
+that is properties such that there exists some *k* such that:
 
 * The property holds during the first *k* steps of the algorithm.
 * From the hypothesis the property has held during *k* consecutive steps, we
@@ -166,7 +166,7 @@
 * If `debugMode` is set to `True`, the SMTLib queries produced by the prover
   are displayed in the standard output.
 
-`Options` is an instance of the `Data.Default` typeclass :
+`Options` is an instance of the `Data.Default` typeclass:
 
 ```haskell
 instance Default Options where
@@ -202,7 +202,7 @@
 in the future. For instance, a *lazy* one such that C launches B only if A has
 returns *unknown* or *error*.
 
-As an example, the following prover is used in `Driver.hs` :
+As an example, the following prover is used in `Driver.hs`:
 
 ```haskell
 prover =
@@ -215,7 +215,7 @@
 
 ### Proof schemes
 
-Let's consider again this example :
+Let's consider again this example:
 
 ```haskell
 spec :: Spec
@@ -235,7 +235,7 @@
 assert "gt0" >> check "neq0"
 ```
 instead of just `check "neq0"`. A proof scheme is chain of primitives schemes
-glued by the `>>` operator. For now, the available primitives are :
+glued by the `>>` operator. For now, the available primitives are:
 
 * `check "prop"` checks whether or not a given property is true in the current
   context.
@@ -256,7 +256,7 @@
 `spec` and a proof scheme `scheme`. You can change the example being run just
 by changing one *import* directive in `Driver.hs`.
 
-These examples include :
+These examples include:
 
 * `Incr.hs` : a straightforward example in the style of the previous one.
 * `Grey.hs` : an example where two different implementations of a periodical
@@ -277,21 +277,21 @@
 set of slides. You can find some additional readings in the *References*
 section.
 
-### Architecture of copilot-kind
+### Architecture of copilot-theorem
 
 #### An overview of the proving process
 
 Each prover first translates the Copilot specification into an intermediate
 representation best suited for model checking. Two representations are
-available :
+available:
 
-* The **IL** format : a Copilot program is translated into a list of
+* The **IL** format: a Copilot program is translated into a list of
   quantifier-free equations over integer sequences, implicitly universally
   quantified by a free variable *n*. Each sequence roughly corresponds to a
   stream. This format is the one used in G. Hagen's thesis [4]. The *light
   prover* works with this format.
 
-* The **TransSys** format : a Copilot program is *flattened* and translated
+* The **TransSys** format: a Copilot program is *flattened* and translated
   into a *state transition system* [1]. Moreover, in order to keep some
   structure in this representation, the variables of this system are grouped by
   *nodes*, each node exporting and importing variables. The *Kind2 prover* uses
@@ -308,7 +308,7 @@
 
 ##### An example
 
-The following program :
+The following program:
 
 ```haskell
 spec = do
@@ -319,7 +319,7 @@
     fib = [1, 1] ++ (fib + drop 1 fib)
 ```
 
-can be translated into this IL specification :
+can be translated into this IL specification:
 
 ```
 SEQUENCES
@@ -336,7 +336,7 @@
     'pos' : s0[n] > 0
 ```
 
-or this modular transition system :
+or this modular transition system:
 
 ```
 NODE 's0' DEPENDS ON []
@@ -399,9 +399,9 @@
 #### The Light prover
 
 As said in the tutorial, the *light prover* is a simple tool implementing the
-basic *k-induction* algorithm [1]. The `Light` directory contains three files :
+basic *k-induction* algorithm [1]. The `Light` directory contains three files:
 
-* `Prover.hs` : the prover and the *k-induction* algorithm are implemented in
+* `Prover.hs`: the prover and the *k-induction* algorithm are implemented in
   this file.
 * `SMT.hs` contains some functions to interact with the Yices SMT provers.
 * `SMTLib.hs` is a set of functions to output SMTLib directives. It uses the
@@ -417,16 +417,16 @@
 Therefore, each stream definition directly gives us a recurrence equation and
 initial conditions for the associated sequence.
 
-The translation process mostly :
+The translation process mostly:
 
-* onverts the types and operators, using uninterpreted functions to handle
+* converts the types and operators, using uninterpreted functions to handle
   non-linear operators and external functions.
 * creates a sequence for each stream, local stream ands external stream.
 
 The reader is invited to use the *light prover* on the examples with `debugMode
 = true`, in order to have a look at the SMTLib code produced. For instance, if
 we check the property `"pos"` on the previous example involving the Fibonacci
-sequence, we get :
+sequence, we get:
 
 ```
 <step>  (set-logic QF_UFLIA)
@@ -468,7 +468,7 @@
 ##### Modular transition systems
 
 Let's look at the definition of a *modular transition systems*, in the
-`TransSys.Spec` module :
+`TransSys.Spec` module:
 
 ```haskell
 type NodeId = String
@@ -513,7 +513,7 @@
 is just a set of variables living in a local namespace and corresponding to the
 `Var` type. The `ExtVar` type is used to identify a variable in the global
 namespace by specifying both a node name and a variable. A node contains two
-types of variables :
+types of variables:
 
 * Some variables imported from other nodes. The structure `nodeImportedVars`
   binds each imported variable to its local name. The set of nodes from which a
@@ -534,12 +534,12 @@
 to *flatten* the copilot specification so the value of all streams at time *n*
 only depends on the values of all the streams at time *n - 1*, which is not the
 case in the `Fib` example shown earlier. This is done by a simple program
-transformation which turns this :
+transformation which turns this:
 
 ```haskell
 fib = [1, 1] ++ (fib + drop 1 fib)
 ```
-into this :
+into this:
 
 ```haskell
 fib0 = [1] ++ fib1
@@ -607,7 +607,7 @@
 
 which discards all the structure of a *modular transition system* and turns it
 into a *non-modular transition system* with only one node. In fact, when
-translating a copilot specification to a kind2 file, two styles are available :
+translating a copilot specification to a kind2 file, two styles are available:
 the `Kind2.toKind2` function takes a `Style` argument which can take the value
 `Inlined` or `Modular`. The only difference is that in the first case, a call
 to `removeCycles` is replaced by a call to `inline`.
@@ -615,7 +615,7 @@
 ### Limitations of copilot-theorem
 
 Now, we will discuss some limitations of the *copilot-theorem* tool. These
-limitations are organized in two categories : the limitations related to the
+limitations are organized in two categories: the limitations related to the
 Copilot language itself and its implementation, and the limitations related to
 the model-checking techniques we are using.
 
@@ -625,7 +625,7 @@
 informations about the structure of the original Copilot program. In fact, a
 stream is kept in the reified program only if it is recursively defined.
 Otherwise, all its occurences will be inlined. Moreover, let's look at the
-`intCounter` function defined in the example `Grey.hs` :
+`intCounter` function defined in the example `Grey.hs`:
 
 ```haskell
 intCounter :: Stream Bool -> Stream Word64
@@ -638,7 +638,7 @@
 If *n* counters are created with this function, the same code will be inlined
 *n* times and the structure of the original code will be lost.
 
-There are many problems with this :
+There are many problems with this:
 
 * It makes some optimizations of the model-checking based on a static analysis
   of the program more difficult (for instance *structural abstraction* - see
@@ -679,7 +679,7 @@
 
 ##### Limitations related to the SMT solvers
 
-The use of SMT solvers introduces two kind of limitations :
+The use of SMT solvers introduces two kind of limitations:
 
 1. We are limited by the computing power needed by the SMT solvers
 2. SMT solvers can't handle quantifiers efficiently
@@ -710,7 +710,7 @@
 why we have no other solution than replacing universal quantification by
 *bounded* universal quantification by assuming all the elements of the input
 stream are in the finite list `allowed` and using the function `forAllCst`
-defined in `Copilot.Kind.Lib` :
+defined in `Copilot.Kind.Lib`:
 
 ```haskell
 conj :: [Stream Bool] -> Stream Bool
@@ -730,7 +730,7 @@
 is hard to follow in our case because of
 
 * The difficulty to deal with universal quantification.
-* The lack of *true* functions in Copilot : the latter offers metaprogramming
+* The lack of *true* functions in Copilot: the latter offers metaprogramming
   facilities but no concept of functions like *Lustre* does with its *nodes*).
 * The inlining policy of the reification process. This point is related to the
   previous one.
@@ -824,7 +824,7 @@
 
 To be honest, I'm not sure producing a modular *Kind2* output is worth the
 complexity added. It's especially true at the time I write this in the sense
-that :
+that:
 
 * Each predicate introduced is used only one time (which is true because
   copilot doesn't handle functions or parametrized streams like Lustre does and
@@ -843,7 +843,7 @@
 
 ## References
 
-1. *An insight into An insight into SMT-based model checking techniques for
+1. *An insight into SMT-based model checking techniques for
    formal software verification of synchronous dataflow programs*, talk,
    Jonathan Laurent  (see the `doc` folder of this repository)
 
@@ -853,7 +853,7 @@
 3. *SMT-based Unbounded Model Checking with IC3 and Approximate Quantifier
    Elimination*, C. Sticksel, C. Tinelli
 
-4. *Verifying safety properties of Lustre programs : an SMT-based approach*,
+4. *Verifying safety properties of Lustre programs: an SMT-based approach*,
    PhD thesis, G. Hagen
 
 5. *Understanding IC3*, Aaron R. Bradley
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -6,7 +6,7 @@
   Some tools to prove properties on Copilot programs with k-induction model
   checking.
 
-version                   : 2.2.0
+version                   : 2.2.1
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : jonathan.laurent@ens.fr
@@ -27,8 +27,19 @@
                             -fno-warn-missing-signatures
                             -fcontext-stack=100
 
+                            -fpackage-trust
+                            -trust=array
+                            -trust=base
+                            -trust=containers
+                            -trust=copilot-core
+                            -trust=directory
+                            -trust=exceptions
+                            -trust=process
+                            -trust=random
+                            -trust=unix
+
   build-depends           : base >= 4.0 && < 5
-                          , copilot-core == 2.2.0
+                          , copilot-core == 2.2.1
                           , mtl
                           , containers
                           , pretty
@@ -40,7 +51,7 @@
                           , xml
                           , random
                           , transformers
-                          , smtlib2 >= 0.3
+                          , smtlib2 >= 0.3 && < 1.0
                           , ansi-terminal
 
   exposed-modules         : Copilot.Theorem
@@ -49,29 +60,29 @@
                           , Copilot.Theorem.Prover.SMT
                           , Copilot.Theorem.Prover.Z3
                           , Copilot.Theorem.Kind2.Prover
-                          
+
   other-modules           : Copilot.Theorem.Tactics
-                          
+
                           , Copilot.Theorem.IL
                           , Copilot.Theorem.IL.PrettyPrint
                           , Copilot.Theorem.IL.Spec
                           , Copilot.Theorem.IL.Translate
                           , Copilot.Theorem.IL.Transform
-                          
+
                           , Copilot.Theorem.Kind2.AST
                           , Copilot.Theorem.Kind2.Output
                           , Copilot.Theorem.Kind2.PrettyPrint
                           , Copilot.Theorem.Kind2.Translate
-                          
+
                           , Copilot.Theorem.Prover.SMTIO
                           , Copilot.Theorem.Prover.SMTLib
                           , Copilot.Theorem.Prover.TPTP
                           , Copilot.Theorem.Prover.Backend
-                          
+
                           , Copilot.Theorem.Misc.Error
                           , Copilot.Theorem.Misc.SExpr
                           , Copilot.Theorem.Misc.Utils
-                          
+
                           , Copilot.Theorem.TransSys
                           , Copilot.Theorem.TransSys.Cast
                           , Copilot.Theorem.TransSys.PrettyPrint
@@ -82,6 +93,3 @@
                           , Copilot.Theorem.TransSys.Invariants
                           , Copilot.Theorem.TransSys.Operators
                           , Copilot.Theorem.TransSys.Type
-                          
-
-  
diff --git a/src/Copilot/Theorem.hs b/src/Copilot/Theorem.hs
--- a/src/Copilot/Theorem.hs
+++ b/src/Copilot/Theorem.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem
   ( module X
   , Proof
diff --git a/src/Copilot/Theorem/IL.hs b/src/Copilot/Theorem/IL.hs
--- a/src/Copilot/Theorem/IL.hs
+++ b/src/Copilot/Theorem/IL.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.IL (module X) where
 
 import Copilot.Theorem.IL.Spec as X
diff --git a/src/Copilot/Theorem/IL/PrettyPrint.hs b/src/Copilot/Theorem/IL/PrettyPrint.hs
--- a/src/Copilot/Theorem/IL/PrettyPrint.hs
+++ b/src/Copilot/Theorem/IL/PrettyPrint.hs
@@ -1,6 +1,7 @@
 ---------------------------------------------------------------------------------
 
 {-# LANGUAGE NamedFieldPuns, GADTs #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.IL.PrettyPrint (prettyPrint, printConstraint) where
 
diff --git a/src/Copilot/Theorem/IL/Spec.hs b/src/Copilot/Theorem/IL/Spec.hs
--- a/src/Copilot/Theorem/IL/Spec.hs
+++ b/src/Copilot/Theorem/IL/Spec.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.IL.Spec
   ( Type (..)
diff --git a/src/Copilot/Theorem/IL/Transform.hs b/src/Copilot/Theorem/IL/Transform.hs
--- a/src/Copilot/Theorem/IL/Transform.hs
+++ b/src/Copilot/Theorem/IL/Transform.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.IL.Transform ( bsimpl ) where
 
diff --git a/src/Copilot/Theorem/IL/Translate.hs b/src/Copilot/Theorem/IL/Translate.hs
--- a/src/Copilot/Theorem/IL/Translate.hs
+++ b/src/Copilot/Theorem/IL/Translate.hs
@@ -2,8 +2,9 @@
 
 {-# LANGUAGE RankNTypes, NamedFieldPuns, ScopedTypeVariables, GADTs,
              LambdaCase #-}
+{-# LANGUAGE Safe #-}
 
-module Copilot.Theorem.IL.Translate ( translate ) where
+module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where
 
 import Copilot.Theorem.IL.Spec
 
@@ -11,7 +12,6 @@
 
 import qualified Data.Map.Strict as Map
 
-import Control.Applicative ((<$>), (<*))
 import Control.Monad.State
 
 import Data.Char
@@ -48,8 +48,14 @@
 -- | Translates a Copilot specification to an IL specification
 
 translate :: C.Spec -> IL
-translate (C.Spec {C.specStreams, C.specProperties}) = runTrans $ do
+translate = translate' False
 
+translateWithBounds :: C.Spec -> IL
+translateWithBounds = translate' True
+
+translate' :: Bool -> C.Spec -> IL
+translate' b (C.Spec {C.specStreams, C.specProperties}) = runTrans b $ do
+
   let modelInit = concatMap streamInit specStreams
 
   mainConstraints <- mapM streamRec specStreams
@@ -81,7 +87,9 @@
   C.Word64  -> bound' C.Word64
   _         -> return ()
   where bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()
-        bound' t = localConstraint (Op2 Bool And
+        bound' t = do
+          b <- addBounds <$> get
+          when b $ localConstraint (Op2 Bool And
             (Op2 Bool Le (trConst t minBound) s)
             (Op2 Bool Ge (trConst t maxBound) s))
 
@@ -181,6 +189,9 @@
   e2'   <- expr e2
   newMux cond' (trType t) e1' e2'
 
+expr (C.ExternStruct _ _ _ _) = undefined
+expr (C.GetField _ _ _ _) = undefined
+
 trConst :: C.Type a -> a -> Expr
 trConst t v = case t of
   C.Bool   -> ConstB v
@@ -245,7 +256,7 @@
   C.Pow t        -> (Pow, trType t)
   -- C.Logb t       ->
 
-  C.Eq t         -> (Eq, Bool)
+  C.Eq _         -> (Eq, Bool)
   -- C.Ne t         ->
 
   C.Le t         -> (Le, trType t)
@@ -281,6 +292,7 @@
   { localConstraints :: [Expr]
   , muxes            :: [(Expr, (Expr, Type, Expr, Expr))]
   , nextFresh        :: Integer
+  , addBounds        :: Bool
   }
 
 newMux :: Expr -> Type -> Expr -> Expr -> Trans Expr
@@ -317,8 +329,8 @@
 popLocalConstraints = liftM2 (++) (localConstraints <$> get) getMuxes
   <* (modify $ \st -> st {localConstraints = [], muxes = []})
 
-runTrans :: Trans a -> a
-runTrans m = evalState m $ TransST [] [] 0
+runTrans :: Bool -> Trans a -> a
+runTrans b m = evalState m $ TransST [] [] 0 b
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Theorem/Kind2.hs b/src/Copilot/Theorem/Kind2.hs
--- a/src/Copilot/Theorem/Kind2.hs
+++ b/src/Copilot/Theorem/Kind2.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.Kind2 (module X) where
 
 import Copilot.Theorem.Kind2.AST as X
diff --git a/src/Copilot/Theorem/Kind2/AST.hs b/src/Copilot/Theorem/Kind2/AST.hs
--- a/src/Copilot/Theorem/Kind2/AST.hs
+++ b/src/Copilot/Theorem/Kind2/AST.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.Kind2.AST where
 
 --------------------------------------------------------------------------------
diff --git a/src/Copilot/Theorem/Kind2/Output.hs b/src/Copilot/Theorem/Kind2/Output.hs
--- a/src/Copilot/Theorem/Kind2/Output.hs
+++ b/src/Copilot/Theorem/Kind2/Output.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Kind2.Output (parseOutput) where
 
diff --git a/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/src/Copilot/Theorem/Kind2/PrettyPrint.hs
--- a/src/Copilot/Theorem/Kind2/PrettyPrint.hs
+++ b/src/Copilot/Theorem/Kind2/PrettyPrint.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where
 
 import Copilot.Theorem.Misc.SExpr
diff --git a/src/Copilot/Theorem/Kind2/Prover.hs b/src/Copilot/Theorem/Kind2/Prover.hs
--- a/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/src/Copilot/Theorem/Kind2/Prover.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Theorem.Kind2.Prover
   ( module Data.Default
diff --git a/src/Copilot/Theorem/Kind2/Translate.hs b/src/Copilot/Theorem/Kind2/Translate.hs
--- a/src/Copilot/Theorem/Kind2/Translate.hs
+++ b/src/Copilot/Theorem/Kind2/Translate.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Kind2.Translate
   ( toKind2
diff --git a/src/Copilot/Theorem/Misc/Error.hs b/src/Copilot/Theorem/Misc/Error.hs
--- a/src/Copilot/Theorem/Misc/Error.hs
+++ b/src/Copilot/Theorem/Misc/Error.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.Misc.Error
   ( badUse
   , impossible
diff --git a/src/Copilot/Theorem/Misc/SExpr.hs b/src/Copilot/Theorem/Misc/SExpr.hs
--- a/src/Copilot/Theorem/Misc/SExpr.hs
+++ b/src/Copilot/Theorem/Misc/SExpr.hs
@@ -1,12 +1,12 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Misc.SExpr where
 
 import Text.ParserCombinators.Parsec
 import Text.PrettyPrint.HughesPJ as PP hiding (char, Str)
-import Control.Applicative hiding ((<|>), empty)
 
 import Control.Monad
 
diff --git a/src/Copilot/Theorem/Misc/Utils.hs b/src/Copilot/Theorem/Misc/Utils.hs
--- a/src/Copilot/Theorem/Misc/Utils.hs
+++ b/src/Copilot/Theorem/Misc/Utils.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.Misc.Utils
  ( isSublistOf, nub', nubBy', nubEq
  , openTempFile
diff --git a/src/Copilot/Theorem/Prove.hs b/src/Copilot/Theorem/Prove.hs
--- a/src/Copilot/Theorem/Prove.hs
+++ b/src/Copilot/Theorem/Prove.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Prove
   ( Output  (..)
@@ -12,13 +13,13 @@
   , Universal, Existential
   , check
   , prove
+  , combine
   ) where
 
 import qualified Copilot.Core as Core
 
 import Data.List (intercalate)
-import Control.Applicative (liftA2, Applicative(..))
-import Control.Monad (liftM, ap)
+import Control.Applicative (liftA2)
 import Control.Monad.Writer
 
 --------------------------------------------------------------------------------
@@ -64,12 +65,12 @@
   (<*>) = ap
 
 instance Monad (ProofScheme a) where
-  (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p -> p)
+  (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p' -> p')
   return a = Proof (return a)
 
 data Action where
-  Check  :: Prover   -> Action
-  Assume :: PropId   -> Action
+  Check  :: Prover -> Action
+  Assume :: PropId -> Action
   Admit  :: Action
 
 --------------------------------------------------------------------------------
@@ -109,9 +110,9 @@
               putStrLn $ propId ++ ": unknown " ++ "(" ++ intercalate ", " infos ++ ")"
               processActions context nextActions
 
-        Assume propId -> do
-          putStrLn $ propId ++ ": assumption"
-          processActions (propId : context) nextActions
+        Assume propId' -> do
+          putStrLn $ propId' ++ ": assumption"
+          processActions (propId' : context) nextActions
 
         Admit -> do
           putStrLn $ propId ++ ": admitted"
@@ -148,6 +149,7 @@
       closeProverR stR
   }
 
+combineOutputs :: [Char] -> [Char] -> Output -> Output -> Output
 combineOutputs nameL nameR (Output stL msgL) (Output stR msgR) =
   Output (combineSt stL stR) infos
 
diff --git a/src/Copilot/Theorem/Prover/Backend.hs b/src/Copilot/Theorem/Prover/Backend.hs
--- a/src/Copilot/Theorem/Prover/Backend.hs
+++ b/src/Copilot/Theorem/Prover/Backend.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where
 
diff --git a/src/Copilot/Theorem/Prover/SMT.hs b/src/Copilot/Theorem/Prover/SMT.hs
--- a/src/Copilot/Theorem/Prover/SMT.hs
+++ b/src/Copilot/Theorem/Prover/SMT.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Theorem.Prover.SMT
   ( module Data.Default
@@ -24,7 +25,6 @@
 import qualified Copilot.Theorem.Prover.SMTLib as SMTLib
 import qualified Copilot.Theorem.Prover.TPTP as TPTP
 
-import Control.Applicative ((<$>), (<*))
 import Control.Monad (msum, unless, mzero)
 import Control.Monad.State (StateT, runStateT, lift, get, modify)
 import Control.Monad.IO.Class (liftIO)
@@ -65,7 +65,7 @@
 onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
 onlySat opts backend = check P.Prover
   { P.proverName  = "OnlySat"
-  , P.startProver = return . ProofState opts backend Map.empty . translate
+  , P.startProver = return . ProofState opts backend Map.empty . translateWithBounds
   , P.askProver   = onlySat'
   , P.closeProver = const $ return ()
   }
@@ -73,7 +73,7 @@
 onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
 onlyValidity opts backend = check P.Prover
   { P.proverName  = "OnlyValidity"
-  , P.startProver = return . ProofState opts backend Map.empty . translate
+  , P.startProver = return . ProofState opts backend Map.empty . translateWithBounds
   , P.askProver   = onlyValidity'
   , P.closeProver = const $ return ()
   }
@@ -81,7 +81,7 @@
 induction :: SmtFormat a => Options -> Backend a -> Proof Universal
 induction opts backend = check P.Prover
   { P.proverName  = "Induction"
-  , P.startProver = return . ProofState opts backend Map.empty . translate
+  , P.startProver = return . ProofState opts backend Map.empty . translateWithBounds
   , P.askProver   = kInduction' 0 0
   , P.closeProver = const $ return ()
   }
@@ -89,7 +89,7 @@
 kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
 kInduction opts backend = check P.Prover
   { P.proverName  = "K-Induction"
-  , P.startProver = return . ProofState opts backend Map.empty . translate
+  , P.startProver = return . ProofState opts backend Map.empty . translateWithBounds
   , P.askProver   = kInduction' (startK opts) (maxK opts)
   , P.closeProver = const $ return ()
   }
diff --git a/src/Copilot/Theorem/Prover/SMTIO.hs b/src/Copilot/Theorem/Prover/SMTIO.hs
--- a/src/Copilot/Theorem/Prover/SMTIO.hs
+++ b/src/Copilot/Theorem/Prover/SMTIO.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Prover.SMTIO
   ( Solver
@@ -15,7 +16,6 @@
 import Control.Monad
 import Control.Monad.Trans
 import Control.Monad.Trans.Maybe
-import Control.Applicative ((<$>))
 import Data.Maybe
 import Data.Set ((\\), fromList, Set, union, empty, elems)
 
diff --git a/src/Copilot/Theorem/Prover/SMTLib.hs b/src/Copilot/Theorem/Prover/SMTLib.hs
--- a/src/Copilot/Theorem/Prover/SMTLib.hs
+++ b/src/Copilot/Theorem/Prover/SMTLib.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE GADTs, FlexibleInstances #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where
 
diff --git a/src/Copilot/Theorem/Prover/TPTP.hs b/src/Copilot/Theorem/Prover/TPTP.hs
--- a/src/Copilot/Theorem/Prover/TPTP.hs
+++ b/src/Copilot/Theorem/Prover/TPTP.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE GADTs, LambdaCase #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where
 
diff --git a/src/Copilot/Theorem/Prover/Z3.hs b/src/Copilot/Theorem/Prover/Z3.hs
--- a/src/Copilot/Theorem/Prover/Z3.hs
+++ b/src/Copilot/Theorem/Prover/Z3.hs
@@ -2,6 +2,7 @@
 
 {-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs,
     MultiParamTypeClasses, FlexibleContexts #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Theorem.Prover.Z3
   ( module Data.Default
@@ -15,13 +16,12 @@
 import Copilot.Theorem.Prove (Output (..), check, Proof, Universal, Existential)
 import qualified Copilot.Theorem.Prove as P
 
-import Control.Applicative ((<$>), (<*))
 import Control.Monad (msum, mzero, when, void, unless)
 import Control.Monad.State (StateT, runStateT, get, modify)
 import Control.Monad.Trans.Maybe (MaybeT (..))
 
 import Data.Word
-import Data.Unit
+import Data.Unit (Unit(..))
 import Data.Maybe (fromJust, fromMaybe)
 import Data.Default (Default(..))
 import Data.List (foldl')
@@ -120,13 +120,12 @@
 data SolverId = Base | Step
   deriving (Show, Ord, Eq)
 
-getModels :: [PropId] -> [PropId] -> ProofScript ([Expr], [Expr], [Expr], Bool)
+getModels :: [PropId] -> [PropId] -> ProofScript ([Expr], [Expr], [Expr], [Expr], Bool)
 getModels assumptionIds toCheckIds = do
   IL {modelInit, modelRec, properties, inductive} <- spec <$> get
   let (as, as')       = selectProps assumptionIds properties
       (as'', toCheck) = selectProps toCheckIds properties
-      modelRec'       = modelRec ++ as ++ as' ++ as''
-  return (modelInit, modelRec', toCheck, inductive)
+  return (as ++ as', modelInit, modelRec ++ as ++ as' ++ as'', toCheck, inductive)
 
 getSolver :: SolverId -> ProofScript Solver
 getSolver sid = do
@@ -231,11 +230,11 @@
 valid msg = return $ Output P.Valid [msg]
 
 kInduction' :: Word32 -> Word32 -> ProofState -> [PropId] -> [PropId] -> IO Output
-kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by k-induction failed"]) . fst)
+kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by " ++ proofKind (toInteger maxK) ++ " failed"]) . fst)
   <$> runPS (msum (map induction [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s
   where
     induction k = do
-      (modelInit, modelRec, toCheck, inductive) <- getModels as ps
+      (assumps, modelInit, modelRec, toCheck, inductive) <- getModels as ps
 
       let base    = [evalAt (Fixed i) m | m <- modelRec, i <- [0 .. k]]
           baseInv = [evalAt (Fixed k) m | m <- toCheck]
@@ -244,47 +243,56 @@
                     ++ [evalAt (_n_plus i) m | m <- toCheck, i <- [0 .. k]]
           stepInv = [evalAt (_n_plus $ k + 1) m | m <- toCheck]
 
-      entailment Base (modelInit ++ base) baseInv >>= \case
-        Sat     -> invalid $ "base case failed for " ++ proofKind k
+      entailment Base assumps [ConstB False] >>= \case
         Unknown -> unknown
-        Unsat   ->
-          if not inductive then valid ("proved without induction")
-          else entailment Step step stepInv >>= \case
-            Sat     -> unknown
-            Unknown -> unknown
-            Unsat   -> valid $ "proved with " ++ proofKind k
+        Unsat   -> invalid $ "inconsistent assumptions"
+        Sat     -> entailment Base (modelInit ++ base) baseInv >>= \case
+          Sat     -> invalid $ "base case failed for " ++ proofKind k
+          Unknown -> unknown
+          Unsat   ->
+            if not inductive then valid ("proved without induction")
+            else entailment Step step stepInv >>= \case
+              Sat     -> unknown
+              Unknown -> unknown
+              Unsat   -> valid $ "proved with " ++ proofKind k
 
 onlySat' :: ProofState -> [PropId] -> [PropId] -> IO Output
 onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s
   where
     script  = do
-      (modelInit, modelRec, toCheck, inductive) <- getModels as ps
+      (assumps, modelInit, modelRec, toCheck, inductive) <- getModels as ps
 
       let base    = map (evalAt (Fixed 0)) modelRec
           baseInv = map (evalAt (Fixed 0)) toCheck
 
-      if inductive
-        then unknown' "proposition requires induction to prove."
-        else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case
-          Unsat   -> invalid "prop not satisfiable"
-          Unknown -> unknown' "failed to find a satisfying model"
-          Sat     -> sat "prop is satisfiable"
+      entailment Base assumps [ConstB False] >>= \case
+        Unknown -> unknown
+        Unsat   -> invalid $ "inconsistent assumptions"
+        Sat     -> if inductive
+          then unknown' "proposition requires induction to prove."
+          else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case
+            Unsat   -> invalid "prop not satisfiable"
+            Unknown -> unknown' "failed to find a satisfying model"
+            Sat     -> sat "prop is satisfiable"
 
 onlyValidity' :: ProofState -> [PropId] -> [PropId] -> IO Output
 onlyValidity' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s
   where
     script  = do
-      (modelInit, modelRec, toCheck, inductive) <- getModels as ps
+      (assumps, modelInit, modelRec, toCheck, inductive) <- getModels as ps
 
       let base    = map (evalAt (Fixed 0)) modelRec
           baseInv = map (evalAt (Fixed 0)) toCheck
 
-      if inductive
-        then unknown' "proposition requires induction to prove."
-        else entailment Base (modelInit ++ base) baseInv >>= \case
-          Unsat   -> valid "proof by Z3"
-          Unknown -> unknown
-          Sat     -> invalid "Z3 found a counter-example."
+      entailment Base assumps [ConstB False] >>= \case
+        Unknown -> unknown
+        Unsat   -> invalid $ "inconsistent assumptions"
+        Sat     -> if inductive
+          then unknown' "proposition requires induction to prove."
+          else entailment Base (modelInit ++ base) baseInv >>= \case
+            Unsat   -> valid "proof by Z3"
+            Unknown -> unknown
+            Sat     -> invalid "Z3 found a counter-example."
 
 selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
 selectProps propIds properties =
@@ -306,6 +314,7 @@
   , ratVars  :: Map String (SMTExpr Rational)
   }
 
+noVars :: TransState
 noVars = TransState Map.empty Map.empty Map.empty Map.empty Map.empty Map.empty
 
 getBoolVar :: String -> Trans (SMTExpr Bool)
@@ -326,234 +335,163 @@
 getRatVar  :: String -> Trans (SMTExpr Rational)
 getRatVar  = getVar ratVars  (\v s -> s {ratVars  = v})
 
-getVar proj mod v = do
+getVar :: (Unit (SMTAnnotation t), SMTType t) => (TransState -> Map String (SMTExpr t)) -> (Map String (SMTExpr t) -> TransState -> TransState) -> String -> Trans (SMTExpr t)
+getVar proj upd v = do
   vs <- proj <$> get
   case Map.lookup v vs of
     Nothing -> do
       newVar <- lift $ varNamed v
-      modify $ mod $ Map.insert v newVar vs
+      modify $ upd $ Map.insert v newVar vs
       return newVar
     Just x -> return x
 
 transB :: Expr -> Trans (SMTExpr Bool)
 transB = \case
-  ConstB b -> return $ constant b
-
-  Ite _ c e1 e2   -> do
-    c' <- transB c
-    trans2B e1 e2 (ite c')
-
-  Op1 _ Not e     -> transB e >>=  return . not'
-
-  Op2 _ And e1 e2 -> do
-    e1' <- transB e1
-    e2' <- transB e2
-    return $ e1' .&&. e2'
-  Op2 _ Or e1 e2 -> do
-    e1' <- transB e1
-    e2' <- transB e2
-    return $ e1' .||. e2'
-
-  Op2 _ Eq e1 e2 -> case typeOf e1 of
-    Bool -> trans2B e1 e2 (.==.)
-    Real -> trans2R e1 e2 (.==.)
-    BV8  -> trans2BV8 e1 e2 (.==.)
-    BV16  -> trans2BV16 e1 e2 (.==.)
-    BV32  -> trans2BV32 e1 e2 (.==.)
-    BV64  -> trans2BV64 e1 e2 (.==.)
-    SBV8  -> trans2BV8 e1 e2 (.==.)
-    SBV16  -> trans2BV16 e1 e2 (.==.)
-    SBV32  -> trans2BV32 e1 e2 (.==.)
-    SBV64  -> trans2BV64 e1 e2 (.==.)
-
-  Op2 _ Le e1 e2 -> case typeOf e1 of
-    Real -> trans2R e1 e2 (.<=.)
-    BV8  -> trans2BV8 e1 e2 bvule
-    BV16  -> trans2BV16 e1 e2 bvule
-    BV32  -> trans2BV32 e1 e2 bvule
-    BV64  -> trans2BV64 e1 e2 bvule
-    SBV8  -> trans2BV8 e1 e2 bvsle
-    SBV16  -> trans2BV16 e1 e2 bvsle
-    SBV32  -> trans2BV32 e1 e2 bvsle
-    SBV64  -> trans2BV64 e1 e2 bvsle
-    _ -> undefined
-  Op2 _ Ge e1 e2 -> case typeOf e1 of
-    Real -> trans2R e1 e2 (.>=.)
-    BV8  -> trans2BV8 e1 e2 bvuge
-    BV16  -> trans2BV16 e1 e2 bvuge
-    BV32  -> trans2BV32 e1 e2 bvuge
-    BV64  -> trans2BV64 e1 e2 bvuge
-    SBV8  -> trans2BV8 e1 e2 bvsge
-    SBV16  -> trans2BV16 e1 e2 bvsge
-    SBV32  -> trans2BV32 e1 e2 bvsge
-    SBV64  -> trans2BV64 e1 e2 bvsge
-    _ -> undefined
-  Op2 _ Lt e1 e2 -> case typeOf e1 of
-    Real -> trans2R e1 e2 (.<.)
-    BV8  -> trans2BV8 e1 e2 bvult
-    BV16  -> trans2BV16 e1 e2 bvult
-    BV32  -> trans2BV32 e1 e2 bvult
-    BV64  -> trans2BV64 e1 e2 bvult
-    SBV8  -> trans2BV8 e1 e2 bvslt
-    SBV16  -> trans2BV16 e1 e2 bvslt
-    SBV32  -> trans2BV32 e1 e2 bvslt
-    SBV64  -> trans2BV64 e1 e2 bvslt
-    _ -> undefined
-  Op2 _ Gt e1 e2 -> case typeOf e1 of
-    Real -> trans2R e1 e2 (.>.)
-    BV8  -> trans2BV8 e1 e2 bvugt
-    BV16  -> trans2BV16 e1 e2 bvugt
-    BV32  -> trans2BV32 e1 e2 bvugt
-    BV64  -> trans2BV64 e1 e2 bvugt
-    SBV8  -> trans2BV8 e1 e2 bvsgt
-    SBV16  -> trans2BV16 e1 e2 bvsgt
-    SBV32  -> trans2BV32 e1 e2 bvsgt
-    SBV64  -> trans2BV64 e1 e2 bvsgt
-    _ -> undefined
-
-  SVal _ s i -> getBoolVar $ ncVar s i
-
-  e -> error $ "Encountered unhandled expression (Bool): " ++ show e
+  ConstB b           -> return $ constant b
+  Ite _ c e1 e2      -> ite <$> transB c <*> transB e1 <*> transB e2
+  Op1 _ Not e        -> not' <$> transB e
+  Op2 _ And e1 e2    -> (.&&.) <$> transB e1 <*> transB e2
+  Op2 _ Or e1 e2     -> (.||.) <$> transB e1 <*> transB e2
+  Op2 _ Eq e1 e2     -> case typeOf e1 of
+    Bool   -> (.==.) <$> transB e1    <*> transB e2
+    Real   -> (.==.) <$> transR e1    <*> transR e2
+    BV8    -> (.==.) <$> transBV8 e1  <*> transBV8 e2
+    BV16   -> (.==.) <$> transBV16 e1 <*> transBV16 e2
+    BV32   -> (.==.) <$> transBV32 e1 <*> transBV32 e2
+    BV64   -> (.==.) <$> transBV64 e1 <*> transBV64 e2
+    SBV8   -> (.==.) <$> transBV8 e1  <*> transBV8 e2
+    SBV16  -> (.==.) <$> transBV16 e1 <*> transBV16 e2
+    SBV32  -> (.==.) <$> transBV32 e1 <*> transBV32 e2
+    SBV64  -> (.==.) <$> transBV64 e1 <*> transBV64 e2
+  e@(Op2 _ Le e1 e2) -> case typeOf e1 of
+    Bool   -> error $ "Comparing Bools: " ++ show e
+    Real   -> (.<=.) <$> transR e1    <*> transR e2
+    BV8    -> bvule  <$> transBV8 e1  <*> transBV8 e2
+    BV16   -> bvule  <$> transBV16 e1 <*> transBV16 e2
+    BV32   -> bvule  <$> transBV32 e1 <*> transBV32 e2
+    BV64   -> bvule  <$> transBV64 e1 <*> transBV64 e2
+    SBV8   -> bvule  <$> transBV8 e1  <*> transBV8 e2
+    SBV16  -> bvule  <$> transBV16 e1 <*> transBV16 e2
+    SBV32  -> bvule  <$> transBV32 e1 <*> transBV32 e2
+    SBV64  -> bvule  <$> transBV64 e1 <*> transBV64 e2
+  e@(Op2 _ Ge e1 e2) -> case typeOf e1 of
+    Bool   -> error $ "Comparing Bools: " ++ show e
+    Real   -> (.>=.) <$> transR e1    <*> transR e2
+    BV8    -> bvuge  <$> transBV8 e1  <*> transBV8 e2
+    BV16   -> bvuge  <$> transBV16 e1 <*> transBV16 e2
+    BV32   -> bvuge  <$> transBV32 e1 <*> transBV32 e2
+    BV64   -> bvuge  <$> transBV64 e1 <*> transBV64 e2
+    SBV8   -> bvuge  <$> transBV8 e1  <*> transBV8 e2
+    SBV16  -> bvuge  <$> transBV16 e1 <*> transBV16 e2
+    SBV32  -> bvuge  <$> transBV32 e1 <*> transBV32 e2
+    SBV64  -> bvuge  <$> transBV64 e1 <*> transBV64 e2
+  e@(Op2 _ Lt e1 e2) -> case typeOf e1 of
+    Bool   -> error $ "Comparing Bools: " ++ show e
+    Real   -> (.<.) <$> transR e1    <*> transR e2
+    BV8    -> bvult <$> transBV8 e1  <*> transBV8 e2
+    BV16   -> bvult <$> transBV16 e1 <*> transBV16 e2
+    BV32   -> bvult <$> transBV32 e1 <*> transBV32 e2
+    BV64   -> bvult <$> transBV64 e1 <*> transBV64 e2
+    SBV8   -> bvult <$> transBV8 e1  <*> transBV8 e2
+    SBV16  -> bvult <$> transBV16 e1 <*> transBV16 e2
+    SBV32  -> bvult <$> transBV32 e1 <*> transBV32 e2
+    SBV64  -> bvult <$> transBV64 e1 <*> transBV64 e2
+  e@(Op2 _ Gt e1 e2) -> case typeOf e1 of
+    Bool   -> error $ "Comparing Bools: " ++ show e
+    Real   -> (.>.) <$> transR e1    <*> transR e2
+    BV8    -> bvugt <$> transBV8 e1  <*> transBV8 e2
+    BV16   -> bvugt <$> transBV16 e1 <*> transBV16 e2
+    BV32   -> bvugt <$> transBV32 e1 <*> transBV32 e2
+    BV64   -> bvugt <$> transBV64 e1 <*> transBV64 e2
+    SBV8   -> bvugt <$> transBV8 e1  <*> transBV8 e2
+    SBV16  -> bvugt <$> transBV16 e1 <*> transBV16 e2
+    SBV32  -> bvugt <$> transBV32 e1 <*> transBV32 e2
+    SBV64  -> bvugt <$> transBV64 e1 <*> transBV64 e2
+  SVal _ s i         -> getBoolVar $ ncVar s i
+  e                  -> error $ "Encountered unhandled expression (Bool): " ++ show e
 
+ncVar :: [Char] -> SeqIndex -> [Char]
 ncVar s (Fixed i) = s ++ "_" ++ show i
 ncVar s (Var   i) = s ++ "_n" ++ show i
 
 transR :: Expr -> Trans (SMTExpr Rational)
 transR = \case
-  ConstR n -> return $ constant $ toRational n
-  Ite _ c e1 e2   -> do
-    c' <- transB c
-    trans2R e1 e2 (ite c')
-
-  Op1 _ Neg e     -> transR e >>=  return . (app neg)
-  Op1 _ Abs e     -> transR e >>= return . (app SMTAbs)
+  ConstR n         -> return $ constant $ toRational n
+  Ite _ c e1 e2    -> ite <$> transB c <*> transR e1 <*> transR e2
 
-  Op2 _ Add e1 e2 -> trans2R e1 e2 $ \x y -> app plus [x, y]
-  Op2 _ Sub e1 e2 -> trans2R e1 e2 $ \x y -> app minus (x, y)
-  Op2 _ Mul e1 e2 -> trans2R e1 e2 $ \x y -> app mult [x, y]
-  Op2 _ Fdiv e1 e2 -> trans2R e1 e2 divide
+  Op1 _ Neg e      -> app neg <$> transR e
+  Op1 _ Abs e      -> app SMTAbs <$> transR e
 
-  Op2 _ Pow e1 e2 -> do
-    let pow = SMTBuiltIn "^" unit :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational
-    trans2R e1 e2 $ \x y -> app pow (x, y)
+  Op2 _ Add e1 e2  -> (\x y -> app plus [x, y]) <$> transR e1 <*> transR e2
+  Op2 _ Sub e1 e2  -> (\x y -> app minus (x, y)) <$> transR e1 <*> transR e2
+  Op2 _ Mul e1 e2  -> (\x y -> app mult [x, y]) <$> transR e1 <*> transR e2
+  Op2 _ Fdiv e1 e2 -> divide <$> transR e1 <*> transR e2
 
-  SVal _ s i -> getRatVar $ ncVar s i
+  Op2 _ Pow e1 e2  -> do
+    let pow = SMTBuiltIn "^" () :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational
+    (\x y -> app pow (x, y)) <$> transR e1 <*> transR e2
 
-  e -> error $ "Encountered unhandled expression (Rat): " ++ show e
+  SVal _ s i       -> getRatVar $ ncVar s i
+  e                -> error $ "Encountered unhandled expression (Rat): " ++ show e
 
 -- TODO(chathhorn): bleghh
 transBV8 :: Expr -> Trans (SMTExpr BV8)
 transBV8 = \case
-  ConstI _ n -> return $ constant $ BitVector n
-  Ite _ c e1 e2   -> do
-    c' <- transB c
-    trans2BV8 e1 e2 (ite c')
-
-  Op1 _ Abs e     -> transBV8 e >>= return . abs
-  Op1 _ Neg e     -> transBV8 e >>= return . negate
-  Op2 _ Add e1 e2 -> trans2BV8 e1 e2 (+)
-  Op2 _ Sub e1 e2 -> trans2BV8 e1 e2 (-)
-  Op2 _ Mul e1 e2 -> trans2BV8 e1 e2 (*)
-  SVal _ s i -> getBV8Var $ ncVar s i
-
-  e -> error $ "Encountered unhandled expression (BV8): " ++ show e
+  ConstI _ n      -> return $ constant $ BitVector n
+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV8 e1 <*> transBV8 e2
+  Op1 _ Abs e     -> abs <$> transBV8 e
+  Op1 _ Neg e     -> negate <$> transBV8 e
+  Op2 _ Add e1 e2 -> (+) <$> transBV8 e1 <*> transBV8 e2
+  Op2 _ Sub e1 e2 -> (-) <$> transBV8 e1 <*> transBV8 e2
+  Op2 _ Mul e1 e2 -> (*) <$> transBV8 e1 <*> transBV8 e2
+  SVal _ s i      -> getBV8Var $ ncVar s i
+  e               -> error $ "Encountered unhandled expression (BV8): " ++ show e
 
 transBV16 :: Expr -> Trans (SMTExpr BV16)
 transBV16 = \case
-  ConstI _ n -> return $ constant $ BitVector n
-  Ite _ c e1 e2   -> do
-    c' <- transB c
-    trans2BV16 e1 e2 (ite c')
-
-  Op1 _ Abs e     -> transBV16 e >>= return . abs
-  Op1 _ Neg e     -> transBV16 e >>= return . negate
-  Op2 _ Add e1 e2 -> trans2BV16 e1 e2 (+)
-  Op2 _ Sub e1 e2 -> trans2BV16 e1 e2 (-)
-  Op2 _ Mul e1 e2 -> trans2BV16 e1 e2 (*)
-  SVal _ s i -> getBV16Var $ ncVar s i
-
-  e -> error $ "Encountered unhandled expression (BV16): " ++ show e
+  ConstI _ n      -> return $ constant $ BitVector n
+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV16 e1 <*> transBV16 e2
+  Op1 _ Abs e     -> abs <$> transBV16 e
+  Op1 _ Neg e     -> negate <$> transBV16 e
+  Op2 _ Add e1 e2 -> (+) <$> transBV16 e1 <*> transBV16 e2
+  Op2 _ Sub e1 e2 -> (-) <$> transBV16 e1 <*> transBV16 e2
+  Op2 _ Mul e1 e2 -> (*) <$> transBV16 e1 <*> transBV16 e2
+  SVal _ s i      -> getBV16Var $ ncVar s i
+  e               -> error $ "Encountered unhandled expression (BV16): " ++ show e
 
 transBV32 :: Expr -> Trans (SMTExpr BV32)
 transBV32 = \case
-  ConstI _ n -> return $ constant $ BitVector n
-  Ite _ c e1 e2   -> do
-    c' <- transB c
-    trans2BV32 e1 e2 (ite c')
-
-  Op1 _ Abs e     -> transBV32 e >>= return . abs
-  Op1 _ Neg e     -> transBV32 e >>= return . negate
-  Op2 _ Add e1 e2 -> trans2BV32 e1 e2 (+)
-  Op2 _ Sub e1 e2 -> trans2BV32 e1 e2 (-)
-  Op2 _ Mul e1 e2 -> trans2BV32 e1 e2 (*)
-  SVal _ s i -> getBV32Var $ ncVar s i
-
-  e -> error $ "Encountered unhandled expression (BV32): " ++ show e
+  ConstI _ n      -> return $ constant $ BitVector n
+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV32 e1 <*> transBV32 e2
+  Op1 _ Abs e     -> abs <$> transBV32 e
+  Op1 _ Neg e     -> negate <$> transBV32 e
+  Op2 _ Add e1 e2 -> (+) <$> transBV32 e1 <*> transBV32 e2
+  Op2 _ Sub e1 e2 -> (-) <$> transBV32 e1 <*> transBV32 e2
+  Op2 _ Mul e1 e2 -> (*) <$> transBV32 e1 <*> transBV32 e2
+  SVal _ s i      -> getBV32Var $ ncVar s i
+  e               -> error $ "Encountered unhandled expression (BV32): " ++ show e
 
 transBV64 :: Expr -> Trans (SMTExpr BV64)
 transBV64 = \case
-  ConstI _ n -> return $ constant $ BitVector n
-  Ite _ c e1 e2   -> do
-    c' <- transB c
-    trans2BV64 e1 e2 (ite c')
-
-  Op1 _ Abs e     -> transBV64 e >>= return . abs
-  Op1 _ Neg e     -> transBV64 e >>= return . negate
-  Op2 _ Add e1 e2 -> trans2BV64 e1 e2 (+)
-  Op2 _ Sub e1 e2 -> trans2BV64 e1 e2 (-)
-  Op2 _ Mul e1 e2 -> trans2BV64 e1 e2 (*)
-  SVal _ s i -> getBV64Var $ ncVar s i
-
-  e -> error $ "Encountered unhandled expression (BV64): " ++ show e
-
-trans2BV8 :: Expr -> Expr -> (SMTExpr BV8 -> SMTExpr BV8 -> SMTExpr a) -> Trans (SMTExpr a)
-trans2BV8 e1 e2 f = do
-  e1' <- transBV8 e1
-  e2' <- transBV8 e2
-  return $ f e1' e2'
-
-trans2BV16 :: Expr -> Expr -> (SMTExpr BV16 -> SMTExpr BV16 -> SMTExpr a) -> Trans (SMTExpr a)
-trans2BV16 e1 e2 f = do
-  e1' <- transBV16 e1
-  e2' <- transBV16 e2
-  return $ f e1' e2'
-
-trans2BV32 :: Expr -> Expr -> (SMTExpr BV32 -> SMTExpr BV32 -> SMTExpr a) -> Trans (SMTExpr a)
-trans2BV32 e1 e2 f = do
-  e1' <- transBV32 e1
-  e2' <- transBV32 e2
-  return $ f e1' e2'
-
-trans2BV64 :: Expr -> Expr -> (SMTExpr BV64 -> SMTExpr BV64 -> SMTExpr a) -> Trans (SMTExpr a)
-trans2BV64 e1 e2 f = do
-  e1' <- transBV64 e1
-  e2' <- transBV64 e2
-  return $ f e1' e2'
-
-trans2R :: Expr -> Expr -> (SMTExpr Rational -> SMTExpr Rational -> SMTExpr a) -> Trans (SMTExpr a)
-trans2R e1 e2 f = do
-  e1' <- transR e1
-  e2' <- transR e2
-  return $ f e1' e2'
-
-trans2B :: Expr -> Expr -> (SMTExpr Bool -> SMTExpr Bool -> SMTExpr a) -> Trans (SMTExpr a)
-trans2B e1 e2 f = do
-  e1' <- transB e1
-  e2' <- transB e2
-  return $ f e1' e2'
+  ConstI _ n      -> return $ constant $ BitVector n
+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV64 e1 <*> transBV64 e2
+  Op1 _ Abs e     -> abs <$> transBV64 e
+  Op1 _ Neg e     -> negate <$> transBV64 e
+  Op2 _ Add e1 e2 -> (+) <$> transBV64 e1 <*> transBV64 e2
+  Op2 _ Sub e1 e2 -> (-) <$> transBV64 e1 <*> transBV64 e2
+  Op2 _ Mul e1 e2 -> (*) <$> transBV64 e1 <*> transBV64 e2
+  SVal _ s i      -> getBV64Var $ ncVar s i
+  e               -> error $ "Encountered unhandled expression (BV64): " ++ show e
 
 -----------------------------------------------------
 -- Debug stuff from the the smtlib2 library github --
 -----------------------------------------------------
 
-debugBackend :: Bool -> b -> DebugBackend b
-debugBackend mute b = DebugBackend b stderr (Just 0) Nothing True mute
-
 namedDebugBackend :: String -> Bool -> b -> DebugBackend b
 namedDebugBackend name mute b = DebugBackend b stderr (Just 0) (Just name) True mute
 
 data DebugBackend b = DebugBackend
-  { debugBackend' :: b
+  { debugBackend  :: b
   , debugHandle   :: Handle
   , debugLines    :: Maybe Integer
   , debugPrefix   :: Maybe String
@@ -562,12 +500,12 @@
   }
 
 instance (SMTBackend b m,MonadIO m) => SMTBackend (DebugBackend b) m where
-  smtGetNames b = smtGetNames (debugBackend' b)
-  smtNextName b = smtNextName (debugBackend' b)
+  smtGetNames b = smtGetNames (debugBackend b)
+  smtNextName b = smtNextName (debugBackend b)
   smtHandle b req = do
-    getName <- smtGetNames (debugBackend' b)
-    nxtName <- smtNextName (debugBackend' b)
-    (dts,b1) <- smtHandle (debugBackend' b) SMTDeclaredDataTypes
+    getName <- smtGetNames (debugBackend b)
+    nxtName <- smtNextName (debugBackend b)
+    (dts,b1) <- smtHandle (debugBackend b) SMTDeclaredDataTypes
     let rendering = renderSMTRequest nxtName getName dts req
     case debugPrefix b of
       Nothing -> return ()
@@ -603,6 +541,6 @@
         when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Blue]
         liftIO $ unless (mute b) $ hPutStrLn (debugHandle b) str
     when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset]
-    return (resp,b { debugBackend' = b2 , debugLines = nline })
+    return (resp,b { debugBackend = b2 , debugLines = nline })
 
 
diff --git a/src/Copilot/Theorem/Tactics.hs b/src/Copilot/Theorem/Tactics.hs
--- a/src/Copilot/Theorem/Tactics.hs
+++ b/src/Copilot/Theorem/Tactics.hs
@@ -1,10 +1,11 @@
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.Tactics
   ( instantiate, assume, admit
   ) where
 
 import Copilot.Theorem.Prove
 
-import Data.Word
 import Control.Monad.Writer
 
 instantiate :: Proof Universal -> Proof Existential
diff --git a/src/Copilot/Theorem/TransSys.hs b/src/Copilot/Theorem/TransSys.hs
--- a/src/Copilot/Theorem/TransSys.hs
+++ b/src/Copilot/Theorem/TransSys.hs
@@ -1,5 +1,7 @@
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE Safe #-}
+
 module Copilot.Theorem.TransSys (module X) where
 
 import Copilot.Theorem.TransSys.Spec as X
diff --git a/src/Copilot/Theorem/TransSys/Cast.hs b/src/Copilot/Theorem/TransSys/Cast.hs
--- a/src/Copilot/Theorem/TransSys/Cast.hs
+++ b/src/Copilot/Theorem/TransSys/Cast.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Cast
   ( Dyn
diff --git a/src/Copilot/Theorem/TransSys/Invariants.hs b/src/Copilot/Theorem/TransSys/Invariants.hs
--- a/src/Copilot/Theorem/TransSys/Invariants.hs
+++ b/src/Copilot/Theorem/TransSys/Invariants.hs
@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -O0 #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Invariants
   ( HasInvariants (..)
diff --git a/src/Copilot/Theorem/TransSys/Operators.hs b/src/Copilot/Theorem/TransSys/Operators.hs
--- a/src/Copilot/Theorem/TransSys/Operators.hs
+++ b/src/Copilot/Theorem/TransSys/Operators.hs
@@ -2,6 +2,7 @@
 
 {-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables,
              RankNTypes #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Operators where
 
@@ -10,8 +11,6 @@
 import Copilot.Theorem.TransSys.Type
 
 import Copilot.Theorem.Misc.Error as Err
-
-import Control.Applicative ((<$>))
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/src/Copilot/Theorem/TransSys/PrettyPrint.hs
--- a/src/Copilot/Theorem/TransSys/PrettyPrint.hs
+++ b/src/Copilot/Theorem/TransSys/PrettyPrint.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE NamedFieldPuns, GADTs #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where
 
diff --git a/src/Copilot/Theorem/TransSys/Renaming.hs b/src/Copilot/Theorem/TransSys/Renaming.hs
--- a/src/Copilot/Theorem/TransSys/Renaming.hs
+++ b/src/Copilot/Theorem/TransSys/Renaming.hs
@@ -1,6 +1,6 @@
 --------------------------------------------------------------------------------
 
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Renaming
   ( Renaming
@@ -14,7 +14,6 @@
 import Copilot.Theorem.TransSys.Spec
 
 import Control.Monad.State.Lazy
-import Control.Applicative
 
 import Data.Maybe (fromMaybe)
 import Data.Map (Map)
@@ -26,8 +25,7 @@
 
 --------------------------------------------------------------------------------
 
-newtype Renaming a = Renaming (State RenamingST a)
-                     deriving (Applicative, Monad, Functor)
+type Renaming = State RenamingST
 
 data RenamingST = RenamingST
   { _reservedNames :: Set Var
@@ -36,14 +34,12 @@
 --------------------------------------------------------------------------------
 
 addReservedName :: Var -> Renaming ()
-addReservedName v =
-  Renaming $ modify $ \st ->
+addReservedName v = modify $ \st ->
     st {_reservedNames = Set.insert v (_reservedNames st)}
 
-
 getFreshName :: [Var] -> Renaming Var
 getFreshName vs = do
-  usedNames <- _reservedNames <$> Renaming get
+  usedNames <- _reservedNames <$> get
   let varAppend (Var s) = Var $ s ++ "_"
       applicants = vs ++ List.iterate varAppend (head vs)
       v = case dropWhile (`member` usedNames) applicants of
@@ -53,20 +49,19 @@
   return v
 
 rename :: NodeId -> Var -> Var -> Renaming ()
-rename n v v' =
-  Renaming $ modify $ \st ->
+rename n v v' = modify $ \st ->
     st {_renaming = Map.insert (ExtVar n v) v' (_renaming st)}
 
 getRenamingF :: Renaming (ExtVar -> Var)
 getRenamingF = do
-  mapping <- _renaming <$> Renaming get
+  mapping <- _renaming <$> get
   return $ \extv -> fromMaybe (extVarLocalPart extv) (Map.lookup extv mapping)
 
 runRenaming :: Renaming a -> (a, ExtVar -> Var)
 runRenaming m =
   evalState st' (RenamingST Set.empty Map.empty)
   where
-    Renaming st' = do
+    st' = do
       r <- m
       f <- getRenamingF
       return (r, f)
diff --git a/src/Copilot/Theorem/TransSys/Spec.hs b/src/Copilot/Theorem/TransSys/Spec.hs
--- a/src/Copilot/Theorem/TransSys/Spec.hs
+++ b/src/Copilot/Theorem/TransSys/Spec.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Spec
   ( module Copilot.Theorem.TransSys.Operators
@@ -32,7 +33,7 @@
 import Control.Monad (foldM, guard)
 
 import Data.Maybe
-import Data.Monoid (Monoid, (<>), mempty, mconcat)
+import Data.Monoid ((<>))
 import Data.Map (Map)
 import Data.Set (Set, isSubsetOf, member)
 import Data.Bimap (Bimap)
diff --git a/src/Copilot/Theorem/TransSys/Transform.hs b/src/Copilot/Theorem/TransSys/Transform.hs
--- a/src/Copilot/Theorem/TransSys/Transform.hs
+++ b/src/Copilot/Theorem/TransSys/Transform.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Transform
   ( mergeNodes
diff --git a/src/Copilot/Theorem/TransSys/Translate.hs b/src/Copilot/Theorem/TransSys/Translate.hs
--- a/src/Copilot/Theorem/TransSys/Translate.hs
+++ b/src/Copilot/Theorem/TransSys/Translate.hs
@@ -2,6 +2,7 @@
 
 {-# LANGUAGE RankNTypes, NamedFieldPuns, ViewPatterns,
              ScopedTypeVariables, GADTs, FlexibleContexts #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Translate ( translate ) where
 
@@ -9,7 +10,6 @@
 import Copilot.Theorem.TransSys.Cast
 import Copilot.Theorem.Misc.Utils
 
-import Control.Applicative ((<$>))
 import Control.Monad.State.Lazy
 
 import Data.Char (isNumber)
@@ -203,9 +203,13 @@
     notHandled (UnhandledOp2 _opName _ta _tb _tc) =
       newUnconstrainedVar t
 
-expr t (C.ExternFun _ta _name _args _ _mtag) = newUnconstrainedVar t
+expr t (C.ExternFun _ _ _ _ _) = newUnconstrainedVar t
 
-expr t (C.ExternArray _ _tb _name _ _ind _ _) = newUnconstrainedVar t
+expr t (C.ExternArray _ _ _ _ _ _ _) = newUnconstrainedVar t
+
+expr t (C.ExternStruct _ _ _ _) = newUnconstrainedVar t
+
+expr t (C.GetField _ _ _ _) = undefined
 
 newUnconstrainedVar :: Type t -> Trans (Expr t)
 newUnconstrainedVar t = do
diff --git a/src/Copilot/Theorem/TransSys/Type.hs b/src/Copilot/Theorem/TransSys/Type.hs
--- a/src/Copilot/Theorem/TransSys/Type.hs
+++ b/src/Copilot/Theorem/TransSys/Type.hs
@@ -1,6 +1,7 @@
 --------------------------------------------------------------------------------
 
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
+{-# LANGUAGE Safe #-}
 
 module Copilot.Theorem.TransSys.Type
   ( Type (..)