diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -98,7 +98,7 @@
   = Bool  Bool
   | Int   Int
   | Float Float
-  deriving Eq
+  deriving (Eq, Ord)
 
 type VarInfo = (Bool, Path, Const)
 
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -99,13 +99,9 @@
                         ||. not_ grantA &&. not_ grantB &&. not_ grantC
   
   -- No grants without requests.
-  --label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA)
-  --label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB)
-  --label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC)
-  label "test" $ label "test2" $ do
-    assert $ imply (not_ requestA) (not_ grantA)
-    assert $ imply (not_ requestB) (not_ grantB)
-    assert $ imply (not_ requestC) (not_ grantC)
+  label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA)
+  label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB)
+  label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC)
 
   -- Grants to single requests.
   label "OnlyRequestA" $ assert $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -1,6 +1,7 @@
 module Language.ImProve.Verify (verify) where
 
 import Control.Monad.State
+import Data.List
 import Math.SMT.Yices.Pipe
 import Math.SMT.Yices.Syntax
 import System.IO
@@ -11,24 +12,25 @@
 -- | 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
+verify yices maxK program' = do
   mapM_ (verifyProgram yices format maxK) $ trimAssertions program
   where
+  program = labelAssertions program'
   format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    "
 
 
 -- | Set of statements containing only one assertion.
 trimAssertions :: Statement -> [Statement]
-trimAssertions program = [ a | a <- trimAssertions' program, length (assertions a) == 1 ]
-
-trimAssertions' :: Statement -> [Statement]
-trimAssertions' a = case a of
-  Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions' a ]
-               ++ [ Sequence (removeAssertions a) b | b <- trimAssertions' b ]
-  Branch cond a b -> [ Branch cond a (removeAssertions b) | a <- trimAssertions' a ]
-                  ++ [ Branch cond (removeAssertions a) b | b <- trimAssertions' b ]
-  Label name a -> [ Label name a | a <- trimAssertions' a ]
-  a -> [a]
+trimAssertions program = [ a | a <- trimAssertions program, length (assertions a) == 1 ]
+  where
+  trimAssertions :: Statement -> [Statement]
+  trimAssertions a = case a of
+    Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions a ]
+                 ++ [ Sequence (removeAssertions a) b | b <- trimAssertions b ]
+    Branch cond a b -> [ Branch cond a (removeAssertions b) | a <- trimAssertions a ]
+                    ++ [ Branch cond (removeAssertions a) b | b <- trimAssertions b ]
+    Label name a -> [ Label name a | a <- trimAssertions a ]
+    a -> [a]
 
 -- | Remove all assertions.
 removeAssertions :: Statement -> Statement
@@ -39,12 +41,11 @@
   Label name a -> Label name $ removeAssertions a
   a -> a
 
-{-
--- | Ensures all assertions are labed, though not uniquely.
+-- | Ensure all assertions are uniquely labed.
 labelAssertions :: Statement -> Statement
-labelAssertions program = evalState (f program) 1
+labelAssertions program = evalState (f program) ([], [], 1)
   where
-  f :: Statement -> State Int Statement
+  f :: Statement -> State (Path, [Path], Int) Statement
   f a = case a of
     Branch a b c -> do
       b <- f b
@@ -55,14 +56,22 @@
       b <- f b
       return $ Sequence a b
     Assert a -> do
-      n <- get
-      put $ n + 1
-      return $ Label (show n) $ Assert a
+      (path, paths, n) <- get
+      if elem path paths
+        then do
+          put (path, paths, n + 1)
+          f $ Label (show n) $ Assert a
+        else do
+          put (path, path : paths, n)
+          return $ Assert a
     Label name a -> do
+      (path, paths, n) <- get
+      put (path ++ [name], paths, n)
       a <- f a
+      (_, paths, n) <- get
+      put (path, paths, n)
       return $ Label name a
     a -> return a
--}
 
 -- | Paths of all assertions.
 assertions :: Statement -> [Path]
@@ -78,7 +87,49 @@
 
 -- | Trim all unneeded stuff from a program.
 trimProgram :: Statement -> Statement
-trimProgram = id --XXX
+trimProgram program = program
+  where
+  vars = fixPoint []
+  fixPoint :: [VarInfo] -> [VarInfo]
+  fixPoint a = if sort (nub a) == sort (nub b) then sort (nub a) else fixPoint b
+    where
+    b = requiredVars program 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
+    Branch a b c    -> case (trim b, trim c) of
+      (Null, Null) -> Null
+      (b, c)       -> Branch a b c
+    Sequence a b    -> case (trim a, trim b) of
+      (Null, a) -> a
+      (a, Null) -> a
+      (a, b)    -> Sequence a b
+    Assert a -> if any (flip elem vars) (exprVars a) then Assert a else Null
+    Assume a -> if any (flip elem vars) (exprVars a) then Assume a else Null
+    Label name a -> case trim a of
+      Null -> Null
+      a    -> Label name a
+
+requiredVars :: Statement -> [VarInfo] -> [VarInfo]
+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
+  Branch a b c    -> if (not $ null $ reqB \\ required) || (not $ null $ reqC \\ required)
+    then nub $ exprVars a ++ requiredVars b (requiredVars c required)
+    else required
+    where
+    reqB = requiredVars b required
+    reqC = requiredVars c required
+  Sequence a b    -> requiredVars a (requiredVars b required)
+  Assert a        -> nub $ exprVars a ++ required
+  Assume a        -> if any (flip elem required) (exprVars a) then nub $ exprVars a ++ required else required
+  Label  _ a      -> requiredVars a required
+  Null            -> required
+
 
 -- | Verify a trimmed program.
 verifyProgram :: FilePath -> String -> Int -> Statement -> IO ()
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.0.6
+version: 0.0.7
 
 category: Language