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                   : 0.1
+version                   : 0.2
 synopsis                  : A compiler for CoPilot targeting SBV.
 description               : Blah blah blah...
 license                   : BSD3
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
@@ -4,6 +4,7 @@
 
 module Copilot.Compile.SBV
   ( compile
+  , sbvDirName
   , module Copilot.Compile.SBV.Params
   ) where
 
@@ -14,7 +15,8 @@
 
 import Copilot.Compile.SBV.Driver (driver, driverName)
 import Copilot.Compile.SBV.Makefile (makefile, makefileName)
-import Copilot.Compile.SBV.Code (updateStates, updateObservers, fireTriggers)
+import Copilot.Compile.SBV.Code 
+  (updateStates, updateObservers, fireTriggers, getExtArrs)
 import Copilot.Compile.SBV.MetaTable (allocMetaTable)
 import Copilot.Compile.SBV.Params
 
@@ -22,10 +24,13 @@
 
 -- Note: we put everything in a directory named by the dirName.
 
+sbvDirName :: String
+sbvDirName = "copilot-sbv"
+
 compile :: Params -> C.Spec -> IO ()
 compile params spec = do
   let meta    = allocMetaTable spec
-      dirName = withPrefix (prefix params) "copilot"
+      dirName = withPrefix (prefix params) sbvDirName
       sbvName = withPrefix (prefix params) "internal"
   putStrLn "Compiling SBV-generated functions .."
 
@@ -34,7 +39,9 @@
     sbvName
     (  updateStates    meta spec
     ++ updateObservers meta spec
-    ++ fireTriggers    meta spec )
+    ++ fireTriggers    meta spec 
+    ++ getExtArrs      meta 
+    )
 
   putStrLn ""
   putStrLn $ "Generating Copilot driver " ++ driverName params ++ " .."
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
@@ -9,6 +9,7 @@
   ( updateStates
   , updateObservers
   , fireTriggers
+  , getExtArrs
   ) where
 
 import Copilot.Compile.SBV.Copilot2SBV
@@ -20,9 +21,10 @@
 import Copilot.Core.Type.Equality ((=~=), coerce, cong)
 
 import qualified Data.SBV as S
-import qualified Data.SBV.Internals as S
+--import qualified Data.SBV.Internals as S
 
 import qualified Data.Map as M
+import Control.Monad (foldM)
 import Prelude hiding (id)
 
 --------------------------------------------------------------------------------
@@ -43,15 +45,16 @@
   updateStreamState C.Stream { C.streamId       = id
                              , C.streamExpr     = e
                              , C.streamExprType = t1
-                                                      } =
-    mkSBVFunc (mkUpdateStFn id) $ do
-      inputs <- mkInputs meta (c2Args e)
-      let e' = c2sExpr inputs e
-      let Just strmInfo = M.lookup id (streamInfoMap meta) 
-      updateStreamState1 t1 e' strmInfo
+                                                      } 
+    = mkSBVFunc (mkUpdateStFn id) $ do
+        inputs <- mkInputs meta (c2Args e)
+        let e' = c2sExpr inputs e
+        let Just strmInfo = M.lookup id (streamInfoMap meta) 
+        updateStreamState1 t1 e' strmInfo
 
-  updateStreamState1 :: C.Type a -> S.SBV a -> StreamInfo -> S.SBVCodeGen ()
-  updateStreamState1 t1 e1 (StreamInfo _ t2) = do
+  updateStreamState1 :: C.Type a -> S.SBV a -> C.Stream -> S.SBVCodeGen ()
+  updateStreamState1 t1 e1 C.Stream { C.streamExprType = t2 }
+    = do
     W.SymWordInst <- return (W.symWordInst t2)
     W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t2)
     Just p <- return (t1 =~= t2)
@@ -112,55 +115,128 @@
 
 --------------------------------------------------------------------------------
 
--- We first need to analyze the expression, running down it to get all the drop
--- ids and externals mentioned in it.  The we use those inputs to process the
--- expression.  XXX MUST be put in the monad in the same order as the function
--- call (argToCall from MetaTable.hs).
+-- Generate an SBV function that calculates the Copilot expression to get the
+-- next index to sample an external array.
+getExtArrs :: MetaTable -> [SBVFunc]
+getExtArrs meta@(MetaTable { externArrInfoMap = arrs })
+  = map mkIdx (M.toList arrs)
+  
+  where
+  mkIdx :: (C.Name, C.ExtArray) -> SBVFunc
+  mkIdx (name, C.ExtArray { C.externArrayIdx     = idx
+                          , C.externArrayIdxType = t   })
+    = 
+    mkSBVFunc (mkExtArrFn name) mkSBVExpr
+    where
+    mkSBVExpr :: S.SBVCodeGen ()
+    mkSBVExpr = do
+      inputs <- mkInputs meta (c2Args idx)
+      W.SymWordInst <- return (W.symWordInst t)
+      W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
+      S.cgReturn (c2sExpr inputs idx)
 
-mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen [Input]
-mkInputs meta args =
-  mapM argToInput args
+--------------------------------------------------------------------------------
 
+-- mkInputs takes the datatype containing the entire spec (meta) as well as all
+-- possible arguments to the SBV function generating the expression.  From those
+-- arguments, it then generates in the SBVCodeGen monad---the actual Inputs---
+-- the queues to hold streams as well as external variables.
+
+-- XXX MUST be put in the monad in the same order as the function call
+-- (argToCall from MetaTable.hs).
+
+mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen Inputs
+mkInputs meta args = 
+  foldM argToInput (Inputs [] [] [] []) args 
+
   where
-  argToInput :: Arg -> S.SBVCodeGen Input
-  argToInput (Extern name) = 
-    let extInfos = externInfoMap meta in
+  argToInput :: Inputs -> Arg -> S.SBVCodeGen Inputs
+
+-----------------------------------------
+ 
+  -- External variables
+  argToInput acc (Extern name) = 
+    let extInfos = externVarInfoMap meta in
     let Just extInfo = M.lookup name extInfos in
     mkExtInput extInfo
 
     where 
-    mkExtInput :: C.UType -> S.SBVCodeGen Input
-    mkExtInput C.UType { C.uTypeType = t } = do
-      ext <- mkExtInput_ t
-      return $ ExtIn name (ExtInput { extInput = ext 
-                                    , extType  = t })
+    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 
+                                              , extType  = t })
+                             ) : extVars acc }
 
-    mkExtInput_ :: C.Type a -> S.SBVCodeGen (S.SBV a)
-    mkExtInput_ t = do
-     W.SymWordInst        <- return (W.symWordInst t)
-     W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
-     ext <- S.cgInput (mkExtTmpVar name)
-     return ext
+-----------------------------------------
 
-  argToInput (Queue id) =
+-- External arrays
+  argToInput acc (ExternArr name) = 
+    let extInfos = externArrInfoMap meta in
+    let Just extInfo = M.lookup name extInfos in
+    mkExtInput extInfo
+
+    where 
+    mkExtInput :: C.ExtArray -> S.SBVCodeGen Inputs
+    mkExtInput C.ExtArray { C.externArrayElemType = t }
+      = do
+      v <- mkExtInput_ t (mkExtTmpVar name)
+      return acc { extArrs = (name, ExtInput 
+                                      { extInput  = v
+                                      , extType   = t }
+                             ) : extArrs acc }
+
+-----------------------------------------
+
+-- External functions
+  argToInput acc (ExternFun name tag) =
+    let extInfos = externFunInfoMap meta in
+    let Just extInfo = M.lookup name extInfos in
+    mkExtInput extInfo
+
+    where
+    mkExtInput :: C.ExtFun -> S.SBVCodeGen Inputs
+    mkExtInput C.ExtFun { C.externFunType = t }
+      = do
+      v <- mkExtInput_ t (mkExtTmpFun name tag)
+      return acc { extFuns = (name, ExtInput 
+                                      { extInput = v
+                                      , extType  = t }
+                             ) : extFuns acc }
+
+-----------------------------------------
+
+-- Stream queues
+  argToInput acc (Queue id) =
     let strmInfos = streamInfoMap meta in
     let Just strmInfo = M.lookup id strmInfos in
-    mkArrInput strmInfo
+    mkQueInput strmInfo
 
     where
-    mkArrInput :: StreamInfo -> S.SBVCodeGen Input
-    mkArrInput StreamInfo { streamInfoQueue = que
-                          , streamInfoType  = t } = do
-      arr <- mkArrInput_ t que
+    mkQueInput :: C.Stream -> S.SBVCodeGen Inputs
+    mkQueInput C.Stream { C.streamBuffer = que
+                        , C.streamExprType  = t } = do
+      arr <- mkQueInput_ t que
       ptr <- S.cgInput (mkQueuePtrVar id)
 
-      return $ ArrIn id (ArrInput (QueueIn { queue   = arr
-                                           , quePtr  = ptr
-                                           , arrType = t }))
-
-    mkArrInput_ :: C.Type a -> [a] -> S.SBVCodeGen [S.SBV a]
-    mkArrInput_ t que = do
+      return acc { extQues = (id, QueInput (QueueIn { queue   = arr
+                                                    , quePtr  = ptr
+                                                    , arrType = t })
+                             ) : extQues acc
+                 }
+                   
+    mkQueInput_ :: C.Type a -> [a] -> S.SBVCodeGen [S.SBV a]
+    mkQueInput_ t que = do
       W.SymWordInst        <- return (W.symWordInst t)
       W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
       arr <- S.cgInputArr (length que) (mkQueueVar id)
       return arr
+
+-----------------------------------------
+
+mkExtInput_ :: C.Type a -> String -> S.SBVCodeGen (S.SBV a)
+mkExtInput_ t name = do
+  W.SymWordInst        <- return (W.symWordInst t)
+  W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
+  ext <- S.cgInput name
+  return ext
diff --git a/src/Copilot/Compile/SBV/Common.hs b/src/Copilot/Compile/SBV/Common.hs
--- a/src/Copilot/Compile/SBV/Common.hs
+++ b/src/Copilot/Compile/SBV/Common.hs
@@ -2,19 +2,23 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
+-- Builds names of functions and variables used.
+
 module Copilot.Compile.SBV.Common
   ( mkTmpStVar
   , mkUpdateStFn
   , mkQueueVar
   , mkQueuePtrVar
   , mkExtTmpVar
+  , mkExtTmpFun
+  , mkExtArrFn
   , mkObserverFn
   , mkTriggerGuardFn
   , mkTriggerArgFn
   , mkTriggerArgIdx
   ) where
 
-import Copilot.Core (Id)
+import Copilot.Core (Id, Tag)
 import Prelude hiding (id)
 
 mkVar :: String -> Id -> String
@@ -35,14 +39,20 @@
 mkExtTmpVar :: String -> String
 mkExtTmpVar = ("ext_" ++)
 
+mkExtTmpFun :: String -> Tag -> String
+mkExtTmpFun name tag = "ext_" ++ name ++ "_" ++ show tag
+
+mkExtArrFn :: String -> String
+mkExtArrFn = (++) "mk_ext_arr_"
+
 mkObserverFn :: String -> String
-mkObserverFn = ("observer_" ++)
+mkObserverFn = ("mk_observer_" ++)
 
 mkTriggerGuardFn :: String -> String
-mkTriggerGuardFn = ("trigger_guard_" ++)
+mkTriggerGuardFn = ("mk_trigger_guard_" ++)
 
 mkTriggerArgFn :: Int -> String -> String
-mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i
+mkTriggerArgFn i nm = "mk_trigger_" ++ nm ++ "_arg_" ++ show i
 
 mkTriggerArgIdx :: [a] -> [(Int, a)]
 mkTriggerArgIdx args = zip [0,1 ..] args
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
@@ -6,9 +6,12 @@
 
 module Copilot.Compile.SBV.Copilot2SBV
   ( c2sExpr
-  , Input(..)
+  , Inputs(..)
+  , Ext
+--  , ExtArr
+  , ExtQue
   , ExtInput(..)
-  , ArrInput(..)
+  , QueInput(..)
   , QueueIn(..)
   ) 
 where
@@ -18,37 +21,45 @@
 import qualified Data.Map as M
 
 import qualified Data.SBV as S
-import qualified Data.SBV.Internals as S
+--import qualified Data.SBV.Internals as S
 
 import qualified Copilot.Compile.SBV.Queue as Q
 import qualified Copilot.Compile.SBV.Witness as W
 
 import Copilot.Core (Op1 (..), Op2 (..), Op3 (..), badUsage)
 import qualified Copilot.Core as C
+import Copilot.Core.Error (impossible)
 import Copilot.Core.Type.Equality ((=~=), coerce, cong)
 
-
 --------------------------------------------------------------------------------
 
-data Input = 
-    ExtIn C.Name ExtInput
-  | ArrIn C.Id ArrInput
+type Ext = (C.Name, ExtInput)
+type ExtQue = (C.Id, QueInput)
 
+-- These are all the inputs to the to the SBV expression we're building.
+data Inputs = Inputs
+  { extVars  :: [Ext] -- external variables
+  , extArrs  :: [Ext] -- external arrays
+  , extFuns  :: [Ext] -- external functions
+  , extQues  :: [ExtQue] }
+
+-- External input -- variables, arrays, and functions
 data ExtInput = forall a. ExtInput 
   { extInput :: S.SBV a
   , extType  :: C.Type a }
 
-data ArrInput = forall a. ArrInput 
+-- Stream queues
+data QueInput = forall a. QueInput 
   { arrInput :: QueueIn a }
 
 data QueueIn a = QueueIn
-  { queue  :: [S.SBV a]
-  , quePtr :: S.SBV Q.QueueSize 
+  { queue    :: [S.SBV a]
+  , quePtr   :: S.SBV Q.QueueSize 
   , arrType  :: C.Type a }
 
 --------------------------------------------------------------------------------
 
-c2sExpr :: [Input] -> C.Expr a -> S.SBV a
+c2sExpr :: Inputs -> C.Expr a -> S.SBV a
 c2sExpr inputs e = c2sExpr_ e M.empty inputs
 
 --------------------------------------------------------------------------------
@@ -61,7 +72,19 @@
 
 --------------------------------------------------------------------------------
 
-c2sExpr_ :: C.Expr a -> Env -> [Input] -> S.SBV a
+lookupInput :: Eq a => a -> [(a,b)] -> b
+lookupInput id prs =
+  case lookup id prs of
+    Nothing   -> impossible "lookupInput" "copilot-sbv"
+    Just val  -> val
+
+--------------------------------------------------------------------------------
+
+-- Translate a Copilot expression into an SBV expression.  The environment
+-- passed in is for tracking let expression bindings (in the Copilot language),
+-- and the list of inputs are all the external things needed as input to the SBV
+-- function.
+c2sExpr_ :: C.Expr a -> Env -> Inputs -> S.SBV a
 c2sExpr_ e0 env inputs = case e0 of
 
   C.Const t x ->
@@ -69,21 +92,13 @@
 
   ----------------------------------------------------
 
-  C.Drop t i id ->
-    let que :: ArrInput
-        Just que = foldl 
-          ( \acc x -> case x of
-                        ArrIn id' q -> if id' == id then Just q 
-                                         else acc
-                        ExtIn _ _ -> acc ) 
-          Nothing
-          inputs 
-    in 
-    drop1 t que
-
+  C.Drop t i id -> drop1 t que
     where
-    drop1 :: C.Type a -> ArrInput -> S.SBV a
-    drop1 t1 ArrInput { arrInput = QueueIn { queue   = que 
+    que :: QueInput
+    que = lookupInput id (extQues inputs)
+
+    drop1 :: C.Type a -> QueInput -> S.SBV a
+    drop1 t1 QueInput { arrInput = QueueIn { queue   = que'
                                            , quePtr  = qPtr
                                            , arrType = t2 } } =
       let Just p = t2 =~= t1 in
@@ -91,7 +106,7 @@
         W.SymWordInst -> 
           case W.hasSignAndSizeInst t2 of
             W.HasSignAndSizeInst ->
-              coerce (cong p) (Q.lookahead i que qPtr)
+              coerce (cong p) (Q.lookahead i que' qPtr)
 
   ----------------------------------------------------
 
@@ -115,39 +130,46 @@
 
   ----------------------------------------------------
 
-  C.ExternVar t name ->
-    let ext :: ExtInput
-        Just ext = foldl 
-          ( \acc x -> case x of
-                        ArrIn _ _ -> acc
-                        ExtIn nm e -> if nm == name then Just e
-                                        else acc ) 
-          Nothing
-          inputs 
-    in getSBV t ext
+  C.ExternVar t name _ -> 
+    getSBV t ext
 
     where 
+    ext :: ExtInput
+    ext = lookupInput name (extVars inputs) 
+
     getSBV :: C.Type a -> ExtInput -> S.SBV a
-    getSBV t1 ExtInput { extInput = ext
+    getSBV t1 ExtInput { extInput = ext'
                        , extType  = t2 } =
       let Just p = t2 =~= t1 in
-      coerce (cong p) ext
+      coerce (cong p) ext'
 
   ----------------------------------------------------
 
-  -- externFun t name _ = C2AExpr $ \ _ meta ->
-  --   let Just extFunInfo = M.lookup name (externFunInfoMap meta) in
-  --   externFun1 t extFunInfo
+  C.ExternArray _ t name _ _ _ _ -> 
+    getSBV t getExtArr
 
-  --   where
-  --   externFun1 t1
-  --     ExternFunInfo
-  --       { externFunInfoVar  = var
-  --       , externFunInfoType = t2
-  --       } =
-  --     let Just p = t2 =~= t1 in
-  --     case W.exprInst t2 of
-  --       W.ExprInst -> coerce (cong p) (A.value var)
+    where 
+    getExtArr :: ExtInput
+    getExtArr = lookupInput name (extArrs inputs)
+
+    getSBV t1 ExtInput { extInput  = v
+                       , extType = t2 }
+      = let Just p = t2 =~= t1 in
+        coerce (cong p) v
+
+  ----------------------------------------------------
+
+  C.ExternFun t name _ _ _ ->
+    getSBV t getExtFun
+
+    where
+    getExtFun :: ExtInput
+    getExtFun = lookupInput name (extFuns inputs)
+
+    getSBV t1 ExtInput { extType  = t2
+                       , extInput = v }
+      = let Just p = t2 =~= t1 in
+        coerce (cong p) v
  
   ----------------------------------------------------
 
@@ -189,6 +211,9 @@
   BwNot t -> case W.bitsInst    t of 
                        W.BitsInst            -> (S.complement)
 
+  Cast t0 t1 -> case W.castInst t0 t1 of 
+                  W.CastInst -> W.sbvCast
+
   Recip _ -> noFloatOpsErr "recip"
   Exp   _ -> noFloatOpsErr "exp"
   Sqrt  _ -> noFloatOpsErr "sqrt"
@@ -235,6 +260,20 @@
   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.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, shiftL only supports constant shift indicies"
+                                         Just x  -> S.shiftL vec (fromIntegral x)
+  BwShiftR tvec tidx -> 
+    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"
+                                         Just x  -> S.shiftR vec (fromIntegral x)
 
   Fdiv  _ -> noFloatOpsErr "fdiv"
   Pow   _ -> noFloatOpsErr "pow"
@@ -245,3 +284,7 @@
   Mux t ->
     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
@@ -24,6 +24,7 @@
 import Copilot.Compile.SBV.Params
 
 import qualified Copilot.Core as C
+--import Copilot.Core.Type.Equality ((=~=), coerce, cong)
 import qualified Copilot.Core.Type.Show as C (showWithType, ShowType(..))
 import Copilot.Compile.Header.C99 (c99HeaderName)
 
@@ -44,6 +45,7 @@
 mkArgs :: [Doc] -> Doc
 mkArgs args = hsep (punctuate comma args)
 
+-- | Call a C function.
 mkFuncCall :: String -> [Doc] -> Doc
 mkFuncCall f args = text f <> lparen <> mkArgs args <> rparen
 
@@ -88,22 +90,24 @@
     mkFunc (withPrefix (prefix params) "step")
            (   mkFuncCall sampleExtsF    [] <> semi
             $$ mkFuncCall updateStatesF  [] <> semi
+            $$ mkFuncCall updateBuffersF [] <> semi
+            $$ mkFuncCall updatePtrsF    [] <> semi
             $$ mkFuncCall observersF     [] <> semi
             $$ mkFuncCall triggersF      [] <> semi
-            $$ mkFuncCall updateBuffersF [] <> semi
-            $$ mkFuncCall updatePtrsF    [] <> semi)
+           )
 
   copilot = vcat $ intersperse (text "")
     [ sampleExts meta
     , updateStates streams
-    , fireTriggers meta
-    , updateObservers params meta
     , updateBuffers meta
-    , updatePtrs meta ]
+    , updatePtrs meta 
+    , updateObservers params meta
+    , fireTriggers meta
+    ]
 
 --------------------------------------------------------------------------------
 
--- Declare gloabl variables.
+-- Declare global variables.
 
 data Decl = Decl { retT    :: Doc
                  , declVar :: Doc
@@ -115,15 +119,15 @@
   where
   getVars :: MetaTable -> [Decl] 
   getVars MetaTable { streamInfoMap = streams 
-                    , externInfoMap = externs } = 
+                    , externVarInfoMap = externs } = 
        map getTmpStVars (M.toList streams)
     ++ map getQueueVars (M.toList streams)
     ++ map getQueuePtrVars (map fst $ M.toList streams)
     ++ map getExtVars (M.toList externs)
 
-  getTmpStVars :: (C.Id, StreamInfo) -> Decl
-  getTmpStVars (id, StreamInfo { streamInfoType  = t
-                               , streamInfoQueue = que }) = 
+  getTmpStVars :: (C.Id, C.Stream) -> Decl
+  getTmpStVars (id, C.Stream { C.streamExprType  = t
+                               , C.streamBuffer = que }) = 
     Decl (retType t) (text $ mkTmpStVar id) getFirst
     where 
     -- ASSUME queue is nonempty!
@@ -131,9 +135,9 @@
     headErr [] = C.impossible "headErr" "copilot-sbv"
     headErr xs = head xs
   
-  getQueueVars :: (C.Id, StreamInfo) -> Decl
-  getQueueVars (id, StreamInfo { streamInfoType = t
-                               , streamInfoQueue = que }) =
+  getQueueVars :: (C.Id, C.Stream) -> Decl
+  getQueueVars (id, C.Stream { C.streamExprType = t
+                             , C.streamBuffer = que }) =
     Decl (retType t) 
          (text (mkQueueVar id) <> lbrack <> int (length que) <> rbrack)
          getInits
@@ -151,8 +155,8 @@
     queSize :: C.Type QueueSize
     queSize = C.typeOf 
 
-  getExtVars :: (C.Name, C.UType) -> Decl
-  getExtVars (var, C.UType { C.uTypeType = t }) = 
+  getExtVars :: (C.Name, C.ExtVar) -> Decl
+  getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) = 
     Decl (retType t) (text $ mkExtTmpVar var) (int 0)
 
   varDecl :: Decl -> Doc
@@ -175,44 +179,89 @@
     C.Observer
       { C.observerName     = name
       , C.observerExprType = t } =
-    retType t <+> text (withPrefix prfx name) <> text ";"
+    retType t <+> text (withPrefix prfx name) <> semi
 
 --------------------------------------------------------------------------------
 
 sampleExts :: MetaTable -> Doc
-sampleExts MetaTable { externInfoMap = extMap } =
-  mkFunc sampleExtsF $ vcat $ map sampleExt ((fst . unzip . M.toList) extMap)
+sampleExts MetaTable { externVarInfoMap = extVMap
+                     , externArrInfoMap = extAMap
+                     , 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.  We could write it
+  -- differently, but it's easier.  The Analyzer.hs copilot-core prevents arrays
+  -- or functions from being used in arrays or functions.
+  mkFunc sampleExtsF $ vcat (extVars ++ extArrs ++ extFuns)
 
   where
-  sampleExt :: C.Name -> Doc
-  sampleExt name = text (mkExtTmpVar name) <+> equals <+> text name <> semi
+  extVars = map sampleVExt ((fst . unzip . M.toList) extVMap)
+  extArrs = map sampleAExt (M.toList extAMap)
+  extFuns = map sampleFExt (M.toList extFMap)
 
 --------------------------------------------------------------------------------
 
+-- Variables
+sampleVExt :: C.Name -> Doc
+sampleVExt name = 
+  text (mkExtTmpVar name) <+> equals <+> text name <> semi
+
+--------------------------------------------------------------------------------
+-- Arrays
+
+-- Currenty, Analyze.hs in copilot-language forbids recurssion in
+-- external arrays or functions (i.e., an external array can't use another
+-- external array to compute it's index), so a lot of what is below isn't
+-- currently necessary.
+sampleAExt :: (C.Name, C.ExtArray) -> Doc
+sampleAExt (name, C.ExtArray { C.externArrayIdx = idx })
+  = 
+  text (mkExtTmpVar name) <+> equals <+> arrIdx name idx
+ 
+  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 = 
+    mkFuncCall (mkExtArrFn name) (map text $ collectArgs e)
+
+--------------------------------------------------------------------------------
+
+-- External functions
+sampleFExt :: (C.Name, C.ExtFun) -> Doc
+sampleFExt (name, C.ExtFun { C.externFunArgs = args })
+  = 
+  text (mkExtTmpVar name) <+> equals <+> text name <> lparen
+    <+> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args))
+    <> rparen <> semi
+
+     where
+     mkArgCall = undefined--  (i, ( C.UType { C.uTypeType = t}
+
+--------------------------------------------------------------------------------
+
 updateStates :: [C.Stream] -> Doc
 updateStates streams =
   mkFunc updateStatesF $ vcat $ map updateSt streams
-
   where
-  -- tmp_X = updateState(arg0, arg1, ... );
   updateSt :: C.Stream -> Doc
   updateSt C.Stream { C.streamId   = id
                     , C.streamExpr = e } =
     text (mkTmpStVar id) <+> equals
       <+> mkFuncCall (mkUpdateStFn id)
-                     (map text getArgs)
-      <> semi
-    where
-    getArgs :: [String]
-    getArgs = concatMap argToCall (c2Args e)
+                     (map text $ collectArgs e)
+      <>  semi
 
 --------------------------------------------------------------------------------
 
 updateObservers :: Params -> MetaTable -> Doc
-updateObservers params MetaTable { observerInfoMap = observers } =
-
+updateObservers params MetaTable { observerInfoMap = observers } 
+  =
   mkFunc observersF $ vcat $ map updateObsv (M.toList observers)
-
   where
   updateObsv :: (C.Name, ObserverInfo) -> Doc
   updateObsv (name, ObserverInfo { observerArgs = args }) =
@@ -222,20 +271,23 @@
 --------------------------------------------------------------------------------
 
 fireTriggers :: MetaTable -> Doc
-fireTriggers MetaTable { triggerInfoMap = triggers } =
-
+fireTriggers MetaTable { triggerInfoMap = triggers } 
+  =
   mkFunc triggersF $ vcat $ map fireTrig (M.toList triggers)
 
   where
   -- if (guard) trigger(args);
   fireTrig :: (C.Name, TriggerInfo) -> Doc
   fireTrig (name, TriggerInfo { guardArgs      = gArgs
-                              , triggerArgArgs = argArgs }) =
-    text "if" <+> lparen <> guardF <> rparen <+>
-      mkFuncCall name (map mkArg (mkTriggerArgIdx argArgs)) <> semi
+                              , triggerArgArgs = argArgs }) 
+    = 
+    let f = mkFuncCall name (map mkArg (mkTriggerArgIdx argArgs)) <> semi in
+    text "if" <+> lparen <> guardF <> rparen $+$ nest 2 f
+
     where
     guardF :: Doc
     guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs)
+
     mkArg :: (Int, [String]) -> Doc
     mkArg (i, args) =
       mkFuncCall (mkTriggerArgFn i name) (map text args)
@@ -243,11 +295,12 @@
 --------------------------------------------------------------------------------
 
 updateBuffers :: MetaTable -> Doc
-updateBuffers MetaTable { streamInfoMap = strMap } =
+updateBuffers MetaTable { streamInfoMap = strMap } 
+  =
   mkFunc updateBuffersF $ vcat $ map updateBuf (M.toList strMap)
 
   where
-  updateBuf :: (C.Id, StreamInfo) -> Doc
+  updateBuf :: (C.Id, C.Stream) -> Doc
   updateBuf (id, _) =
     updateFunc (mkQueueVar id) (mkQueuePtrVar id) (mkTmpStVar id)
 
@@ -263,8 +316,8 @@
   mkFunc updatePtrsF $ vcat $ map varAndUpdate (M.toList strMap)
 
   where 
-  varAndUpdate :: (C.Id, StreamInfo) -> Doc
-  varAndUpdate (id, StreamInfo { streamInfoQueue = que }) =
+  varAndUpdate :: (C.Id, C.Stream) -> Doc
+  varAndUpdate (id, C.Stream { C.streamBuffer = que }) =
     updateFunc (fromIntegral $ length que) (mkQueuePtrVar id)
 
   -- idx = (idx + 1) % queueSize;
@@ -276,7 +329,8 @@
 
 --------------------------------------------------------------------------------
 
-sampleExtsF, triggersF, observersF, updatePtrsF, updateBuffersF, updateStatesF :: String
+sampleExtsF, triggersF, observersF, updatePtrsF :: String
+updateBuffersF, updateStatesF :: String
 updatePtrsF    = "updatePtrs"
 updateBuffersF = "updateBuffers"
 updateStatesF  = "updateStates"
diff --git a/src/Copilot/Compile/SBV/Makefile.hs b/src/Copilot/Compile/SBV/Makefile.hs
--- a/src/Copilot/Compile/SBV/Makefile.hs
+++ b/src/Copilot/Compile/SBV/Makefile.hs
@@ -28,7 +28,8 @@
   wr (text "# Makefile rules for the Copilot driver.")
   wr (text "")
   wr $ text "driver" <> colon 
-        <+> text (driverName params) <+> text fileName <> text ".h"
+        <+> text (driverName params) <+> text fileName <> text ".h" 
+        <+> text "internal.a"
   wr $ text "\t" 
          <> (hsep [ text "$" <> braces (text "CC")
                   , text "$" <> braces (text "CCFLAGS")
diff --git a/src/Copilot/Compile/SBV/MetaTable.hs b/src/Copilot/Compile/SBV/MetaTable.hs
--- a/src/Copilot/Compile/SBV/MetaTable.hs
+++ b/src/Copilot/Compile/SBV/MetaTable.hs
@@ -5,10 +5,11 @@
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
 
 module Copilot.Compile.SBV.MetaTable
-  ( StreamInfo (..)
-  , StreamInfoMap
-  , ExternInfoMap
-  , ExternFunInfo (..)
+  ( --StreamInfo (..)
+    StreamInfoMap
+  , ExternVarInfoMap
+  , ExternArrInfoMap
+--  , ExternFunInfo (..)
   , ExternFunInfoMap
   , TriggerInfo (..)
   , TriggerInfoMap
@@ -16,39 +17,26 @@
   , ObserverInfoMap
   , MetaTable (..)
   , allocMetaTable
-  , argToCall
+  , collectArgs
   , Arg(..)
   , c2Args
   ) where
 
 import Copilot.Compile.SBV.Common
 import qualified Copilot.Core as C
---import qualified Copilot.Core.External as C (ExternVar (..), externVars)
 
 import Data.Map (Map)
 import Data.List (nub)
+import Data.Maybe (fromJust)
 import qualified Data.Map as M
 import Prelude hiding (id)
 
 --------------------------------------------------------------------------------
 
-data StreamInfo = forall a . StreamInfo
-  { streamInfoQueue   :: [a]
-  , streamInfoType    :: C.Type a }
-
-type StreamInfoMap = Map C.Id StreamInfo
-
---------------------------------------------------------------------------------
-
-type ExternInfoMap = Map C.Name C.UType
-
---------------------------------------------------------------------------------
-
-data ExternFunInfo = forall a . ExternFunInfo
-  { externFunInfoArgs :: [(C.UType, C.UExpr)]
-  , externFunInfoType :: C.Type a }
-
-type ExternFunInfoMap = Map C.Name ExternFunInfo
+type StreamInfoMap = Map C.Id C.Stream
+type ExternVarInfoMap = Map C.Name C.ExtVar
+type ExternArrInfoMap = Map C.Name C.ExtArray
+type ExternFunInfoMap = Map C.Name C.ExtFun
 
 --------------------------------------------------------------------------------
 
@@ -69,7 +57,8 @@
 
 data MetaTable = MetaTable
   { streamInfoMap     :: StreamInfoMap
-  , externInfoMap     :: ExternInfoMap
+  , externVarInfoMap  :: ExternVarInfoMap
+  , externArrInfoMap  :: ExternArrInfoMap
   , externFunInfoMap  :: ExternFunInfoMap
   , triggerInfoMap    :: TriggerInfoMap
   , observerInfoMap   :: ObserverInfoMap }
@@ -79,50 +68,56 @@
 allocMetaTable :: C.Spec -> MetaTable
 allocMetaTable spec =
   let
-    streamInfoMap_   = M.fromList $ map allocStream (C.specStreams spec)
-    externInfoMap_   = M.fromList $ map allocExtern (C.externVars spec)
-    triggerInfoMap_  = M.fromList $ map allocTrigger (C.specTriggers spec)
-    observerInfoMap_ = M.fromList $ map allocObserver (C.specObservers spec)
+    streamInfoMap_    = M.fromList $ map allocStream     (C.specStreams spec)
+    externVarInfoMap_ = M.fromList $ map allocExternVars (C.externVars spec)
+    externArrInfoMap_ = M.fromList $ map allocExternArrs (C.externArrays spec)
+    externFunInfoMap_ = M.fromList $ map allocExternFuns (C.externFuns spec)
+    triggerInfoMap_   = M.fromList $ map allocTrigger    (C.specTriggers spec)
+    observerInfoMap_  = M.fromList $ map allocObserver   (C.specObservers spec)
   in
-    MetaTable
-      streamInfoMap_
-      externInfoMap_
-      (error "undefined in MetaTable.hs in copilot-sbv.")
-      triggerInfoMap_
-      observerInfoMap_
+    MetaTable { streamInfoMap    = streamInfoMap_
+              , externVarInfoMap = externVarInfoMap_
+              , externArrInfoMap = externArrInfoMap_
+              , externFunInfoMap = externFunInfoMap_
+              , triggerInfoMap   = triggerInfoMap_
+              , observerInfoMap  = observerInfoMap_
+              }
+      
+--------------------------------------------------------------------------------
 
+allocStream :: C.Stream -> (C.Id, C.Stream)
+allocStream strm = 
+  (C.streamId strm, strm)
+
 --------------------------------------------------------------------------------
 
-allocStream :: C.Stream -> (C.Id, StreamInfo)
-allocStream C.Stream
-              { C.streamId       = id
-              , C.streamBuffer   = buf
-              , C.streamExprType = t
-              } =
-  let
-    strmInfo =
-      StreamInfo
-        { streamInfoQueue       = buf
-        , streamInfoType        = t } in
-  (id, strmInfo)
+allocExternVars :: C.ExtVar -> (C.Name, C.ExtVar)
+allocExternVars var =
+  (C.externVarName var, var)
 
 --------------------------------------------------------------------------------
 
-allocExtern :: C.ExtVar -> (C.Name, C.UType)
-allocExtern (C.ExtVar name t) =
-  (name, t)
+allocExternArrs :: C.ExtArray -> (C.Name, C.ExtArray)
+allocExternArrs arr =
+  (C.externArrayName arr, arr)
 
 --------------------------------------------------------------------------------
 
+allocExternFuns :: C.ExtFun -> (C.Name, C.ExtFun)
+allocExternFuns fun =
+  (C.externFunName fun, fun)
+
+--------------------------------------------------------------------------------
+
 allocTrigger :: C.Trigger -> (C.Name, TriggerInfo)
 allocTrigger C.Trigger { C.triggerName  = name
                        , C.triggerGuard = guard
-                       , C.triggerArgs  = args } = 
+                       , C.triggerArgs  = args } 
+  =
   let mkArgArgs :: C.UExpr -> [String]
-      mkArgArgs C.UExpr { C.uExprExpr = e } = 
-        nub (concatMap argToCall (c2Args e)) in
+      mkArgArgs C.UExpr { C.uExprExpr = e } = collectArgs e in
   let triggerInfo = 
-        TriggerInfo { guardArgs      = nub (concatMap argToCall (c2Args guard))
+        TriggerInfo { guardArgs      = collectArgs guard 
                     , triggerArgArgs = map mkArgArgs args } in
   (name, triggerInfo)
 
@@ -130,31 +125,38 @@
 
 allocObserver :: C.Observer -> (C.Name, ObserverInfo)
 allocObserver C.Observer { C.observerName = name
-                         , C.observerExpr = e } =
-  let
-    observerInfo =
-      ObserverInfo { observerArgs = nub (concatMap argToCall (c2Args e)) }
-  in
-    (name, observerInfo)
+                         , C.observerExpr = e } 
+  = 
+  let observerInfo = ObserverInfo { observerArgs = collectArgs e } in
+  (name, observerInfo)
 
 --------------------------------------------------------------------------------
--- Getting SBV function args from the expressions.
 
-c2Args :: C.Expr a -> [Arg]
-c2Args e = nub $ c2Args_ e
-
 -- Kinds of arguments to SBV functions
 data Arg = Extern    C.Name
-         | ExternFun C.Name
+         | ExternFun C.Name C.Tag
          | ExternArr C.Name
          | Queue     C.Id
   deriving Eq
 
+-- | Normal argument calls.
 argToCall :: Arg -> [String]
-argToCall (Extern name) = [mkExtTmpVar name]
-argToCall (Queue id ) = [ mkQueueVar id 
-                        , mkQueuePtrVar id ]
+argToCall (Extern name)        = [mkExtTmpVar name]
+argToCall (ExternArr name)     = [mkExtTmpVar name]
+argToCall (ExternFun name tag) = [mkExtTmpFun name tag]
+argToCall (Queue id)           = [ mkQueueVar id 
+                                 , mkQueuePtrVar id ]
 
+--------------------------------------------------------------------------------
+
+collectArgs :: C.Expr a -> [String]
+collectArgs e = concatMap argToCall (nub $ c2Args e)
+
+-- extCollectArgs :: C.Expr a -> [String]
+-- extCollectArgs e = nub (concatMap extArgToCall (c2Args e))
+
+--------------------------------------------------------------------------------
+
 -- Gathers the names of the arguments to the SBV updateState function so that we
 -- can construct the prototypes.
 
@@ -163,27 +165,33 @@
 -- are pushed into the SBVCodeGen.  However, there should really be an API for
 -- getting the prototypes.
 
+c2Args :: C.Expr a -> [Arg]
+c2Args e = nub $ c2Args_ e
+
 c2Args_ :: C.Expr a -> [Arg]
 c2Args_ e0 = case e0 of
-  C.Const _ _ -> [] 
+  C.Const _ _            -> [] 
 
-  C.Drop _ _ id -> [ Queue id ]
+  C.Drop _ _ id          -> [ Queue id ]
  
-  C.Local _ _ _ e1 e2 -> c2Args_ e1 ++ c2Args_ e2
+  C.Local _ _ _ e1 e2    -> c2Args_ e1 ++ c2Args_ e2
 
-  C.Var _ _ -> []
+  C.Var _ _              -> []
 
-  C.ExternVar   _ name -> [Extern name]
+  C.ExternVar   _ name _ -> [Extern name]
 
-  C.ExternFun   _ name args _ -> 
-    ExternFun name : concatMap (\C.UExpr { C.uExprExpr = expr } 
-                                             -> c2Args expr) 
-                                        args
+  C.ExternFun   _ name args _ tag -> 
+    (ExternFun name (fromJust tag)) : 
+      concatMap (\C.UExpr { C.uExprExpr = expr } 
+                     -> c2Args expr) 
+                args
 
-  C.ExternArray _ _ name idx _ -> ExternArr name : c2Args_ idx
+  C.ExternArray _ _ name _ _ _ _  -> [ExternArr name] 
 
-  C.Op1 _ e -> c2Args_ e
+  C.Op1 _ e        -> c2Args_ e
 
-  C.Op2 _ e1 e2 -> c2Args_ e1 ++ c2Args_ e2
+  C.Op2 _ e1 e2    -> c2Args_ e1 ++ c2Args_ e2
 
   C.Op3 _ e1 e2 e3 -> c2Args_ e1 ++ c2Args_ e2 ++ c2Args_ e3
+
+--------------------------------------------------------------------------------
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
@@ -2,12 +2,14 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
-{-# LANGUAGE FlexibleContexts, GADTs #-}
+{-# LANGUAGE FlexibleContexts, GADTs, MultiParamTypeClasses #-}
 
 module Copilot.Compile.SBV.Witness
   ( SymWordInst(..)       , symWordInst
+  , NumInst(..)           , numInst
   , HasSignAndSizeInst(..), hasSignAndSizeInst
   , EqInst(..)            , eqInst 
+  , CastInst(..)          , castInst   , sbvCast
   , BVDivisibleInst(..)   , divInst
   , OrdInst(..)           , ordInst 
   , MergeableInst(..)     , mergeableInst 
@@ -18,6 +20,8 @@
 import qualified Data.SBV.Internals as S
 import qualified Copilot.Core as C
 
+import Data.Word (Word8, Word16, Word32, Word64)
+import Data.Int (Int8, Int16, Int32, Int64)
 import Data.Bits
 
 --------------------------------------------------------------------------------
@@ -42,6 +46,21 @@
 
 --------------------------------------------------------------------------------
 
+data NumInst a = Num a => NumInst
+
+numInst :: C.Type a -> NumInst a
+numInst t =
+  case t of
+    C.Bool   -> badInst
+    C.Int8   -> NumInst ; C.Int16  -> NumInst
+    C.Int32  -> NumInst ; C.Int64  -> NumInst
+    C.Word8  -> NumInst ; C.Word16 -> NumInst
+    C.Word32 -> NumInst ; C.Word64 -> NumInst
+    C.Float  -> badInst
+    C.Double -> badInst
+
+--------------------------------------------------------------------------------
+
 data HasSignAndSizeInst a = S.HasSignAndSize a => HasSignAndSizeInst
 
 hasSignAndSizeInst :: C.Type a -> HasSignAndSizeInst a
@@ -139,3 +158,187 @@
     C.Double -> badInst
 
 --------------------------------------------------------------------------------
+
+data CastInst a b = SBVCast a b => CastInst
+
+castInst :: C.Type a -> C.Type b -> CastInst a b
+castInst t0 t1 = 
+  case t0 of
+    C.Bool   -> case t1 of
+                  C.Bool    -> CastInst
+                  C.Word8   -> CastInst
+                  C.Word16  -> CastInst
+                  C.Word32  -> CastInst
+                  C.Word64  -> CastInst
+                  C.Int8    -> CastInst
+                  C.Int16   -> CastInst
+                  C.Int32   -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+
+    C.Word8  -> case t1 of
+                  C.Word8   -> CastInst
+                  C.Word16  -> CastInst
+                  C.Word32  -> CastInst
+                  C.Word64  -> CastInst
+                  C.Int16   -> CastInst
+                  C.Int32   -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Word16 -> case t1 of
+                  C.Word16  -> CastInst
+                  C.Word32  -> CastInst
+                  C.Word64  -> CastInst
+                  C.Int32   -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Word32 -> case t1 of
+                  C.Word32  -> CastInst
+                  C.Word64  -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Word64 -> case t1 of
+                  C.Word64  -> CastInst
+                  _         -> badInst
+
+    C.Int8   -> case t1 of
+                  C.Int8    -> CastInst
+                  C.Int16   -> CastInst
+                  C.Int32   -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Int16  -> case t1 of
+                  C.Int16   -> CastInst
+                  C.Int32   -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Int32  -> case t1 of
+                  C.Int32   -> CastInst
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Int64  -> case t1 of
+                  C.Int64   -> CastInst
+                  _         -> badInst
+    C.Float  -> badInst
+    C.Double -> badInst
+
+--------------------------------------------------------------------------------
+-- | A class for casting SBV values.  We return errors for casts allowed by
+-- Copilot.
+
+class SBVCast a b where
+  sbvCast :: S.SBV a -> S.SBV b
+
+--------------------------------------------------------------------------------
+
+castBool :: (Num a, S.SymWord a) => S.SBV Bool -> S.SBV a
+castBool x = case S.unliteral x of
+               Just bool -> if bool then 1 else 0
+               Nothing   -> S.ite x 1 0
+
+castErr :: a
+castErr = C.badUsage $ "the SBV backend does not currently support casts to signed word types"
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Bool Bool where
+  sbvCast = id
+instance SBVCast Bool Word8 where
+  sbvCast = castBool
+instance SBVCast Bool Word16 where
+  sbvCast = castBool
+instance SBVCast Bool Word32 where
+  sbvCast = castBool
+instance SBVCast Bool Word64 where
+  sbvCast = castBool
+
+instance SBVCast Bool Int8 where
+  sbvCast = castErr 
+instance SBVCast Bool Int16 where
+  sbvCast = castErr 
+instance SBVCast Bool Int32 where
+  sbvCast = castErr 
+instance SBVCast Bool Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Word8 Word8 where
+  sbvCast = id
+instance SBVCast Word8 Word16 where
+  sbvCast = S.extend
+instance SBVCast Word8 Word32 where
+  sbvCast = S.extend . S.extend
+instance SBVCast Word8 Word64 where
+  sbvCast = S.extend . S.extend . S.extend
+
+instance SBVCast Word8 Int16 where
+  sbvCast = castErr 
+instance SBVCast Word8 Int32 where
+  sbvCast = castErr 
+instance SBVCast Word8 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Word16 Word16 where
+  sbvCast = id
+instance SBVCast Word16 Word32 where
+  sbvCast = S.extend
+instance SBVCast Word16 Word64 where
+  sbvCast = S.extend . S.extend
+
+instance SBVCast Word16 Int32 where
+  sbvCast = castErr 
+instance SBVCast Word16 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Word32 Word32 where
+  sbvCast = id
+instance SBVCast Word32 Word64 where
+  sbvCast = S.extend
+
+instance SBVCast Word32 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Word64 Word64 where
+  sbvCast = id
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Int8 Int8 where
+  sbvCast = castErr 
+instance SBVCast Int8 Int16 where
+  sbvCast = castErr 
+instance SBVCast Int8 Int32 where
+  sbvCast = castErr 
+instance SBVCast Int8 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Int16 Int16 where
+  sbvCast = castErr 
+instance SBVCast Int16 Int32 where
+  sbvCast = castErr 
+instance SBVCast Int16 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Int32 Int32 where
+  sbvCast = castErr 
+instance SBVCast Int32 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+
+instance SBVCast Int64 Int64 where
+  sbvCast = castErr 
+
+--------------------------------------------------------------------------------
+