diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,7 @@
+2022-05-06
+        * Version bump (3.9). (#320)
+        * Compliance with style guide (partial). (#316)
+
 2022-03-07
         * Version bump (3.8). (#298)
         * Mark package as uncurated to avoid modification. (#288)
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -14,7 +14,7 @@
   <https://copilot-language.github.io>.
 
 
-version                   : 3.8
+version                   : 3.9
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -74,7 +74,7 @@
                           , xml           >= 1.3 && < 1.4
                           , what4         >= 1.1 && < 1.3
 
-                          , copilot-core  >= 3.8 && < 3.9
+                          , copilot-core  >= 3.9 && < 3.10
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Highly automated proof techniques are a necessary step for the widespread
@@ -22,5 +20,3 @@
 
 import Copilot.Theorem.Tactics as X
 import Copilot.Theorem.Prove
-
---------------------------------------------------------------------------------
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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Each prover first translates the Copilot specification into an
@@ -16,5 +14,3 @@
 import Copilot.Theorem.IL.Translate as X
 import Copilot.Theorem.IL.Transform as X
 import Copilot.Theorem.IL.PrettyPrint 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,7 +1,6 @@
----------------------------------------------------------------------------------
-
-{-# LANGUAGE NamedFieldPuns, GADTs #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE Safe           #-}
 
 -- | This module implements a pretty printer for the IL format, an intermediate
 -- representation used in copilot-theorem to facilitate model checking.
@@ -13,8 +12,6 @@
 
 import Prelude hiding ((<>))
 
---------------------------------------------------------------------------------
-
 -- | Pretty print an IL specification.
 prettyPrint :: IL -> String
 prettyPrint = render . ppSpec
@@ -87,5 +84,3 @@
 
 ppOp2 :: Op2 -> Doc
 ppOp2 = text . show
-
---------------------------------------------------------------------------------
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,7 +1,7 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE LambdaCase                #-}
+{-# LANGUAGE Safe                      #-}
 
 -- | This module implements the specification language for the IL format, an
 -- intermediate representation used in copilot-theorem to facilitate model
@@ -35,8 +35,6 @@
 import Data.Map (Map)
 import Data.Function (on)
 
---------------------------------------------------------------------------------
-
 -- | Identifier of a sequence.
 type SeqId    =  String
 
@@ -77,8 +75,6 @@
   | FunApp Type String [Expr]   -- ^ Function application.
   deriving (Eq, Ord, Show)
 
---------------------------------------------------------------------------------
-
 -- | A description of a variable (or function) together with its type.
 data VarDescr = VarDescr
   { varName :: String
@@ -92,8 +88,6 @@
 instance Ord VarDescr where
   compare = compare `on` varName
 
---------------------------------------------------------------------------------
-
 -- | Identifier for a property.
 type PropId = String
 
@@ -111,8 +105,6 @@
   , inductive   :: Bool
   }
 
---------------------------------------------------------------------------------
-
 -- | Unary operators.
 data Op1 = Not | Neg | Abs | Exp | Sqrt | Log | Sin | Tan | Cos | Asin | Atan
          | Acos | Sinh | Tanh | Cosh | Asinh | Atanh | Acosh
@@ -122,8 +114,6 @@
 data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow
          deriving (Eq, Ord)
 
--------------------------------------------------------------------------------
-
 instance Show Op1 where
   show op = case op of
     Neg   -> "-"
@@ -167,8 +157,6 @@
     Lt   -> "<"
     Gt   -> ">"
 
--------------------------------------------------------------------------------
-
 -- | Return the type of an expression.
 typeOf :: Expr -> Type
 typeOf e = case e of
@@ -202,5 +190,3 @@
 evalAt _ e@(SVal _ _ (Fixed _)) = e
 evalAt (Fixed n) (SVal t s (Var d)) = SVal t s (Fixed $ n + d)
 evalAt (Var   k) (SVal t s (Var d)) = SVal t s (Var   $ k + d)
-
---------------------------------------------------------------------------------
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,5 +1,5 @@
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe       #-}
 
 -- | Simplify IL expressions by partly evaluating operations on booleans.
 module Copilot.Theorem.IL.Transform ( bsimpl ) where
@@ -45,4 +45,3 @@
       FunApp t f args             -> FunApp t f (map bsimpl' args)
 
       e                           -> e
-
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
@@ -1,8 +1,9 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE RankNTypes, NamedFieldPuns, ScopedTypeVariables, GADTs,
-             LambdaCase #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NamedFieldPuns      #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE Safe                #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 -- | Translate Copilot specifications into IL specifications.
 module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where
@@ -24,8 +25,6 @@
 
 import Data.Typeable (Typeable)
 
---------------------------------------------------------------------------------
-
 -- 'nc' stands for naming convention.
 ncSeq :: C.Id -> SeqId
 ncSeq = printf "s%d"
@@ -43,8 +42,6 @@
 ncMux :: Integer -> SeqId
 ncMux n = "mux" ++ show n
 
---------------------------------------------------------------------------------
-
 -- | Translate a Copilot specification to an IL specification.
 translate :: C.Spec -> IL
 translate = translate' False
@@ -88,22 +85,24 @@
   C.Word32  -> bound' C.Word32
   C.Word64  -> bound' C.Word64
   _         -> return ()
-  where bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()
-        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))
+  where
+    bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()
+    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))
 
 streamInit :: C.Stream -> [Expr]
 streamInit (C.Stream { C.streamId       = id
                      , C.streamBuffer   = b :: [val]
                      , C.streamExprType = t }) =
   zipWith initConstraint [0..] b
-  where initConstraint :: Integer -> val -> Expr
-        initConstraint p v = Op2 Bool Eq
-          (SVal (trType t) (ncSeq id) (Fixed p))
-          $ trConst t v
+  where
+    initConstraint :: Integer -> val -> Expr
+    initConstraint p v = Op2 Bool Eq
+      (SVal (trType t) (ncSeq id) (Fixed p))
+      $ trConst t v
 
 streamRec :: C.Stream -> Trans Expr
 streamRec (C.Stream { C.streamId       = id
@@ -116,8 +115,6 @@
   e' <- expr e
   return $ Op2 Bool Eq s e'
 
---------------------------------------------------------------------------------
-
 expr :: Typeable a => C.Expr a -> Trans Expr
 
 expr (C.Const t v) = return $ trConst t v
@@ -134,7 +131,8 @@
 expr (C.Var t name) = return $ SVal (trType t) (ncLocal name) _n_
 
 expr (C.ExternVar t name _) = bound s t >> return s
-  where s = SVal (trType t) (ncExternVar name) _n_
+  where
+    s = SVal (trType t) (ncExternVar name) _n_
 
 expr (C.Op1 (C.Sign ta) e) = case ta of
   C.Int8   -> trSign ta e
@@ -144,15 +142,16 @@
   C.Float  -> trSign ta e
   C.Double -> trSign ta e
   _        -> expr $ C.Const ta 1
-  where trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr
-        trSign ta e =
-          expr (C.Op3 (C.Mux ta)
-            (C.Op2 (C.Lt ta) e (C.Const ta 0))
-            (C.Const ta (-1))
-            (C.Op3 (C.Mux ta)
-              (C.Op2 (C.Gt ta) e (C.Const ta 0))
-              (C.Const ta 1)
-              (C.Const ta 0)))
+  where
+    trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr
+    trSign ta e =
+      expr (C.Op3 (C.Mux ta)
+        (C.Op2 (C.Lt ta) e (C.Const ta 0))
+        (C.Const ta (-1))
+        (C.Op3 (C.Mux ta)
+          (C.Op2 (C.Gt ta) e (C.Const ta 0))
+          (C.Const ta 1)
+          (C.Const ta 0)))
 expr (C.Op1 (C.Sqrt _) e) = do
   e' <- expr e
   return $ Op2 Real Pow e' (ConstR 0.5)
@@ -160,19 +159,22 @@
 expr (C.Op1 op e) = do
   e' <- expr e
   return $ Op1 t' op' e'
-  where (op', t') = trOp1 op
+  where
+    (op', t') = trOp1 op
 
 expr (C.Op2 (C.Ne t) e1 e2) = do
   e1' <- expr e1
   e2' <- expr e2
   return $ Op1 Bool Not (Op2 t' Eq e1' e2')
-  where t' = trType t
+  where
+    t' = trType t
 
 expr (C.Op2 op e1 e2) = do
   e1' <- expr e1
   e2' <- expr e2
   return $ Op2 t' op' e1' e2'
-  where (op', t') = trOp2 op
+  where
+    (op', t') = trOp2 op
 
 expr (C.Op3 (C.Mux t) cond e1 e2) = do
   cond' <- expr cond
@@ -193,14 +195,15 @@
   t@C.Word16 -> negifyI v (trType t)
   t@C.Word32 -> negifyI v (trType t)
   t@C.Word64 -> negifyI v (trType t)
-  where negifyR :: Double -> Expr
-        negifyR v
-          | v >= 0    = ConstR v
-          | otherwise = Op1 Real Neg $ ConstR $ negate $ v
-        negifyI :: Integral a => a -> Type -> Expr
-        negifyI v t
-          | v >= 0    = ConstI t $ toInteger v
-          | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v
+  where
+    negifyR :: Double -> Expr
+    negifyR v
+      | v >= 0    = ConstR v
+      | otherwise = Op1 Real Neg $ ConstR $ negate $ v
+    negifyI :: Integral a => a -> Type -> Expr
+    negifyI v t
+      | v >= 0    = ConstI t $ toInteger v
+      | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v
 
 trOp1 :: C.Op1 a b -> (Op1, Type)
 trOp1 = \case
@@ -225,7 +228,7 @@
   C.Acosh t -> (Acosh, trType t)
   -- C.BwNot t ->
   -- C.Cast t  ->
-  _ -> error "Unsupported unary operator in input." -- TODO(chathhorn)
+  _ -> error "Unsupported unary operator in input."
 
 trOp2 :: C.Op2 a b c -> (Op2, Type)
 trOp2 = \case
@@ -258,7 +261,7 @@
   -- C.BwShiftL t _ ->
   -- C.BwShiftR t _ ->
 
-  _ -> error "Unsupported binary operator in input." -- TODO(chathhorn)
+  _ -> error "Unsupported binary operator in input."
 
 trType :: C.Type a -> Type
 trType = \case
@@ -274,8 +277,6 @@
   C.Float  -> Real
   C.Double -> Real
 
---------------------------------------------------------------------------------
-
 -- | Translation state.
 data TransST = TransST
   { localConstraints :: [Expr]
@@ -294,14 +295,16 @@
       modify $ \st -> st { muxes = (v, mux) : ms }
       return v
     Just (v, _) -> return v
-  where mux = (c, t, e1, e2)
+  where
+    mux = (c, t, e1, e2)
 
 getMuxes :: Trans [Expr]
 getMuxes = muxes <$> get >>= return . concat . (map toConstraints)
-  where toConstraints (v, (c, _, e1, e2)) =
-          [ Op2 Bool Or (Op1 Bool Not c) (Op2 Bool Eq v e1)
-          , Op2 Bool Or c (Op2 Bool Eq v e2)
-          ]
+  where
+    toConstraints (v, (c, _, e1, e2)) =
+      [ Op2 Bool Or (Op1 Bool Not c) (Op2 Bool Eq v e1)
+      , Op2 Bool Or c (Op2 Bool Eq v e2)
+      ]
 
 -- | A state monad over the translation state ('TransST').
 type Trans = State TransST
@@ -321,6 +324,3 @@
 
 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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Copilot backend for the <https://kind2-mc.github.io/kind2/ Kind 2> SMT
@@ -11,5 +9,3 @@
 import Copilot.Theorem.Kind2.Translate as X
 import Copilot.Theorem.Kind2.PrettyPrint as X
 import Copilot.Theorem.Kind2.Prover 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,12 +1,8 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Abstract syntax tree of Kind2 files.
 module Copilot.Theorem.Kind2.AST where
 
---------------------------------------------------------------------------------
-
 -- | A file is a sequence of predicates and propositions.
 data File = File
   { filePreds     :: [PredDef]
@@ -54,5 +50,3 @@
   | StateVar       String
   | FunApp         String [Term]
   | PredApp        String PredType [Term]
-
---------------------------------------------------------------------------------
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,7 +1,5 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe       #-}
 
 -- | Parse output of Kind2.
 module Copilot.Theorem.Kind2.Output (parseOutput) where
@@ -12,8 +10,6 @@
 
 import qualified Copilot.Theorem.Misc.Error as Err
 
---------------------------------------------------------------------------------
-
 simpleName s = QName s Nothing Nothing
 
 -- | Parse output of Kind2.
@@ -52,5 +48,3 @@
     err msg = Err.fatal $
       "Parse error while reading the Kind2 XML output : \n"
       ++ msg ++ "\n\n" ++ xml
-
---------------------------------------------------------------------------------
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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Pretty print a Kind2 file defining predicates and propositions.
@@ -11,16 +9,12 @@
 
 import Data.List (intercalate)
 
---------------------------------------------------------------------------------
-
 -- | A tree of expressions, in which the leafs are strings.
 type SSExpr = SExpr String
 
 -- | Reserved keyword prime.
 kwPrime = "prime"
 
---------------------------------------------------------------------------------
-
 -- | Pretty print a Kind2 file.
 prettyPrint :: File -> String
 prettyPrint =
@@ -34,8 +28,6 @@
 shouldIndent (List [Atom a, Atom _])    = a `notElem` [kwPrime]
 shouldIndent _                          = True
 
---------------------------------------------------------------------------------
-
 -- | Convert a file into a sequence of expressions.
 ppFile :: File -> [SSExpr]
 ppFile (File preds props) = map ppPredDef preds ++ ppProps props
@@ -75,8 +67,7 @@
 ppTerm (StateVar v) = atom v
 ppTerm (FunApp f args) = node f $ map ppTerm args
 ppTerm (PredApp p t args) = node (p ++ "." ++ ext) $ map ppTerm args
-  where ext = case t of
-         Init -> "init"
-         Trans -> "trans"
-
---------------------------------------------------------------------------------
+  where
+    ext = case t of
+      Init -> "init"
+      Trans -> "trans"
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,4 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LambdaCase  #-}
 {-# LANGUAGE Trustworthy #-}
 
 -- | A prover backend based on Kind2.
@@ -26,8 +24,6 @@
 
 import qualified Copilot.Theorem.TransSys as TS
 
---------------------------------------------------------------------------------
-
 -- | Options for Kind2
 data Options = Options
   { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and
@@ -52,13 +48,9 @@
   , askProver    = askKind2
   , closeProver  = const $ return () }
 
---------------------------------------------------------------------------------
-
 kind2Prog        = "kind2"
 kind2BaseOptions = ["--input-format", "native", "-xml"]
 
---------------------------------------------------------------------------------
-
 askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output
 askKind2 (ProverST opts spec) assumptions toCheck = do
 
@@ -76,6 +68,4 @@
   putStrLn kind2Input
 
   removeFile tempName
-  return $ parseOutput (head toCheck) output -- TODO support multiple toCheck props
-
---------------------------------------------------------------------------------
+  return $ parseOutput (head toCheck) output
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,7 +1,8 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes     #-}
+{-# LANGUAGE Safe           #-}
+{-# LANGUAGE ViewPatterns   #-}
 
 -- | Convert modular transition systems ('TransSys') into Kind2 file
 -- specifications.
@@ -24,20 +25,14 @@
 import qualified Data.Map as Map
 import qualified Data.Bimap as Bimap
 
---------------------------------------------------------------------------------
-
 -- The following properties MUST hold for the given transition system :
 -- * Nodes are sorted by topological order
 -- * Nodes are `completed`, which means the dependency graph is transitive
 --   and each node imports all the local variables of its dependencies
 --
 
---------------------------------------------------------------------------------
-
 type DepGraph = Map NodeId [NodeId]
 
---------------------------------------------------------------------------------
-
 -- | Style of the Kind2 files produced: modular (with multiple separate nodes),
 -- or all inlined (with only one node).
 --
@@ -58,17 +53,19 @@
 toKind2 style assumptions checkedProps spec =
   addAssumptions spec assumptions
   $ trSpec (complete spec') predCallsGraph assumptions checkedProps
-  where predCallsGraph = specDependenciesGraph spec'
-        spec' = case style of
-          Inlined -> inline spec
-          Modular -> removeCycles spec
+  where
+    predCallsGraph = specDependenciesGraph spec'
+    spec' = case style of
+      Inlined -> inline spec
+      Modular -> removeCycles spec
 
 trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File
 trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props
-  where preds = map (trNode spec predCallsGraph) (specNodes spec)
-        props = map trProp $
-          filter ((`elem` checkedProps) . fst) $
-          Map.toList (specProps spec)
+  where
+    preds = map (trNode spec predCallsGraph) (specNodes spec)
+    props = map trProp $
+      filter ((`elem` checkedProps) . fst) $
+      Map.toList (specProps spec)
 
 trProp :: (PropId, ExtVar) -> K.Prop
 trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var)
@@ -86,7 +83,6 @@
                          ++ map (trExpr True) (nodeConstrs node)
                          ++ predCalls False spec predCallsGraph node
 
-
 addAssumptions :: TransSys -> [PropId] -> K.File -> K.File
 addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) =
   K.File (changeTail aux filePreds) fileProps
@@ -106,15 +102,12 @@
           toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v
       in map (varName . toTopVar . toExtVar) assumptions
 
---------------------------------------------------------------------------------
-
-{- The ordering really matters here because the variables
-   have to be given in this order in a pred call
-   Our convention :
-   * First the local variables, sorted by alphabetical order
-   * Then the imported variables, by alphabetical order on
-     the father node then by alphabetical order on the variable name
--}
+-- The ordering really matters here because the variables
+-- have to be given in this order in a pred call
+-- Our convention :
+-- * First the local variables, sorted by alphabetical order
+-- * Then the imported variables, by alphabetical order on
+--   the father node then by alphabetical order on the variable name
 
 gatherPredStateVars :: TransSys -> Node -> [K.StateVarDef]
 gatherPredStateVars spec node = locals ++ imported
@@ -136,8 +129,6 @@
       map (\(v, ev) -> K.StateVarDef (varName v) (extVarType ev) [])
       . sortBy (compare `on` snd) . Bimap.toList $ nodeImportedVars node
 
---------------------------------------------------------------------------------
-
 mkConj :: [K.Term] -> K.Term
 mkConj []  = trConst Bool True
 mkConj [x] = x
@@ -158,8 +149,6 @@
 trConst Bool    True  = K.ValueLiteral "true"
 trConst Bool    False = K.ValueLiteral "false"
 
---------------------------------------------------------------------------------
-
 initLocals :: Node -> [K.Term]
 initLocals node =
   concatMap f (Map.toList $ nodeLocalVars node)
@@ -170,7 +159,6 @@
         Expr    e   -> [mkEquality (trVar v) (trExpr False e)]
         Constrs cs  -> map (trExpr False) cs
 
-
 transLocals :: Node -> [K.Term]
 transLocals node =
   concatMap f (Map.toList $ nodeLocalVars node)
@@ -214,8 +202,6 @@
         argsSeq trVarF =
           map (localAlias trVarF) (calleeLocals ++ calleeImported)
 
---------------------------------------------------------------------------------
-
 trExpr :: Bool -> Expr t -> K.Term
 trExpr primed = tr
   where
@@ -225,5 +211,3 @@
     tr (Op1 _ op e) = K.FunApp (show op) [tr e]
     tr (Op2 _ op e1 e2) = K.FunApp (show op) [tr e1, tr e2]
     tr (VarE _ v) = if primed then trPrimedVar v else trVar v
-
---------------------------------------------------------------------------------
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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Custom functions to report error messages to users.
@@ -10,8 +8,6 @@
   , fatal
   ) where
 
---------------------------------------------------------------------------------
-
 -- | Tag used with error messages to help users locate the component that
 -- failed or reports the error.
 errorHeader :: String
@@ -34,5 +30,3 @@
 -- | Report an unrecoverable error (e.g., incorrect format).
 fatal :: String -> a
 fatal = error
-
---------------------------------------------------------------------------------
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,7 +1,5 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe              #-}
 
 -- | A representation for structured expression trees, with support for pretty
 -- printing and for parsing.
@@ -12,8 +10,6 @@
 
 import Control.Monad
 
---------------------------------------------------------------------------------
-
 -- | A structured expression is either an atom, or a sequence of expressions,
 -- where the first in the sequence denotes the tag or label of the tree.
 data SExpr a = Atom a
@@ -38,8 +34,6 @@
 -- additional expressions or arguments..
 node a l = List (Atom a : l)    -- (s ss)
 
---------------------------------------------------------------------------------
-
 -- A straightforward string representation for 'SExpr's of Strings that
 -- parenthesizes lists of expressions.
 instance Show (SExpr String) where
@@ -48,7 +42,6 @@
       show' (Atom s) = text s
       show' (List ts) = parens . hsep . map show' $ ts
 
-
 -- More advanced printing with some basic indentation
 
 -- | Indent by a given number.
@@ -71,13 +64,12 @@
   Atom a  -> text (printAtom a)
   List l  -> parens (foldl renderItem empty l)
 
-  where renderItem doc s
-          | shouldIndent s =
-            doc $$ indent (toDoc shouldIndent printAtom s)
-          | otherwise =
-            doc <+> toDoc shouldIndent printAtom s
-
---------------------------------------------------------------------------------
+  where
+    renderItem doc s
+      | shouldIndent s =
+        doc $$ indent (toDoc shouldIndent printAtom s)
+      | otherwise =
+        doc <+> toDoc shouldIndent printAtom s
 
 -- | Parser for strings of characters separated by spaces into a structured
 -- tree.
@@ -88,19 +80,20 @@
 parser =
   choice [try unitP, nodeP, leafP]
 
-  where symbol     = oneOf "!#$%&|*+-/:<=>?@^_~."
-        lonelyStr  = many1 (alphaNum <|> symbol)
+  where
+    symbol     = oneOf "!#$%&|*+-/:<=>?@^_~."
+    lonelyStr  = many1 (alphaNum <|> symbol)
 
-        unitP      = string "()" >> return unit
+    unitP      = string "()" >> return unit
 
-        leafP      = atom <$> lonelyStr
+    leafP      = atom <$> lonelyStr
 
-        nodeP      = do void $ char '('
-                        spaces
-                        st <- sepBy parser spaces
-                        spaces
-                        void $ char ')'
-                        return $ List st
+    nodeP      = do void $ char '('
+                    spaces
+                    st <- sepBy parser spaces
+                    spaces
+                    void $ char ')'
+                    return $ List st
 
 -- | Parser for strings of characters separated by spaces into a structured
 -- tree.
@@ -111,5 +104,3 @@
 parseSExpr str = case parse parser "" str of
   Left s -> error (show s) -- Nothing
   Right t -> Just t
-
---------------------------------------------------------------------------------
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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Utility / auxiliary functions.
@@ -8,8 +6,6 @@
  , openTempFile
  ) where
 
---------------------------------------------------------------------------------
-
 import Data.Function (on)
 import Data.List (groupBy, sortBy, group, sort)
 
@@ -22,8 +18,6 @@
 import System.Random
 import System.Directory
 
---------------------------------------------------------------------------------
-
 -- | True if the given list is a subset of the second list, when both are
 -- considered as sets.
 isSublistOf :: Ord a => [a] -> [a] -> Bool
@@ -46,8 +40,6 @@
 nubBy' :: (a -> a -> Ordering) -> [a] -> [a]
 nubBy' f = map head . groupBy (\x y -> f x y == EQ) . sortBy f
 
---------------------------------------------------------------------------------
-
 -- | Create a temporary file and open it for writing.
 openTempFile :: String  -- ^ Directory where the file should be created.
              -> String  -- ^ Base name for the file (prefix).
@@ -72,5 +64,3 @@
 
     pathFromSuff :: String -> FilePath
     pathFromSuff suf = loc ++ "/" ++ baseName ++ suf ++ "." ++ extension
-
---------------------------------------------------------------------------------
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,7 +1,8 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE NamedFieldPuns            #-}
+{-# LANGUAGE Safe                      #-}
+{-# LANGUAGE ViewPatterns              #-}
 
 -- | Connection to theorem provers.
 module Copilot.Theorem.Prove
@@ -23,8 +24,6 @@
 import Control.Applicative (liftA2)
 import Control.Monad.Writer
 
---------------------------------------------------------------------------------
-
 -- | Output produced by a prover, containing the 'Status' of the proof and
 -- additional information.
 data Output = Output Status [String]
@@ -92,8 +91,6 @@
   Assume :: PropId -> Action
   Admit  :: Action
 
---------------------------------------------------------------------------------
-
 -- | Record a requirement for satisfiability checking.
 check :: Prover -> Proof a
 check prover = Proof $ tell [Check prover]
@@ -214,5 +211,3 @@
       ++ msgL
       ++ [decoName nameR]
       ++ msgR
-
---------------------------------------------------------------------------------
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,5 +1,5 @@
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe       #-}
 
 -- | Backend to  SMT solvers and theorem provers.
 --
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,7 +1,9 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-}
-{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE NamedFieldPuns    #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE Trustworthy       #-}
 
 -- | Connections to various SMT solvers and theorem provers.
 module Copilot.Theorem.Prover.SMT
@@ -50,8 +52,6 @@
 
 import System.IO (hClose)
 
---------------------------------------------------------------------------------
-
 -- * Tactics
 
 -- | Options to configure the provers.
@@ -115,8 +115,6 @@
   , P.closeProver = const $ return ()
   }
 
--------------------------------------------------------------------------------
-
 -- * Backends
 
 -- | Backend to the Yices 2 SMT solver.
@@ -238,8 +236,6 @@
   , interpret       = TPTP.interpret
   }
 
--------------------------------------------------------------------------------
-
 -- | Checks the Copilot specification with k-induction
 
 type ProofScript b = MaybeT (StateT (ProofState b) IO)
@@ -331,18 +327,19 @@
 
 getVars :: [Expr] -> [VarDescr]
 getVars = nubBy' (compare `on` varName) . concatMap getVars'
-  where getVars' :: Expr -> [VarDescr]
-        getVars' = \case
-          ConstB _             -> []
-          ConstI _ _           -> []
-          ConstR _             -> []
-          Ite _ e1 e2 e3       -> getVars' e1 ++ getVars' e2 ++ getVars' e3
-          Op1 _ _ e            -> getVars' e
-          Op2 _ _ e1 e2        -> getVars' e1 ++ getVars' e2
-          SVal t seq (Fixed i) -> [VarDescr (seq ++ "_" ++ show i) t []]
-          SVal t seq (Var i)   -> [VarDescr (seq ++ "_n" ++ show i) t []]
-          FunApp t name args   -> [VarDescr name t (map typeOf args)]
-                                  ++ concatMap getVars' args
+  where
+    getVars' :: Expr -> [VarDescr]
+    getVars' = \case
+      ConstB _             -> []
+      ConstI _ _           -> []
+      ConstR _             -> []
+      Ite _ e1 e2 e3       -> getVars' e1 ++ getVars' e2 ++ getVars' e3
+      Op1 _ _ e            -> getVars' e
+      Op2 _ _ e1 e2        -> getVars' e1 ++ getVars' e2
+      SVal t seq (Fixed i) -> [VarDescr (seq ++ "_" ++ show i) t []]
+      SVal t seq (Var i)   -> [VarDescr (seq ++ "_n" ++ show i) t []]
+      FunApp t name args   -> [VarDescr name t (map typeOf args)]
+                              ++ concatMap getVars' args
 
 unknown :: ProofScript b a
 unknown = mzero
@@ -383,7 +380,6 @@
             Unknown -> unknown
             Unsat   -> valid $ "proved with " ++ proofKind k
 
-
 onlySat' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
 onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s
   where
@@ -419,6 +415,5 @@
 selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
 selectProps propIds properties =
   (squash . unzip) [(as, p) | (id, (as, p)) <- Map.toList properties, id `elem` propIds]
-    where squash (a, b) = (concat a, b)
-
---------------------------------------------------------------------------------
+    where
+      squash (a, b) = (concat a, b)
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,7 +1,8 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE LambdaCase     #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes     #-}
+{-# LANGUAGE Safe           #-}
+{-# LANGUAGE ViewPatterns   #-}
 
 -- | Communication with SMT solvers or theorem provers.
 --
@@ -23,8 +24,6 @@
 import Data.Maybe
 import Data.Set ((\\), fromList, Set, union, empty, elems)
 
---------------------------------------------------------------------------------
-
 -- | A connection with a running SMT solver or theorem prover.
 data Solver a = Solver
   { solverName :: String
@@ -37,8 +36,6 @@
   , backend    :: Backend a
   }
 
---------------------------------------------------------------------------------
-
 -- | Output a debugging message if debugging is enabled for the solver.
 debug :: Bool -> Solver a -> String -> IO ()
 debug printName s str = when (debugMode s) $
@@ -64,8 +61,6 @@
           liftIO $ debug True s $ "[received: " ++ ln ++ "]"
           MaybeT $ return $ (interpret $ backend s) ln
 
---------------------------------------------------------------------------------
-
 -- | Create a new solver implemented by the backend specified.
 --
 -- The error handle from the backend handle is immediately closed/discarded,
@@ -86,8 +81,6 @@
   hClose $ outh s
   terminateProcess $ process s
 
---------------------------------------------------------------------------------
-
 -- | Register the given expressions as assumptions or axioms with the solver.
 assume :: SmtFormat a => Solver a -> [Expr] -> IO (Solver a)
 assume s@(Solver { model }) cs = do
@@ -119,6 +112,3 @@
   forM_ newVars $ \(VarDescr {varName, varType, args}) ->
     send s $ declFun varName varType args
   return s { vars = vars `union` fromList newVars }
-
---------------------------------------------------------------------------------
-
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,7 +1,6 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE GADTs, FlexibleInstances #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE Safe              #-}
 
 -- | A backend to the SMT-Lib format, enabling to produce commands for SMT-Lib
 -- implementing solvers, and parse results.
@@ -14,8 +13,6 @@
 
 import Text.Printf
 
---------------------------------------------------------------------------------
-
 -- | Type used to represent SMT-lib commands.
 --
 -- Use the interface in 'SmtFormat' to create such commands.
@@ -29,8 +26,6 @@
 smtTy Real    = "Real"
 smtTy _       = "Int"
 
---------------------------------------------------------------------------------
-
 -- | Interface for SMT-Lib conforming backends.
 instance SmtFormat SmtLib where
   push = SmtLib $ node "push" [atom "1"]
@@ -48,8 +43,6 @@
 interpret "unsat" = Just Unsat
 interpret _       = Just Unknown
 
---------------------------------------------------------------------------------
-
 expr :: Expr -> SExpr String
 
 expr (ConstB v) = atom $ if v then "true" else "false"
@@ -104,5 +97,3 @@
 expr (SVal _ f ix) = atom $ case ix of
   Fixed i -> f ++ "_" ++ show i
   Var off -> f ++ "_n" ++ show off
-
---------------------------------------------------------------------------------
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,7 +1,6 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE GADTs, LambdaCase #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE Safe       #-}
 
 -- | A backend to <http://www.tptp.org/ TPTP>, enabling to produce assertions
 -- and to parse the results from TPTP.
@@ -12,8 +11,6 @@
 
 import Data.List
 
---------------------------------------------------------------------------------
-
 -- | Type used to represent TPTP expressions.
 --
 -- Although this type implements the 'SmtFormat' interface, only 'assert' is
@@ -33,8 +30,6 @@
   show (Atom atom)     = atom
   show (Fun name args) = name ++ "(" ++ intercalate ", " (map show args) ++ ")"
 
---------------------------------------------------------------------------------
-
 instance SmtFormat Tptp where
   push     = Null
   pop      = Null
@@ -50,8 +45,6 @@
   | "SZS status"               `isPrefixOf` str = Just Unknown
   | otherwise                                   = Nothing
 
---------------------------------------------------------------------------------
-
 expr :: Expr -> TptpExpr
 expr = \case
   ConstB v        -> Atom $ if v then "$true" else "$false"
@@ -109,5 +102,3 @@
   Mod   -> "mod"
   Fdiv  -> "/"
   Pow   -> "^"
-
---------------------------------------------------------------------------------
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,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | Each prover first translates the Copilot specification into an
@@ -17,5 +15,3 @@
 import Copilot.Theorem.TransSys.PrettyPrint as X
 import Copilot.Theorem.TransSys.Translate as X
 import Copilot.Theorem.TransSys.Transform 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,7 +1,7 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE Safe                #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 -- | Casting of values with dynamic types and translating from Copilot core
 -- types to Copilot theorem types.
@@ -14,8 +14,6 @@
   , casting
   ) where
 
---------------------------------------------------------------------------------
-
 import Copilot.Core as C
 
 import Data.Dynamic (Dynamic(..), fromDynamic, toDyn)
@@ -23,8 +21,6 @@
 
 import qualified Copilot.Theorem.TransSys.Type as K
 
---------------------------------------------------------------------------------
-
 -- | Synonym for a dynamic type in Copilot core.
 type Dyn = Dynamic
 
@@ -60,8 +56,6 @@
   K.U K.Integer -> f K.Integer
   K.U K.Real    -> f K.Real
 
---------------------------------------------------------------------------------
-
 class Casted b where
   _cast :: Dyn -> Maybe b
 
@@ -87,5 +81,3 @@
     | Just (v :: Float)  <- fromDynamic d = Just $ float2Double v
     | Just (v :: Double) <- fromDynamic d = Just v
     | otherwise                           = Nothing
-
---------------------------------------------------------------------------------
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
@@ -1,8 +1,9 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables,
-             RankNTypes #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE LambdaCase                #-}
+{-# LANGUAGE RankNTypes                #-}
+{-# LANGUAGE Safe                      #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
 
 -- | Operators in modular transition systems and their translation.
 module Copilot.Theorem.TransSys.Operators where
@@ -13,8 +14,6 @@
 
 import Copilot.Theorem.Misc.Error as Err
 
---------------------------------------------------------------------------------
-
 -- | Unary operators.
 data Op1 a where
   Not   :: Op1 Bool
@@ -55,8 +54,6 @@
 
   Pow    :: (Num a) => Op2 a a
 
--------------------------------------------------------------------------------
-
 instance Show (Op1 a) where
   show op = case op of
     Neg   -> "-"
@@ -94,8 +91,6 @@
     Fdiv -> "/"
     Pow  -> "^"
 
--------------------------------------------------------------------------------
-
 -- | Unhandled unary operator.
 --
 --   Unhandled operators are monomorphic, and their names are labeled so that
@@ -195,8 +190,6 @@
     notHandled ta s = casting ta $ \ta' ->
       notHandledF $ UnhandledOp1 s ta' resT
 
---------------------------------------------------------------------------------
-
 -- | Translate an Op2.
 --
 -- This function is parameterized so that it can be used to translate
@@ -228,7 +221,6 @@
 
   -> m (expr resT)
 
-
 handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of
 
   C.And        -> boolConnector And
@@ -328,10 +320,6 @@
     notHandled ta s = casting ta $ \ta' ->
       notHandledF (UnhandledOp2 s ta' ta' ta')
 
---------------------------------------------------------------------------------
-
 -- | Error message for unexpected behavior / internal errors.
 typeErrMsg :: String
 typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'"
-
---------------------------------------------------------------------------------
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,7 +1,6 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE NamedFieldPuns, GADTs #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE Safe           #-}
 
 -- | Pretty print a TransSys specification as a Kind2/Lustre specification.
 module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where
@@ -15,8 +14,6 @@
 
 import Prelude hiding ((<>))
 
---------------------------------------------------------------------------------
-
 indent     = nest 4
 emptyLine  = text ""
 
@@ -82,24 +79,24 @@
 
 pLVar :: Var -> VarDescr -> Doc
 pLVar l (VarDescr {varType, varDef}) = header $$ indent body
-  where header =
-          text (varName l)
-          <+> text ":"
-          <+> pType varType
-          <+> text "="
-
-        body = case varDef of
-          Pre val var ->
-            pConst varType val
-            <+> text "->" <+> text "pre"
-            <+> text (varName var)
-          Expr e -> pExpr e
+  where
+    header =
+      text (varName l)
+      <+> text ":"
+      <+> pType varType
+      <+> text "="
 
-          Constrs cs ->
-            text "{"
-            <+> (hsep . punctuate (space <> text ";" <> space)) (map pExpr cs)
-            <+> text "}"
+    body = case varDef of
+      Pre val var ->
+        pConst varType val
+        <+> text "->" <+> text "pre"
+        <+> text (varName var)
+      Expr e -> pExpr e
 
+      Constrs cs ->
+        text "{"
+        <+> (hsep . punctuate (space <> text ";" <> space)) (map pExpr cs)
+        <+> text "}"
 
 pExpr :: Expr t -> Doc
 
@@ -122,5 +119,3 @@
 
 pOp2 :: Op2 a b -> Doc
 pOp2 = text . show
-
---------------------------------------------------------------------------------
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,5 +1,3 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE Safe #-}
 
 -- | A monad capable of keeping track of variable renames and of providing
@@ -25,8 +23,6 @@
 import qualified Data.Set  as Set
 import qualified Data.List as List
 
---------------------------------------------------------------------------------
-
 -- | A monad capable of keeping track of variable renames and of providing
 -- fresh names for variables.
 type Renaming = State RenamingST
@@ -36,8 +32,6 @@
   { _reservedNames :: Set Var
   , _renaming      :: Map ExtVar Var }
 
---------------------------------------------------------------------------------
-
 -- | Register a name as reserved or used.
 addReservedName :: Var -> Renaming ()
 addReservedName v = modify $ \st ->
@@ -86,5 +80,3 @@
       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,7 +1,7 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE RankNTypes                #-}
+{-# LANGUAGE Safe                      #-}
 
 -- | Specification of Copilot streams as modular transition systems.
 module Copilot.Theorem.TransSys.Spec
@@ -44,8 +44,6 @@
 import qualified Data.Set   as Set
 import qualified Data.Bimap as Bimap
 
---------------------------------------------------------------------------------
-
 -- | Unique name that identifies a node.
 type NodeId = String
 
@@ -76,7 +74,6 @@
                                            --   its local name.
   , nodeConstrs       :: [Expr Bool] }
 
-
 -- | Identifer of a variable in the local (within one node) namespace.
 data Var      =  Var {varName :: String}
   deriving (Eq, Show, Ord)
@@ -103,8 +100,6 @@
   Op2   :: Type t -> Op2 a t -> Expr a -> Expr a -> Expr t
   VarE  :: Type t -> Var -> Expr t
 
---------------------------------------------------------------------------------
-
 -- | Constructor for variables identifiers in the global namespace.
 mkExtVar node name = ExtVar node (Var name)
 
@@ -130,8 +125,6 @@
     tre (Op2 t op e1 e2)  = f (Op2 t op (tre e1) (tre e2))
     tre e                 = f e
 
---------------------------------------------------------------------------------
-
 -- | The set of variables related to a node (union of the local variables and
 -- the imported variables after deferencing them).
 nodeVarsSet :: Node -> Set Var
@@ -160,8 +153,6 @@
 nodeExportedExtVarsSet :: Node -> Set ExtVar
 nodeExportedExtVarsSet n = Set.map (ExtVar $ nodeId n) (nodeLocalVarsSet n)
 
---------------------------------------------------------------------------------
-
 instance HasInvariants Node where
 
   invariants n =
@@ -178,8 +169,6 @@
       in preVars `isSubsetOf` nodeLocalVarsSet n
     ]
 
---------------------------------------------------------------------------------
-
 specNodesIds :: TransSys -> Set NodeId
 specNodesIds s = Set.fromList . map nodeId $ specNodes s
 
@@ -195,8 +184,6 @@
   ((== specTopNodeId spec) . nodeId)
   (specNodes spec)
 
---------------------------------------------------------------------------------
-
 instance HasInvariants TransSys where
 
   invariants s =
@@ -218,14 +205,11 @@
 isTopologicallySorted :: TransSys -> Bool
 isTopologicallySorted spec =
   isJust $ foldM inspect Set.empty (specNodes spec)
-  where inspect acc n = do
-          guard $ Set.fromList (nodeDependencies n) `isSubsetOf` acc
-          return . Set.insert (nodeId n) $ acc
-
---------------------------------------------------------------------------------
+  where
+    inspect acc n = do
+      guard $ Set.fromList (nodeDependencies n) `isSubsetOf` acc
+      return . Set.insert (nodeId n) $ acc
 
 -- For debugging purposes
 instance Show ExtVar where
   show (ExtVar n v) = "(" ++ n ++ " : " ++ show v ++ ")"
-
---------------------------------------------------------------------------------
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,7 +1,5 @@
---------------------------------------------------------------------------------
-
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe       #-}
 
 -- | Helper module to manipulate and simplify TransSys graphs.
 module Copilot.Theorem.TransSys.Transform
@@ -31,15 +29,11 @@
 import qualified Data.Graph as Graph
 import qualified Data.Bimap as Bimap
 
---------------------------------------------------------------------------------
-
 prefix :: String -> Var -> Var
 prefix s1 (Var s2) = Var $ s1 ++ "." ++ s2
 
 ncNodeIdSep = "-"
 
---------------------------------------------------------------------------------
-
 -- | Merge all the given nodes, replacing all references to the given node Ids
 -- with a reference to a fresh node id (unless the nodes given as argument
 -- contain the top node), in which case its ID is chosen instead.
@@ -92,7 +86,6 @@
 
     constrs = mergeConstrs toMerge renamingF
 
-
 updateOtherNode :: NodeId -> [NodeId] -> (ExtVar -> ExtVar) -> Node -> Node
 updateOtherNode newNodeId mergedNodesIds renamingF n = n
   { nodeDependencies =
@@ -105,8 +98,6 @@
                      | (lv, gv) <- Bimap.toList $ nodeImportedVars n ]
   }
 
-
-
 updateExpr :: NodeId -> (ExtVar -> Var) -> Expr t -> Expr t
 updateExpr nId renamingF = transformExpr aux
   where
@@ -114,7 +105,6 @@
     aux (VarE t v) = VarE t (renamingF (ExtVar nId v))
     aux e = e
 
-
 mergeVarsDescrs :: [Node] -> (ExtVar -> Var) -> Map Var VarDescr
 mergeVarsDescrs toMerge renamingF = Map.fromList $ do
   n <- toMerge
@@ -169,8 +159,6 @@
             then Bimap.insert v' (ExtVar nId v) acc
             else acc
 
-
-
 redirectLocalImports :: [Node] -> Renaming ()
 redirectLocalImports toMerge = do
   renamingF <- getRenamingF
@@ -186,8 +174,6 @@
       guard $ n' `member` mergedNodesSet
       return (nId, alias, n', v)
 
---------------------------------------------------------------------------------
-
 -- | Discard all the structure of a /modular transition system/ and turn it
 -- into a /non-modular transition system/ with only one node.
 inline :: TransSys -> TransSys
@@ -224,8 +210,6 @@
     topoSort s = s { specNodes =
       map (\(Graph.AcyclicSCC n) -> n) $ buildScc id (specNodes s) }
 
---------------------------------------------------------------------------------
-
 -- | Completes each node of a specification with imported variables such that
 -- each node contains a copy of all its dependencies.
 --
@@ -289,5 +273,3 @@
                 return $ Bimap.tryInsert alias ev acc
 
           foldM tryImport (nodeImportedVars n) toImportVars
-
---------------------------------------------------------------------------------
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
@@ -1,8 +1,10 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE RankNTypes, NamedFieldPuns, ViewPatterns,
-             ScopedTypeVariables, GADTs, FlexibleContexts #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE NamedFieldPuns      #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE Safe                #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns        #-}
 
 -- | Translate Copilot specifications into a modular transition system.
 --
@@ -57,8 +59,6 @@
 import qualified Data.Map     as Map
 import qualified Data.Bimap   as Bimap
 
---------------------------------------------------------------------------------
-
 -- Naming conventions
 -- These are important in order to avoid name conflicts
 
@@ -80,8 +80,6 @@
   | d == 0    = s
   | otherwise = s ++ ncSep ++ show d
 
---------------------------------------------------------------------------------
-
 -- | Translate Copilot specifications into a modular transition system.
 translate :: C.Spec -> TransSys
 translate cspec =
@@ -108,9 +106,6 @@
     topNode = mkTopNode topNodeId (map nodeId propNodes) cprops
     extVarNodes = map mkExtVarNode extvarNodesNames
 
---------------------------------------------------------------------------------
-
-
 mkTopNode :: String -> [NodeId] -> [C.Property] -> Node
 mkTopNode topNodeId dependencies cprops =
   Node { nodeId = topNodeId
@@ -123,8 +118,6 @@
       [ (Var cp, mkExtVar (ncPropNode cp) ncMain)
       | cp <- C.propertyName <$> cprops ]
 
-
-
 mkExtVarNode (name, U t) =
   Node { nodeId = name
        , nodeDependencies = []
@@ -132,7 +125,6 @@
        , nodeImportedVars = Bimap.empty
        , nodeConstrs = []}
 
-
 mkPropNodes :: [C.Property] -> Trans [Node]
 mkPropNodes = mapM propNode
   where
@@ -149,8 +141,6 @@
            , C.streamExpr = C.propertyExpr prop
            , C.streamExprType = C.Bool }
 
---------------------------------------------------------------------------------
-
 stream :: C.Stream -> Trans Node
 stream (C.Stream { C.streamId
                  , C.streamBuffer
@@ -180,8 +170,6 @@
       { nodeId, nodeDependencies, nodeLocalVars
       , nodeImportedVars, nodeConstrs = [] }
 
---------------------------------------------------------------------------------
-
 expr :: Type t -> C.Expr t' -> Trans (Expr t)
 
 expr t (C.Const _ v) = return $ Const t (cast t $ toDyn v)
@@ -219,12 +207,6 @@
   newImportedVar localAlias (ExtVar nodeName (Var ncMain))
   return $ VarE t localAlias
 
--- TODO : Use uninterpreted functions to handle
--- * Unhandled operators
--- * Extern functions
--- * Extern arrays
--- For now, the result of these operations is a new unconstrained variable
-
 expr t (C.Op1 op e) = handleOp1
   t (op, e) expr notHandled Op1
   where
@@ -244,8 +226,6 @@
   newDep newNode
   return $ VarE t (Var newNode)
 
---------------------------------------------------------------------------------
-
 runTrans :: Trans a -> (a, [(NodeId, U Type)])
 runTrans mx =
   (x, nubBy' (compare `on` fst) $ _extVarsNodes st)
@@ -293,7 +273,6 @@
     , _dependencies = [] }
   return (lvs, ivs, nub' dps)
 
-
 getUid :: Trans Int
 getUid = do
   uid <- _nextUid <$> get
@@ -312,5 +291,3 @@
 
 newExtVarNode id t =
   modify $ \st -> st { _extVarsNodes = (id, t) : _extVarsNodes st }
-
---------------------------------------------------------------------------------
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,7 +1,6 @@
---------------------------------------------------------------------------------
-
-{-# LANGUAGE ExistentialQuantification, GADTs #-}
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE Safe                      #-}
 
 -- | Types suported by the modular transition systems.
 module Copilot.Theorem.TransSys.Type
@@ -11,8 +10,6 @@
 
 import Copilot.Core.Type.Equality
 
---------------------------------------------------------------------------------
-
 -- | A type at both value and type level.
 --
 -- Real numbers are mapped to 'Double's.
@@ -28,18 +25,12 @@
   Real    =~= Real     = Just Refl
   _       =~= _        = Nothing
 
---------------------------------------------------------------------------------
-
 -- | Unknown types.
 --
 -- For instance, 'U Expr' is the type of an expression of unknown type
 data U f = forall t . U (f t)
 
---------------------------------------------------------------------------------
-
 instance Show (Type t) where
   show Integer = "Int"
   show Bool    = "Bool"
   show Real    = "Real"
-
---------------------------------------------------------------------------------
diff --git a/src/Copilot/Theorem/What4.hs b/src/Copilot/Theorem/What4.hs
--- a/src/Copilot/Theorem/What4.hs
+++ b/src/Copilot/Theorem/What4.hs
@@ -1,18 +1,18 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiWayIf #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures             #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE MultiWayIf                 #-}
+{-# LANGUAGE PatternSynonyms            #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE TemplateHaskell            #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE TypeOperators              #-}
 
 -- |
 -- Module      : Copilot.Theorem.What4
@@ -98,7 +98,6 @@
 import GHC.TypeNats (KnownNat)
 import qualified Panic as Panic
 
---------------------------------------------------------------------------------
 -- 'prove' function
 --
 -- To prove properties of a spec, we translate them into What4 using the TransM
@@ -185,7 +184,6 @@
   (res, _) <- runStateT (unTransM proveProperties) st
   return res
 
---------------------------------------------------------------------------------
 -- What4 translation
 
 -- | the state for translating Copilot expressions into What4 expressions. As we
@@ -303,8 +301,9 @@
   XDouble e ->
     Some . CopilotValue CT.Double . fst . bfToDouble NearEven <$> WG.groundEval ge e
   _ -> error "valFromExpr unhandled case"
-  where fromBV :: forall a w . Num a => BV.BV w -> a
-        fromBV = fromInteger . BV.asUnsigned
+  where
+    fromBV :: forall a w . Num a => BV.BV w -> a
+    fromBV = fromInteger . BV.asUnsigned
 
 -- | A view of an XExpr as a bitvector expression, a natrepr for its width, its
 -- signed/unsigned status, and the constructor used to reconstruct an XExpr from
@@ -519,7 +518,8 @@
       if k' < length buf
         then liftIO $ translateConstExpr sym tp (buf !! k')
         else translateExprAt sym (k' - length buf) e
-      where k' = k + fromIntegral ix
+      where
+        k' = k + fromIntegral ix
     CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented"
     CE.Var _ _ -> error "translateExpr: Var unimplemented"
     CE.ExternVar tp nm _prefix -> getExternConstantAt sym tp nm k
@@ -558,37 +558,40 @@
   (CE.Not, XBool e) -> XBool <$> WI.notPred sym e
   (CE.Not, _) -> panic
   (CE.Abs _, xe) -> numOp bvAbs fpAbs xe
-    where bvAbs :: BVOp1 w t
-          bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat)
-                       e_neg <- WI.bvSlt sym e zero
-                       neg_e <- WI.bvSub sym zero e
-                       WI.bvIte sym e_neg neg_e e
-          fpAbs :: FPOp1 fpp t
-          fpAbs e = do zero <- WI.floatLit sym knownRepr bfPosZero
-                       e_neg <- WI.floatLt sym e zero
-                       neg_e <- WI.floatSub sym fpRM zero e
-                       WI.floatIte sym e_neg neg_e e
+    where
+      bvAbs :: BVOp1 w t
+      bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat)
+                   e_neg <- WI.bvSlt sym e zero
+                   neg_e <- WI.bvSub sym zero e
+                   WI.bvIte sym e_neg neg_e e
+      fpAbs :: FPOp1 fpp t
+      fpAbs e = do zero <- WI.floatLit sym knownRepr bfPosZero
+                   e_neg <- WI.floatLt sym e zero
+                   neg_e <- WI.floatSub sym fpRM zero e
+                   WI.floatIte sym e_neg neg_e e
   (CE.Sign _, xe) -> numOp bvSign fpSign xe
-    where bvSign :: BVOp1 w t
-          bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)
-                        neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1))
-                        pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1)
-                        e_zero <- WI.bvEq sym e zero
-                        e_neg <- WI.bvSlt sym e zero
-                        t <- WI.bvIte sym e_neg neg_one pos_one
-                        WI.bvIte sym e_zero zero t
-          fpSign :: FPOp1 fpp t
-          fpSign e = do zero <- WI.floatLit sym knownRepr bfPosZero
-                        neg_one <- WI.floatLit sym knownRepr (bfFromDouble (-1.0))
-                        pos_one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)
-                        e_zero <- WI.floatEq sym e zero
-                        e_neg <- WI.floatLt sym e zero
-                        t <- WI.floatIte sym e_neg neg_one pos_one
-                        WI.floatIte sym e_zero zero t
+    where
+      bvSign :: BVOp1 w t
+      bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)
+                    neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1))
+                    pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1)
+                    e_zero <- WI.bvEq sym e zero
+                    e_neg <- WI.bvSlt sym e zero
+                    t <- WI.bvIte sym e_neg neg_one pos_one
+                    WI.bvIte sym e_zero zero t
+      fpSign :: FPOp1 fpp t
+      fpSign e = do zero <- WI.floatLit sym knownRepr bfPosZero
+                    neg_one <- WI.floatLit sym knownRepr (bfFromDouble (-1.0))
+                    pos_one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)
+                    e_zero <- WI.floatEq sym e zero
+                    e_neg <- WI.floatLt sym e zero
+                    t <- WI.floatIte sym e_neg neg_one pos_one
+                    WI.floatIte sym e_zero zero t
   (CE.Recip _, xe) -> fpOp recip xe
-    where recip :: FPOp1 fpp t
-          recip e = do one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)
-                       WI.floatDiv sym fpRM one e
+    where
+      recip :: FPOp1 fpp t
+      recip e = do one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)
+                   WI.floatDiv sym fpRM one e
   (CE.Exp _, xe) -> realOp (WI.realExp sym) xe
   (CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe
   (CE.Log _, xe) -> realOp (WI.realLog sym) xe
@@ -652,51 +655,53 @@
       Just ix -> return $ xes !! ix
       Nothing -> panic
   _ -> panic
-  where numOp :: (forall w . BVOp1 w t)
-              -> (forall fpp . FPOp1 fpp t)
-              -> XExpr t
-              -> IO (XExpr t)
-        numOp bvOp fpOp xe = case xe of
-          XInt8 e -> XInt8 <$> bvOp e
-          XInt16 e -> XInt16 <$> bvOp e
-          XInt32 e -> XInt32 <$> bvOp e
-          XInt64 e -> XInt64 <$> bvOp e
-          XWord8 e -> XWord8 <$> bvOp e
-          XWord16 e -> XWord16 <$> bvOp e
-          XWord32 e -> XWord32 <$> bvOp e
-          XWord64 e -> XWord64 <$> bvOp e
-          XFloat e -> XFloat <$> fpOp e
-          XDouble e -> XDouble <$> fpOp e
-          _ -> panic
+  where
+    numOp :: (forall w . BVOp1 w t)
+          -> (forall fpp . FPOp1 fpp t)
+          -> XExpr t
+          -> IO (XExpr t)
+    numOp bvOp fpOp xe = case xe of
+      XInt8 e -> XInt8 <$> bvOp e
+      XInt16 e -> XInt16 <$> bvOp e
+      XInt32 e -> XInt32 <$> bvOp e
+      XInt64 e -> XInt64 <$> bvOp e
+      XWord8 e -> XWord8 <$> bvOp e
+      XWord16 e -> XWord16 <$> bvOp e
+      XWord32 e -> XWord32 <$> bvOp e
+      XWord64 e -> XWord64 <$> bvOp e
+      XFloat e -> XFloat <$> fpOp e
+      XDouble e -> XDouble <$> fpOp e
+      _ -> panic
 
-        bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)
-        bvOp f xe = case xe of
-          XInt8 e -> XInt8 <$> f e
-          XInt16 e -> XInt16 <$> f e
-          XInt32 e -> XInt32 <$> f e
-          XInt64 e -> XInt64 <$> f e
-          XWord8 e -> XWord8 <$> f e
-          XWord16 e -> XWord16 <$> f e
-          XWord32 e -> XWord32 <$> f e
-          XWord64 e -> XWord64 <$> f e
-          _ -> panic
+    bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)
+    bvOp f xe = case xe of
+      XInt8 e -> XInt8 <$> f e
+      XInt16 e -> XInt16 <$> f e
+      XInt32 e -> XInt32 <$> f e
+      XInt64 e -> XInt64 <$> f e
+      XWord8 e -> XWord8 <$> f e
+      XWord16 e -> XWord16 <$> f e
+      XWord32 e -> XWord32 <$> f e
+      XWord64 e -> XWord64 <$> f e
+      _ -> panic
 
-        fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)
-        fpOp g xe = case xe of
-          XFloat e -> XFloat <$> g e
-          XDouble e -> XDouble <$> g e
-          _ -> panic
+    fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)
+    fpOp g xe = case xe of
+      XFloat e -> XFloat <$> g e
+      XDouble e -> XDouble <$> g e
+      _ -> panic
 
-        realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
-        realOp h xe = fpOp hf xe
-          where hf :: (forall fpp . FPOp1 fpp t)
-                hf e = do re <- WI.floatToReal sym e
-                          hre <- h re
-                          WI.realToFloat sym knownRepr fpRM hre
+    realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
+    realOp h xe = fpOp hf xe
+      where
+        hf :: (forall fpp . FPOp1 fpp t)
+        hf e = do re <- WI.floatToReal sym e
+                  hre <- h re
+                  WI.realToFloat sym knownRepr fpRM hre
 
-        realRecip :: RealOp1 t
-        realRecip e = do one <- WI.realLit sym 1
-                         WI.realDiv sym one e
+    realRecip :: RealOp1 t
+    realRecip e = do one <- WI.realLit sym 1
+                     WI.realDiv sym one e
 
 type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w)
 
@@ -734,30 +739,33 @@
   (CE.Div _, xe1, xe2) -> bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2
   (CE.Fdiv _, xe1, xe2) -> fpOp (WI.floatDiv sym fpRM) xe1 xe2
   (CE.Pow _, xe1, xe2) -> fpOp powFn' xe1 xe2
-    where powFn' :: FPOp2 fpp t
-          powFn' e1 e2 = do re1 <- WI.floatToReal sym e1
-                            re2 <- WI.floatToReal sym e2
-                            let args = (Empty :> re1 :> re2)
-                            rpow <- WI.applySymFn sym powFn args
-                            WI.realToFloat sym knownRepr fpRM rpow
+    where
+      powFn' :: FPOp2 fpp t
+      powFn' e1 e2 = do re1 <- WI.floatToReal sym e1
+                        re2 <- WI.floatToReal sym e2
+                        let args = (Empty :> re1 :> re2)
+                        rpow <- WI.applySymFn sym powFn args
+                        WI.realToFloat sym knownRepr fpRM rpow
   (CE.Logb _, xe1, xe2) -> fpOp logbFn' xe1 xe2
-    where logbFn' :: FPOp2 fpp t
-          logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1
-                             re2 <- WI.floatToReal sym e2
-                             let args = (Empty :> re1 :> re2)
-                             rpow <- WI.applySymFn sym logbFn args
-                             WI.realToFloat sym knownRepr fpRM rpow
+    where
+      logbFn' :: FPOp2 fpp t
+      logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1
+                         re2 <- WI.floatToReal sym e2
+                         let args = (Empty :> re1 :> re2)
+                         rpow <- WI.applySymFn sym logbFn args
+                         WI.realToFloat sym knownRepr fpRM rpow
   (CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym) (WI.floatEq sym) xe1 xe2
   (CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2
-    where neqPred :: BoolCmp2 t
-          neqPred e1 e2 = do e <- WI.eqPred sym e1 e2
-                             WI.notPred sym e
-          bvNeq :: forall w . BVCmp2 w t
-          bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2
-                           WI.notPred sym e
-          fpNeq :: forall fpp . FPCmp2 fpp t
-          fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2
-                           WI.notPred sym e
+    where
+      neqPred :: BoolCmp2 t
+      neqPred e1 e2 = do e <- WI.eqPred sym e1 e2
+                         WI.notPred sym e
+      bvNeq :: forall w . BVCmp2 w t
+      bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2
+                       WI.notPred sym e
+      fpNeq :: forall fpp . FPCmp2 fpp t
+      fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2
+                       WI.notPred sym e
   (CE.Le _, xe1, xe2) -> numCmp (WI.bvSle sym) (WI.bvUle sym) (WI.floatLe sym) xe1 xe2
   (CE.Ge _, xe1, xe2) -> numCmp (WI.bvSge sym) (WI.bvUge sym) (WI.floatGe sym) xe1 xe2
   (CE.Lt _, xe1, xe2) -> numCmp (WI.bvSlt sym) (WI.bvUlt sym) (WI.floatLt sym) xe1 xe2
@@ -797,131 +805,131 @@
       (XArray xes, XWord32 ix) -> buildIndexExpr sym 0 ix xes
       _ -> panic
   _ -> panic
-  where numOp :: (forall w . BVOp2 w t)
-              -> (forall fpp . FPOp2 fpp t)
-              -> XExpr t
-              -> XExpr t
-              -> IO (XExpr t)
-        numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of
-          (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2
-          (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2
-          (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2
-          (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2
-          (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2
-          (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2
-          (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2
-          (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2
-          (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2
-          (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2
-          _ -> panic
-
-        bvOp :: (forall w . BVOp2 w t)
-             -> (forall w . BVOp2 w t)
-             -> XExpr t
-             -> XExpr t
-             -> IO (XExpr t)
-        bvOp opS opU xe1 xe2 = case (xe1, xe2) of
-          (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2
-          (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2
-          (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2
-          (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2
-          (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2
-          (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2
-          (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2
-          (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2
-          _ -> panic
+  where
+    numOp :: (forall w . BVOp2 w t)
+          -> (forall fpp . FPOp2 fpp t)
+          -> XExpr t
+          -> XExpr t
+          -> IO (XExpr t)
+    numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of
+      (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2
+      (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2
+      (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2
+      (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2
+      (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2
+      (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2
+      (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2
+      (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2
+      (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2
+      (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2
+      _ -> panic
 
-        fpOp :: (forall fpp . FPOp2 fpp t)
-             -> XExpr t
-             -> XExpr t
-             -> IO (XExpr t)
-        fpOp op xe1 xe2 = case (xe1, xe2) of
-          (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2
-          (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2
-          _ -> panic
+    bvOp :: (forall w . BVOp2 w t)
+         -> (forall w . BVOp2 w t)
+         -> XExpr t
+         -> XExpr t
+         -> IO (XExpr t)
+    bvOp opS opU xe1 xe2 = case (xe1, xe2) of
+      (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2
+      (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2
+      (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2
+      (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2
+      (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2
+      (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2
+      (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2
+      (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2
+      _ -> panic
 
-        cmp :: BoolCmp2 t
-            -> (forall w . BVCmp2 w t)
-            -> (forall fpp . FPCmp2 fpp t)
-            -> XExpr t
-            -> XExpr t
-            -> IO (XExpr t)
-        cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of
-          (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2
-          (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2
-          (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2
-          (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2
-          (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2
-          (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2
-          (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2
-          (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2
-          (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2
-          (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2
-          (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2
-          _ -> panic
+    fpOp :: (forall fpp . FPOp2 fpp t)
+         -> XExpr t
+         -> XExpr t
+         -> IO (XExpr t)
+    fpOp op xe1 xe2 = case (xe1, xe2) of
+      (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2
+      (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2
+      _ -> panic
 
-        numCmp :: (forall w . BVCmp2 w t)
-               -> (forall w . BVCmp2 w t)
-               -> (forall fpp . FPCmp2 fpp t)
-               -> XExpr t
-               -> XExpr t
-               -> IO (XExpr t)
-        numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of
-          (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2
-          (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2
-          (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2
-          (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2
-          (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2
-          (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2
-          (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2
-          (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2
-          (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2
-          (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2
-          _ -> panic
+    cmp :: BoolCmp2 t
+        -> (forall w . BVCmp2 w t)
+        -> (forall fpp . FPCmp2 fpp t)
+        -> XExpr t
+        -> XExpr t
+        -> IO (XExpr t)
+    cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of
+      (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2
+      (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2
+      (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2
+      (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2
+      (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2
+      (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2
+      (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2
+      (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2
+      (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2
+      (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2
+      (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2
+      _ -> panic
 
-        buildIndexExpr :: 1 <= n
-                       => WB.ExprBuilder t st fs
-                       -> Word32
-                       -- ^ Index
-                       -> WB.Expr t (WT.BaseBVType 32)
-                       -- ^ Index
-                       -> V.Vector n (XExpr t)
-                       -- ^ Elements
-                       -> IO (XExpr t)
-        buildIndexExpr sym curIx ix xelts = case V.uncons xelts of
-          (xe, Left Refl) -> return xe
-          (xe, Right xelts') -> do
-            LeqProof <- return $ V.nonEmpty xelts'
-            rstExpr <- buildIndexExpr sym (curIx+1) ix xelts'
-            curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx)
-            ixEq <- WI.bvEq sym curIxExpr ix
-            mkIte sym ixEq xe rstExpr
+    numCmp :: (forall w . BVCmp2 w t)
+           -> (forall w . BVCmp2 w t)
+           -> (forall fpp . FPCmp2 fpp t)
+           -> XExpr t
+           -> XExpr t
+           -> IO (XExpr t)
+    numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of
+      (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2
+      (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2
+      (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2
+      (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2
+      (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2
+      (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2
+      (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2
+      (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2
+      (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2
+      (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2
+      _ -> panic
 
-        mkIte :: WB.ExprBuilder t st fs
-              -> WB.Expr t WT.BaseBoolType
-              -> XExpr t
-              -> XExpr t
-              -> IO (XExpr t)
-        mkIte sym pred xe1 xe2 = case (xe1, xe2) of
-              (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2
-              (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2
-              (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2
-              (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2
-              (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2
-              (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2
-              (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2
-              (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2
-              (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2
-              (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2
-              (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2
-              (XStruct xes1, XStruct xes2) ->
-                XStruct <$> zipWithM (mkIte sym pred) xes1 xes2
-              (XArray xes1, XArray xes2) ->
-                case V.length xes1 `testEquality` V.length xes2 of
-                  Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2
-                  Nothing -> panic
-              _ -> panic
+    buildIndexExpr :: 1 <= n
+                   => WB.ExprBuilder t st fs
+                   -> Word32
+                   -- ^ Index
+                   -> WB.Expr t (WT.BaseBVType 32)
+                   -- ^ Index
+                   -> V.Vector n (XExpr t)
+                   -- ^ Elements
+                   -> IO (XExpr t)
+    buildIndexExpr sym curIx ix xelts = case V.uncons xelts of
+      (xe, Left Refl) -> return xe
+      (xe, Right xelts') -> do
+        LeqProof <- return $ V.nonEmpty xelts'
+        rstExpr <- buildIndexExpr sym (curIx+1) ix xelts'
+        curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx)
+        ixEq <- WI.bvEq sym curIxExpr ix
+        mkIte sym ixEq xe rstExpr
 
+    mkIte :: WB.ExprBuilder t st fs
+          -> WB.Expr t WT.BaseBoolType
+          -> XExpr t
+          -> XExpr t
+          -> IO (XExpr t)
+    mkIte sym pred xe1 xe2 = case (xe1, xe2) of
+          (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2
+          (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2
+          (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2
+          (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2
+          (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2
+          (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2
+          (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2
+          (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2
+          (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2
+          (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2
+          (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2
+          (XStruct xes1, XStruct xes2) ->
+            XStruct <$> zipWithM (mkIte sym pred) xes1 xes2
+          (XArray xes1, XArray xes2) ->
+            case V.length xes1 `testEquality` V.length xes2 of
+              Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2
+              Nothing -> panic
+          _ -> panic
 
 translateOp3 :: forall t st fs a b c d .
                 WB.ExprBuilder t st fs