diff --git a/RELEASE-NOTES b/RELEASE-NOTES
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,20 +1,25 @@
-afv 0.0.0    01/12/10
+afv 0.0.4    01/21/10
 
-- Initial release.
+- Moved branches into model.
+- Improved counter example generation.
 
-afv 0.0.1    01/14/10
+afv 0.0.3    01/19/10
 
-- Checks for duplicate top-level names.
-- Uses yices new 'quickCheckY'.
-- Fixed bug affecting 'assume'.
+- Bug fix to --yices command option.
+- Added basic counter example generation.
 
 afv 0.0.2    01/17/10
 
 - Support for function arguments.  Still no support for return values.
 - Stronger type checking.
 
-afv 0.0.3    01/19/10
+afv 0.0.1    01/14/10
 
-- Bug fix to --yices command option.
-- Added basic counter example generation.
+- Checks for duplicate top-level names.
+- Uses yices new 'quickCheckY'.
+- Fixed bug affecting 'assume'.
+
+afv 0.0.0    01/12/10
+
+- Initial release.
 
diff --git a/afv.cabal b/afv.cabal
--- a/afv.cabal
+++ b/afv.cabal
@@ -1,5 +1,5 @@
 name:    afv
-version: 0.0.3
+version: 0.0.4
 
 category: Formal Methods
 
diff --git a/src/AFV.hs b/src/AFV.hs
--- a/src/AFV.hs
+++ b/src/AFV.hs
@@ -8,7 +8,7 @@
 import Parse
 import Verify
 
-version = "0.0.3"
+version = "0.0.4"
 
 main :: IO ()
 main = do
diff --git a/src/Compile.hs b/src/Compile.hs
--- a/src/Compile.hs
+++ b/src/Compile.hs
@@ -24,7 +24,7 @@
 rewrite name units = if not $ null asms
   then notSupported (head asms) "inline assembly"
   else if not $ null duplicateNames
-    then error $ "duplicate top-level names found (hiding names with static is not supported): " ++ show duplicateNames
+    then error $ "duplicate top-level names found (hiding names with static is not supported): " ++ show duplicateNames  --XXX Should not allow top level static decls.  An improper name reference in one file could reference a static variable in another.
     else CCompound [] (vars ++ funcs ++ [CBlockStmt call]) none
   where
   items = [ a | CTranslUnit items _ <- units, a <- items ]
@@ -47,7 +47,6 @@
 data MDB = MDB
   { nextId' :: Int
   , stack   :: [Ident]
-  , enabled :: E
   , model   :: Model
   }
 
@@ -55,7 +54,6 @@
 initMDB = MDB
   { nextId' = 0
   , stack   = []
-  , enabled = true
   , model   = Model { variables = [], actions = [] }
   }
 
@@ -90,17 +88,17 @@
   m = [ a | EnvFunction n a <- values env, n == name ]
 
 -- | Creates a branch.
-branch :: Position -> E -> M a -> M a -> M (a, a)
+branch :: Position -> V -> M a -> M a -> M (a, a)
 branch n a onTrue onFalse = do
-  a <- latchBranch n a
   m1 <- get
-  put m1 { enabled = And (enabled m1) a n }
+  put m1 { model = (model m1) { actions = [] } }
   r1 <- onTrue
   m2 <- get
-  put m2 { enabled = And (enabled m1) (Not a n) n }
+  put m1 { model = (model m2) { actions = [] } }
   r2 <- onFalse
   m3 <- get
-  put m3 { enabled = enabled m1 }
+  put m3 { model = (model m3) { actions = actions $ model m1 } }
+  newAction $ Branch a (reverse $ actions $ model m2) (reverse $ actions $ model m3) n
   return (r1, r2)
 
 -- | Push an identifier onto the call stack, do something, then pop it off.
@@ -113,11 +111,11 @@
   put m { stack = tail $ stack m }
   return a
 
-callPath :: M ([String], Position)
+callPath :: M String
 callPath = do
   m <- get
   let s = stack m
-  return ([ n | Ident n _ _ <- reverse s ], posOf $ head s)
+  return $ intercalate "." [ n | Ident n _ _ <- reverse $ tail s ]
 
 -- | The initial environment defines the assert and assume functions.
 initEnv :: Env
@@ -128,18 +126,18 @@
     ]
   }
   where
-  assert a = do
-    (s, n) <- callPath
-    m <- get
-    let x = imply (enabled m) (head a) n
-    newAction $ Assert x s
-    return x
-  assume a = do
-    (s, n) <- callPath
-    m <- get
-    let x = imply (enabled m) (head a) n
-    newAction $ Assume x s
-    return x
+  assert a' = do
+    let a = head a'
+    s <- callPath
+    x <- latch (posOf a) a
+    newAction $ Assert x s (posOf a)
+    return $ Var x
+  assume a' = do
+    let a = head a'
+    s <- callPath
+    x <- latch (posOf a) a
+    newAction $ Assume x s (posOf a)
+    return $ Var x
 
 -- | Adds new action.
 newAction :: Action -> M ()
@@ -177,7 +175,7 @@
     f (a:b) = callStack a $ f b
   CIf a b Nothing n -> evalStat env $ CIf a b (Just $ CCompound [] [] n) n
   CIf a b (Just c) n -> do
-    a <- evalExpr env a
+    a <- evalExpr env a >>= latch (posOf n)
     branch (posOf n) a (evalStat env b) (evalStat env c)
     return ()
   _ -> notSupported a "statement"
@@ -189,13 +187,13 @@
   CNestedFunDef a -> evalFunc env a
 
 evalExpr :: Env -> CExpr -> M E
-evalExpr env a = latch (posOf a) =<< case a of
+evalExpr env a = case a of
   CAssign op a b n -> case op of
     CAssignOp -> do
       a' <- evalExpr env a
       b' <- evalExpr env b
       case a' of
-        Var v -> assign False (posOf n) v b' >> return a'
+        Var v -> assign (posOf n) v b' >> return a'
         _ -> unexpected a "non variable in left hand of assignment"
     CMulAssOp -> f CMulOp
     CDivAssOp -> f CDivOp
@@ -211,12 +209,12 @@
     f :: CBinaryOp -> M E
     f op = evalExpr env (CAssign CAssignOp a (CBinary op a b n) n)
   CCond a (Just b) c n -> do
-    a <- evalExpr env a
+    a <- evalExpr env a >>= latch (posOf a)
     (b, c) <- branch (posOf n) a (evalExpr env b) (evalExpr env c)
-    return $ Mux a b c $ posOf n
+    return $ Mux (Var a) b c $ posOf n
   CCond a Nothing b n -> do
-    a <- evalExpr env a
-    (a, b) <- branch (posOf n) a (return a) (evalExpr env b)
+    a <- evalExpr env a >>= latch (posOf a)
+    (a, b) <- branch (posOf n) a (return $ Var a) (evalExpr env b)
     return $ Mux a a b $ posOf n
   CBinary op a b n -> case op of
     CMulOp -> f Mul
@@ -236,12 +234,12 @@
     CXorOp -> notSupported a "(^)"
     COrOp  -> notSupported a "(|)"
     CLndOp -> do
-      a <- evalExpr env a
-      (b, a) <- branch n' a (evalExpr env b) (return a)
+      a <- evalExpr env a >>= latch (posOf a)
+      (b, a) <- branch n' a (evalExpr env b) (return $ Var a)
       return $ Mux a b a n'
     CLorOp -> do
-      a <- evalExpr env a
-      (a, b) <- branch n' a (return a) (evalExpr env b)
+      a <- evalExpr env a >>= latch (posOf a)
+      (a, b) <- branch n' a (return $ Var a) (evalExpr env b)
       return $ Mux a a b n'
     where
     n' = posOf n
@@ -255,19 +253,19 @@
     a <- evalExpr env a
     case (op, a) of
       (CPreIncOp, Var a) -> do
-        assign False p a $ Add (Var a) one p
+        assign p a $ Add (Var a) one p
         return $ Var a
       (CPreDecOp, Var a) -> do
-        assign False p a $ Sub (Var a) one p
+        assign p a $ Sub (Var a) one p
         return $ Var a
       (CPostIncOp, Var a) -> do
         b <- latch p $ Var a
-        assign False p a $ Add (Var a) one p
-        return b
+        assign p a $ Add (Var a) one p
+        return $ Var b
       (CPostDecOp, Var a) -> do
         b <- latch p $ Var a
-        assign False p a $ Sub (Var a) one p
-        return b
+        assign p a $ Sub (Var a) one p
+        return $ Var b
       (CPlusOp, a) -> return a
       (CMinOp,  a) -> return $ Sub zero a p
       (CNegOp,  a) -> return $ Not a p
@@ -333,7 +331,7 @@
           else do
             i <- nextId
             return $ Local name typ i (posOf e')
-        assign True (posOf e') v e
+        declare (posOf e') v e
         addVar env v
       _ -> notSupported i "variable declaration"
     _ -> notSupported d "arrays, pointers, or functional pointers (So what good is this tool anyway?)"
@@ -358,7 +356,7 @@
   else do
     i <- nextId
     let v = Local name typ i (posOf n)
-    assign True (posOf n) v a
+    declare (posOf n) v a
     addVar env v
 
 funcArgs :: CDecl -> [(Ident, (TypeInfo, Type))]
@@ -371,39 +369,30 @@
 
 
 
+-- | Declares a new variable with a value.
+declare :: Position -> V -> E -> M ()
+declare n v a = case v of
+  Volatile _ _ _ -> return ()
+  _ -> newAction $ Declare v a n
 
--- | Assgins a value to a variable.
-assign :: Bool -> Position -> V -> E -> M ()
-assign decl n v a = case v of
+-- | Assigns a value to an existing variable.
+assign :: Position -> V -> E -> M ()
+assign n v a = case v of
   Volatile _ _ _ -> return ()
-  _ -> do
-    m <- get
-    newAction $ Assign v $ if decl then a else Mux (enabled m) a (Var v) n  --XXX Is this correct for local and tmp variables?
+  _ -> newAction $ Assign v a n
 
--- | Latch a value at a point in time and return the expression of the latch variable.
-latch :: Position -> E -> M E
-latch _ (Var a)   = return (Var a)
-latch _ (Const a) = return (Const a)
+-- | Latch a value at a point in time.
+latch :: Position -> E -> M V  -- XXX When is it appropriate to latch and when not?
+--latch _ (Var a) = return a
 latch n a = do
   i <- nextId
   let v = Tmp (typeOf a) i n
-  assign True n v a
-  return $ Var v
-
--- | Latch a value for a branch point.
-latchBranch :: Position -> E -> M E
-latchBranch n a = do
-  i <- nextId
-  let v = Branch (typeOf a) i n
-  assign True n v a
-  return $ Var v
-
--- | Logical implication.  Assumes Bool inputs.
-imply :: E -> E -> Position -> E
-imply a b n = Or (Not a n) b n
-
-
-
+  case typeOf a of
+    Integer  Nothing -> error "Compile.latch1"
+    Rational Nothing -> error "Compile.latch2"
+    _ -> do
+      declare n v a
+      return v
 
 
 
diff --git a/src/Model.hs b/src/Model.hs
--- a/src/Model.hs
+++ b/src/Model.hs
@@ -94,7 +94,6 @@
   | Volatile String Type     Position
   | Local    String Type Int Position
   | Tmp             Type Int Position
-  | Branch          Type Int Position
   deriving (Show, Eq)
      
 instance TypeOf V where
@@ -103,7 +102,6 @@
     Volatile _ a _   -> a
     Local    _ a _ _ -> a
     Tmp      a _ _   -> a
-    Branch a _ _ -> a
 
 instance Pos V where
   posOf a = case a of
@@ -111,7 +109,6 @@
     Volatile _ _ n -> n
     Local _ _ _ n -> n
     Tmp _ _ n -> n
-    Branch _ _ n -> n
 
 -- | Expressions.
 data E
@@ -156,7 +153,7 @@
     Const a     -> typeOf a
     Not a _     -> unify' Bool (typeOf a)
     And a b _   -> unify' Bool $ unify' (typeOf a) (typeOf b)
-    Or  a b _   -> unify' (typeOf a) (typeOf b)
+    Or  a b _   -> unify' Bool $ unify' (typeOf a) (typeOf b)
     Mul a b _   -> unify' (typeOf a) (typeOf b)
     Div a b _   -> unify' (typeOf a) (typeOf b)
     Mod a b _   -> unify' (typeOf a) (typeOf b)
@@ -195,9 +192,11 @@
 
 typeCheckAction :: Action -> Action
 typeCheckAction a = case a of
-  Assign v a -> seq (unify a (typeOf v) (typeOf a)) $ Assign v a
-  Assert a n -> seq (unify a Bool (typeOf a))       $ Assert a n
-  Assume a n -> seq (unify a Bool (typeOf a))       $ Assume a n
+  Declare v a p  -> seq (unify a (typeOf v) (typeOf a)) $ Declare v a p
+  Assign v a p   -> seq (unify a (typeOf v) (typeOf a)) $ Assign  v a p
+  Assert a n p   -> seq (unify a Bool (typeOf a))       $ Assert a n p
+  Assume a n p   -> seq (unify a Bool (typeOf a))       $ Assume a n p
+  Branch a b c p -> seq (unify a Bool (typeOf a))       $ Branch a (map typeCheckAction b) (map typeCheckAction c) p
 
 true :: E
 true = Const $ CBool True nopos
@@ -208,10 +207,20 @@
 instance Pos Position where posOf = id
 
 data Action
-  = Assign V E
-  | Assert E [String]
-  | Assume E [String]
+  = Declare V E Position
+  | Assign  V E Position
+  | Assert  V String Position
+  | Assume  V String Position
+  | Branch  V [Action] [Action] Position
   deriving (Show, Eq)
+
+instance Pos Action where
+  posOf a = case a of
+    Declare _ _ a -> a
+    Assign  _ _ a -> a
+    Assert  _ _ a -> a
+    Assume  _ _ a -> a
+    Branch  _ _ _ a -> a
 
 data Model = Model
   { variables :: [VS]
diff --git a/src/Verify.hs b/src/Verify.hs
--- a/src/Verify.hs
+++ b/src/Verify.hs
@@ -1,7 +1,7 @@
 module Verify (verify) where
 
 import Control.Monad.State hiding (State)
-import Data.List
+import Language.C.Data.Position
 import Math.SMT.Yices.Pipe
 import Math.SMT.Yices.Syntax
 import System.IO
@@ -17,43 +17,53 @@
   mapM_ (verifyModel yices format maxK) models
   where
   model = typeCheckModel m
-  assertions = [ a | a@(Assert _ _) <- actions model ]
-  models = map (trimModel . trimAssertions model) assertions
-  format = "verifying %-" ++ show (maximum [ length (intercalate "." n) | (Assert _ n) <- actions model ]) ++ "s    "
+  models = [ (name, trimModel model { actions = actions }) | (name, actions) <- trimAssertions (actions model) ]
+  format = "verifying %-" ++ show (maximum [ length n | (n, _) <- models ]) ++ "s    "
 
 -- | Remove all assertions except one.
-trimAssertions :: Model -> Action -> Model
-trimAssertions m a = m { actions = filter keep $ actions m }
-  where
-  keep b@(Assert _ _) = a == b
-  keep _ = True
+trimAssertions :: [Action] -> [(String, [Action])]
+trimAssertions [] = []
+trimAssertions (a:b) = case a of
+  Assert _ n _ -> (n, a : removeAssertions b) : trimAssertions b
+  Branch c t f p -> [ (name, Branch c actions (removeAssertions f) p : removeAssertions b)   | (name, actions) <- trimAssertions t ]
+                 ++ [ (name, Branch c (removeAssertions t) actions p : removeAssertions b)   | (name, actions) <- trimAssertions f ]
+                 ++ [ (name, Branch c (removeAssertions t) (removeAssertions f) p : actions) | (name, actions) <- trimAssertions b ]
+  _ -> [ (name, a : actions) | (name, actions) <- trimAssertions b ]
 
+-- | Remove all assertions.
+removeAssertions :: [Action] -> [Action]
+removeAssertions [] = []
+removeAssertions (a:b) = case a of
+  Assert _ _ _ -> removeAssertions b
+  Branch c t f p -> Branch c (removeAssertions t) (removeAssertions f) p : removeAssertions b
+  _ -> a : removeAssertions b
+
 -- | Trim all unneeded stuff from a model.
 trimModel :: Model -> Model
 trimModel = id  --XXX
 
 -- | Verify a trimmed model.
-verifyModel :: FilePath -> String -> Int -> Model -> IO ()
-verifyModel y format maxK m = do
-  printf format name >> hFlush stdout
+verifyModel :: FilePath -> String -> Int -> (String, Model) -> IO ()
+verifyModel y format maxK (name, m) = do
+  printf format name
+  hFlush stdout
   env0 <- initEnv y m
   execStateT (check env0 1) env0
   return ()
   where
-  name = intercalate "." $ head [ path | Assert _ path <- actions m ]
   check :: Env -> Int -> Y ()
   check env0 k = do
     transition m
     resultBasis <- checkBasis m env0
     case resultBasis of
-      Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> trace name a
-      Problem -> return ()
+      Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace name a
+      Problem -> error "Verify.check1"
       Pass -> do
         resultStep <- checkStep
         case resultStep of
           Fail a | k < maxK  -> check env0 (k + 1)
-                 | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> trace name a
-          Problem -> return ()
+                 | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace name a
+          Problem -> error "Verify.check2"
           Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k
         
 data Result = Pass | Fail [ExpY] | Problem
@@ -61,15 +71,17 @@
 -- | Check induction step.
 checkStep :: Y Result
 checkStep = do
-  Env y _ _ cmds asserts <- get
-  r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ head asserts] ++ cmds
+  env <- get
+  let cmds' = reverse $ [CHECK] ++ [ASSERT $ NOT $ head $ asserts env] ++ cmds env
+  r <- liftIO $ quickCheckY' (yices env) [] $ cmds'
   return $ result r
 
 -- | Check induction basis.
 checkBasis :: Model -> Env -> Y Result
 checkBasis m env0 = do
-  Env y _ _ cmds asserts <- get
-  r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ AND asserts] ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ] ++ cmds
+  env <- get
+  let cmds' = reverse $ [CHECK] ++ [ASSERT $ NOT $ AND $ asserts env] ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ] ++ cmds env
+  r <- liftIO $ quickCheckY' (yices env) [] cmds'
   return $ result r
 
 result :: ResY -> Result
@@ -82,24 +94,52 @@
 
 -- | Transition relation.  Returns assertion.
 transition :: Model -> Y ()
-transition m = mapM_ action $ actions m
+transition m = mapM_ (action $ LitB True) $ actions m
 
-action :: Action -> Y ()
-action a = case a of
-  Assign v e -> do
+assign :: Position -> V -> String -> Y ()
+assign p v n = do
+  env <- get
+  case v of
+    State (VS name _ _ _) -> put env { trace = Assign' p name n : trace env }
+    Local name _ _ _      -> put env { trace = Assign' p name n : trace env }
+    _ -> return ()
+    
+action :: ExpY -> Action -> Y ()
+action enabled a = case a of
+  Declare v e p -> do
     e <- expr (typeOf v) e
-    v <- addVar v
-    Env y i table cmds asserts <- get
-    put $ Env y i table (ASSERT (VarE v := e) : cmds) asserts
-  Assert a _ -> do
-    a <- expr Bool a
-    Env y i table cmds asserts <- get
-    put $ Env y i table cmds (a : asserts)
-  Assume a _ -> do
-    a <- expr Bool a
-    Env y i table cmds asserts <- get
-    put $ Env y i table (ASSERT a : cmds) asserts
+    v' <- addVar v
+    env <- get
+    put env { cmds = ASSERT (VarE v' := e) : cmds env }
+    assign p v v'
+  Assign v e p -> do
+    e <- expr (typeOf v) e
+    vLast <- getVar v
+    v' <- addVar v
+    env <- get
+    put env { cmds = ASSERT (VarE v' := IF enabled e (VarE vLast)) : cmds env }
+    assign p v v'
+  Assert a n p -> do
+    a <- getVar a
+    env <- get
+    put env { asserts = (enabled :=> VarE a) : asserts env, trace = Assert' p n a : trace env }
+  Assume a _ _ -> do
+    a <- getVar a
+    env <- get
+    put env { cmds = ASSERT (enabled :=> VarE a) : cmds env }
+  Branch a onTrue onFalse p -> do
+    a' <- getVar a
+    env0 <- get
+    put env0 { trace = [] }
+    mapM_ (action $ AND [enabled,       VarE a']) onTrue
+    env1 <- get
+    put env1 { trace = [] }
+    mapM_ (action $ AND [enabled, NOT $ VarE a']) onFalse
+    env2 <- get
+    put env2 { trace = Branch' p a' (reverse $ trace env1) (reverse $ trace env2) : trace env0 }
+  
 
+
 expr :: Type -> E -> Y ExpY
 expr t a = case a of
   Var a@(Volatile _ _ _) -> addVar a >>= return . VarE
@@ -169,26 +209,45 @@
   Deref _ _ -> notSupported a "indirection operator"
 
 exprConst :: Type -> Const -> ExpY
-exprConst t a = case a of 
-  CBool     a _ -> LitB a
-  CInteger  a _ | t == Bool -> LitB $ a /= 0
-                | otherwise -> LitI a
-  CRational a _ -> LitR a
+exprConst t a = case t of
+  --Integer  Nothing -> error "Verify.exprConst1"
+  --Rational Nothing -> error "Verify.exprConst2"
+  _ -> case a of 
+    CBool     a _ -> LitB a
+    CInteger  a _ | t == Bool -> LitB $ a /= 0
+                  | otherwise -> LitI a
+    CRational a _ -> LitR a
 
 
 
 type Y = StateT Env IO
 
-data Env = Env FilePath Int [(V, String)] [CmdY] [ExpY]  -- Env yices nextId table cmds assertions
+data Env = Env
+  { yices   :: FilePath
+  , nextId  :: Int
+  , vars    :: [(V, String)]
+  , cmds    :: [CmdY]
+  , asserts :: [ExpY]
+  , trace   :: [Trace]
+  }
+ 
+data Trace = Assign' Position String String | Assert' Position String String | Branch' Position String [Trace] [Trace] 
 
 initEnv :: FilePath -> Model -> IO Env
-initEnv y m = execStateT (mapM_ addVar $ map State $ variables m) (Env y 0 [] [] [])
+initEnv y m = execStateT (mapM_ f $ variables m) (Env y 0 [] [] [] [])
+  where
+  f :: VS -> Y ()
+  f a = do
+    n <- addVar v
+    assign (posOf v) v n
+    where
+    v = State a
 
 addVar :: V -> Y String
 addVar v = do
-  Env y i table cmds asserts <- get
-  let name = printf "n%d" i
-  put $ Env y (i + 1) ((v, name) : table) (DEFINE (name, VarT $ typeY v) Nothing : cmds) asserts
+  env <- get
+  let name = printf "n%d" $ nextId env
+  put env { nextId = nextId env + 1, vars = (v, name) : vars env, cmds = DEFINE (name, VarT $ typeY v) Nothing : cmds env }
   return name
 
 getVar :: V -> Y String
@@ -197,9 +256,9 @@
   return $ getVar' env v
 
 getVar' :: Env -> V -> String
-getVar' (Env _ _ table _ _) v = case lookup v table of
+getVar' env v = case lookup v $ vars env of
   Just a -> a
-  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (fst $ unzip table)
+  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (vars env)
 
 typeY :: TypeOf a => a -> String
 typeY a = case typeOf a of
@@ -209,21 +268,31 @@
   Integer  _ -> "int"
   Rational _ -> "real"
 
-trace :: String -> [ExpY] -> Y ()
-trace name vars = do
-  Env _ _ table _ _ <- get
-  liftIO $ writeFile (name ++ ".trace") $ concatMap (traceVar vars) $ reverse table
-
-traceVar :: [ExpY] -> (V, String) -> String
-traceVar vars (a, n) = case a of
-  State (VS name _ _ p) -> "global state " ++ name ++ "(" ++ position p ++ ") = " ++ value ++ ";\n"
-  Branch _ _ p          -> "branch (" ++ position p ++ ") = " ++ value ++ ";\n"
-  _ -> ""
+writeTrace :: String -> [ExpY] -> Y ()
+writeTrace name table' = do
+  env <- get
+  let format p = printf ("%-" ++ show (maximum $ map maxPosWidth $ trace env) ++ "s    ") $ position p
+  liftIO $ writeFile (name ++ ".trace") $ concatMap (f format) $ reverse $ trace env
   where
-  value = case lookup n table of
-    Nothing -> error $ "Variable not found: " ++ show a
-    Just a  -> a
-  table = [ (n, show v) | VarE n := LitB v <- vars ]
-       ++ [ (n, show v) | VarE n := LitI v <- vars ]
-       ++ [ (n, show v) | VarE n := LitR v <- vars ]
+  table = [ (n, if v then "true" else "false") | VarE n := LitB v <- table' ]
+       ++ [ (n, show v) | VarE n := LitI v <- table' ]
+       ++ [ (n, show v) | VarE n := LitR v <- table' ]
+  f :: (Position -> String) -> Trace -> String
+  f format a = case a of
+    Assign' p name var -> case lookup var table of
+      Nothing -> ""
+      Just value -> format p ++ name ++ " = " ++ value ++ ";\n"
+    Assert' p name var -> case lookup var table of
+      Just "true"  -> format p ++ "assertion passed: " ++ name ++ "\n"
+      Just "false" -> format p ++ "assertion FAILED: " ++ name ++ "\n"
+      _ -> ""
+    Branch' p cond onTrue onFalse -> case lookup cond table of
+      Just "true"  -> format p ++ "branch true\n"  ++ concatMap (f format) onTrue
+      Just "false" -> format p ++ "branch false\n" ++ concatMap (f format) onFalse
+      _ -> ""
 
+  maxPosWidth :: Trace -> Int
+  maxPosWidth a = case a of
+    Assign' p _ _ -> length $ position p
+    Assert' p _ _ -> length $ position p
+    Branch' p _ a b -> maximum $ [length (position p)] ++ map maxPosWidth a ++ map maxPosWidth b