diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -456,9 +456,9 @@
 
 class Assign a where
   (<==) :: V a -> E a -> Stmt ()
-instance Assign Bool  where a <== b = statement $ AssignBool  a b
-instance Assign Int   where a <== b = statement $ AssignInt   a b
-instance Assign Float where a <== b = statement $ AssignFloat a b
+instance Assign Bool  where a <== b = statement $ Assign a b
+instance Assign Int   where a <== b = statement $ Assign a b
+instance Assign Float where a <== b = statement $ Assign a b
 
 -- | Assert that a condition is true.
 assert :: E Bool -> Stmt ()
@@ -497,7 +497,7 @@
 
 -- | Verify a program.
 --
--- ^ verify pathToYices maxK program
+-- > verify pathToYices maxK program
 verify :: FilePath -> Int -> Stmt () -> IO ()
 verify yices maxK program = V.verify yices maxK $ snd $ evalStmt [] program
 
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -15,30 +15,31 @@
     ++ "#include <assert.h>\n\n"
     ++ codeVariables True scope ++ "\n"
     ++ "void " ++ name ++ "()\n{\n"
-    ++ indent (codeStmt [] stmt)
+    ++ indent (codeStmt name [] stmt)
     ++ "}\n\n"
   writeFile (name ++ ".h") $
        "/* Generated by ImProve. */\n\n"
     ++ codeVariables False scope ++ "\n"
     ++ "void " ++ name ++ "(void);\n\n"
   where
-  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of
-    [] -> error "program contains no usefull statements"
+  scope = case tree (\ (_, path, _) -> path) $ map varInfo $ stmtVars stmt of
+    [] -> error "program contains no useful statements"
     a  -> T.Branch (name ++ "_variables") a
 
-  codeStmt :: [Name] -> Statement -> String
-  codeStmt path a = case a of
-    AssignBool  a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"
-    AssignInt   a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"
-    AssignFloat a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"
-    Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt path b) ++ "}\n"
-    Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt path b) ++ "}\nelse {\n" ++ indent (codeStmt path c) ++ "}\n"
-    Sequence a b -> codeStmt path a ++ codeStmt path b
-    Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
-    Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
-    Label  name a -> "/*" ++ name ++ "*/\n" ++ indent (codeStmt (path ++ [name]) a)
-    Null -> ""
-  
+instance Show Statement where show = codeStmt "none" []
+
+codeStmt :: Name -> [Name] -> Statement -> String
+codeStmt name path a = case a of
+  Assign a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"
+  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n"
+  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n"
+  Sequence a b -> codeStmt name path a ++ codeStmt name path b
+  Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
+  Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"
+  Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)
+  Null -> ""
+  where
+
   codeExpr :: E a -> String
   codeExpr a = case a of
     Ref a     -> name ++ "_variables." ++ pathName a
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -1,6 +1,7 @@
 module Language.ImProve.Core
   ( E (..)
   , V (..)
+  , UV (..)
   , Name
   , Path
   , PathName (..)
@@ -22,28 +23,39 @@
 type Path = [Name]
 
 -- | A mutable variable.
-data V a = V Bool [Name] a deriving Eq
+data V a = V Bool [Name] a deriving (Eq, Ord)
 
+-- | An untyped variable.
+data UV
+  = UVBool  (V Bool)
+  | UVInt   (V Int)
+  | UVFloat (V Float)
+  deriving (Eq, Ord)
+
 class    PathName a         where pathName :: a -> String
 instance PathName Path      where pathName = intercalate "."
 instance PathName (V a)     where pathName (V _ path _) = pathName path
 instance PathName VarInfo   where pathName (_, path, _) = pathName path
 
-class AllE a where
+class Eq a => AllE a where
   zero   :: (Name -> a -> m (V a)) -> a
   const' :: a -> Const
+  untype :: V a -> UV
 
 instance AllE Bool where
   zero = const False
   const' = Bool
+  untype = UVBool
 
 instance AllE Int where
   zero = const 0
   const' = Int
+  untype = UVInt
   
 instance AllE Float where
   zero = const 0
   const' = Float
+  untype = UVFloat
 
 class    AllE a => NumE a
 instance NumE Int
@@ -85,16 +97,14 @@
   recip a = 1 / a
   fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r)
 
-data Statement
-  = AssignBool  (V Bool ) (E Bool )
-  | AssignInt   (V Int  ) (E Int  )
-  | AssignFloat (V Float) (E Float)
-  | Branch      (E Bool) Statement Statement
-  | Sequence    Statement Statement
-  | Assert      (E Bool)
-  | Assume      (E Bool)
-  | Label       Name Statement
-  | Null
+data Statement where
+  Assign   :: AllE a => V a -> E a -> Statement
+  Branch   :: E Bool -> Statement -> Statement -> Statement
+  Sequence :: Statement -> Statement -> Statement
+  Assert   :: E Bool -> Statement
+  Assume   :: E Bool -> Statement
+  Label    :: Name -> Statement -> Statement
+  Null     :: Statement
 
 data Const
   = Bool  Bool
@@ -104,26 +114,29 @@
 
 type VarInfo = (Bool, Path, Const)
 
-varInfo :: AllE a => V a -> VarInfo
-varInfo (V input path init) = (input, path, const' init)
+class VarInfo' a where varInfo :: a -> VarInfo
+instance AllE a => VarInfo' (V a) where varInfo (V input path init) = (input, path, const' init)
+instance VarInfo' UV where
+  varInfo a = case a of
+    UVBool a  -> varInfo a
+    UVInt  a  -> varInfo a
+    UVFloat a -> varInfo a
 
--- Information about all of a program's variables.
-stmtVars :: Statement -> [VarInfo]
+-- Variables in a program.
+stmtVars :: Statement -> [UV]
 stmtVars a = case a of
-  AssignBool  a b -> nub $ varInfo a : exprVars b
-  AssignInt   a b -> nub $ varInfo a : exprVars b
-  AssignFloat a b -> nub $ varInfo a : exprVars b
-  Branch a b c    -> nub $ exprVars a ++ stmtVars b ++ stmtVars c
-  Sequence a b    -> nub $ stmtVars a ++ stmtVars b
-  Assert a        -> exprVars a
-  Assume a        -> exprVars a
-  Label  _ a      -> stmtVars a
-  Null            -> []
+  Assign a b   -> nub $ untype a : exprVars b
+  Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c
+  Sequence a b -> nub $ stmtVars a ++ stmtVars b
+  Assert a     -> exprVars a
+  Assume a     -> exprVars a
+  Label  _ a   -> stmtVars a
+  Null         -> []
 
--- Information about all of an expressions's variables.
-exprVars :: E a -> [VarInfo]
+-- Variables in an expression.
+exprVars :: E a -> [UV]
 exprVars a = case a of
-  Ref a     -> [varInfo a]
+  Ref a     -> [untype a]
   Const _   -> []
   Add a b   -> exprVars a ++ exprVars b
   Sub a b   -> exprVars a ++ exprVars b
diff --git a/Language/ImProve/Narrow.hs b/Language/ImProve/Narrow.hs
--- a/Language/ImProve/Narrow.hs
+++ b/Language/ImProve/Narrow.hs
@@ -11,40 +11,38 @@
   assumes = foldl Sequence Null [ Label lab $ Assume assume | (lab, opt) <- optimizations, assume <- opt stmt ]
   optimizations =
     [ ("constantAssigns", constantAssigns)
+    , ("timerRanges",     timerRanges)
     ]
 
 constantAssigns :: Statement -> [E Bool]
 constantAssigns stmt = mapMaybe f1 $ stmtVars stmt
   where
-  f1 :: VarInfo -> Maybe (E Bool)
-  f1 info@(input, path, init)
+  f1 :: UV -> Maybe (E Bool)
+  f1 uv
     | input = Nothing
     | otherwise = do
-      assigns <- lastConstAssign info stmt
+      assigns <- lastConstAssign uv stmt
       case (init, nub $ init : assigns) of
         (Bool _, [_, _]) -> Nothing
 	(_, a) -> return $ foldl1 Or $ map f2 a
-      where
-      f2 :: Const -> E Bool
-      f2 assign = case (init, assign) of
-        (Bool  a, Bool  b) -> Eq (Ref (V input path a)) (Const b)
-        (Int   a, Int   b) -> Eq (Ref (V input path a)) (Const b)
-        (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)
-        _ -> undefined
+    where
+    f2 :: Const -> E Bool
+    f2 assign = case (init, assign) of
+      (Bool  a, Bool  b) -> Eq (Ref (V input path a)) (Const b)
+      (Int   a, Int   b) -> Eq (Ref (V input path a)) (Const b)
+      (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)
+      _ -> undefined
+    (input, path, init) = varInfo uv
 
-lastConstAssign :: VarInfo -> Statement -> Maybe [Const]
-lastConstAssign info a = do
+lastConstAssign :: UV -> Statement -> Maybe [Const]
+lastConstAssign uv a = do
   (_, a) <- lastConstAssign a
   return $ nub a
   where
   lastConstAssign :: Statement -> Maybe (Bool, [Const])
   lastConstAssign a = case a of
-    AssignBool  v (Const a) | varInfo v == info -> Just (True, [const' a])
-    AssignInt   v (Const a) | varInfo v == info -> Just (True, [const' a])
-    AssignFloat v (Const a) | varInfo v == info -> Just (True, [const' a])
-    AssignBool  v _ | varInfo v == info -> Nothing
-    AssignInt   v _ | varInfo v == info -> Nothing
-    AssignFloat v _ | varInfo v == info -> Nothing
+    Assign v (Const a) | untype v == uv -> Just (True, [const' a])
+    Assign v _         | untype v == uv -> Nothing
     Branch _ a b -> do
       (aDone, a) <- lastConstAssign a
       (bDone, b) <- lastConstAssign b
@@ -58,4 +56,23 @@
           return (aDone, a ++ b)
     Label  _ a -> lastConstAssign a
     _ -> Just (False, [])
+
+timerRanges :: Statement -> [E Bool]
+timerRanges stmt = [] --XXX
+  where
+  intCode :: [(VarInfo, Statement)]
+  intCode = [ (varInfo a, assignedVar a stmt) | a@(UVInt _) <- stmtVars stmt ]
+
+-- | Reduces a program only to assignments of a certain variable.
+assignedVar :: UV -> Statement -> Statement
+assignedVar v a = case a of
+  Assign v' _ | v == untype v' -> a
+  Branch cond a b -> case (assignedVar v a, assignedVar v b) of
+    (Null, Null) -> Null
+    (a, b)       -> Branch cond a b
+  Sequence a b -> case (assignedVar v a, assignedVar v b) of
+    (Null, Null) -> Null
+    (a, b)       -> Sequence a b
+  Label a b -> Label a $ assignedVar v b
+  _ -> Null
 
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -7,20 +7,18 @@
 import System.IO
 import Text.Printf
 
-import Language.ImProve.Code
+import Language.ImProve.Code ()
 import Language.ImProve.Core
 import Language.ImProve.Narrow
 
 -- | Verify a program with k-induction.
 verify :: FilePath -> Int -> Statement -> IO ()
 verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"
-verify yices maxK program' = do
-  code "narrowing" narrowing
-  mapM_ (verifyProgram yices format maxK) $ trimAssertions program
+verify yices maxK program = do
+  putStrLn "state variable narrowing ..."
+  print $ narrow program
+  mapM_ (verifyProgram yices format maxK $ narrow program) $ trimAssertions $ labelAssertions program
   where
-  --XXX Not efficient.  Constraints will get added on every stage.  Only needed at the begining.
-  narrowing = narrow program'
-  program = labelAssertions $ Sequence narrowing program'
   format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    "
 
 -- | Set of statements containing only one assertion.
@@ -90,20 +88,18 @@
     _ -> []
 
 -- | Trim all unneeded stuff from a program.
-trimProgram :: Statement -> Statement
-trimProgram program = trim program
+trimProgram :: Statement -> Statement -> Statement
+trimProgram base program = trim program
   where
   vars = fixPoint []
-  fixPoint :: [VarInfo] -> [VarInfo]
+  fixPoint :: [UV] -> [UV]
   fixPoint a = if sort (nub a) == sort (nub b) then sort (nub a) else fixPoint b
     where
-    b = requiredVars program a
+    b = requiredVars base a
   trim :: Statement -> Statement
   trim a = case a of
     Null -> Null
-    AssignBool  b _ -> if elem (varInfo b) vars then a else Null
-    AssignInt   b _ -> if elem (varInfo b) vars then a else Null
-    AssignFloat b _ -> if elem (varInfo b) vars then a else Null
+    Assign b _ -> if elem (untype b) vars then a else Null
     Branch a b c    -> case (trim b, trim c) of
       (Null, Null) -> Null
       (b, c)       -> Branch a b c
@@ -117,11 +113,9 @@
       Null -> Null
       a    -> Label name a
 
-requiredVars :: Statement -> [VarInfo] -> [VarInfo]
+requiredVars :: Statement -> [UV] -> [UV]
 requiredVars a required = case a of
-  AssignBool  a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required
-  AssignInt   a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required
-  AssignFloat a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required
+  Assign a b -> if elem (untype a) required then nub $ untype a : exprVars b ++ required else required
   Branch a b c    -> if any (flip elem $ modifiedVars b ++ modifiedVars c) required || (not $ null $ requiredVars b []) || (not $ null $ requiredVars c [])
     then nub $ exprVars a ++ requiredVars b (requiredVars c required)
     else required
@@ -131,11 +125,9 @@
   Label  _ a      -> requiredVars a required
   Null            -> required
 
-modifiedVars :: Statement -> [VarInfo]
+modifiedVars :: Statement -> [UV]
 modifiedVars a = case a of
-  AssignBool  a _ -> [varInfo a]
-  AssignInt   a _ -> [varInfo a]
-  AssignFloat a _ -> [varInfo a]
+  Assign a _      -> [untype a]
   Branch _ b c    -> modifiedVars b ++ modifiedVars c
   Sequence a b    -> modifiedVars a ++ modifiedVars b
   Assert _        -> []
@@ -144,16 +136,15 @@
   Null            -> []
 
 -- | Verify a trimmed program.
-verifyProgram :: FilePath -> String -> Int -> Statement -> IO ()
-verifyProgram yices format maxK program' = do
+verifyProgram :: FilePath -> String -> Int -> Statement -> Statement -> IO ()
+verifyProgram yices format maxK narrowing program' = do
   printf format name
   hFlush stdout
-  env0 <- initEnv program
+  env0 <- initEnv program  --XXX Need to add narrowing assumptions.
   execStateT (check yices name maxK program env0 1) env0
   return ()
   where
-  program = trimProgram program'
-  --program = program'
+  program = Sequence (trimProgram program' narrowing) (trimProgram program' program')
   name = pathName $ head' "a1" $ assertions program
 
 head' msg a = if null a then error msg else head a
@@ -191,13 +182,13 @@
   env <- get
   r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env)
           ++ [ASSERT $ NOT $ AND $ asserts env]
-          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- stmtVars program, not input ]
+          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- map varInfo $ stmtVars program, not input ]
           ++ [CHECK]
   return $ result r
 
 -- | Insert new input variables.
 inputs :: Statement -> Y ()
-inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- stmtVars program, input ]
+inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, input ]
 
 result :: ResY -> Result
 result a = case a of
@@ -211,9 +202,7 @@
 evalStmt enabled a = case a of
   Null -> return ()
   Sequence a b -> evalStmt enabled a >> evalStmt enabled b
-  AssignBool  a b -> assign a b
-  AssignInt   a b -> assign a b
-  AssignFloat a b -> assign a b
+  Assign a b -> assign a b
   Assert a -> do
     a <- evalExpr a
     b <- newBoolVar
@@ -334,7 +323,7 @@
   }
  
 initEnv :: Statement -> IO Env
-initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- stmtVars program, not input ]) Env
+initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, not input ]) Env
   { nextId  = 0
   , var     = \ v -> error $ "variable not found in environment: " ++ pathName v
   , cmds    = []
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.1.5
+version: 0.1.6
 
 category: Language, Formal Methods, Embedded