diff --git a/copilot-sbv.cabal b/copilot-sbv.cabal
--- a/copilot-sbv.cabal
+++ b/copilot-sbv.cabal
@@ -1,6 +1,6 @@
 cabal-version             : >= 1.10
 name                      : copilot-sbv
-version                   : 2.2.0
+version                   : 2.2.1
 synopsis                  : A compiler for CoPilot targeting SBV.
 description               :
   The Copilot back-end targeting SBV <http://hackage.haskell.org/package/sbv>.
@@ -36,12 +36,12 @@
   default-language        : Haskell2010
   hs-source-dirs          : src
   ghc-options             : -Wall -fwarn-tabs
---  ghc-prof-options        : -auto-all -caf-all
+  ghc-prof-options        : -auto-all -caf-all
 
-  build-depends           : sbv >= 5.0
+  build-depends           : sbv >= 5.0 
                           , base >= 4.0 && < 5
                           , containers >= 0.4
-                          , copilot-core == 2.2.0
+                          , copilot-core == 2.2.1
                           , directory >= 1.2.1
                           , pretty >= 1
                           , filepath >= 1.1
diff --git a/src/Copilot/Compile/SBV.hs b/src/Copilot/Compile/SBV.hs
--- a/src/Copilot/Compile/SBV.hs
+++ b/src/Copilot/Compile/SBV.hs
@@ -15,11 +15,11 @@
 import qualified Copilot.Core.PrettyDot as C
 import Copilot.Compile.Header.C99 (c99HeaderName, genC99Header)
 
-import qualified Data.SBV as S
+import qualified Data.SBV.Tools.CodeGen as S
 
 import Copilot.Compile.SBV.Driver (driver, driverName)
 import Copilot.Compile.SBV.Makefile (makefile, makefileName)
-import Copilot.Compile.SBV.Code 
+import Copilot.Compile.SBV.Code
   (updateStates, updateObservers, fireTriggers, getExtArrs, getExtFuns)
 import Copilot.Compile.SBV.MetaTable (allocMetaTable)
 import Copilot.Compile.SBV.Params
@@ -38,7 +38,7 @@
 
 proofACSL :: Params -> C.Spec -> IO ()
 proofACSL p s = do
-  writeFile "main.gv" (C.prettyPrintDot $ (s))
+  writeFile "main.gv" (C.prettyPrintDot s)
   compileWithSBV p [] (T.transformProofACSL s)
 
 compile :: Params -> C.Spec -> IO ()
@@ -57,9 +57,9 @@
     sbvName $ omitSBVDriver
     (  updateStates    meta spec
     ++ updateObservers meta spec
-    ++ fireTriggers    meta spec 
-    ++ getExtArrs      meta 
-    ++ getExtFuns      meta 
+    ++ fireTriggers    meta spec
+    ++ getExtArrs      meta
+    ++ getExtFuns      meta
     ++ sbvs
     )
 
@@ -88,7 +88,7 @@
 --------------------------------------------------------------------------------
 
 readme :: [String]
-readme = 
+readme =
   [ "These files are automatically generated by Copilot using the SBV code generator backend."
   , ""
   , "To build, you will need to ensure that all external variables and triggers are visible."
@@ -107,7 +107,7 @@
 --------------------------------------------------------------------------------
 
 omitSBVDriver :: [(a, S.SBVCodeGen ())] -> [(a, S.SBVCodeGen ())]
-omitSBVDriver = map omit 
+omitSBVDriver = map omit
   where
   omit (a, cg) = (a, S.cgGenerateDriver False >> cg)
 
diff --git a/src/Copilot/Compile/SBV/ACSLexpr.hs b/src/Copilot/Compile/SBV/ACSLexpr.hs
--- a/src/Copilot/Compile/SBV/ACSLexpr.hs
+++ b/src/Copilot/Compile/SBV/ACSLexpr.hs
@@ -31,41 +31,38 @@
 --------------------------------------------------------------------------------
 
 ppExpr :: MT.MetaTable -> Expr a -> Doc
-ppExpr meta e0 = parens $ case e0 of
+ppExpr meta e0 = case e0 of
   Const t x                  -> text (showWithType Haskell t x)
-  Drop _ 0 id                -> 
+  Drop _ 0 id                ->
         let aa = M.lookup id (MT.streamInfoMap meta)
         in case aa of
-          Just Stream { streamBuffer = ll } -> 
-            let streamSize = (length ll) in
-            case streamSize of 
-              1 -> strmName id <> lbrack <> (text "0") <> rbrack
-              _ -> strmName id <> lbrack <> (ptrName id) <> rbrack
-  Drop _ i id                -> 
+          Just Stream { streamBuffer = ll } ->
+            let streamSize = length ll in
+            case streamSize of
+              1 -> strmName id <> lbrack <> text "0" <> rbrack
+              _ -> strmName id <> lbrack <> ptrName id <> rbrack
+  Drop _ i id                ->
         let aa = M.lookup id (MT.streamInfoMap meta)
         in case aa of
-          Just Stream { streamBuffer = ll } -> 
-            let streamSize = (length ll) in
-            strmName id <> lbrack <> lparen <> ptrName id <> text (" + " ++ show i) <> rparen <> text " % " <> int streamSize <> rbrack 
+          Just Stream { streamBuffer = ll } ->
+            let streamSize = length ll in
+            strmName id <> lbrack <> lparen <> ptrName id <> text (" + " ++ show i) <> rparen <> text " % " <> int streamSize <> rbrack
   ExternVar _ name _        -> text $ mkExtTmpVar name
-  ExternFun _ name _ _ tag  -> (text $ mkExtTmpTag name tag)
-  ExternArray _ _ name 
-              _ _ _ tag      -> (text $ mkExtTmpTag name tag)
-  Local _ _ name e1 e2       -> text "\\let" <+> (text name) <+> equals
-                                          <+> (ppExpr meta e1) <+> text ";" <+> (ppExpr meta e2)
-  Var _ name                 -> (text name)
-  Op1 op e                   -> ppOp1 op (ppExpr meta e)
-  Op2 op e1 e2               -> ppOp2 op (ppExpr meta e1) (ppExpr meta e2)
-  Op3 op e1 e2 e3            -> ppOp3 op (ppExpr meta e1) (ppExpr meta e2) (ppExpr meta e3)
-  Label t s e                -> (ppExpr meta e)
-
-ppUExpr :: MT.MetaTable -> UExpr -> Doc
-ppUExpr meta UExpr { uExprExpr = e0 } = ppExpr meta e0
+  ExternFun _ name _ _ tag  -> text $ mkExtTmpTag name tag
+  ExternArray _ _ name
+              _ _ _ tag      -> text $ mkExtTmpTag name tag
+  Local _ _ name e1 e2       -> parens $ text "\\let" <+> text name <+> equals
+                                          <+> ppExpr meta e1 <+> text ";" <+> ppExpr meta e2
+  Var _ name                 -> text name
+  Op1 op e                   -> parens $ ppOp1 op (ppExpr meta e)
+  Op2 op e1 e2               -> parens $ ppOp2 op (ppExpr meta e1) (ppExpr meta e2)
+  Op3 op e1 e2 e3            -> parens $ ppOp3 op (ppExpr meta e1) (ppExpr meta e2) (ppExpr meta e3)
+  Label t s e                -> ppExpr meta e
 
 ppOp1 :: Op1 a b -> Doc -> Doc
 ppOp1 op = case op of
   Not      -> ppPrefix "!"
-  Abs _    -> \x -> ((parens $ x <> (text " > 0")) <> text "? " <> x <> text " : -" <> x )
+  Abs _    -> ppPrefix "\\abs"
   Sign _   -> \x -> ((parens $ x <> (text " > 0")) <> text "? 1 : ") <> (parens $ x <> (text " < 0 ? -1 : ") <> x)
   Recip _  -> ppPrefix "\\recip"
   Exp _    -> ppPrefix "\\exp"
@@ -118,10 +115,9 @@
     text ":" <+> doc3 <> text ")"
 
 --------------------------------------------------------------------------------
-  
+
 ppInfix :: String -> Doc -> Doc -> Doc
 ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2
-
 
 ppPrefix2 :: String -> Doc -> Doc -> Doc
 ppPrefix2 cs doc1 doc2 = parens $ text cs <+> doc1 <> text "," <+> doc2
diff --git a/src/Copilot/Compile/SBV/ACSLproof.hs b/src/Copilot/Compile/SBV/ACSLproof.hs
--- a/src/Copilot/Compile/SBV/ACSLproof.hs
+++ b/src/Copilot/Compile/SBV/ACSLproof.hs
@@ -2,11 +2,11 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
-{-# LANGUAGE GADTs, ExistentialQuantification #-}
+{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase #-}
 
 module Copilot.Compile.SBV.ACSLproof
   ( transformProofACSL
-  ) 
+  )
 where
 
 import Prelude hiding (id)
@@ -82,24 +82,8 @@
   , triggerArgs      = map transformUExpr uexprl }
 --------------------------------------------------------------------------------
 
--- | A property.
---data Property = Property
---  { propertyName     :: Name
---  , propertyExpr     :: Expr Bool }
-  
-
-transformProperty :: Property -> Property
-transformProperty Property
-  { propertyName     = name
-  , propertyExpr     = bexpr } =
-  Property
-  { propertyName     = name
-  , propertyExpr     = transformExpr bexpr }
-
---------------------------------------------------------------------------------
-
 -- | A Copilot specification consists of a list of variables bound to anonymous
--- streams, a lost of anomymous streams, a list of observers, and a list of
+-- streams, a list of anomymous streams, a list of observers, and a list of
 -- triggers.
 --data Spec = Spec
 --  { specStreams      :: [Stream]
@@ -118,19 +102,20 @@
     { specStreams    = map transformStream strms
     , specObservers  = map transformObserver obsvs
     , specTriggers   = map transformTrigger trigs
-    , specProperties = map transformProperty props
+    , specProperties = []
     }
 
-
-
 --------------------------------------------------------------------------------
 --data UExpr = forall a. UExpr
 --  { uExprType :: Type a
 --  , uExprExpr :: Expr a }
 transformUExpr :: UExpr -> UExpr
-transformUExpr UExpr { uExprExpr = e, uExprType = t } = 
+transformUExpr UExpr { uExprExpr = e, uExprType = t } =
   UExpr { uExprExpr = transformExpr e, uExprType = t }
 
+transformUExpr' :: UExpr -> UExpr
+transformUExpr' UExpr { uExprExpr = e, uExprType = t } =
+  UExpr { uExprExpr = transformExpr' e, uExprType = t }
 
 --------------------------------------------------------------------------------
 -- Expr transformation
@@ -143,35 +128,37 @@
 --  Const        :: Type a -> a -> Expr a
 --  Drop         :: Type a -> DropIdx -> Id -> Expr a
 --  Local        :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
---  Var          :: Type a -> Name -> Expr a 
---  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a 
---  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a) 
+--  Var          :: Type a -> Name -> Expr a
+--  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a
+--  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a)
 --               -> Maybe Tag -> Expr a
 --  ExternArray  :: Integral a => Type a -> Type b -> Name -> Int -> Expr a
---               -> Maybe [[b]] -> Maybe Tag -> Expr b 
---  Op1          :: Op1 a b -> Expr a -> Expr b 
+--               -> Maybe [[b]] -> Maybe Tag -> Expr b
+--  Op1          :: Op1 a b -> Expr a -> Expr b
 --  Op2          :: Op2 a b c -> Expr a -> Expr b -> Expr c
 --  Op3          :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
 
-transformExpr :: Expr a -> Expr a 
-transformExpr e0 = case e0 of
-  Const t x                      -> Const t x
-  Drop t k id                    -> Drop t k id
-  Local t1 t2 name e1 e2         -> Local t1 t2 name (transformExpr e1) (transformExpr e2) 
-  Var t name                     -> Var t name
-  ExternVar t name e             -> ExternVar t name e
-  ExternFun t name args contxt yy-> ExternFun t name (map transformUExpr args) contxt yy
-  ExternArray t1 t2 name 
-              size idx context yy-> ExternArray t1 t2 name size (transformExpr idx) context yy
-  Op1 op e                       -> transformOp1 op e
-  Op2 op e1 e2                   -> transformOp2 op e1 e2
-  Op3 op e1 e2 e3                -> transformOp3 op e1 e2 e3
+transformExpr :: Expr a -> Expr a
+transformExpr = simpl . transformExpr'
 
-  Label t s e                    -> case s of 
-    '?':m -> ExternFun t ("ident_"++(showType t)) [UExpr {uExprExpr = transformExpr $ Label t m $ e, uExprType = t}] Nothing Nothing
-    _     -> Label t s $ transformExpr e
-    
+transformExpr' :: Expr a -> Expr a
+transformExpr' e0 = case e0 of
+  Const t x                       -> Const t x
+  Drop t k id                     -> Drop t k id
+  Local t1 t2 name e1 e2          -> Local t1 t2 name (transformExpr' e1) (transformExpr e2)
+  Var t name                      -> Var t name
+  ExternVar t name e              -> ExternVar t name e
+  ExternFun t name args contxt yy -> ExternFun t name (map transformUExpr' args) contxt yy
+  ExternArray t1 t2 name
+              size idx context yy -> ExternArray t1 t2 name size (transformExpr' idx) context yy
+  Op1 op e                        -> transformOp1 op (transformExpr' e)
+  Op2 op e1 e2                    -> transformOp2 op (transformExpr' e1) (transformExpr' e2)
+  Op3 op e1 e2 e3                 -> transformOp3 op (transformExpr' e1) (transformExpr' e2) (transformExpr' e3)
 
+  Label t s e                     -> case s of
+    '?':m -> ExternFun t ("ident_" ++ showType t) [UExpr {uExprExpr = Label t m $ transformExpr' e, uExprType = t}] Nothing Nothing
+    _     -> Label t s $ transformExpr' e
+
 showType :: Type a -> String
 showType t = case t of
   Bool  -> "bool"
@@ -189,117 +176,171 @@
 transformOp1 :: Op1 a b -> Expr a -> Expr b
 transformOp1 op e = case op of
     -- Boolean operators.
-  Not          -> Op1 Not $ transformExpr e
+  Not          -> Op1 Not e
   -- Numeric operators.
-  Abs   t      -> Op2 (Mul t) (transformExpr e) (transformExpr $ Label t "?absolute_value_splitting" $ Op1 (Sign t) $ e)
-  Sign  t      -> Op1 (Sign t) $ transformExpr e
+--  Abs   t      -> Op2 (Mul t) e (Label t "?absolute_value_splitting" $ Op1 (Sign t) e)
+  Sign  t      -> Op1 (Sign t) e
   -- Fractional operators.
-  Recip a      -> Op2 (Fdiv a) (Const a 1.0) (transformExpr e)
+  Recip t      -> Op2 (Fdiv t) (Const t 1.0) e
   -- Floating operators.
-  Exp Float    -> ExternFun Float "expf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Exp Double   -> ExternFun Double "exp" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Sqrt Float   -> ExternFun Float "sqrtf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Sqrt Double  -> ExternFun Double "sqrt" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Log Float    -> ExternFun Float "logf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Log Double   -> ExternFun Double "log" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Sin Float    -> ExternFun Float "sinf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Sin Double   -> ExternFun Double "sin" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Cos Float    -> ExternFun Float "cosf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Cos Double   -> ExternFun Double "cos" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Tan Float    -> ExternFun Float "tanf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Tan Double   -> ExternFun Double "tan" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Asin Float   -> ExternFun Float "asinf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Asin Double  -> ExternFun Double "asin" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Acos Float   -> ExternFun Float "acosf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Acos Double  -> ExternFun Double "acos" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Atan Float   -> ExternFun Float "atanf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Atan Double  -> ExternFun Double "atan" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Sinh Float   -> ExternFun Float "sinhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Sinh Double  -> ExternFun Double "sinh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Cosh Float   -> ExternFun Float "coshf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Cosh Double  -> ExternFun Double "cosh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Tanh Float   -> ExternFun Float "tanhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Tanh Double  -> ExternFun Double "tanh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Asinh Float  -> ExternFun Float "asinhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Asinh Double -> ExternFun Double "asinh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Acosh Float  -> ExternFun Float "acoshf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Acosh Double -> ExternFun Double "acosh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Atanh Float  -> ExternFun Float "atanhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Atanh Double -> ExternFun Double "atanh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+--  Exp Float    -> ExternFun Float "expf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Exp Double   -> ExternFun Double "exp"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+-- Sqrt t       -> Op2 (Pow t) (Const t 0.5) e
+--  Log Float    -> ExternFun Float "logf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Log Double   -> ExternFun Double "log"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Sin Float    -> ExternFun Float "sinf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Sin Double   -> ExternFun Double "sin"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Cos Float    -> ExternFun Float "cosf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Cos Double   -> ExternFun Double "cos"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Tan Float    -> ExternFun Float "tanf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Tan Double   -> ExternFun Double "tan"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Asin Float   -> ExternFun Float "asinf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Asin Double  -> ExternFun Double "asin"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Acos Float   -> ExternFun Float "acosf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Acos Double  -> ExternFun Double "acos"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Atan Float   -> ExternFun Float "atanf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Atan Double  -> ExternFun Double "atan"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Sinh Float   -> ExternFun Float "sinhf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Sinh Double  -> ExternFun Double "sinh"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Cosh Float   -> ExternFun Float "coshf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Cosh Double  -> ExternFun Double "cosh"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Tanh Float   -> ExternFun Float "tanhf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Tanh Double  -> ExternFun Double "tanh"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Asinh Float  -> ExternFun Float "asinhf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Asinh Double -> ExternFun Double "asinh"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Acosh Float  -> ExternFun Float "acoshf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Acosh Double -> ExternFun Double "acosh"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
+--  Atanh Float  -> ExternFun Float "atanhf"
+--                    [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing
+--  Atanh Double -> ExternFun Double "atanh"
+--                    [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing
   -- Bitwise operators.
-  BwNot    t   -> Op1 (BwNot t) $ transformExpr e
+  BwNot    t   -> Op1 (BwNot t) e
   -- Casting operator.
-  Cast     t s -> Op1 (Cast t s) $ transformExpr e
+  Cast     t s -> Op1 (Cast t s) e
+  op -> Op1 op e
 
 transformOp2 :: Op2 a b c -> Expr a -> Expr b -> Expr c
 transformOp2 op e1 e2 = case op of
-  -- Boolean operators.
-  And          -> Op2 And (transformExpr e1) (transformExpr e2)
-  Or           -> Op2 Or (transformExpr e1) (transformExpr e2)
-  -- Numeric operators.
-  Add    t     -> Op2 (Add t) (transformExpr e1) (transformExpr e2)
-  Sub    t     -> Op2 (Sub t) (transformExpr e1) (transformExpr e2)
-  Mul    t     -> Op2 (Mul t) (transformExpr e1) (transformExpr e2)
-  -- Integral operators.
-  Mod    t     -> Op2 (Mod t) (transformExpr e1) (transformExpr e2)
-  Div    t     -> Op2 (Div t) (transformExpr e1) (transformExpr e2)
-  -- Fractional operators.
-  Fdiv   t     -> Op2 (Fdiv t) (transformExpr e1) (transformExpr e2)
   -- Floating operators.
-  Pow    Float -> ExternFun Float "powf" 
-                    [UExpr { uExprExpr = transformExpr e1, uExprType = Float } 
-                    , UExpr { uExprExpr = transformExpr e2, uExprType = Float }] Nothing Nothing
-  Pow    Double-> ExternFun Double "pow" 
-                    [UExpr { uExprExpr = transformExpr e1, uExprType = Double } 
-                    , UExpr { uExprExpr = transformExpr e2, uExprType = Double }] Nothing Nothing
-  Logb   t     -> Op2 (Fdiv t) (transformExpr $ Op1 (Log t) e1) (transformExpr $ Op1 (Log t) e2)
-  -- Equality operators.
-  Eq    t      -> Op2 (Eq t) (transformExpr e1) (transformExpr e2)
-  Ne    t      -> Op2 (Ne t) (transformExpr e1) (transformExpr e2)
-  -- Relational operators.
-  Le    t      -> Op2 (Le t) (transformExpr e1) (transformExpr e2)
-  Ge    t      -> Op2 (Ge t) (transformExpr e1) (transformExpr e2)
-  Lt    t      -> Op2 (Lt t) (transformExpr e1) (transformExpr e2)
-  Gt    t      -> Op2 (Gt t) (transformExpr e1) (transformExpr e2)
-  -- Bitwise operators.
-  BwAnd t      -> Op2 (BwAnd t) (transformExpr e1) (transformExpr e2)
-  BwOr  t      -> Op2 (BwOr t) (transformExpr e1) (transformExpr e2)
-  BwXor t      -> Op2 (BwXor t) (transformExpr e1) (transformExpr e2)
-  BwShiftL t s -> Op2 (BwShiftL t s) (transformExpr e1) (transformExpr e2)
-  BwShiftR t s -> Op2 (BwShiftR t s) (transformExpr e1) (transformExpr e2)
+  -- Pow    Float -> ExternFun Float "powf"
+  --                   [UExpr { uExprExpr = e1, uExprType = Float }
+  --                   , UExpr { uExprExpr = e2, uExprType = Float }] Nothing Nothing
+  -- Pow    Double-> ExternFun Double "pow"
+  --                   [UExpr { uExprExpr = e1, uExprType = Double }
+  --                   , UExpr { uExprExpr = e2, uExprType = Double }] Nothing Nothing
+  Logb   t     -> Op2 (Fdiv t) (transformExpr' $ Op1 (Log t) e1) (transformExpr' $ Op1 (Log t) e2)
+  op           -> Op2 op e1 e2
 
 
 transformOp3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
-transformOp3 op e1 e2 e3 = case op of 
-  Mux   Bool   -> Op2 Or (transformExpr $ Op2 And (e2) (e1)) (transformExpr $ Op2 And (e3) (Op1 Not e1))
-  Mux   t      -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3) 
+transformOp3 op e1 e2 e3 = case op of
+  Mux   Bool   -> Op2 Or (transformExpr' $ Op2 And e2 e1) (transformExpr' $ Op2 And (e3) (Op1 Not e1))
+  Mux   t      -> Op3 (Mux t) e1 e2 e3
+
+-----------------------------------------
+
+simpl :: Expr a -> Expr a
+simpl = \ case
+  Op1 op e                  -> simplOp1 (simpl e) op
+  Op2 op e1 e2              -> simplOp2 (simpl e1) (simpl e2) op
+  Op3 op e1 e2 e3           -> simplOp3 (simpl e1) (simpl e2) (simpl e3) op
+  Local t1 t2 n e1 e2       -> Local t1 t2 n (simpl e1) (simpl e2)
+  Label _ _ e               -> simpl e
+  ExternFun t n args ctx yy -> ExternFun t n (map simplUExpr args) ctx yy
+
+  c                         -> c
+
+simplUExpr :: UExpr -> UExpr
+simplUExpr UExpr { uExprExpr = e, uExprType = t } =
+  UExpr { uExprExpr = simpl e, uExprType = t }
+
+simplOp1 :: Expr a -> Op1 a b -> Expr b
+simplOp1 e@(Const Bool x) = \ case
+  Not      -> Const Bool $ not x
+  op       -> Op1 op e
+simplOp1 e@(Const Double x) = \ case
+  Abs _    -> Const Double $ abs x
+  --Sign _   -> sign x
+  --Recip _  ->
+  --Exp _    ->
+  Sqrt _   -> Const Double $ sqrt x
+  --Log _    ->
+  Sin _    -> Const Double $ sin x
+  Tan _    -> Const Double $ tan x
+  Cos _    -> Const Double $ cos x
+  Asin _   -> Const Double $ asin x
+  Atan _   -> Const Double $ atan x
+  Acos _   -> Const Double $ acos x
+  Sinh _   -> Const Double $ sinh x
+  Tanh _   -> Const Double $ tanh x
+  Cosh _   -> Const Double $ cosh x
+  Asinh _  -> Const Double $ asinh x
+  Atanh _  -> Const Double $ atanh x
+  Acosh _  -> Const Double $ acosh x
+  --BwNot _  ->
+  --Cast _ _ ->
+  op           -> Op1 op e
+simplOp1 e = \ op -> Op1 op e
+
+simplOp2 :: Expr a -> Expr b -> Op2 a b c -> Expr c
+simplOp2 e1@(Const Bool x1) e2@(Const Bool x2) = \ case
+  And          -> Const Bool $ x1 && x2
+  Or           -> Const Bool $ x1 || x2
+  Eq       _   -> Const Bool $ x1 == x2
+  Ne       _   -> Const Bool $ x1 /= x2
+  op           -> Op2 op e1 e2
+simplOp2 e1@(Const t x1) e2@(Const _ x2) = \ case
+  Add      _   -> Const t $ x1 + x2
+  Sub      _   -> Const t $ x1 - x2
+  Mul      _   -> Const t $ x1 * x2
+  Div      _   -> Const t $ x1 `div` x2
+  Mod      _   -> Const t $ x1 `mod` x2
+  Fdiv     _   -> Const t $ x1 / x2
+  Pow      _   -> Const t $ x1 ** x2
+  --Logb     _   ->
+  Eq       _   -> Const Bool $ x1 == x2
+  Ne       _   -> Const Bool $ x1 /= x2
+  Le       _   -> Const Bool $ x1 <= x2
+  Ge       _   -> Const Bool $ x1 >= x2
+  Lt       _   -> Const Bool $ x1 < x2
+  Gt       _   -> Const Bool $ x1 > x2
+  --BwAnd    _   ->
+  --BwOr     _   ->
+  --BwXor    _   ->
+  --BwShiftL _ _ ->
+  --BwShiftR _ _ ->
+  op           -> Op2 op e1 e2
+simplOp2 e1 e2 = \ op -> Op2 op e1 e2
+
+simplOp3 :: Expr a -> Expr b -> Expr c -> Op3 a b c d -> Expr d
+-- simplOp3 (Const _ x1) (Const _ x2) (Const _ x3) = \ case
+--   Mux _    -> if x1 then x2 else x3
+simplOp3 e1 e2 e3 = \ op -> Op3 op e1 e2 e3
+
diff --git a/src/Copilot/Compile/SBV/Code.hs b/src/Copilot/Compile/SBV/Code.hs
--- a/src/Copilot/Compile/SBV/Code.hs
+++ b/src/Copilot/Compile/SBV/Code.hs
@@ -4,6 +4,7 @@
 
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE LambdaCase #-}
 
 module Copilot.Compile.SBV.Code
   ( updateStates
@@ -14,7 +15,7 @@
   ) where
 
 import Copilot.Compile.SBV.Copilot2SBV
-import Copilot.Compile.SBV.MetaTable
+import Copilot.Compile.SBV.MetaTable as T
 import qualified Copilot.Compile.SBV.Witness as W
 import Copilot.Compile.SBV.Common
 import Copilot.Compile.SBV.ACSLexpr
@@ -22,10 +23,11 @@
 import qualified Copilot.Core.PrettyDot as PD
 import qualified Text.PrettyPrint.HughesPJ as PJ
 
-import qualified Copilot.Core as C
+import Copilot.Core as C
 import Copilot.Core.Type.Equality ((=~=), coerce, cong)
 
-import qualified Data.SBV as S
+import qualified Data.SBV  as V
+import qualified Data.SBV.Tools.CodeGen as S
 
 import qualified Data.Map as M
 import Control.Monad (foldM)
@@ -40,6 +42,9 @@
 
 --------------------------------------------------------------------------------
 
+epsilon :: Double
+epsilon = 0.1
+
 updateStates :: MetaTable -> C.Spec -> [SBVFunc]
 updateStates meta (C.Spec streams _ _ _) =
   map updateStreamState streams
@@ -47,18 +52,17 @@
   where
   updateStreamState :: C.Stream -> SBVFunc
   updateStreamState C.Stream { C.streamId       = id
-                             , C.streamBuffer   = buffer
                              , C.streamExpr     = e
                              , C.streamExprType = t1
-                                                      } 
+                                                      }
     = mkSBVFunc (mkUpdateStFn id) $ do
-        S.cgAddDecl [("/*test 001*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")]
+        S.cgAddDecl [("/*test 001*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta e) ++ ") <= " ++ show epsilon ++ ";\n*/")]
         inputs <- mkInputs meta (c2Args e)
         let e' = c2sExpr inputs e
-        let Just strmInfo = M.lookup id (streamInfoMap meta) 
+        let Just strmInfo = M.lookup id (streamInfoMap meta)
         updateStreamState1 t1 e' strmInfo
 
-  updateStreamState1 :: C.Type a -> S.SBV a -> C.Stream -> S.SBVCodeGen ()
+  updateStreamState1 :: C.Type a -> V.SBV a -> C.Stream -> S.SBVCodeGen ()
   updateStreamState1 t1 e1 C.Stream { C.streamExprType = t2 }
     = do
     W.SymWordInst <- return (W.symWordInst t2)
@@ -82,7 +86,7 @@
     where
     mkSBVExp =
       do
-        S.cgAddDecl [("/*test 005*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")]
+        S.cgAddDecl [("/*test 005*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta e) ++ ") <= " ++ show epsilon ++ ";\n*/")]
         inputs <- mkInputs meta (c2Args e)
         let e' = c2sExpr inputs e
         W.SymWordInst <- return (W.symWordInst t)
@@ -105,7 +109,7 @@
     where
     go (i,e) = mkArgCall meta (mkTriggerArgFn i name) e
     mkSBVExp = do
-      S.cgAddDecl [("/*test 006*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False guard) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta guard) ++ ";\n*/")]
+      S.cgAddDecl [("/*test 006*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta guard) ++ ";\n*/")]
       inputs <- mkInputs meta (c2Args guard)
       let e = c2sExpr inputs guard
       S.cgReturn e
@@ -114,12 +118,12 @@
 
 mkArgCall :: MetaTable -> String -> C.UExpr -> SBVFunc
 mkArgCall meta fnCallName C.UExpr { C.uExprExpr = e
-                            , C.uExprType = t } 
+                            , C.uExprType = t }
   =
   mkSBVFunc fnCallName mkExpr
   where
   mkExpr = do
-    S.cgAddDecl [("/*test 003*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")]
+    S.cgAddDecl [("/*test 003*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta e) ++ ") <= " ++ show epsilon ++ ";\n*/")]
     inputs <- mkInputs meta (c2Args e)
     let e' = c2sExpr inputs e
     W.SymWordInst <- return (W.symWordInst t)
@@ -133,18 +137,18 @@
 getExtArrs :: MetaTable -> [SBVFunc]
 getExtArrs meta@(MetaTable { externArrInfoMap = arrs })
   = map mkIdx (M.toList arrs)
-  
+
   where
   mkIdx :: (Int, C.ExtArray) -> SBVFunc
   mkIdx (_, C.ExtArray { C.externArrayName    = name
                        , C.externArrayIdx     = idx
                        , C.externArrayIdxType = t    })
-    = 
+    =
     mkSBVFunc (mkExtArrFn name) mkSBVExpr
     where
     mkSBVExpr :: S.SBVCodeGen ()
     mkSBVExpr = do
-      S.cgAddDecl [("/*test 002*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False idx) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta idx) ++ ";\n*/")]
+      S.cgAddDecl [("/*test 002*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False idx) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta idx) ++ ") <= " ++ show epsilon ++ ";\n*/")]
       inputs <- mkInputs meta (c2Args idx)
       W.SymWordInst <- return (W.symWordInst t)
       W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
@@ -157,13 +161,13 @@
 getExtFuns :: MetaTable -> [SBVFunc]
 getExtFuns meta@(MetaTable { externFunInfoMap = exts })
   = concatMap mkExtF (M.toList exts)
-  
+
   where
   mkExtF :: (Int, C.ExtFun) -> [SBVFunc]
   mkExtF (_, C.ExtFun { C.externFunName = name
                       , C.externFunTag  = tag
                       , C.externFunArgs = args })
-    = 
+    =
     map go (mkArgIdx args)
     where
     go (i,e) = mkArgCall meta (mkExtFunArgFn i name tag) e
@@ -179,42 +183,42 @@
 -- (argToCall from MetaTable.hs).
 
 mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen Inputs
-mkInputs meta args = 
-  foldM argToInput (Inputs [] [] [] []) args 
+mkInputs meta args =
+  foldM argToInput (Inputs [] [] [] []) args
 
   where
   argToInput :: Inputs -> Arg -> S.SBVCodeGen Inputs
 
   -----------------------------------------
- 
+
   -- External variables
-  argToInput acc (Extern name) = 
+  argToInput acc (Extern name) =
     let extInfos = externVarInfoMap meta in
     let Just extInfo = M.lookup (name) extInfos in
     mkExtInput extInfo
 
-    where 
+    where
     mkExtInput :: C.ExtVar -> S.SBVCodeGen Inputs
     mkExtInput (C.ExtVar _ C.UType { C.uTypeType = t }) = do
       ext <- mkExtInput_ t (mkExtTmpVar name)
-      return acc { extVars = (name, (ExtInput { extInput = ext 
+      return acc { extVars = (name, (ExtInput { extInput = ext
                                               , extType  = t })
                              ) : extVars acc }
 
   -----------------------------------------
 
   -- External arrays
-  argToInput acc (ExternArr name tag) = 
+  argToInput acc (ExternArr name tag) =
     let extInfos = externArrInfoMap meta in
     let Just extInfo = M.lookup tag extInfos in
     mkExtInput extInfo
 
-    where 
+    where
     mkExtInput :: C.ExtArray -> S.SBVCodeGen Inputs
     mkExtInput C.ExtArray { C.externArrayElemType = t }
       = do
       v <- mkExtInput_ t (mkExtTmpTag name (Just tag))
-      return acc { extArrs = ((mkExtTmpTag name (Just tag)), ExtInput 
+      return acc { extArrs = ((mkExtTmpTag name (Just tag)), ExtInput
                                       { extInput  = v
                                       , extType   = t }
                              ) : extArrs acc }
@@ -222,7 +226,7 @@
   -----------------------------------------
 
   -- External functions
-  argToInput acc (ExternFun name tag) =
+  argToInput acc (T.ExternFun name tag) =
     let extInfos = externFunInfoMap meta in
     let Just extInfo = M.lookup tag extInfos in
     mkExtInput extInfo
@@ -232,7 +236,7 @@
     mkExtInput C.ExtFun { C.externFunType = t }
       = do
       v <- mkExtInput_ t (mkExtTmpTag name (Just tag))
-      return acc { extFuns = ((mkExtTmpTag name (Just tag)), ExtInput 
+      return acc { extFuns = ((mkExtTmpTag name (Just tag)), ExtInput
                                       { extInput = v
                                       , extType  = t }
                              ) : extFuns acc }
@@ -257,8 +261,8 @@
                                                     , arrType = t })
                              ) : extQues acc
                  }
-                   
-    mkQueInput_ :: C.Type a -> [a] -> S.SBVCodeGen [S.SBV a]
+
+    mkQueInput_ :: C.Type a -> [a] -> S.SBVCodeGen [V.SBV a]
     mkQueInput_ t que = do
       W.SymWordInst        <- return (W.symWordInst t)
       W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
@@ -267,7 +271,7 @@
 
 -----------------------------------------
 
-mkExtInput_ :: C.Type a -> String -> S.SBVCodeGen (S.SBV a)
+mkExtInput_ :: C.Type a -> String -> S.SBVCodeGen (V.SBV a)
 mkExtInput_ t name = do
   W.SymWordInst        <- return (W.symWordInst t)
   W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
diff --git a/src/Copilot/Compile/SBV/Copilot2SBV.hs b/src/Copilot/Compile/SBV/Copilot2SBV.hs
--- a/src/Copilot/Compile/SBV/Copilot2SBV.hs
+++ b/src/Copilot/Compile/SBV/Copilot2SBV.hs
@@ -12,7 +12,7 @@
   , ExtInput(..)
   , QueInput(..)
   , QueueIn(..)
-  ) 
+  )
 where
 
 import Prelude hiding (id)
@@ -46,17 +46,17 @@
   , extQues  :: [ExtQue] }
 
 -- External input -- variables, arrays, and functions
-data ExtInput = forall a. ExtInput 
+data ExtInput = forall a. ExtInput
   { extInput :: S.SBV a
   , extType  :: C.Type a }
 
 -- Stream queues
-data QueInput = forall a. QueInput 
+data QueInput = forall a. QueInput
   { arrInput :: QueueIn a }
 
 data QueueIn a = QueueIn
   { queue    :: [S.SBV a]
-  , quePtr   :: S.SBV Q.QueueSize 
+  , quePtr   :: S.SBV Q.QueueSize
   , arrType  :: C.Type a }
 
 --------------------------------------------------------------------------------
@@ -105,7 +105,7 @@
                                            , arrType = t2 } } =
       let Just p = t2 =~= t1 in
       case W.symWordInst t2 of
-        W.SymWordInst -> 
+        W.SymWordInst ->
           case W.hasSignAndSizeInst t2 of
             W.HasSignAndSizeInst ->
               coerce (cong p) (Q.lookahead i que' qPtr)
@@ -120,10 +120,8 @@
   ----------------------------------------------------
 
   C.Var t1 name ->
-    let Just local = M.lookup name env
-    in
-      case local of
-        Local
+    case M.lookup name env of
+      Just Local
           { localSBVExpr = e
           , localType    = t2
           } ->
@@ -132,10 +130,10 @@
 
   ----------------------------------------------------
 
-  C.ExternVar t name _ -> 
+  C.ExternVar t name _ ->
     getSBV t ext
 
-    where 
+    where
     ext :: ExtInput
     ext = lookupInput name (extVars inputs)
 
@@ -147,10 +145,10 @@
 
   ----------------------------------------------------
 
-  C.ExternArray _ t name _ _ _ tag -> 
+  C.ExternArray _ t name _ _ _ tag ->
     getSBV t getExtArr
 
-    where 
+    where
     getExtArr :: ExtInput
     getExtArr = lookupInput (mkExtTmpTag name (tag)) (extArrs inputs)
 
@@ -172,7 +170,7 @@
                        , extInput = v }
       = let Just p = t2 =~= t1 in
         coerce (cong p) v
- 
+
   ----------------------------------------------------
 
   C.Op1 op e ->
@@ -184,7 +182,7 @@
   C.Op2 op e1 e2 ->
     let res1 = c2sExpr_ e1 env inputs in
     let res2 = c2sExpr_ e2 env inputs in
-    c2sOp2 op res1 res2 
+    c2sOp2 op res1 res2
 
   ----------------------------------------------------
 
@@ -194,29 +192,29 @@
     let res3 = c2sExpr_ e3 env inputs in
     c2sOp3 op res1 res2 res3
 
-  C.Label t s e -> case W.symWordInst t of 
+  C.Label t s e -> case W.symWordInst t of
                        W.SymWordInst -> S.label s (c2sExpr_ e env inputs)
 
---------------------------------------------------------------------------------      
+--------------------------------------------------------------------------------
 
 noFloatOpsErr :: String -> a
-noFloatOpsErr op = 
-  badUsage ("The operation you used is not supported by the SBV backend: " 
+noFloatOpsErr op =
+  badUsage ("The operation you used is not supported by the SBV backend: "
          ++ "operator " ++ op ++ " not supported. Please change it with your math skills to something supported.")
 
---------------------------------------------------------------------------------      
+--------------------------------------------------------------------------------
 
 c2sOp1 :: C.Op1 a b -> S.SBV a -> S.SBV b
 c2sOp1 op = case op of
   Not     -> (S.bnot)
-  Abs   t -> case W.symWordInst t of 
-                       W.SymWordInst         -> abs 
-  Sign  t -> case W.symWordInst t of 
+  Abs   t -> case W.symWordInst t of
+                       W.SymWordInst         -> abs
+  Sign  t -> case W.symWordInst t of
                        W.SymWordInst         -> signum
-  BwNot t -> case W.bitsInst    t of 
+  BwNot t -> case W.bitsInst    t of
                        W.BitsInst            -> (S.complement)
 
-  Cast t0 t1 -> case W.castInst t0 t1 of 
+  Cast t0 t1 -> case W.castInst t0 t1 of
                   W.CastInst -> W.sbvCast
 
   Recip _      -> noFloatOpsErr "recip"
@@ -228,9 +226,9 @@
   Log   C.Float  -> log
   Log   C.Double -> log
   Sin   C.Float  -> sin
-  Sin   C.Double -> sin
+  Sin   C.Double -> S.uninterpret "sin"
   Cos   C.Float  -> cos
-  Cos   C.Double -> cos
+  Cos   C.Double -> S.uninterpret "cos"
   Tan   C.Float  -> tan
   Tan   C.Double -> tan
   Asin  C.Float  -> asin
@@ -269,30 +267,30 @@
   Lt    t -> case W.ordInst      t of W.OrdInst        ->  (S..<)
   Gt    t -> case W.ordInst      t of W.OrdInst        ->  (S..>)
 
-  Div   t -> case W.divInst      t of W.BVDivisibleInst  ->  
+  Div   t -> case W.divInst      t of W.BVDivisibleInst  ->
                                                   \x y -> fst (S.sQuotRem x y)
-  Mod   t -> case W.divInst      t of W.BVDivisibleInst  ->  
+  Mod   t -> case W.divInst      t of W.BVDivisibleInst  ->
                                                   \x y -> snd (S.sQuotRem x y)
 
   BwAnd t -> case W.bitsInst     t of W.BitsInst       -> (S..&.)
   BwOr  t -> case W.bitsInst     t of W.BitsInst       -> (S..|.)
   BwXor t -> case W.bitsInst     t of W.BitsInst       -> (S.xor)
-  BwShiftL tvec tidx -> 
-    case W.integralInst tvec of 
-      W.IntegralInst -> 
+  BwShiftL tvec tidx ->
+    case W.integralInst tvec of
+      W.IntegralInst ->
         \vec idx -> case (W.integralInst tidx) of
                       W.IntegralInst -> S.sShiftLeft vec idx
                                 --case S.unliteral idx of
                                  --        Nothing -> badUsage "Using the SBV backend, shiftL only supports constant shift indicies"
                                  --        Just x  -> S.shiftL vec (fromIntegral x)
-  BwShiftR tvec tidx -> 
-    case W.integralInst tvec of 
-      W.IntegralInst -> 
+  BwShiftR tvec tidx ->
+    case W.integralInst tvec of
+      W.IntegralInst ->
         \vec idx -> case (W.integralInst tidx) of
                       W.IntegralInst -> S.sShiftRight vec idx
 
---    case W.bitsInst tvec of 
---      W.BitsInst -> 
+--    case W.bitsInst tvec of
+--      W.BitsInst ->
 --        \vec idx -> case W.symWordInst tidx of
 --                      W.SymWordInst -> case S.unliteral idx of
 --                                         Nothing -> badUsage "Using the SBV backend, shiftR only supports constant shift indicies"
@@ -309,7 +307,7 @@
 c2sOp3 :: C.Op3 a b c d -> S.SBV a -> S.SBV b -> S.SBV c -> S.SBV d
 c2sOp3 op = case op of
   Mux t ->
-    case W.mergeableInst t of 
+    case W.mergeableInst t of
       W.MergeableInst -> \b c1 c2 -> S.ite b c1 c2
 
 
diff --git a/src/Copilot/Compile/SBV/Driver.hs b/src/Copilot/Compile/SBV/Driver.hs
--- a/src/Copilot/Compile/SBV/Driver.hs
+++ b/src/Copilot/Compile/SBV/Driver.hs
@@ -81,7 +81,7 @@
   wr (text "")
 
   wr copilot
-  
+
   wr (text "/* Idents */\n")
   wr (text "/*@\n assigns \\nothing;\n */\nSBool ident_bool(SBool a) {return a;}")
   wr (text "/*@\n assigns \\nothing;\n */\nSWord8 ident_word8(SWord8 a) {return a;}")
@@ -117,7 +117,7 @@
   testFn :: Doc
   testFn =
     mkFunc (withPrefix (prefix params) "testing")
-           (   text "for(;;) step()"<> semi
+           (   text "for(;;)" <> (text (withPrefix (prefix params)  "step()")) <> semi
            )
 
   copilot = vcat $ intersperse (text "")
@@ -126,7 +126,7 @@
     , updateObservers params meta
     , updateStates streams
     , updateBuffers meta
-    , updatePtrs meta 
+    , updatePtrs meta
     ]
 
 --------------------------------------------------------------------------------
@@ -141,12 +141,12 @@
 varDecls meta = vcat $ map varDecl (getVars meta)
 
   where
-  getVars :: MetaTable -> [Decl] 
-  getVars MetaTable { streamInfoMap    = streams 
-                    , externVarInfoMap = externs 
+  getVars :: MetaTable -> [Decl]
+  getVars MetaTable { streamInfoMap    = streams
+                    , externVarInfoMap = externs
                     , externArrInfoMap = externArrs
                     , externFunInfoMap = externFuns }
-    = 
+    =
        map getTmpStVars strLst
     ++ map getQueueVars strLst
     ++ map getQueuePtrVars (map fst strLst)
@@ -158,41 +158,41 @@
 
   getTmpStVars :: (C.Id, C.Stream) -> Decl
   getTmpStVars (id, C.Stream { C.streamExprType  = t
-                               , C.streamBuffer = que }) = 
+                               , C.streamBuffer = que }) =
     Decl (retType t) (text $ mkTmpStVar id) getFirst
-    where 
+    where
     -- ASSUME queue is nonempty!
     getFirst = text (cShow $ C.showWithType C.Haskell t (headErr que))
     headErr [] = C.impossible "headErr" "copilot-sbv"
     headErr xs = head xs
-  
+
   getQueueVars :: (C.Id, C.Stream) -> Decl
   getQueueVars (id, C.Stream { C.streamExprType = t
                              , C.streamBuffer = que }) =
-    Decl (retType t) 
+    Decl (retType t)
          (text (mkQueueVar id) <> lbrack <> int (length que) <> rbrack)
          getInits
-    where 
+    where
     getInits = lbrace <+> vals <+> rbrace
-      where 
-      vals = hcat $ punctuate (comma <> text " ") 
-                              (map (text . cShow . C.showWithType C.Haskell t) 
+      where
+      vals = hcat $ punctuate (comma <> text " ")
+                              (map (text . cShow . C.showWithType C.Haskell t)
                                    que)
 
   getQueuePtrVars :: C.Id -> Decl
-  getQueuePtrVars id = 
+  getQueuePtrVars id =
     Decl (retType queSize) (text $ mkQueuePtrVar id) (int 0)
-    where 
+    where
     queSize :: C.Type QueueSize
-    queSize = C.typeOf 
+    queSize = C.typeOf
 
   getExtVars :: (C.Name, C.ExtVar) -> Decl
-  getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) = 
+  getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) =
     Decl (retType t) (text $ mkExtTmpVar var) (int 0)
 
-  getExtArrs :: (Int, C.ExtArray) -> Decl 
+  getExtArrs :: (Int, C.ExtArray) -> Decl
   getExtArrs (_, C.ExtArray { C.externArrayName     = name
-                            , C.externArrayElemType = t 
+                            , C.externArrayElemType = t
                             , C.externArrayTag      = tag  })
     =
     Decl (retType t) (text $ mkExtTmpTag name tag) (int 0)
@@ -231,19 +231,19 @@
 sampleExts :: MetaTable -> Doc
 sampleExts MetaTable { externVarInfoMap = extVMap
                      , externArrInfoMap = extAMap
-                     , externFunInfoMap = extFMap } 
+                     , externFunInfoMap = extFMap }
   =
   -- Arrays and functions have to come after vars.  This is because we may use
   -- the assignment of extVars in the definition of extArrs.  The Analyzer.hs
   -- copilot-core prevents arrays or functions from being used in arrays or
   -- functions.
-  --extACSL $$ 
+  --extACSL $$
   (mkFunc ("static " ++ sampleExtsF) $ vcat (extVars ++ extArrs ++  extFuns))
 
   where
   --ll = sampleVExtACSL extVMap ++ sampleAExtACSL extAMap ++ sampleFExtACSL extFMap
   --extACSL = vcat [text "/*@",
---			(case ll of 
+--			(case ll of
   --			[] -> text " assigns \\nothing;"
 --			_ -> vcat $ ll)
 --			,text "*/"]
@@ -258,17 +258,17 @@
 -- Variables
 
 --sampleVExtACSL :: M.Map C.Name C.ExtVar -> [Doc]
---sampleVExtACSL extVMap = 
+--sampleVExtACSL extVMap =
 --  (map sampleVExtACSL1 ((fst . unzip . M.toList) extVMap)) ++ (map sampleVExtACSL2 ((fst . unzip . M.toList) extVMap))
 --sampleVExtACSL1 :: C.Name -> Doc
---sampleVExtACSL1 name = 
+--sampleVExtACSL1 name =
 --  text " assigns" <+> text (mkExtTmpVar name) <> semi
 --sampleVExtACSL2 :: C.Name -> Doc
---sampleVExtACSL2 name = 
+--sampleVExtACSL2 name =
 --  text " //ensures" <+> text (mkExtTmpVar name) <+> text "==" <+> text name <> semi
 
 sampleVExt :: C.Name -> Doc
-sampleVExt name = 
+sampleVExt name =
   text (mkExtTmpVar name) <+> equals <+> text name <> semi
 
 --------------------------------------------------------------------------------
@@ -278,55 +278,55 @@
 -- arrays or functions (i.e., an external array can't use another external array
 -- to compute it's index).
 --sampleAExtACSL :: M.Map C.Tag C.ExtArray -> [Doc]
---sampleAExtACSL extAMap = 
+--sampleAExtACSL extAMap =
 --  (map sampleAExtACSL1 (M.toList extAMap)) ++ (map sampleAExtACSL2 (M.toList extAMap))
 --
 --sampleAExtACSL1 :: (Int, C.ExtArray) -> Doc
 --sampleAExtACSL1 (_, C.ExtArray { C.externArrayName = name
---                          , C.externArrayIdx = idx 
+--                          , C.externArrayIdx = idx
 --                          , C.externArrayTag = t     })
---  = 
+--  =
 --  text " assigns" <+> text (mkExtTmpTag name t) <+> semi
 
 
 --sampleAExtACSL2 :: (Int, C.ExtArray) -> Doc
 --sampleAExtACSL2 (_, C.ExtArray { C.externArrayName = name
---                          , C.externArrayIdx = idx 
+--                          , C.externArrayIdx = idx
 --                          , C.externArrayTag = t     })
---  = 
+--  =
 --  text " //ensures" <+> text (mkExtTmpTag name t) <+> text "==" <+> text ("tmp_"++(mkExtTmpTag name t)) <> semi
 
 --sampleAExt1 :: (Int, C.ExtArray) -> Doc
 --sampleAExt1 (_, C.ExtArray { C.externArrayName = name
---                          , C.externArrayIdx = idx 
---			  , C.externArrayElemType = tttt 
+--                          , C.externArrayIdx = idx
+--			  , C.externArrayElemType = tttt
 --                          , C.externArrayTag = t     })
 --  = (retType tttt) <+> text ("tmp_"++(mkExtTmpTag name t)) <+> equals <+> arrIdx name idx
--- 
---  where 
+--
+--  where
 --  arrIdx :: C.Name -> C.Expr a -> Doc
 --  arrIdx name' e = text name' <> lbrack <> idxFCall e <> rbrack <> semi
 
   -- Ok, because the analyzer disallows arrays or function calls in index
   -- expressions, and we assign all variables before arrays.
 --  idxFCall :: C.Expr a -> Doc
---  idxFCall e = 
+--  idxFCall e =
 --    mkFuncCall (mkExtArrFn name) (map text $ collectArgs e)
 
 sampleAExt :: (Int, C.ExtArray) -> Doc
 sampleAExt (_, C.ExtArray { C.externArrayName = name
-                          , C.externArrayIdx = idx 
-			  , C.externArrayElemType = tttt 
+                          , C.externArrayIdx = idx
+			  , C.externArrayElemType = tttt
                           , C.externArrayTag = t     })
   = text (mkExtTmpTag name t) <+> equals <+> arrIdx name idx <> semi
-  where 
+  where
   arrIdx :: C.Name -> C.Expr a -> Doc
   arrIdx name' e = text name' <> lbrack <> idxFCall e <> rbrack <> semi
 
   -- Ok, because the analyzer disallows arrays or function calls in index
   -- expressions, and we assign all variables before arrays.
   idxFCall :: C.Expr a -> Doc
-  idxFCall e = 
+  idxFCall e =
     mkFuncCall (mkExtArrFn name) (map text $ collectArgs e)
 
 --------------------------------------------------------------------------------
@@ -337,46 +337,46 @@
 
 --sampleFExtACSL1 :: (Int, C.ExtFun) -> Doc
 --sampleFExtACSL1 (_, C.ExtFun { C.externFunName = name
---                        , C.externFunArgs = args 
+--                        , C.externFunArgs = args
 --                        , C.externFunTag  = tag  })
---  = 
+--  =
 --  text " assigns" <+> text (mkExtTmpTag name tag) <> semi
 --sampleFExtACSL2 :: (Int, C.ExtFun) -> Doc
 --sampleFExtACSL2 (_, C.ExtFun { C.externFunName = name
---                        , C.externFunArgs = args 
+--                        , C.externFunArgs = args
 --                        , C.externFunTag  = tag  })
---  = 
+--  =
 --  text " //ensures" <+> text (mkExtTmpTag name tag) <+> text "==" <+> text ("tmp_"++(mkExtTmpTag name tag)) <> semi
 
 
 -- External functions
 --sampleFExt1 :: (Int, C.ExtFun) -> Doc
 --sampleFExt1 (_, C.ExtFun { C.externFunName = name
---                        , C.externFunArgs = args 
+--                        , C.externFunArgs = args
 --                        , C.externFunType = tttt
 --                        , C.externFunTag  = tag  })
---  = 
+--  =
 --  (retType tttt) <+> text ("tmp_"++(mkExtTmpTag name tag)) <+> equals <+> text name <> lparen
 --    <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args))
 --    <> rparen <> semi
 --
 --     where
---     mkArgCall :: (Int, C.UExpr) -> Doc 
---     mkArgCall (i, C.UExpr { C.uExprExpr = e }) = 
+--     mkArgCall :: (Int, C.UExpr) -> Doc
+--     mkArgCall (i, C.UExpr { C.uExprExpr = e }) =
 --       mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e)
 
 sampleFExt :: (Int, C.ExtFun) -> Doc
 sampleFExt (_, C.ExtFun { C.externFunName = name
-                        , C.externFunArgs = args 
+                        , C.externFunArgs = args
                         , C.externFunType = tttt
                         , C.externFunTag  = tag  })
-  = 
+  =
   text (mkExtTmpTag name tag) <+> equals <+> text name <> lparen
     <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args))
     <> rparen <> semi
   where
-     mkArgCall :: (Int, C.UExpr) -> Doc 
-     mkArgCall (i, C.UExpr { C.uExprExpr = e }) = 
+     mkArgCall :: (Int, C.UExpr) -> Doc
+     mkArgCall (i, C.UExpr { C.uExprExpr = e }) =
        mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e)
 
 --------------------------------------------------------------------------------
@@ -412,7 +412,7 @@
 --------------------------------------------------------------------------------
 
 updateObservers :: Params -> MetaTable -> Doc
-updateObservers params MetaTable { observerInfoMap = observers } 
+updateObservers params MetaTable { observerInfoMap = observers }
   = let ll = M.toList observers
   in (case ll of
   [] -> text "/*@\n assigns \\nothing;\n */"
@@ -432,7 +432,7 @@
 --------------------------------------------------------------------------------
 
 fireTriggers :: MetaTable -> Doc
-fireTriggers MetaTable { triggerInfoMap = triggers } 
+fireTriggers MetaTable { triggerInfoMap = triggers }
   = -- text "/*@\n assigns \\nothing; \n*/" $$
   (mkFunc ("static " ++ triggersF) $ vcat $ map fireTrig (M.toList triggers))
 
@@ -440,14 +440,14 @@
   -- if (guard) trigger(args);
   fireTrig :: (C.Name, TriggerInfo) -> Doc
   fireTrig (name, TriggerInfo { guardArgs      = gArgs
-                              , triggerArgArgs = argArgs }) 
-    = 
+                              , triggerArgArgs = argArgs })
+    =
     text "if" <+> lparen <> guardF <> rparen $+$ nest 2 f
 
     where
-    f = text name <> lparen 
-          <> vcat (punctuate comma $ map mkArg (mkArgIdx argArgs)) 
-          <> rparen <> semi 
+    f = text name <> lparen
+          <> vcat (punctuate comma $ map mkArg (mkArgIdx argArgs))
+          <> rparen <> semi
 
     guardF :: Doc
     guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs)
@@ -460,14 +460,14 @@
 writeACSLqueues :: MetaTable -> Doc
 writeACSLqueues MetaTable { streamInfoMap = strMap } =
   let ll = M.toList strMap
-  in 
+  in
 
   vcat $ (text "/*ACSL following*/\n"):(case ll of
   [] -> [text ""]
   _ -> (text "/*@" :(map varAndUpdate (ll) ++ [(text "*/")]))
-  ) 
+  )
 
-  where 
+  where
   varAndUpdate :: (C.Id, C.Stream) -> Doc
   varAndUpdate (id, C.Stream { C.streamBuffer = que }) =
     updateFunc (mkQueueVar id) (fromIntegral $ length que) (mkQueuePtrVar id)
@@ -482,7 +482,7 @@
 --------------------------------------------------------------------------------
 
 updateBuffers :: MetaTable -> Doc
-updateBuffers MetaTable { streamInfoMap = strMap } 
+updateBuffers MetaTable { streamInfoMap = strMap }
   = let ll = M.toList strMap
   in (case ll of
   [] -> text "/*@\n assigns \\nothing;\n */"
@@ -522,7 +522,7 @@
   )$$
   (mkFunc ("static " ++ updatePtrsF) $ vcat $ map varAndUpdate (ll))
 
-  where 
+  where
 
   varAndUpdateACSL :: (C.Id, C.Stream) -> Doc
   varAndUpdateACSL (id, C.Stream { C.streamBuffer = que }) =
@@ -531,8 +531,8 @@
   -- idx = (idx + 1) % queueSize;
   updateFuncACSL :: QueueSize -> String -> Doc
   updateFuncACSL sz ptr =
-    text " assigns" <+> text ptr <> semi <> (text "\n ensures" <+> text ptr <+> text "==" 
-      <+> lparen <> text "\\old (" <> text ptr <+> text ") +" <+> int 1 <> rparen 
+    text " assigns" <+> text ptr <> semi <> (text "\n ensures" <+> text ptr <+> text "=="
+      <+> lparen <> text "\\old (" <> text ptr <+> text ") +" <+> int 1 <> rparen
       <+> text "%" <+> int (fromIntegral sz) <> semi <> text "\n")
 
 
@@ -543,8 +543,8 @@
   -- idx = (idx + 1) % queueSize;
   updateFunc :: QueueSize -> String -> Doc
   updateFunc sz ptr =
-    text ptr <+> equals 
-      <+> lparen <> text ptr <+> text "+" <+> int 1 <> rparen 
+    text ptr <+> equals
+      <+> lparen <> text ptr <+> text "+" <+> int 1 <> rparen
       <+> text "%" <+> int (fromIntegral sz) <> semi
 
 --------------------------------------------------------------------------------
@@ -578,4 +578,4 @@
     C.Float  -> "SFloat"
     C.Double -> "SDouble"
 
-    _          -> C.badUsage "You've tried to compile a Copilot program to SBV with a type SBV does not support.  SBV does not support floats or doubles.  To compile programs using these types, use the copilot-c99 (Atom) backend.  See README.md for more information."
+    _          -> C.badUsage "You've tried to compile a Copilot program to SBV with a type SBV does not support.  To compile programs using these types, use the copilot-c99 (Atom) backend.  See README.md for more information."
diff --git a/src/Copilot/Compile/SBV/Transform.hs b/src/Copilot/Compile/SBV/Transform.hs
--- a/src/Copilot/Compile/SBV/Transform.hs
+++ b/src/Copilot/Compile/SBV/Transform.hs
@@ -6,7 +6,7 @@
 
 module Copilot.Compile.SBV.Transform
   ( transform
-  ) 
+  )
 where
 
 import Prelude hiding (id)
@@ -86,8 +86,8 @@
 --data Property = Property
 --  { propertyName     :: Name
 --  , propertyExpr     :: Expr Bool }
-  
 
+
 transformProperty :: Property -> Property
 transformProperty Property
   { propertyName     = name
@@ -99,7 +99,7 @@
 --------------------------------------------------------------------------------
 
 -- | A Copilot specification consists of a list of variables bound to anonymous
--- streams, a lost of anomymous streams, a list of observers, and a list of
+-- streams, a list of anomymous streams, a list of observers, and a list of
 -- triggers.
 --data Spec = Spec
 --  { specStreams      :: [Stream]
@@ -128,14 +128,9 @@
 --  { uExprType :: Type a
 --  , uExprExpr :: Expr a }
 transformUExpr :: UExpr -> UExpr
-transformUExpr UExpr { uExprExpr = e, uExprType = t } = 
+transformUExpr UExpr { uExprExpr = e, uExprType = t } =
   UExpr { uExprExpr = transformExpr e, uExprType = t }
 
-transformSExpr :: (Name, UExpr) -> (Name, UExpr)
-transformSExpr (name, UExpr { uExprExpr = e, uExprType = t }) =
-  (name, transformUExpr UExpr { uExprExpr = e, uExprType = t })
-
-
 --------------------------------------------------------------------------------
 -- Expr transformation
 --
@@ -147,46 +142,32 @@
 --  Const        :: Type a -> a -> Expr a
 --  Drop         :: Type a -> DropIdx -> Id -> Expr a
 --  Local        :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
---  Var          :: Type a -> Name -> Expr a 
---  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a 
---  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a) 
+--  Var          :: Type a -> Name -> Expr a
+--  ExternVar    :: Type a -> Name -> Maybe [a] -> Expr a
+--  ExternFun    :: Type a -> Name -> [UExpr] -> Maybe (Expr a)
 --               -> Maybe Tag -> Expr a
 --  ExternArray  :: Integral a => Type a -> Type b -> Name -> Int -> Expr a
---               -> Maybe [[b]] -> Maybe Tag -> Expr b 
---  Op1          :: Op1 a b -> Expr a -> Expr b 
+--               -> Maybe [[b]] -> Maybe Tag -> Expr b
+--  Op1          :: Op1 a b -> Expr a -> Expr b
 --  Op2          :: Op2 a b c -> Expr a -> Expr b -> Expr c
 --  Op3          :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
 
-transformExpr :: Expr a -> Expr a 
+transformExpr :: Expr a -> Expr a
 transformExpr e0 = case e0 of
   Const t x                      -> Const t x
   Drop t k id                    -> Drop t k id
-  Local t1 t2 name e1 e2         -> Local t1 t2 name (transformExpr e1) (transformExpr e2) 
+  Local t1 t2 name e1 e2         -> Local t1 t2 name (transformExpr e1) (transformExpr e2)
   Var t name                     -> Var t name
   ExternVar t name e             -> ExternVar t name e
   ExternFun t name args contxt yy-> ExternFun t name (map transformUExpr args) contxt yy
-  ExternArray t1 t2 name 
+  ExternArray t1 t2 name
               size idx context yy-> ExternArray t1 t2 name size (transformExpr idx) context yy
   Op1 op e                       -> transformOp1 op e
   Op2 op e1 e2                   -> transformOp2 op e1 e2
   Op3 op e1 e2 e3                -> transformOp3 op e1 e2 e3
 
   Label t s e                    -> Label t s $ transformExpr e
-    
 
-{-showType :: Type a -> String
-showType t = case t of
-  Bool  -> "bool"
-  Int8  -> "int8"
-  Int16 -> "int16"
-  Int32 -> "int32"
-  Int64 -> "int64"
-  Word8 -> "word8"
-  Word16-> "word16"
-  Word32-> "word32"
-  Word64-> "word64"
-  Float -> "float"
-  Double-> "double"-}
 
 transformOp1 :: Op1 a b -> Expr a -> Expr b
 transformOp1 op e = case op of
@@ -198,66 +179,66 @@
   -- Fractional operators.
   Recip a      -> Op2 (Fdiv a) (Const a 1.0) (transformExpr e)
   -- Floating operators.
-  Exp Float    -> ExternFun Float "expf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Exp Double   -> ExternFun Double "exp" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Sqrt Float   -> ExternFun Float "sqrtf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Sqrt Double  -> ExternFun Double "sqrt" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Log Float    -> ExternFun Float "logf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Log Double   -> ExternFun Double "log" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Sin Float    -> ExternFun Float "sinf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Sin Double   -> ExternFun Double "sin" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Cos Float    -> ExternFun Float "cosf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Cos Double   -> ExternFun Double "cos" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Tan Float    -> ExternFun Float "tanf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Tan Double   -> ExternFun Double "tan" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Asin Float   -> ExternFun Float "asinf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Asin Double  -> ExternFun Double "asin" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Acos Float   -> ExternFun Float "acosf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Acos Double  -> ExternFun Double "acos" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Atan Float   -> ExternFun Float "atanf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Atan Double  -> ExternFun Double "atan" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Sinh Float   -> ExternFun Float "sinhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Sinh Double  -> ExternFun Double "sinh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Cosh Float   -> ExternFun Float "coshf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Cosh Double  -> ExternFun Double "cosh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Tanh Float   -> ExternFun Float "tanhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Tanh Double  -> ExternFun Double "tanh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Asinh Float  -> ExternFun Float "asinhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Asinh Double -> ExternFun Double "asinh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Acosh Float  -> ExternFun Float "acoshf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Acosh Double -> ExternFun Double "acosh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
-  Atanh Float  -> ExternFun Float "atanhf" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
-  Atanh Double -> ExternFun Double "atanh" 
-                    [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Exp Float    -> ExternFun Float "expf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Exp Double   -> ExternFun Double "exp"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Sqrt Float   -> ExternFun Float "sqrtf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Sqrt Double  -> ExternFun Double "sqrt"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Log Float    -> ExternFun Float "logf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Log Double   -> ExternFun Double "log"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Sin Float    -> ExternFun Float "sinf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Sin Double   -> ExternFun Double "sin"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Cos Float    -> ExternFun Float "cosf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Cos Double   -> ExternFun Double "cos"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Tan Float    -> ExternFun Float "tanf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Tan Double   -> ExternFun Double "tan"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Asin Float   -> ExternFun Float "asinf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Asin Double  -> ExternFun Double "asin"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Acos Float   -> ExternFun Float "acosf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Acos Double  -> ExternFun Double "acos"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Atan Float   -> ExternFun Float "atanf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Atan Double  -> ExternFun Double "atan"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Sinh Float   -> ExternFun Float "sinhf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Sinh Double  -> ExternFun Double "sinh"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Cosh Float   -> ExternFun Float "coshf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Cosh Double  -> ExternFun Double "cosh"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Tanh Float   -> ExternFun Float "tanhf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Tanh Double  -> ExternFun Double "tanh"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Asinh Float  -> ExternFun Float "asinhf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Asinh Double -> ExternFun Double "asinh"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Acosh Float  -> ExternFun Float "acoshf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Acosh Double -> ExternFun Double "acosh"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
+  -- Atanh Float  -> ExternFun Float "atanhf"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing
+  -- Atanh Double -> ExternFun Double "atanh"
+  --                   [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing
   -- Bitwise operators.
   BwNot    t   -> Op1 (BwNot t) $ transformExpr e
   -- Casting operator.
@@ -278,11 +259,11 @@
   -- Fractional operators.
   Fdiv   t     -> Op2 (Fdiv t) (transformExpr e1) (transformExpr e2)
   -- Floating operators.
-  Pow    Float -> ExternFun Float "powf" 
-                    [UExpr { uExprExpr = transformExpr e1, uExprType = Float } 
+  Pow    Float -> ExternFun Float "powf"
+                    [UExpr { uExprExpr = transformExpr e1, uExprType = Float }
                     , UExpr { uExprExpr = transformExpr e2, uExprType = Float }] Nothing Nothing
-  Pow    Double-> ExternFun Double "pow" 
-                    [UExpr { uExprExpr = transformExpr e1, uExprType = Double } 
+  Pow    Double-> ExternFun Double "pow"
+                    [UExpr { uExprExpr = transformExpr e1, uExprType = Double }
                     , UExpr { uExprExpr = transformExpr e2, uExprType = Double }] Nothing Nothing
   Logb   t     -> Op2 (Fdiv t) (transformExpr $ Op1 (Log t) e1) (transformExpr $ Op1 (Log t) e2)
   -- Equality operators.
@@ -302,5 +283,5 @@
 
 
 transformOp3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
-transformOp3 op e1 e2 e3 = case op of 
-  Mux   t      -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3) 
+transformOp3 op e1 e2 e3 = case op of
+  Mux   t      -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3)