diff --git a/copilot-sbv.cabal b/copilot-sbv.cabal
--- a/copilot-sbv.cabal
+++ b/copilot-sbv.cabal
@@ -1,16 +1,16 @@
 cabal-version             : >= 1.10
 name                      : copilot-sbv
-version                   : 0.6
+version                   : 2.1.1
 synopsis                  : A compiler for CoPilot targeting SBV.
-description               : 
+description               :
   The Copilot back-end targeting SBV <http://hackage.haskell.org/package/sbv>.
-  . 
+  .
   Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
   Haskell that compiles into embedded C.  Copilot contains an interpreter,
   multiple back-end compilers, and other verification tools.  A tutorial, bug
   reports, and todos are available at
-  <https://github.com/niswegmann/copilot-discussion>.  
-  .  
+  <https://github.com/niswegmann/copilot-discussion>.
+  .
   Examples are available at
   <https://github.com/leepike/Copilot/tree/master/Examples>.
 
@@ -38,11 +38,11 @@
   ghc-options             : -Wall -fwarn-tabs
   ghc-prof-options        : -auto-all -caf-all
 
-  build-depends           : sbv >= 1.0 && <= 1.3
-                          , base >= 4.3 && < 5
+  build-depends           : sbv >= 2.4
+                          , base >= 4.0 && <= 5.0
                           , containers >= 0.4
-                          , copilot-core
-                          , pretty >= 1                         
+                          , copilot-core >= 0.2.4
+                          , pretty >= 1
                           , filepath >= 1.1
 
   exposed-modules         : Copilot.Compile.SBV
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
@@ -252,9 +252,9 @@
   Gt    t -> case W.ordInst      t of W.OrdInst        ->  (S..>)
 
   Div   t -> case W.divInst      t of W.BVDivisibleInst  ->  
-                                                  \x y -> fst (S.bvQuotRem x y)
+                                                  \x y -> fst (S.sQuotRem x y)
   Mod   t -> case W.divInst      t of W.BVDivisibleInst  ->  
-                                                  \x y -> snd (S.bvQuotRem x y)
+                                                  \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..|.)
diff --git a/src/Copilot/Compile/SBV/Queue.hs b/src/Copilot/Compile/SBV/Queue.hs
--- a/src/Copilot/Compile/SBV/Queue.hs
+++ b/src/Copilot/Compile/SBV/Queue.hs
@@ -12,7 +12,6 @@
 
 import Prelude hiding (id, rem)
 import qualified Data.SBV as S
-import qualified Data.SBV.Internals as S
 
 import Copilot.Core.Expr (DropIdx)
 import Copilot.Core.Error (impossible)
@@ -26,11 +25,10 @@
 
 --------------------------------------------------------------------------------
 
-lookahead :: (S.HasSignAndSize a, S.SymWord a) 
-          => DropIdx -> [S.SBV a] -> S.SBV QueueSize -> S.SBV a
+lookahead :: (S.SymWord a) => DropIdx -> [S.SBV a] -> S.SBV QueueSize -> S.SBV a
 lookahead i buf ptr = 
   let sz = fromIntegral $ length buf in
-  let (_, rem) = (ptr + fromIntegral i) `S.bvQuotRem` sz in
+  let (_, rem) = (ptr + fromIntegral i) `S.sQuotRem` sz in
   let defaultVal = if null buf 
                      then impossible "lookahead" "copilot-sbv"
                      else head buf                    in
diff --git a/src/Copilot/Compile/SBV/Witness.hs b/src/Copilot/Compile/SBV/Witness.hs
--- a/src/Copilot/Compile/SBV/Witness.hs
+++ b/src/Copilot/Compile/SBV/Witness.hs
@@ -17,7 +17,6 @@
   ) where
 
 import qualified Data.SBV as S
-import qualified Data.SBV.Internals as S
 import qualified Copilot.Core as C
 
 import Data.Word (Word8, Word16, Word32, Word64)
@@ -27,7 +26,7 @@
 --------------------------------------------------------------------------------
 
 badInst :: a
-badInst = C.impossible "witnesses" "copilot-sbv"
+badInst =  error "Fatal cast in the witnesses of SBV in copilot-sbv.  Are you sure that SBV supports the type you are using?  (It doesn't support floats or doubles.)  If you you are, or you don't understand the error, email leepike @ gmail . com (remove spaces) or file a bug report on github.com"
 
 --------------------------------------------------------------------------------
 
@@ -61,7 +60,7 @@
 
 --------------------------------------------------------------------------------
 
-data HasSignAndSizeInst a = S.HasSignAndSize a => HasSignAndSizeInst
+data HasSignAndSizeInst a = S.SymWord a => HasSignAndSizeInst
 
 hasSignAndSizeInst :: C.Type a -> HasSignAndSizeInst a
 hasSignAndSizeInst t =
@@ -95,16 +94,16 @@
 
 --------------------------------------------------------------------------------
 
-data BVDivisibleInst a = S.BVDivisible (S.SBV a) => BVDivisibleInst
+data BVDivisibleInst a = S.SDivisible (S.SBV a) => BVDivisibleInst
 
 divInst :: C.Type a -> BVDivisibleInst a
 divInst t =
   case t of
     C.Bool   -> badInst
-    C.Int8   -> badInst
-    C.Int16  -> badInst
-    C.Int32  -> badInst
-    C.Int64  -> badInst
+    C.Int8   -> BVDivisibleInst
+    C.Int16  -> BVDivisibleInst
+    C.Int32  -> BVDivisibleInst
+    C.Int64  -> BVDivisibleInst
     C.Word8  -> BVDivisibleInst
     C.Word16 -> BVDivisibleInst
     C.Word32 -> BVDivisibleInst