diff --git a/cryptol.cabal b/cryptol.cabal
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -1,5 +1,5 @@
 Name:                cryptol
-Version:             2.2.2
+Version:             2.2.3
 Synopsis:            Cryptol: The Language of Cryptography
 Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
 License:             BSD3
@@ -23,7 +23,7 @@
 source-repository this
   type:     git
   location: https://github.com/GaloisInc/cryptol.git
-  tag:      v2.2.2
+  tag:      v2.2.3
 
 flag static
   default: False
@@ -56,7 +56,7 @@
                        process         >= 1.2,
                        QuickCheck      >= 2.7,
                        random          >= 1.0.1,
-                       sbv             >= 4.2 && < 4.3,
+                       sbv             >= 4.3,
                        smtLib          >= 1.0.7,
                        syb             >= 0.4,
                        text            >= 1.1,
@@ -138,7 +138,6 @@
                        Cryptol.Testing.Random,
 
                        Cryptol.Symbolic,
-                       Cryptol.Symbolic.BitVector,
                        Cryptol.Symbolic.Prims,
                        Cryptol.Symbolic.Value,
 
@@ -152,8 +151,9 @@
                        Paths_cryptol,
                        GitRev
 
+  default-extensions:  CPP
   GHC-options:         -Wall -O2
-  ghc-prof-options: -fprof-auto -prof
+  ghc-prof-options:    -fprof-auto -prof
 
   if flag(relocatable)
       cpp-options: -DRELOCATABLE
@@ -185,8 +185,9 @@
                      , sbv
                      , tf-random
                      , transformers
+  default-extensions:  CPP
   GHC-options:         -Wall -O2
-  ghc-prof-options: -auto-all -prof -rtsopts
+  ghc-prof-options:    -auto-all -prof -rtsopts
 
   if os(linux) && flag(static)
       ld-options:      -static -pthread
diff --git a/cryptol/Main.hs b/cryptol/Main.hs
--- a/cryptol/Main.hs
+++ b/cryptol/Main.hs
@@ -27,13 +27,16 @@
 import Paths_cryptol (version)
 
 import Data.Version (showVersion)
-import Data.Monoid (mconcat)
 import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
 import System.Environment (getArgs, getProgName, lookupEnv)
 import System.Exit (exitFailure)
 import System.FilePath (searchPathSeparator, splitSearchPath, takeDirectory)
+
+#if __GLASGOW_HASKELL__ < 710
+import Data.Monoid (mconcat)
+#endif
 
 data Options = Options
   { optLoad            :: [FilePath]
diff --git a/cryptol/OptParser.hs b/cryptol/OptParser.hs
--- a/cryptol/OptParser.hs
+++ b/cryptol/OptParser.hs
@@ -9,7 +9,11 @@
 
 module OptParser where
 
-import Data.Monoid (Endo(..),Monoid(..))
+import Data.Monoid (Endo(..))
+
+#if __GLASGOW_HASKELL__ < 710
+import Data.Monoid (Monoid(..))
+#endif
 
 data OptParser opt
   = OptSuccess (Endo opt)
diff --git a/dist/build/Cryptol/Parser.hs b/dist/build/Cryptol/Parser.hs
--- a/dist/build/Cryptol/Parser.hs
+++ b/dist/build/Cryptol/Parser.hs
@@ -3735,6 +3735,27 @@
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 {-# LINE 1 "<built-in>" #-}
+{-# LINE 19 "<built-in>" #-}
+{-# LINE 1 "/usr/local/Cellar/ghc/7.10.1/lib/ghc-7.10.1/include/ghcversion.h" #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{-# LINE 20 "<built-in>" #-}
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 -- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp 
 
diff --git a/dist/build/Cryptol/Parser/Lexer.hs b/dist/build/Cryptol/Parser/Lexer.hs
--- a/dist/build/Cryptol/Parser/Lexer.hs
+++ b/dist/build/Cryptol/Parser/Lexer.hs
@@ -257,6 +257,27 @@
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 {-# LINE 1 "<built-in>" #-}
+{-# LINE 18 "<built-in>" #-}
+{-# LINE 1 "/usr/local/Cellar/ghc/7.10.1/lib/ghc-7.10.1/include/ghcversion.h" #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{-# LINE 19 "<built-in>" #-}
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 -- -----------------------------------------------------------------------------
 -- ALEX TEMPLATE
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@@ -29,9 +29,11 @@
 import Cryptol.Prims.Eval
 
 import Data.List (transpose)
-import Data.Monoid (Monoid(..),mconcat)
 import qualified Data.Map as Map
 
+#if __GLASGOW_HASKELL__ < 710
+import Data.Monoid (Monoid(..),mconcat)
+#endif
 
 -- Expression Evaluation -------------------------------------------------------
 
diff --git a/src/Cryptol/Eval/Env.hs b/src/Cryptol/Eval/Env.hs
--- a/src/Cryptol/Eval/Env.hs
+++ b/src/Cryptol/Eval/Env.hs
@@ -15,9 +15,11 @@
 import Cryptol.TypeCheck.AST
 import Cryptol.Utils.PP
 
-import           Data.Monoid (Monoid(..))
 import qualified Data.Map as Map
 
+#if __GLASGOW_HASKELL__ < 710
+import           Data.Monoid (Monoid(..))
+#endif
 
 -- Evaluation Environment ------------------------------------------------------
 
@@ -62,6 +64,3 @@
 -- | Lookup a type variable.
 lookupType :: TVar -> EvalEnv -> Maybe TValue
 lookupType p env = Map.lookup p (envTypes env)
-
-
-
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -33,7 +33,6 @@
 import Control.DeepSeq
 import qualified Control.Exception as X
 import Control.Monad (unless)
-import Data.Foldable (foldMap)
 import Data.Function (on)
 import Data.List (nubBy)
 import Data.Maybe (mapMaybe,fromMaybe)
@@ -48,6 +47,10 @@
                        )
 import qualified System.IO.Error as IOE
 import qualified Data.Map as Map
+
+#if __GLASGOW_HASKELL__ < 710
+import Data.Foldable (foldMap)
+#endif
 
 -- Renaming --------------------------------------------------------------------
 
diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs
--- a/src/Cryptol/ModuleSystem/Env.hs
+++ b/src/Cryptol/ModuleSystem/Env.hs
@@ -26,11 +26,15 @@
 import Data.Foldable (fold)
 import Data.Function (on)
 import qualified Data.Map as Map
-import Data.Monoid ((<>), Monoid(..))
+import Data.Monoid ((<>))
 import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
 import System.Environment(getExecutablePath)
 import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory)
 import qualified Data.List as List
+
+#if __GLASGOW_HASKELL__ < 710
+import Data.Monoid (Monoid(..))
+#endif
 
 -- Module Environment ----------------------------------------------------------
 
diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs
--- a/src/Cryptol/ModuleSystem/Interface.hs
+++ b/src/Cryptol/ModuleSystem/Interface.hs
@@ -24,8 +24,10 @@
 import           Cryptol.TypeCheck.AST
 
 import qualified Data.Map as Map
-import           Data.Monoid (Monoid(..))
 
+#if __GLASGOW_HASKELL__ < 710
+import           Data.Monoid (Monoid(..))
+#endif
 
 -- | The resulting interface generated by a module that has been typechecked.
 data Iface = Iface
diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs
--- a/src/Cryptol/ModuleSystem/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Monad.hs
@@ -25,12 +25,14 @@
 import           Cryptol.Parser.Position (Range)
 import           Cryptol.Utils.PP
 
-import Control.Applicative (Applicative(..))
 import Control.Exception (IOException)
 import Data.Function (on)
 import Data.Maybe (isJust)
 import MonadLib
 
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative (Applicative(..))
+#endif
 
 -- Errors ----------------------------------------------------------------------
 
diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs
--- a/src/Cryptol/ModuleSystem/NamingEnv.hs
+++ b/src/Cryptol/ModuleSystem/NamingEnv.hs
@@ -16,12 +16,14 @@
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic (panic)
 
+import qualified Data.Map as Map
+
+#if __GLASGOW_HASKELL__ < 710
 import Control.Applicative (Applicative, (<$>), (<*>))
 import Data.Monoid (Monoid(..))
 import Data.Foldable (foldMap)
 import Data.Traversable (traverse)
-import qualified Data.Map as Map
-
+#endif
 
 -- Name Locations --------------------------------------------------------------
 
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -26,13 +26,15 @@
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.PP
 
+import MonadLib
+import qualified Data.Map as Map
+
+#if __GLASGOW_HASKELL__ < 710
 import Control.Applicative(Applicative(..),(<$>))
 import Data.Foldable (foldMap)
 import Data.Monoid (Monoid(..))
 import Data.Traversable (traverse)
-import MonadLib
-import qualified Data.Map as Map
-
+#endif
 
 -- Errors ----------------------------------------------------------------------
 
diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs
--- a/src/Cryptol/Parser/AST.hs
+++ b/src/Cryptol/Parser/AST.hs
@@ -68,8 +68,11 @@
 import           Data.List(intersperse)
 import           Data.Bits(shiftR)
 import           Data.Maybe (catMaybes)
-import           Data.Monoid (Monoid(..))
 import           Numeric(showIntAtBase)
+
+#if __GLASGOW_HASKELL__ < 710
+import           Data.Monoid (Monoid(..))
+#endif
 
 -- | Module names are just namespaces.
 --
diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs
--- a/src/Cryptol/Parser/NoPat.hs
+++ b/src/Cryptol/Parser/NoPat.hs
@@ -21,12 +21,14 @@
 import Cryptol.Utils.Panic(panic)
 
 import           MonadLib
-import           Control.Applicative(Applicative(..),(<$>))
 import           Data.Maybe(maybeToList)
 import           Data.Either(partitionEithers)
 import qualified Data.Map as Map
-import           Data.Traversable(traverse)
 
+#if __GLASGOW_HASKELL__ < 710
+import           Control.Applicative(Applicative(..),(<$>))
+import           Data.Traversable(traverse)
+#endif
 
 class RemovePatterns t where
   -- | Eliminate all patterns in a program.
diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs
--- a/src/Cryptol/Parser/ParserUtils.hs
+++ b/src/Cryptol/Parser/ParserUtils.hs
@@ -19,10 +19,14 @@
 
 import Data.Maybe(listToMaybe,fromMaybe)
 import Data.Bits(testBit,setBit)
-import Control.Applicative ((<$>),Applicative(..))
 import Control.Monad(liftM,ap)
-import qualified Data.Traversable as T (mapM)
 
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative ((<$>),Applicative(..))
+import Data.Traversable (mapM)
+import Prelude hiding (mapM)
+#endif
+
 parse :: Config -> ParseM a -> String -> Either ParseError a
 parse cfg p cs    = case unP p cfg eofPos (S toks) of
                       Left err    -> Left err
@@ -220,8 +224,8 @@
 
 eFromTo :: Range -> Expr -> Maybe Expr -> Maybe Expr -> ParseM Expr
 eFromTo r e1 e2 e3 = EFromTo <$> exprToNumT r e1
-                             <*> T.mapM (exprToNumT r) e2
-                             <*> T.mapM (exprToNumT r) e3
+                             <*> mapM (exprToNumT r) e2
+                             <*> mapM (exprToNumT r) e3
 exprToNumT :: Range -> Expr -> ParseM Type
 exprToNumT r expr =
   case translateExprToNumT expr of
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -56,7 +56,6 @@
 import qualified Cryptol.Transform.Specialize as S
 import qualified Cryptol.Symbolic as Symbolic
 
-import Control.Applicative ((<$>))
 import Control.DeepSeq
 import qualified Control.Exception as X
 import Control.Monad (guard,unless,forM_,when)
@@ -64,7 +63,7 @@
 import Data.Function (on)
 import Data.List (intercalate,isPrefixOf,nub)
 import Data.Maybe (fromMaybe,mapMaybe)
-import Data.Monoid (mempty)
+import System.Environment (lookupEnv)
 import System.Exit (ExitCode(ExitSuccess))
 import System.Process (shell,createProcess,waitForProcess)
 import qualified System.Process as Process(runCommand)
@@ -76,35 +75,9 @@
 import System.Random.TF(newTFGen)
 import Numeric (showFFloat)
 
-#if __GLASGOW_HASKELL__ < 706
-import Control.Monad (liftM)
-import qualified Text.ParserCombinators.ReadP as P
-import Text.Read hiding (step)
-import System.Environment (getEnvironment)
-
-lookupEnv :: String -> IO (Maybe String)
-lookupEnv key = lookup key `liftM` getEnvironment
-
-readEither :: Read a => String -> Either String a
-readEither s =
-  case [ x | (x,"") <- readPrec_to_S read' minPrec s ] of
-    [x] -> Right x
-    []  -> Left "Prelude.read: no parse"
-    _   -> Left "Prelude.read: ambiguous parse"
- where
-  read' =
-    do x <- readPrec
-       lift P.skipSpaces
-       return x
-
--- | Parse a string using the 'Read' instance.
--- Succeeds if there is exactly one valid result.
-readMaybe :: Read a => String -> Maybe a
-readMaybe s = case readEither s of
-                Left _  -> Nothing
-                Right a -> Just a
-#else
-import System.Environment (lookupEnv)
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative ((<$>))
+import Data.Monoid (mempty)
 #endif
 
 -- Commands --------------------------------------------------------------------
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -82,21 +82,23 @@
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Symbolic (proverNames, lookupProver)
 
-import Control.Applicative ((<$>), Applicative(..))
 import Control.Monad (ap,unless,when)
 import Data.IORef
     (IORef,newIORef,readIORef,modifyIORef)
 import Data.List (intercalate, isPrefixOf)
 import Data.Maybe (catMaybes)
-import Data.Monoid (Monoid(..))
 import Data.Typeable (Typeable)
 import System.Directory (findExecutable)
 import qualified Control.Exception as X
 import qualified Data.Map as Map
 import Text.Read (readMaybe)
 
-import qualified Data.SBV as SBV (sbvCheckSolverInstallation)
+import Data.SBV.Dynamic (sbvCheckSolverInstallation)
 
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative ((<$>), Applicative(..))
+import Data.Monoid (Monoid(..))
+#endif
 
 -- REPL Environment ------------------------------------------------------------
 
@@ -563,7 +565,7 @@
     | s `notElem` proverNames     -> return $ Just $ "Prover must be " ++ proverListString
     | s `elem` ["offline", "any"] -> return Nothing
     | otherwise                   -> do let prover = lookupProver s
-                                        available <- SBV.sbvCheckSolverInstallation prover
+                                        available <- sbvCheckSolverInstallation prover
                                         unless available $
                                           putStrLn $ "Warning: " ++ s ++ " installation not found"
                                         return Nothing
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -12,22 +12,18 @@
 
 module Cryptol.Symbolic where
 
-import Control.Applicative
 import Control.Monad (replicateM, when, zipWithM)
 import Control.Monad.IO.Class
 import Data.List (transpose, intercalate)
 import qualified Data.Map as Map
 import Data.Maybe
-import Data.Monoid (Monoid(..))
-import Data.Traversable (traverse)
 import qualified Control.Exception as X
 
-import qualified Data.SBV as SBV
+import qualified Data.SBV.Dynamic as SBV
 
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.Env as M
 
-import Cryptol.Symbolic.BitVector
 import Cryptol.Symbolic.Prims
 import Cryptol.Symbolic.Value
 
@@ -39,6 +35,12 @@
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)
 
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+import Data.Monoid (Monoid(..))
+import Data.Traversable (traverse)
+#endif
+
 -- External interface ----------------------------------------------------------
 
 proverConfigs :: [(String, SBV.SMTConfig)]
@@ -198,13 +200,13 @@
 
 parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW])
 parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
-parseValue FTBit (cw : cws) = (Eval.VBit (SBV.fromCW cw), cws)
+parseValue FTBit (cw : cws) = (Eval.VBit (SBV.cwToBool cw), cws)
 parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws)
-parseValue (FTSeq n FTBit) (cw : cws)
-  | SBV.isBounded cw = (Eval.VWord (Eval.BV (toInteger n) (SBV.fromCW cw)), cws)
-  | otherwise = panic "Cryptol.Symbolic.parseValue" [ "unbounded concrete word" ]
-parseValue (FTSeq n FTBit) cws = (Eval.VSeq True vs, cws')
-  where (vs, cws') = parseValues (replicate n FTBit) cws
+parseValue (FTSeq n FTBit) cws =
+  case SBV.genParse (SBV.KBounded False n) cws of
+    Just (x, cws') -> (Eval.VWord (Eval.BV (toInteger n) x), cws')
+    Nothing        -> (Eval.VSeq True vs, cws')
+      where (vs, cws') = parseValues (replicate n FTBit) cws
 parseValue (FTSeq n t) cws = (Eval.VSeq False vs, cws')
   where (vs, cws') = parseValues (replicate n t) cws
 parseValue (FTTuple ts) cws = (Eval.VTuple vs, cws')
@@ -265,8 +267,8 @@
 forallFinType :: FinType -> SBV.Symbolic Value
 forallFinType ty =
   case ty of
-    FTBit         -> VBit <$> SBV.forall_
-    FTSeq 0 FTBit -> return $ VWord (SBV.literal (bv 0 0))
+    FTBit         -> VBit <$> forallSBool_
+    FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0)
     FTSeq n FTBit -> VWord <$> (forallBV_ n)
     FTSeq n t     -> VSeq False <$> replicateM n (forallFinType t)
     FTTuple ts    -> VTuple <$> mapM forallFinType ts
@@ -275,8 +277,8 @@
 existsFinType :: FinType -> SBV.Symbolic Value
 existsFinType ty =
   case ty of
-    FTBit         -> VBit <$> SBV.exists_
-    FTSeq 0 FTBit -> return $ VWord (SBV.literal (bv 0 0))
+    FTBit         -> VBit <$> existsSBool_
+    FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0)
     FTSeq n FTBit -> VWord <$> existsBV_ n
     FTSeq n t     -> VSeq False <$> replicateM n (existsFinType t)
     FTTuple ts    -> VTuple <$> mapM existsFinType ts
@@ -333,7 +335,7 @@
     ERec fields       -> VRecord [ (f, eval e) | (f, e) <- fields ]
     ESel e sel        -> evalSel sel (eval e)
     EIf b e1 e2       -> evalIf (fromVBit (eval b)) (eval e1) (eval e2)
-                           where evalIf = if envIteSolver env then SBV.sBranch else SBV.ite
+                           where evalIf = if envIteSolver env then sBranchValue else iteValue
     EComp ty e mss    -> evalComp env (evalType env ty) e mss
     EVar n            -> case lookupVar n env of
                            Just x -> x
@@ -377,7 +379,7 @@
         _ -> panic "Cryptol.Symbolic.evalSel" [ "Record selector applied to non-record" ]
 
     ListSel n _   -> case v of
-                       VWord s -> VBit (SBV.sbvTestBit s n)
+                       VWord s -> VBit (SBV.svTestBit s n)
                        _       -> fromSeq v !! n  -- 0-based indexing
 
 -- Declarations ----------------------------------------------------------------
diff --git a/src/Cryptol/Symbolic/BitVector.hs b/src/Cryptol/Symbolic/BitVector.hs
deleted file mode 100644
--- a/src/Cryptol/Symbolic/BitVector.hs
+++ /dev/null
@@ -1,205 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2013-2015 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
-
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE ViewPatterns #-}
-
-module Cryptol.Symbolic.BitVector where
-
-import Data.Bits
-import Data.List (foldl')
-import Control.Monad (replicateM)
-import System.Random
-
-import Data.SBV.Bridge.Yices
-import Data.SBV.Internals
-
-import Cryptol.Utils.Panic
-
--- BitVector type --------------------------------------------------------------
-
-data BitVector = BV { signedcxt :: Bool, width :: !Int, val :: !Integer }
-    deriving (Eq, Ord, Show)
--- ^ Invariant: BV w x requires that 0 <= w and 0 <= x < 2^w.
-
-bitMask :: Int -> Integer
-bitMask w = bit w - 1
-
--- | Smart constructor for bitvectors.
-bv :: Int -> Integer -> BitVector
-bv = sbv False
-
-sbv :: Bool -> Int -> Integer -> BitVector
-sbv b w x = BV b w (x .&. bitMask w)
-
-unsigned :: Int -> Integer -> Integer
-unsigned w x = x + bit w
-
-signed :: Int -> Integer -> Integer
-signed w x
-  | w > 0 && testBit x (w - 1) = x - bit w
-  | otherwise                  = x
-
-same :: Int -> Int -> Int
-same m n | m == n = m
-         | otherwise = panic "Cryptol.Symbolic.BitVector.same"
-                         [ "BitVector size mismatch: " ++ show (m, n) ]
-
-instance SignCast SWord SWord where
-  signCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
-    SBV k (Left (CW k (CWInteger (signed w x)))) where
-      k = KBounded True w
-  signCast x@(SBV (KBounded _ w) _) = SBV k (Right (cache y)) where
-    k = KBounded True w
-    y st = do xsw <- sbvToSW st x
-              newExpr st k (SBVApp (Extract (w - 1) 0) [xsw])
-  signCast _ = panic "Cryptol.Symbolic.BitVector"
-                 [ "signCast called on non-bitvector value" ]
-  unsignCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
-    SBV k (Left (CW k (CWInteger (unsigned w x)))) where
-      k = KBounded False w
-  unsignCast x@(SBV (KBounded _ w) _) = SBV k (Right (cache y)) where
-    k = KBounded False w
-    y st = do xsw <- sbvToSW st x
-              newExpr st k (SBVApp (Extract (w - 1) 0) [xsw])
-  unsignCast _ = panic "Cryptol.Symbolic.BitVector"
-                   [ "unsignCast called on non-bitvector value" ]
-
-instance Num BitVector where
-  fromInteger n = panic "Cryptol.Symbolic.BitVector"
-                    [ "fromInteger " ++ show n ++ " :: BitVector" ]
-  BV s m x + BV _ n y = sbv s (same m n) (x + y)
-  BV s m x - BV _ n y = sbv s (same m n) (x - y)
-  BV s m x * BV _ n y = sbv s (same m n) (x * y)
-  negate (BV s m x) = sbv s m (- x)
-  abs = id
-  signum (BV s m _) = sbv s m 1
-
-instance Bits BitVector where
-  BV s m x .&. BV _ n y        = BV s (same m n) (x .&. y)
-  BV s m x .|. BV _ n y        = BV s (same m n) (x .|. y)
-  BV s m x `xor` BV _ n y      = BV s (same m n) (x `xor` y)
-  complement (BV s m x)        = BV s m (x `xor` bitMask m)
-  shift (BV s m x) i           = sbv s m (shift x i)
-  rotate (BV s m x) i          = sbv s m (shift x j .|. shift x (j - m))
-                                  where j = i `mod` m
-  bit _i                       = panic "Cryptol.Symbolic.BitVector"
-                                   [ "bit: can't determine width" ]
-  setBit (BV s m x) i          = BV s m (setBit x i)
-  clearBit (BV s m x) i        = BV s m (clearBit x i)
-  complementBit (BV s m x) i   = BV s m (complementBit x i)
-  testBit (BV _ _ x) i         = testBit x i
-  bitSize x
-    | Just m <- bitSizeMaybe x = m
-    | otherwise                = panic "Cryptol.Symbolic.BitVector"
-                                   [ "bitSize should be total for BitVector" ]
-  bitSizeMaybe (BV _ m _)      = Just m
-  isSigned (BV s _ _)          = s
-  popCount (BV _ _ x)          = popCount x
-
-instance FiniteBits BitVector where
-  finiteBitSize (BV _ m _) = m
-
-instance FiniteBits (SBV BitVector) where
-  finiteBitSize (SBV (KBounded _ w) _) = w
-  finiteBitSize _ = panic "Cryptol.Symbolic.BitVector"
-                          [ "finiteBitSize called on non-bitvector value" ]
-
---------------------------------------------------------------------------------
--- SBV class instances
-
-type SWord = SBV BitVector
-
-instance HasKind BitVector where
-  kindOf (BV s w _) = KBounded s w
-
-instance SymWord BitVector where
-  literal (BV s w x) = SBV k (Left (mkConstCW k x))
-      where k = KBounded s w
-  fromCW c@(CW (KBounded s w) _) = BV s w (fromCW c)
-  fromCW c = panic "Cryptol.Symbolic.BitVector"
-               [ "fromCW: Unsupported non-integral value: " ++ show c ]
-  mkSymWord _ _ = panic "Cryptol.Symbolic.BitVector"
-                    [ "mkSymWord unimplemented for type BitVector" ]
-
-instance SIntegral BitVector where
-
-instance FromBits (SBV BitVector) where
-  fromBitsLE bs = foldl' f (literalSWord 0 0) bs
-    where f w b = cat (ite b (literalSWord 1 1) (literalSWord 1 0)) w
-
-instance SDivisible BitVector where
-  sQuotRem (BV _ m x) (BV _ n y) = (BV False w q, BV False w r)
-    where (q, r) = quotRem x y
-          w = same m n
-  sDivMod (BV _ m x) (BV _ n y) = (BV False w q, BV False w r)
-    where (q, r) = divMod x y
-          w = same m n
-
-instance SDivisible (SBV BitVector) where
-  sQuotRem = liftQRem
-  sDivMod  = liftDMod
-
-extract :: Int -> Int -> SWord -> SWord
-extract i j x@(SBV (KBounded s _) _) =
-  case x of
-    _ | i < j -> SBV k (Left (CW k (CWInteger 0)))
-    SBV _ (Left cw) ->
-      case cw of
-        CW _ (CWInteger v) -> SBV k (Left (normCW (CW k (CWInteger (v `shiftR` j)))))
-        _ -> panic "Cryptol.Symbolic.BitVector.extract" [ "non-integer concrete word" ]
-    _ -> SBV k (Right (cache y))
-      where y st = do sw <- sbvToSW st x
-                      newExpr st k (SBVApp (Extract i j) [sw])
-  where
-    k = KBounded s (i - j + 1)
-extract _ _ _ = panic "Cryptol.Symbolic.BitVector.extract" [ "non-bitvector value" ]
-
-cat :: SWord -> SWord -> SWord
-cat x y | finiteBitSize x == 0 = y
-        | finiteBitSize y == 0 = x
-cat x@(SBV _ (Left a)) y@(SBV _ (Left b)) =
-  case (a, b) of
-    (CW _ (CWInteger m), CW _ (CWInteger n)) ->
-      SBV k (Left (CW k (CWInteger ((m `shiftL` (finiteBitSize y) .|. n)))))
-    _ -> panic "Cryptol.Symbolic.BitVector.cat" [ "non-integer concrete word" ]
-  where k = KBounded False (finiteBitSize x + finiteBitSize y)
-cat x y = SBV k (Right (cache z))
-  where k = KBounded False (finiteBitSize x + finiteBitSize y)
-        z st = do xsw <- sbvToSW st x
-                  ysw <- sbvToSW st y
-                  newExpr st k (SBVApp Join [xsw, ysw])
-
-literalSWord :: Int -> Integer -> SWord
-literalSWord w i = genLiteral (KBounded False w) i
-
-randomSBVBitVector :: Int -> IO (SBV BitVector)
-randomSBVBitVector w = do
-  bs <- replicateM w randomIO
-  let x = sum [ bit i | (i, b) <- zip [0..] bs, b ]
-  return (literal (bv w x))
-
-mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector)
-mkSymBitVector mbQ mbNm w =
-  mkSymSBVWithRandom (randomSBVBitVector w) mbQ (KBounded False w) mbNm
-
-forallBV :: String -> Int -> Symbolic (SBV BitVector)
-forallBV nm w = mkSymBitVector (Just ALL) (Just nm) w
-
-forallBV_ :: Int -> Symbolic (SBV BitVector)
-forallBV_ w = mkSymBitVector (Just ALL) Nothing w
-
-existsBV :: String -> Int -> Symbolic (SBV BitVector)
-existsBV nm w = mkSymBitVector (Just EX) (Just nm) w
-
-existsBV_ :: Int -> Symbolic (SBV BitVector)
-existsBV_ w = mkSymBitVector (Just EX) Nothing w
diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@@ -11,22 +11,24 @@
 {-# LANGUAGE FlexibleContexts #-}
 module Cryptol.Symbolic.Prims where
 
-import Control.Applicative
 import Data.Bits
 import Data.List (genericDrop, genericReplicate, genericSplitAt, genericTake, sortBy, transpose)
 import Data.Ord (comparing)
 
+import Cryptol.Eval.Value (BitWord(..))
 import Cryptol.Prims.Eval (binary, unary, tlamN)
 import Cryptol.Prims.Syntax (ECon(..))
-import Cryptol.Symbolic.BitVector
 import Cryptol.Symbolic.Value
 import Cryptol.TypeCheck.AST (Name)
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
 import Cryptol.Utils.Panic
 
-import qualified Data.SBV as SBV
-import Data.SBV (SBool)
+import qualified Data.SBV.Dynamic as SBV
 
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+
 traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
 traverseSnd f (x, y) = (,) x <$> f y
 
@@ -36,25 +38,25 @@
 evalECon :: ECon -> Value
 evalECon econ =
   case econ of
-    ECTrue        -> VBit SBV.true
-    ECFalse       -> VBit SBV.false
+    ECTrue        -> VBit SBV.svTrue
+    ECFalse       -> VBit SBV.svFalse
     ECDemote      -> ecDemoteV -- Converts a numeric type into its corresponding value.
                                -- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
-    ECPlus        -> binary (arithBinary (+)) -- {a} (Arith a) => a -> a -> a
-    ECMinus       -> binary (arithBinary (-)) -- {a} (Arith a) => a -> a -> a
-    ECMul         -> binary (arithBinary (*)) -- {a} (Arith a) => a -> a -> a
-    ECDiv         -> binary (arithBinary (SBV.sQuot)) -- {a} (Arith a) => a -> a -> a
-    ECMod         -> binary (arithBinary (SBV.sRem)) -- {a} (Arith a) => a -> a -> a
+    ECPlus        -> binary (arithBinary SBV.svPlus) -- {a} (Arith a) => a -> a -> a
+    ECMinus       -> binary (arithBinary SBV.svMinus) -- {a} (Arith a) => a -> a -> a
+    ECMul         -> binary (arithBinary SBV.svTimes) -- {a} (Arith a) => a -> a -> a
+    ECDiv         -> binary (arithBinary SBV.svQuot) -- {a} (Arith a) => a -> a -> a
+    ECMod         -> binary (arithBinary SBV.svRem) -- {a} (Arith a) => a -> a -> a
     ECExp         -> binary (arithBinary sExp) -- {a} (Arith a) => a -> a -> a
     ECLg2         -> unary (arithUnary sLg2) -- {a} (Arith a) => a -> a
-    ECNeg         -> unary (arithUnary negate)
+    ECNeg         -> unary (arithUnary SBV.svUNeg)
 
-    ECLt          -> binary (cmpBinary cmpLt cmpLt SBV.false)
-    ECGt          -> binary (cmpBinary cmpGt cmpGt SBV.false)
-    ECLtEq        -> binary (cmpBinary cmpLtEq cmpLtEq SBV.true)
-    ECGtEq        -> binary (cmpBinary cmpGtEq cmpGtEq SBV.true)
-    ECEq          -> binary (cmpBinary cmpEq cmpEq SBV.true)
-    ECNotEq       -> binary (cmpBinary cmpNotEq cmpNotEq SBV.false)
+    ECLt          -> binary (cmpBinary cmpLt cmpLt SBV.svFalse)
+    ECGt          -> binary (cmpBinary cmpGt cmpGt SBV.svFalse)
+    ECLtEq        -> binary (cmpBinary cmpLtEq cmpLtEq SBV.svTrue)
+    ECGtEq        -> binary (cmpBinary cmpGtEq cmpGtEq SBV.svTrue)
+    ECEq          -> binary (cmpBinary cmpEq cmpEq SBV.svTrue)
+    ECNotEq       -> binary (cmpBinary cmpNotEq cmpNotEq SBV.svFalse)
 
     -- FIXME: the next 4 "primitives" should be defined in the Cryptol prelude.
     ECFunEq       -> -- {a b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
@@ -63,7 +65,7 @@
       tlam $ \b ->
       VFun $ \f ->
       VFun $ \g ->
-      VFun $ \x -> cmpBinary cmpEq cmpEq SBV.true b (fromVFun f x) (fromVFun g x)
+      VFun $ \x -> cmpBinary cmpEq cmpEq SBV.svTrue b (fromVFun f x) (fromVFun g x)
 
     ECFunNotEq    -> -- {a b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
       -- (f !== g) x = (f x != g x)
@@ -71,24 +73,24 @@
       tlam $ \b ->
       VFun $ \f ->
       VFun $ \g ->
-      VFun $ \x -> cmpBinary cmpNotEq cmpNotEq SBV.false b (fromVFun f x) (fromVFun g x)
+      VFun $ \x -> cmpBinary cmpNotEq cmpNotEq SBV.svFalse b (fromVFun f x) (fromVFun g x)
 
     ECMin         -> -- {a} (Cmp a) => a -> a -> a
       -- min x y = if x <= y then x else y
       binary $ \a x y ->
-        let c = cmpBinary cmpLtEq cmpLtEq SBV.false a x y
-        in SBV.ite (fromVBit c) x y
+        let c = cmpBinary cmpLtEq cmpLtEq SBV.svFalse a x y
+        in iteValue (fromVBit c) x y
 
     ECMax         -> -- {a} (Cmp a) => a -> a -> a
       -- max x y = if y <= x then x else y
       binary $ \a x y ->
-        let c = cmpBinary cmpLtEq cmpLtEq SBV.false a y x
-        in SBV.ite (fromVBit c) x y
+        let c = cmpBinary cmpLtEq cmpLtEq SBV.svFalse a y x
+        in iteValue (fromVBit c) x y
 
-    ECAnd         -> binary (logicBinary (SBV.&&&) (.&.))
-    ECOr          -> binary (logicBinary (SBV.|||) (.|.))
-    ECXor         -> binary (logicBinary (SBV.<+>) xor)
-    ECCompl       -> unary (logicUnary (SBV.bnot) complement)
+    ECAnd         -> binary (logicBinary SBV.svAnd SBV.svAnd)
+    ECOr          -> binary (logicBinary SBV.svOr SBV.svOr)
+    ECXor         -> binary (logicBinary SBV.svXOr SBV.svXOr)
+    ECCompl       -> unary (logicUnary SBV.svNot SBV.svNot)
     ECZero        -> VPoly zeroV
 
     ECShiftL      -> -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a
@@ -98,7 +100,7 @@
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvShiftLeft x (fromVWord y))
+          VWord x -> VWord (SBV.svShiftLeft x (fromVWord y))
           _ -> selectV shl y
             where
               shl :: Integer -> Value
@@ -115,7 +117,7 @@
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvShiftRight x (fromVWord y))
+          VWord x -> VWord (SBV.svShiftRight x (fromVWord y))
           _ -> selectV shr y
             where
               shr :: Integer -> Value
@@ -132,7 +134,7 @@
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvRotateLeft x (fromVWord y))
+          VWord x -> VWord (SBV.svRotateLeft x (fromVWord y))
           _ -> selectV rol y
             where
               rol :: Integer -> Value
@@ -146,7 +148,7 @@
       VFun $ \xs ->
       VFun $ \y ->
         case xs of
-          VWord x -> VWord (SBV.sbvRotateRight x (fromVWord y))
+          VWord x -> VWord (SBV.svRotateRight x (fromVWord y))
           _ -> selectV ror y
             where
               ror :: Integer -> Value
@@ -235,13 +237,13 @@
     ECInfFrom    ->
       tlam $ \(finTValue -> bits)  ->
        lam $ \(fromVWord  -> first) ->
-      toStream [ VWord (first + SBV.literal (bv (fromInteger bits) i)) | i <- [0 ..] ]
+      toStream [ VWord (SBV.svPlus first (literalSWord (fromInteger bits) i)) | i <- [0 ..] ]
 
     ECInfFromThen -> -- {a} (fin a) => [a] -> [a] -> [inf][a]
       tlam $ \_ ->
        lam $ \(fromVWord -> first) ->
        lam $ \(fromVWord -> next) ->
-      toStream (map VWord (iterate (+ (next - first)) first))
+      toStream (map VWord (iterate (SBV.svPlus (SBV.svMinus next first)) first))
 
     -- {at,len} (fin len) => [len][8] -> at
     ECError ->
@@ -256,10 +258,10 @@
       VFun $ \v2 ->
         let k = max 1 (i + j) - 1
             mul _  []     ps = ps
-            mul as (b:bs) ps = mul (SBV.false : as) bs (ites b (as `addPoly` ps) ps)
+            mul as (b:bs) ps = mul (SBV.svFalse : as) bs (ites b (as `addPoly` ps) ps)
             xs = map fromVBit (fromSeq v1)
             ys = map fromVBit (fromSeq v2)
-            zs = take (fromInteger k) (mul xs ys [] ++ repeat SBV.false)
+            zs = take (fromInteger k) (mul xs ys [] ++ repeat SBV.svFalse)
         in VSeq True (map VBit zs)
 
     ECPDiv        -> -- {a,b} (fin a, fin b) => [a] -> [b] -> [a]
@@ -269,7 +271,7 @@
       VFun $ \v2 ->
         let xs = map fromVBit (fromSeq v1)
             ys = map fromVBit (fromSeq v2)
-            zs = take (fromInteger i) (fst (mdp (reverse xs) (reverse ys)) ++ repeat SBV.false)
+            zs = take (fromInteger i) (fst (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse)
         in VSeq True (map VBit (reverse zs))
 
     ECPMod        -> -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b]
@@ -279,7 +281,7 @@
       VFun $ \v2 ->
         let xs = map fromVBit (fromSeq v1)
             ys = map fromVBit (fromSeq v2)
-            zs = take (fromInteger j) (snd (mdp (reverse xs) (reverse ys)) ++ repeat SBV.false)
+            zs = take (fromInteger j) (snd (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse)
         in VSeq True (map VBit (reverse zs))
 
     ECRandom      -> panic "Cryptol.Symbolic.Prims.evalECon"
@@ -293,7 +295,7 @@
 
     sel :: Integer -> [SBool] -> Value
     sel offset []       = f offset
-    sel offset (b : bs) = SBV.ite b m1 m2
+    sel offset (b : bs) = iteValue b m1 m2
       where m1 = sel (offset + 2 ^ length bs) bs
             m2 = sel offset bs
 
@@ -311,9 +313,9 @@
   case v of
     VStream xs -> nth err xs (fromInteger n)
     VSeq _ xs  -> nth err xs (fromInteger n)
-    VWord x                 -> let i = finiteBitSize x - 1 - fromInteger n
+    VWord x                 -> let i = SBV.svBitSize x - 1 - fromInteger n
                                in if i < 0 then err else
-                                    VBit (SBV.sbvTestBit x i)
+                                    VBit (SBV.svTestBit x i)
     _                       -> err
 
 mapV :: Bool -> (Value -> Value) -> Value -> Value
@@ -325,8 +327,8 @@
 
 catV :: Value -> Value -> Value
 catV xs          (VStream ys) = VStream (fromSeq xs ++ ys)
-catV (VWord x)   ys           = VWord (cat x (fromVWord ys))
-catV xs          (VWord y)    = VWord (cat (fromVWord xs) y)
+catV (VWord x)   ys           = VWord (SBV.svJoin x (fromVWord ys))
+catV xs          (VWord y)    = VWord (SBV.svJoin (fromVWord xs) y)
 catV (VSeq b xs) (VSeq _ ys)  = VSeq b (xs ++ ys)
 catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ]
 
@@ -336,13 +338,13 @@
   case xs of
     VSeq b xs'  -> VSeq b (genericDrop n xs')
     VStream xs' -> VStream (genericDrop n xs')
-    VWord w     -> VWord $ extract (finiteBitSize w - 1 - fromInteger n) 0 w
+    VWord w     -> VWord $ SBV.svExtract (SBV.svBitSize w - 1 - fromInteger n) 0 w
     _           -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ]
 
 takeV :: Integer -> Value -> Value
 takeV n xs =
   case xs of
-    VWord w     -> VWord $ extract (finiteBitSize w - 1) (finiteBitSize w - fromInteger n) w
+    VWord w     -> VWord $ SBV.svExtract (SBV.svBitSize w - 1) (SBV.svBitSize w - fromInteger n) w
     VSeq b xs'  -> VSeq b (genericTake n xs')
     VStream xs' -> VSeq b (genericTake n xs')
                      where b = case xs' of VBit _ : _ -> True
@@ -355,7 +357,7 @@
 ecDemoteV = tlam $ \valT ->
             tlam $ \bitT ->
             case (numTValue valT, numTValue bitT) of
-              (Nat v, Nat bs) -> VWord (SBV.literal (bv (fromInteger bs) v))
+              (Nat v, Nat bs) -> VWord (literalSWord (fromInteger bs) v)
               _ -> evalPanic "Cryptol.Prove.evalECon"
                        ["Unexpected Inf in constant."
                        , show valT
@@ -418,19 +420,19 @@
         TVFun _ t     -> VFun (\x -> loop t (fromVFun v x))
 
 sExp :: SWord -> SWord -> SWord
-sExp x y = go (SBV.blastLE y)
-  where go []       = SBV.literal (bv (finiteBitSize x) 1)
-        go (b : bs) = SBV.ite b (x * s) s
+sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order
+  where go []       = literalSWord (SBV.svBitSize x) 1
+        go (b : bs) = SBV.svIte b (SBV.svTimes x s) s
             where a = go bs
-                  s = a * a
+                  s = SBV.svTimes a a
 
 -- | Ceiling (log_2 x)
 sLg2 :: SWord -> SWord
 sLg2 x = go 0
   where
-    lit n = SBV.literal (bv (finiteBitSize x) n)
-    go i | i < finiteBitSize x = SBV.ite ((SBV..<=) x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
-         | otherwise     = lit (toInteger i)
+    lit n = literalSWord (SBV.svBitSize x) n
+    go i | i < SBV.svBitSize x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
+         | otherwise           = lit (toInteger i)
 
 -- Cmp -------------------------------------------------------------------------
 
@@ -461,19 +463,19 @@
     cmpValues (x1 : xs1) (x2 : xs2) k = cmp x1 x2 (cmpValues xs1 xs2 k)
     cmpValues _ _ k = k
 
-cmpEq :: SBV.EqSymbolic a => a -> a -> SBool -> SBool
-cmpEq x y k = (SBV.&&&) ((SBV..==) x y) k
+cmpEq :: SWord -> SWord -> SBool -> SBool
+cmpEq x y k = SBV.svAnd (SBV.svEqual x y) k
 
-cmpNotEq :: SBV.EqSymbolic a => a -> a -> SBool -> SBool
-cmpNotEq x y k = (SBV.|||) ((SBV../=) x y) k
+cmpNotEq :: SWord -> SWord -> SBool -> SBool
+cmpNotEq x y k = SBV.svOr (SBV.svNotEqual x y) k
 
-cmpLt, cmpGt :: SBV.OrdSymbolic a => a -> a -> SBool -> SBool
-cmpLt x y k = (SBV.|||) ((SBV..<) x y) (cmpEq x y k)
-cmpGt x y k = (SBV.|||) ((SBV..>) x y) (cmpEq x y k)
+cmpLt, cmpGt :: SWord -> SWord -> SBool -> SBool
+cmpLt x y k = SBV.svOr (SBV.svLessThan x y) (cmpEq x y k)
+cmpGt x y k = SBV.svOr (SBV.svGreaterThan x y) (cmpEq x y k)
 
-cmpLtEq, cmpGtEq :: SBV.OrdSymbolic a => a -> a -> SBool -> SBool
-cmpLtEq x y k = (SBV.&&&) ((SBV..<=) x y) (cmpNotEq x y k)
-cmpGtEq x y k = (SBV.&&&) ((SBV..>=) x y) (cmpNotEq x y k)
+cmpLtEq, cmpGtEq :: SWord -> SWord -> SBool -> SBool
+cmpLtEq x y k = SBV.svAnd (SBV.svLessEq x y) (cmpNotEq x y k)
+cmpGtEq x y k = SBV.svAnd (SBV.svGreaterEq x y) (cmpNotEq x y k)
 
 cmpBinary :: (SBool -> SBool -> SBool -> SBool)
           -> (SWord -> SWord -> SBool -> SBool)
@@ -500,8 +502,8 @@
   where
     go ty =
       case ty of
-        TVBit         -> VBit SBV.false
-        TVSeq n TVBit -> VWord (SBV.literal (bv n 0))
+        TVBit         -> VBit SBV.svFalse
+        TVSeq n TVBit -> VWord (literalSWord n 0)
         TVSeq n t     -> VSeq False (replicate n (go t))
         TVStream t    -> VStream (repeat (go t))
         TVTuple ts    -> VTuple [ go t | t <- ts ]
@@ -575,7 +577,7 @@
     case (first, next, len, bits) of
       (Nat first', Nat next', Nat len', Nat bits') ->
         let nums = enumFromThen first' next'
-            lit i = VWord (SBV.literal (bv (fromInteger bits') i))
+            lit i = VWord (literalSWord (fromInteger bits') i)
          in VSeq False (genericTake len' (map lit nums))
       _ -> evalPanic "fromThenV" ["invalid arguments"]
 
@@ -590,7 +592,7 @@
       (Nat first', Nat lst', Nat bits') ->
         let nums = enumFromThenTo first' (first' + 1) lst'
             len  = 1 + (lst' - first')
-            lit i = VWord (SBV.literal (bv (fromInteger bits') i))
+            lit i = VWord (literalSWord (fromInteger bits') i)
          in VSeq False (genericTake len (map lit nums))
 
       _ -> evalPanic "fromThenV" ["invalid arguments"]
@@ -607,7 +609,7 @@
 
       (Nat first', Nat next', Nat lst', Nat len', Nat bits') ->
         let nums = enumFromThenTo first' next' lst'
-            lit i = VWord (SBV.literal (bv (fromInteger bits') i))
+            lit i = VWord (literalSWord (fromInteger bits') i)
          in VSeq False (genericTake len' (map lit nums))
 
       _ -> evalPanic "fromThenV" ["invalid arguments"]
@@ -621,25 +623,25 @@
 addPoly :: [SBool] -> [SBool] -> [SBool]
 addPoly xs    []      = xs
 addPoly []    ys      = ys
-addPoly (x:xs) (y:ys) = x SBV.<+> y : addPoly xs ys
+addPoly (x:xs) (y:ys) = SBV.svXOr x y : addPoly xs ys
 
 ites :: SBool -> [SBool] -> [SBool] -> [SBool]
 ites s xs ys
- | Just t <- SBV.unliteral s
+ | Just t <- SBV.svAsBool s
  = if t then xs else ys
  | True
  = go xs ys
  where go [] []         = []
-       go []     (b:bs) = SBV.ite s SBV.false b : go [] bs
-       go (a:as) []     = SBV.ite s a SBV.false : go as []
-       go (a:as) (b:bs) = SBV.ite s a b : go as bs
+       go []     (b:bs) = SBV.svIte s SBV.svFalse b : go [] bs
+       go (a:as) []     = SBV.svIte s a SBV.svFalse : go as []
+       go (a:as) (b:bs) = SBV.svIte s a b : go as bs
 
 -- conservative over-approximation of the degree
 degree :: [SBool] -> Int
 degree xs = walk (length xs - 1) $ reverse xs
   where walk n []     = n
         walk n (b:bs)
-         | Just t <- SBV.unliteral b
+         | Just t <- SBV.svAsBool b
          = if t then n else walk (n-1) bs
          | True
          = n -- over-estimate
@@ -653,13 +655,13 @@
          | True     = let (rqs, rrs) = go (n-1) bs
                       in (ites b (reverse qs) rqs, ites b rs rrs)
          where degQuot = degTop - n
-               ys' = replicate degQuot SBV.false ++ ys
+               ys' = replicate degQuot SBV.svFalse ++ ys
                (qs, rs) = divx (degQuot+1) degTop xs ys'
 
 -- return the element at index i; if not enough elements, return false
 -- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient
 idx :: [SBool] -> Int -> SBool
-idx []     _ = SBV.false
+idx []     _ = SBV.svFalse
 idx (x:_)  0 = x
 idx (_:xs) i = idx xs (i-1)
 
diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@@ -12,64 +12,108 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Cryptol.Symbolic.Value
-  ( Value
+  ( SBool, SWord
+  , literalSWord
+  , fromBitsLE
+  , forallBV_, existsBV_
+  , forallSBool_, existsSBool_
+  , Value
   , TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
   , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
   , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
   , fromSeq, fromVWord
   , evalPanic
+  , iteValue, sBranchValue, mergeValue
   )
   where
 
-import Data.Bits (finiteBitSize)
+import Data.List (foldl')
 
-import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,
-                           GenValue(..), BitWord(..), lam, tlam, toStream, toFinSeq, toSeq, fromSeq,
-                           fromVBit, fromVWord, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
-import Cryptol.Symbolic.BitVector
+import Data.SBV.Dynamic
+
+import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
+                           isTFun, isTSeq, isTTuple, isTRec, tvSeq, GenValue(..),
+                           BitWord(..), lam, tlam, toStream, toFinSeq, toSeq,
+                           fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
+                           fromVTuple, fromVRecord, lookupRecord)
 import Cryptol.Utils.Panic (panic)
 
-import Data.SBV (SBool, fromBitsBE, Mergeable(..), HasKind(..), EqSymbolic(..))
-import Data.SBV.Internals (symbolicMergeWithKind)
+-- SBool and SWord -------------------------------------------------------------
 
+type SBool = SVal
+type SWord = SVal
+
+fromBitsLE :: [SBool] -> SWord
+fromBitsLE bs = foldl' f (literalSWord 0 0) bs
+  where f w b = svJoin (svToWord1 b) w
+
+literalSWord :: Int -> Integer -> SWord
+literalSWord w i = svInteger (KBounded False w) i
+
+forallBV_ :: Int -> Symbolic SWord
+forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing
+
+existsBV_ :: Int -> Symbolic SWord
+existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing
+
+forallSBool_ :: Symbolic SBool
+forallSBool_ = svMkSymVar (Just ALL) KBool Nothing
+
+existsSBool_ :: Symbolic SBool
+existsSBool_ = svMkSymVar (Just EX) KBool Nothing
+
 -- Values ----------------------------------------------------------------------
 
 type Value = GenValue SBool SWord
 
 -- Symbolic Conditionals -------------------------------------------------------
 
-instance Mergeable Value where
-  symbolicMerge f c v1 v2 =
-    case (v1, v2) of
-      (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2
-      (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (symbolicMerge f c) vs1 vs2
-      (VBit b1    , VBit b2    ) -> VBit $ symbolicMerge f c b1 b2
-      (VWord w1   , VWord w2   ) -> VWord $ mergeWord w1 w2
-      (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ symbolicMerge f c vs1 vs2
-      (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2
-      (VFun f1    , VFun f2    ) -> VFun $ symbolicMerge f c f1 f2
-      (VPoly f1   , VPoly f2   ) -> VPoly $ symbolicMerge f c f1 f2
-      (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)
-      (_          , VWord w2   ) -> VWord $ mergeWord (fromVWord v1) w2
-      (_          , _          ) -> panic "Cryptol.Symbolic.Value"
-                                      [ "symbolicMerge: incompatible values" ]
-    where
-      mergeWord w1 w2 = symbolicMergeWithKind (kindOf w1) f c w1 w2
-      mergeField (n1, x1) (n2, x2)
-        | n1 == n2  = (n1, symbolicMerge f c x1 x2)
-        | otherwise = panic "Cryptol.Symbolic.Value"
-                        [ "symbolicMerge.mergeField: incompatible values" ]
-      mergeStream xs ys =
-        symbolicMerge f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)
+iteValue :: SBool -> Value -> Value -> Value
+iteValue c x y =
+  case svAsBool c of
+    Just True  -> x
+    Just False -> y
+    Nothing    -> mergeValue True c x y
 
+sBranchValue :: SBool -> Value -> Value -> Value
+sBranchValue t x y =
+  case svAsBool c of
+    Just True  -> x
+    Just False -> y
+    Nothing    -> mergeValue False c x y
+  where
+    c = svReduceInPathCondition t
+
+mergeValue :: Bool -> SBool -> Value -> Value -> Value
+mergeValue f c v1 v2 =
+  case (v1, v2) of
+    (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2
+    (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (mergeValue f c) vs1 vs2
+    (VBit b1    , VBit b2    ) -> VBit $ mergeBit b1 b2
+    (VWord w1   , VWord w2   ) -> VWord $ mergeWord w1 w2
+    (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ zipWith (mergeValue f c) vs1 vs2
+    (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2
+    (VFun f1    , VFun f2    ) -> VFun $ \x -> mergeValue f c (f1 x) (f2 x)
+    (VPoly f1   , VPoly f2   ) -> VPoly $ \x -> mergeValue f c (f1 x) (f2 x)
+    (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)
+    (_          , VWord w2   ) -> VWord $ mergeWord (fromVWord v1) w2
+    (_          , _          ) -> panic "Cryptol.Symbolic.Value"
+                                  [ "mergeValue: incompatible values" ]
+  where
+    mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2
+    mergeWord w1 w2 = svSymbolicMerge (svKind w1) f c w1 w2
+    mergeField (n1, x1) (n2, x2)
+      | n1 == n2  = (n1, mergeValue f c x1 x2)
+      | otherwise = panic "Cryptol.Symbolic.Value"
+                    [ "mergeValue.mergeField: incompatible values" ]
+    mergeStream xs ys =
+      mergeValue f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)
+
 -- Big-endian Words ------------------------------------------------------------
 
 instance BitWord SBool SWord where
-  packWord bs = Data.SBV.fromBitsBE bs
-  unpackWord w = [ sbvTestBit' w i | i <- reverse [0 .. finiteBitSize w - 1] ]
-
-sbvTestBit' :: SWord -> Int -> SBool
-sbvTestBit' w i = extract i i w .== literalSWord 1 1
+  packWord bs = fromBitsLE (reverse bs)
+  unpackWord x = [ svTestBit x i | i <- reverse [0 .. svBitSize x - 1] ]
 
 -- Errors ----------------------------------------------------------------------
 
diff --git a/src/Cryptol/Testing/Exhaust.hs b/src/Cryptol/Testing/Exhaust.hs
--- a/src/Cryptol/Testing/Exhaust.hs
+++ b/src/Cryptol/Testing/Exhaust.hs
@@ -12,8 +12,11 @@
 import Cryptol.TypeCheck.AST
 import Cryptol.Eval.Value
 
-import Control.Applicative((<$>))
 import Data.List(genericReplicate)
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative((<$>))
+#endif
 
 {- | Given a (function) type, compute all possible inputs for it.
 We also return the total number of test (i.e., the length of the outer list. -}
diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs
--- a/src/Cryptol/Transform/MonoValues.hs
+++ b/src/Cryptol/Transform/MonoValues.hs
@@ -79,11 +79,14 @@
 import Cryptol.Parser.AST (Pass(MonoValues))
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.TypeMap
-import Control.Applicative
 import Data.List(sortBy,groupBy)
 import Data.Either(partitionEithers)
 import Data.Map (Map)
 import MonadLib
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
 
 {- (f,t,n) |--> x  means that when we spot instantiations of `f` with `ts` and
 `n` proof argument, we should replace them with `Var x` -}
diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs
--- a/src/Cryptol/Transform/Specialize.hs
+++ b/src/Cryptol/Transform/Specialize.hs
@@ -16,15 +16,17 @@
 import qualified Cryptol.ModuleSystem.Env as M
 import qualified Cryptol.ModuleSystem.Monad as M
 
-import Control.Applicative
 import Data.List (intercalate)
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Maybe (catMaybes)
-import Data.Traversable (traverse)
 
 import MonadLib
 
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+import Data.Traversable (traverse)
+#endif
 
 -- Specializer Monad -----------------------------------------------------------
 
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -35,7 +35,10 @@
 import           MonadLib
 import qualified Control.Applicative as A
 import           Control.Monad.Fix(MonadFix(..))
+
+#if __GLASGOW_HASKELL__ < 710
 import           Data.Functor
+#endif
 
 -- | Information needed for type inference.
 data InferInput = InferInput
diff --git a/src/Cryptol/TypeCheck/Solver/Smtlib.hs b/src/Cryptol/TypeCheck/Solver/Smtlib.hs
--- a/src/Cryptol/TypeCheck/Solver/Smtlib.hs
+++ b/src/Cryptol/TypeCheck/Solver/Smtlib.hs
@@ -6,7 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
-{-# LANGUAGE OverloadedStrings, RecordWildCards, PatternGuards, Trustworthy #-}
+{-# LANGUAGE OverloadedStrings, RecordWildCards, PatternGuards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 module Cryptol.TypeCheck.Solver.Smtlib (simpDelayed) where
 
diff --git a/src/Cryptol/TypeCheck/Unify.hs b/src/Cryptol/TypeCheck/Unify.hs
--- a/src/Cryptol/TypeCheck/Unify.hs
+++ b/src/Cryptol/TypeCheck/Unify.hs
@@ -15,10 +15,13 @@
 import Cryptol.TypeCheck.Subst
 import Cryptol.Utils.Panic (panic)
 
-import Control.Applicative (Applicative(..))
 import Data.Ord(comparing)
 import Data.List(sortBy)
 import qualified Data.Set as Set
+
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative (Applicative(..))
+#endif
 
 -- | The most general unifier is a substitution and a set of constraints
 -- on bound variables.