diff --git a/Language/ImProve/Narrow.hs b/Language/ImProve/Narrow.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Narrow.hs
@@ -0,0 +1,61 @@
+module Language.ImProve.Narrow (narrow) where
+
+import Data.List
+import Data.Maybe
+
+import Language.ImProve.Core
+
+narrow :: Statement -> Statement
+narrow stmt = assumes
+  where
+  assumes = foldl Sequence Null [ Label lab $ Assume assume | (lab, opt) <- optimizations, assume <- opt stmt ]
+  optimizations =
+    [ ("constantAssigns", constantAssigns)
+    ]
+
+constantAssigns :: Statement -> [E Bool]
+constantAssigns stmt = mapMaybe f1 $ stmtVars stmt
+  where
+  f1 :: VarInfo -> Maybe (E Bool)
+  f1 info@(input, path, init)
+    | input = Nothing
+    | otherwise = do
+      assigns <- lastConstAssign info 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
+
+lastConstAssign :: VarInfo -> Statement -> Maybe [Const]
+lastConstAssign info 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
+    Branch _ a b -> do
+      (aDone, a) <- lastConstAssign a
+      (bDone, b) <- lastConstAssign b
+      return (aDone && bDone, a ++ b)
+    Sequence a b -> do
+      (bDone, b) <- lastConstAssign b
+      if bDone
+        then return (True, b)
+	else do
+          (aDone, a) <- lastConstAssign a
+          return (aDone, a ++ b)
+    Label  _ a -> lastConstAssign a
+    _ -> Just (False, [])
+
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -7,17 +7,21 @@
 import System.IO
 import Text.Printf
 
+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
   where
-  program = labelAssertions program'
+  --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.
 trimAssertions :: Statement -> [Statement]
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.1.2
+version: 0.1.3
 
 category: Language, Formal Methods, Embedded
 
@@ -33,6 +33,7 @@
         Language.ImProve.Code
         Language.ImProve.Core
         Language.ImProve.Examples
+        Language.ImProve.Narrow
         Language.ImProve.Tree
         Language.ImProve.Verify