diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -49,7 +49,7 @@
   , Stmt
   -- ** Hierarchical Scope and Annotations
   , scope
-  , annotate
+  , label
   -- ** Variable Declarations
   , bool
   , bool'
@@ -214,7 +214,7 @@
 mux :: AllE a => E Bool -> E a -> E a -> E a
 mux = Mux
 
--- | Creates a hierarchical scope.
+-- | Creates a hierarchical scope for variable names.
 scope :: Name -> Stmt a -> Stmt a
 scope name stmt = do
   (path0, stmt0) <- get
@@ -224,15 +224,15 @@
   put (path0, stmt1)
   return a
 
--- | Add an annotation to a statement.  Useful for requirement trace tags.
-annotate :: Name -> Stmt a -> Stmt a
-annotate name stmt = do
+-- | Labels a statement.  Useful for requirement trace tags or other annotations.
+label :: Name -> Stmt a -> Stmt a
+label name stmt = do
   (path0, stmt0) <- get
   put (path0, Null)
   a <- stmt
   (_, stmt1) <- get
   put (path0, stmt0)
-  statement $ Annotate name stmt1
+  statement $ Label name stmt1
   return a
   
 get :: Stmt ([Name], Statement)
@@ -322,28 +322,24 @@
 instance Assign Float where a <== b = statement $ AssignFloat a b
 
 -- | Assert that a condition is true.
-assert :: Name -> E Bool -> Stmt ()
-assert a b = do
-  path <- getPath
-  statement $ Assert (path ++ [a]) b
+assert :: E Bool -> Stmt ()
+assert = statement . Assert
 
 -- | Declare an assumption condition is true.
-assume :: Name -> E Bool -> Stmt ()
-assume a b = do
-  path <- getPath
-  statement $ Assume (path ++ [a]) b
+assume :: E Bool -> Stmt ()
+assume = statement . Assume
 
 -- | Conditional if-else.
-ifelse :: Name -> E Bool -> Stmt () -> Stmt () -> Stmt ()
-ifelse name cond onTrue onFalse = do
+ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()
+ifelse cond onTrue onFalse = do
   path <- getPath
   let (_, stmt1) = evalStmt path onTrue
       (_, stmt2) = evalStmt path onFalse
-  statement $ Branch (path ++ [name]) cond stmt1 stmt2
+  statement $ Branch cond stmt1 stmt2
 
 -- | Conditional if without the else.
-if_ :: Name -> E Bool -> Stmt () -> Stmt()
-if_ name cond stmt = ifelse name cond stmt $ return ()
+if_ :: E Bool -> Stmt () -> Stmt()
+if_ cond stmt = ifelse cond stmt $ return ()
 
 -- | Verify a program.
 --
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -29,12 +29,12 @@
   AssignBool  a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"
   AssignInt   a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"
   AssignFloat a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"
-  Branch path a b Null -> "// if_ "    ++ pathName path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"
-  Branch path a b c    -> "// ifelse " ++ pathName path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"
+  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"
+  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"
   Sequence a b -> codeStmt a ++ codeStmt b
-  Assert path a -> "// assert " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"
-  Assume path a -> "// assume " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"
-  Annotate name a -> "// annotate " ++ name ++ "\n" ++ indent (codeStmt a)
+  Assert a -> "assert(" ++ codeExpr a ++ ");\n"
+  Assume a -> "assert(" ++ codeExpr a ++ ");\n"
+  Label  name a -> "// " ++ name ++ "\n" ++ indent (codeStmt a)
   Null -> ""
 
 codeExpr :: E a -> String
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -27,12 +27,6 @@
 instance PathName Path      where pathName = intercalate "."
 instance PathName (V a)     where pathName (V _ path _) = pathName path
 instance PathName VarInfo   where pathName (_, path, _) = pathName path
-instance PathName Statement where
-  pathName a = case a of
-    Branch p _ _ _ -> pathName p
-    Assert p _     -> pathName p
-    Assume p _     -> pathName p
-    _ -> undefined
 
 class AllE a where
   zero   :: (Name -> a -> m (V a)) -> a
@@ -93,11 +87,11 @@
   = AssignBool  (V Bool ) (E Bool )
   | AssignInt   (V Int  ) (E Int  )
   | AssignFloat (V Float) (E Float)
-  | Branch      Path (E Bool) Statement Statement
+  | Branch      (E Bool) Statement Statement
   | Sequence    Statement Statement
-  | Assert      Path (E Bool)
-  | Assume      Path (E Bool)
-  | Annotate    Name Statement
+  | Assert      (E Bool)
+  | Assume      (E Bool)
+  | Label       Name Statement
   | Null
 
 data Const
@@ -117,11 +111,11 @@
   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
+  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
-  Annotate _ a    -> stmtVars a
+  Assert a        -> exprVars a
+  Assume a        -> exprVars a
+  Label  _ a      -> stmtVars a
   Null            -> []
 
 -- Information about all of an expressions's variables.
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -25,18 +25,18 @@
   b1 <- int "b1" 0  -- Working copy of 'b'.
 
   -- A new input to process.
-  if_ "startNew" (a /=. ref a0 ||. b /=. ref b0) $ do
+  label "startNew" $ if_ (a /=. ref a0 ||. b /=. ref b0) $ do
     a0 <== a
     b0 <== b
     a1 <== a
     b1 <== b
 
   -- Reduce a1.
-  if_ "reduceA" (ref a1 >. ref b1) $ do
+  label "reduceA" $ if_ (ref a1 >. ref b1) $ do
     a1 <== ref a1 - ref b1
 
   -- Reduce b1.
-  if_ "reduceB" (ref b1 >. ref a1) $ do
+  label "reduceB" $ if_ (ref b1 >. ref a1) $ do
     b1 <== ref b1 - ref a1
 
   -- Done if a1 == b1.
@@ -72,11 +72,11 @@
   counter <- int "counter" 0
 
   -- Specification.
-  assert "GreaterThanOrEqualTo0" $ ref counter >=. 0
-  assert "LessThan10"            $ ref counter <.  10
+  label "GreaterThanOrEqualTo0" $ assert $ ref counter >=. 0
+  label "LessThan10"            $ assert $ ref counter <.  10
 
   -- Implementation.
-  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)
+  ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)
 
   -- Alternatives to try.
   --ifelse "ResetCounter" (ref counter >=. 9) (counter <== 0) (counter <== ref counter + 1)
@@ -93,25 +93,29 @@
 arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
 
   -- Mutual exclusion.  At most, only one requester granted at a time.
-  assert "OneHot" $      grantA &&. not_ grantB &&. not_ grantC
-                ||. not_ grantA &&.      grantB &&. not_ grantC
-                ||. not_ grantA &&. not_ grantB &&.      grantC
-                ||. not_ grantA &&. not_ grantB &&. not_ grantC
+  label "OneHot" $ assert $      grantA &&. not_ grantB &&. not_ grantC
+                        ||. not_ grantA &&.      grantB &&. not_ grantC
+                        ||. not_ grantA &&. not_ grantB &&.      grantC
+                        ||. not_ grantA &&. not_ grantB &&. not_ grantC
   
   -- No grants without requests.
-  assert "NotRequestedA" $ imply (not_ requestA) (not_ grantA)
-  assert "NotRequestedB" $ imply (not_ requestB) (not_ grantB)
-  assert "NotRequestedC" $ 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)
+  label "test" $ label "test2" $ do
+    assert $ imply (not_ requestA) (not_ grantA)
+    assert $ imply (not_ requestB) (not_ grantB)
+    assert $ imply (not_ requestC) (not_ grantC)
 
   -- Grants to single requests.
-  assert "OnlyRequestA" $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA
-  assert "OnlyRequestB" $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB
-  assert "OnlyRequestC" $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC
+  label "OnlyRequestA" $ assert $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA
+  label "OnlyRequestB" $ assert $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB
+  label "OnlyRequestC" $ assert $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC
 
   -- Priority.
-  assert "Highest" $ imply requestA grantA
-  assert "Medium"  $ imply (not_ requestA &&. requestB) grantB
-  assert "Lowest"  $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC
+  label "Highest" $ assert $ imply requestA grantA
+  label "Medium"  $ assert $ imply (not_ requestA &&. requestB) grantB
+  label "Lowest"  $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC
 
 -- | An arbiter implementation.
 arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
@@ -128,9 +132,9 @@
   grantB <- bool "grantB" False
   grantC <- bool "grantC" False
 
-  if_ "GrantA" (requestA)                                     (grantA <== true)
-  if_ "GrantB" (not_ requestA &&. requestB)                   (grantB <== true)
-  if_ "GrantC" (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
+  label "GrantA" $ if_ (requestA)                                     (grantA <== true)
+  label "GrantB" $ if_ (not_ requestA &&. requestB)                   (grantB <== true)
+  label "GrantC" $ if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
 
   return (ref grantA, ref grantB, ref grantC)
 
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,6 @@
 module Language.ImProve.Verify (verify) where
 
-import Control.Monad.State hiding (State)
+import Control.Monad.State
 import Math.SMT.Yices.Pipe
 import Math.SMT.Yices.Syntax
 import System.IO
@@ -16,6 +16,7 @@
   where
   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 ]
@@ -24,28 +25,56 @@
 trimAssertions' a = case a of
   Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions' a ]
                ++ [ Sequence (removeAssertions a) b | b <- trimAssertions' b ]
-  Branch path cond a b -> [ Branch path cond a (removeAssertions b) | a <- trimAssertions' a ]
-                       ++ [ Branch path cond (removeAssertions a) b | b <- trimAssertions' b ]
-  Annotate name a -> [ Annotate name a | a <- trimAssertions a ]
+  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
 removeAssertions a = case a of
-  Assert _ _ -> Null
+  Assert _ -> Null
   Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)
-  Branch path cond a b -> Branch path cond (removeAssertions a) (removeAssertions b)
-  Annotate name a -> Annotate name $ removeAssertions a
+  Branch cond a b -> Branch cond (removeAssertions a) (removeAssertions b)
+  Label name a -> Label name $ removeAssertions a
   a -> a
 
+{-
+-- | Ensures all assertions are labed, though not uniquely.
+labelAssertions :: Statement -> Statement
+labelAssertions program = evalState (f program) 1
+  where
+  f :: Statement -> State Int Statement
+  f a = case a of
+    Branch a b c -> do
+      b <- f b
+      c <- f c
+      return $ Branch a b c
+    Sequence a b -> do
+      a <- f a
+      b <- f b
+      return $ Sequence a b
+    Assert a -> do
+      n <- get
+      put $ n + 1
+      return $ Label (show n) $ Assert a
+    Label name a -> do
+      a <- f a
+      return $ Label name a
+    a -> return a
+-}
+
 -- | Paths of all assertions.
 assertions :: Statement -> [Path]
-assertions a = case a of
-  Assert path _  -> [path]
-  Sequence a b   -> assertions a ++ assertions b
-  Branch _ _ a b -> assertions a ++ assertions b
-  Annotate _ a   -> assertions a
-  _ -> []
+assertions = assertions []
+  where
+  assertions :: Path -> Statement -> [Path]
+  assertions path a = case a of
+    Assert _ -> [path]
+    Sequence a b -> assertions path a ++ assertions path b
+    Branch _ a b -> assertions path a ++ assertions path b
+    Label name a -> assertions (path ++ [name]) a
+    _ -> []
 
 -- | Trim all unneeded stuff from a program.
 trimProgram :: Statement -> Statement
@@ -75,13 +104,13 @@
   evalStmt (LitB True) program
   resultBasis <- checkBasis yices program env0
   case resultBasis of
-    Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace name a
+    Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see %s.trace)\n" k name) >> writeTrace name a
     Problem -> error "Verify.check1"
     Pass -> do
       resultStep <- checkStep yices
       case resultStep of
         Fail a | k < maxK  -> check yices name maxK program env0 (k + 1)
-               | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace name a
+               | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see %s.trace)\n" k name) >> writeTrace name a
         Problem -> error "Verify.check2"
         Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k
         
@@ -121,17 +150,17 @@
   AssignBool  a b -> assign a b
   AssignInt   a b -> assign a b
   AssignFloat a b -> assign a b
-  Assert path a -> do
+  Assert a -> do
     a <- evalExpr a
     b <- newBoolVar
     addCmd $ ASSERT (VarE b := (enabled :=> a))
     env <- get
     put env { asserts = VarE b : asserts env }
-    addTrace $ Assert' (pathName path) b
-  Assume _ a -> do
+    addTrace $ Assert' b
+  Assume a -> do
     a <- evalExpr a
     addCmd $ ASSERT (enabled :=> a)
-  Branch path a onTrue onFalse -> do
+  Branch a onTrue onFalse -> do
     a <- evalExpr a
     b <- newBoolVar
     addCmd $ ASSERT (VarE b := a)
@@ -142,13 +171,13 @@
     put env1 { trace = [] }
     evalStmt (AND [enabled, NOT a]) onFalse
     env2 <- get
-    put env2 { trace = Branch' (pathName path) b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }
-  Annotate name a -> do
+    put env2 { trace = Branch' b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }
+  Label name a -> do
     env0 <- get
     put env0 { trace = [] }
     evalStmt enabled a
     env1 <- get
-    put env1 { trace = Annotate' name (reverse $ trace env1) : trace env0 }
+    put env1 { trace = Label' name (reverse $ trace env1) : trace env0 }
   where
   assign :: AllE a => V a -> E a -> Y ()
   assign a b = do
@@ -250,13 +279,13 @@
   }
 
 data Trace
-  = Init'     Name Var
-  | Cycle'    Int
-  | Input'    Name Var
-  | Assign'   Name Var
-  | Assert'   Name Var
-  | Branch'   Name Var [Trace] [Trace] 
-  | Annotate' Name [Trace]
+  = Init'   Name Var
+  | Cycle'  Int
+  | Input'  Name Var
+  | Assign' Name Var
+  | Assert' Var
+  | Branch' Var [Trace] [Trace] 
+  | Label'  Name [Trace]
 
 addVar' :: VarInfo -> Y String
 addVar' v = do
@@ -316,15 +345,15 @@
     Assign' path var -> case lookup var table of
       Nothing -> ""
       Just value -> path ++ " <== " ++ value ++ "\n"
-    Assert' path var -> case lookup var table of
-      Just "true"  -> "assertion passed: " ++ path ++ "\n"
-      Just "false" -> "assertion FAILED: " ++ path ++ "\n"
+    Assert' var -> case lookup var table of
+      Just "true"  -> "assertion passed\n"
+      Just "false" -> "assertion FAILED\n"
       _ -> ""
-    Branch' path cond onTrue onFalse -> case lookup cond table of
-      Just "true"  -> "ifelse " ++ path ++ " true\n"  ++ indent (concatMap f onTrue)
-      Just "false" -> "ifelse " ++ path ++ " false\n" ++ indent (concatMap f onFalse)
+    Branch' cond onTrue onFalse -> case lookup cond table of
+      Just "true"  -> "ifelse true:\n"  ++ indent (concatMap f onTrue)
+      Just "false" -> "ifelse false:\n" ++ indent (concatMap f onFalse)
       _ -> ""
-    Annotate' name traces -> "annotate " ++ name ++ "\n" ++ indent (concatMap f traces)
+    Label' name traces -> name ++ ":\n" ++ indent (concatMap f traces)
 
 indent :: String -> String
 indent = unlines . map ("    " ++) . lines
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.0.5
+version: 0.0.6
 
 category: Language