diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -329,8 +329,10 @@
 if_ name cond stmt = ifelse name cond stmt $ return ()
 
 -- | Verify a program.
-verify :: Stmt () -> IO (Maybe Bool)
-verify program = V.verify $ snd $ evalStmt [] program
+--
+-- ^ verify pathToYices maxK program
+verify :: FilePath -> Int -> Stmt () -> IO ()
+verify yices maxK program = V.verify yices maxK $ snd $ evalStmt [] program
 
 -- | Generate C code.
 code :: Name -> Stmt () -> IO ()
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -22,43 +22,37 @@
     ++ codeVariables False scope ++ "\n"
     ++ "void " ++ name ++ "(void);\n\n"
   where
-  [scope] = tree (\ (path, _, _, _) -> path) $ varsInStmt stmt
-
-varName :: V a -> String
-varName a = intercalate "." names
-  where
-  names = case a of
-    V _ names _ -> names
+  [scope] = tree (\ (_, path, _) -> path) $ stmtVars stmt
 
 codeStmt :: Statement -> String
 codeStmt a = case a of
-  AssignBool  a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
-  AssignInt   a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
-  AssignFloat a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"
-  Branch path a b Null -> "// if_ "    ++ intercalate "." path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"
-  Branch path a b c    -> "// ifelse " ++ intercalate "." path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"
+  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"
   Sequence a b -> codeStmt a ++ codeStmt b
-  Assert path a -> "// assert " ++ intercalate "." path ++ "\nassert(" ++ codeExpr a ++ ");\n"
-  Assume path a -> "// assume " ++ intercalate "." path ++ "\nassert(" ++ codeExpr a ++ ");\n"
+  Assert path a -> "// assert " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"
+  Assume path a -> "// assume " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"
   Null -> ""
 
 codeExpr :: E a -> String
 codeExpr a = case a of
-  Ref a -> varName a
-  Const a -> showConst a
-  Add a b -> group [codeExpr a, "+", codeExpr b]
-  Sub a b -> group [codeExpr a, "-", codeExpr b]
-  Mul a b -> group [codeExpr a, "*", showConst b]
-  Div a b -> group [codeExpr a, "/", showConst b]
-  Mod a b -> group [codeExpr a, "%", showConst b]
-  Not a   -> group ["!", codeExpr a]
-  And a b -> group [codeExpr a, "&&",  codeExpr b]
-  Or  a b -> group [codeExpr a, "||",  codeExpr b]
-  Eq  a b -> group [codeExpr a, "==",  codeExpr b]
-  Lt  a b -> group [codeExpr a, "<",   codeExpr b]
-  Gt  a b -> group [codeExpr a, ">",   codeExpr b]
-  Le  a b -> group [codeExpr a, "<=",  codeExpr b]
-  Ge  a b -> group [codeExpr a, ">=",  codeExpr b]
+  Ref a     -> pathName a
+  Const a   -> showConst $ const' a
+  Add a b   -> group [codeExpr a, "+", codeExpr b]
+  Sub a b   -> group [codeExpr a, "-", codeExpr b]
+  Mul a b   -> group [codeExpr a, "*", showConst (const' b)]
+  Div a b   -> group [codeExpr a, "/", showConst (const' b)]
+  Mod a b   -> group [codeExpr a, "%", showConst (const' b)]
+  Not a     -> group ["!", codeExpr a]
+  And a b   -> group [codeExpr a, "&&",  codeExpr b]
+  Or  a b   -> group [codeExpr a, "||",  codeExpr b]
+  Eq  a b   -> group [codeExpr a, "==",  codeExpr b]
+  Lt  a b   -> group [codeExpr a, "<",   codeExpr b]
+  Gt  a b   -> group [codeExpr a, ">",   codeExpr b]
+  Le  a b   -> group [codeExpr a, "<=",  codeExpr b]
+  Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]
   Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] 
   where
   group :: [String] -> String
@@ -72,47 +66,27 @@
   [] -> []
   (a:b) -> a ++ "\n" ++ indent (unlines b)
 
-codeVariables :: Bool -> (Tree Name ([Name], Bool, String, String)) -> String
+codeVariables :: Bool -> (Tree Name (Bool, Path, Const)) -> String
 codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n  " ++ f2 a else "") ++ ";\n"
   where
   f1 a = case a of
     T.Branch name items -> "struct {  // " ++ name ++ "\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"
-    Leaf name (_, input, typ, _) -> printf "%-5s %-25s;%s\n" typ name (if input then "  // input" else "")
+    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  // input" else "")
 
   f2 a = case a of
     T.Branch name items -> indent' $ "{ " ++ (intercalate ", " $ map f2 items) ++ "}  // " ++ name ++ "\n"
-    Leaf name (_, _, _, init) -> printf "%-15s  // %s\n" init name
-
-varInfo :: AllE a => V a -> ([Name], Bool, String, String)
-varInfo (V input path a) = (path, input, showType a, showConst a)
+    Leaf name (_, _, init) -> printf "%-15s  // %s\n" (showConst init) name
 
-varsInStmt :: Statement -> [([Name], Bool, String, String)] -- (path, isInput, type, init)
-varsInStmt a = case a of
-  AssignBool  a b -> nub $ varInfo a : varsInExpr b
-  AssignInt   a b -> nub $ varInfo a : varsInExpr b
-  AssignFloat a b -> nub $ varInfo a : varsInExpr b
-  Branch _ a b c  -> nub $ varsInExpr a ++ varsInStmt b ++ varsInStmt c
-  Sequence a b    -> nub $ varsInStmt a ++ varsInStmt b
-  Assert _ a      -> varsInExpr a
-  Assume _ a      -> varsInExpr a
-  Null            -> []
+showConst :: Const -> String
+showConst a = case a of
+  Bool  True  -> "1"
+  Bool  False -> "0"
+  Int   a     -> show a
+  Float a     -> show a
 
-varsInExpr :: E a -> [([Name], Bool, String, String)] -- (path, isInput, type, init)
-varsInExpr a = case a of
-  Ref a     -> [varInfo a]
-  Const _   -> []
-  Add a b   -> varsInExpr a ++ varsInExpr b
-  Sub a b   -> varsInExpr a ++ varsInExpr b
-  Mul a _   -> varsInExpr a
-  Div a _   -> varsInExpr a
-  Mod a _   -> varsInExpr a
-  Not a     -> varsInExpr a
-  And a b   -> varsInExpr a ++ varsInExpr b
-  Or  a b   -> varsInExpr a ++ varsInExpr b
-  Eq  a b   -> varsInExpr a ++ varsInExpr b
-  Lt  a b   -> varsInExpr a ++ varsInExpr b
-  Gt  a b   -> varsInExpr a ++ varsInExpr b
-  Le  a b   -> varsInExpr a ++ varsInExpr b
-  Ge  a b   -> varsInExpr a ++ varsInExpr b
-  Mux a b c -> varsInExpr a ++ varsInExpr b ++ varsInExpr c
+showConstType :: Const -> String
+showConstType a = case a of
+  Bool  _ -> "int"
+  Int   _ -> "int"
+  Float _ -> "float"
 
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -2,38 +2,53 @@
   ( E (..)
   , V (..)
   , Name
+  , Path
+  , PathName (..)
   , AllE (..)
   , NumE
+  , Const (..)
   , Statement (..)
+  , VarInfo
+  , varInfo
+  , stmtVars
+  , exprVars
   ) where
 
+import Data.List
 import Data.Ratio
 
 type Name = String
 
-data V a = V Bool [Name] a
+type Path = [Name]
 
+data V a = V Bool [Name] a deriving Eq
+
+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
+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
-  showConst :: a -> String
-  showType  :: a -> String
-  zero      :: (Name -> a -> m (V a)) -> a
+  zero   :: (Name -> a -> m (V a)) -> a
+  const' :: a -> Const
 
 instance AllE Bool where
-  showConst a = case a of
-    True  -> "1"
-    False -> "0"
-  showType _ = "int"
   zero = const False
+  const' = Bool
 
 instance AllE Int where
-  showConst = show
-  showType _ = "int"
   zero = const 0
+  const' = Int
   
 instance AllE Float where
-  showConst = show
-  showType _ = "float"
   zero = const 0
+  const' = Float
 
 class    AllE a => NumE a
 instance NumE Int
@@ -78,9 +93,52 @@
   = AssignBool  (V Bool ) (E Bool )
   | AssignInt   (V Int  ) (E Int  )
   | AssignFloat (V Float) (E Float)
-  | Branch      [Name] (E Bool) Statement Statement
+  | Branch      Path (E Bool) Statement Statement
   | Sequence    Statement Statement
-  | Assert      [Name] (E Bool)
-  | Assume      [Name] (E Bool)
+  | Assert      Path (E Bool)
+  | Assume      Path (E Bool)
   | Null
+
+data Const
+  = Bool  Bool
+  | Int   Int
+  | Float Float
+  deriving Eq
+
+type VarInfo = (Bool, Path, Const)
+
+varInfo :: AllE a => V a -> VarInfo
+varInfo (V input path init) = (input, path, const' init)
+
+-- Information about all of a program's variables.
+stmtVars :: Statement -> [VarInfo]
+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
+  Null            -> []
+
+-- Information about all of an expressions's variables.
+exprVars :: E a -> [VarInfo]
+exprVars a = case a of
+  Ref a     -> [varInfo a]
+  Const _   -> []
+  Add a b   -> exprVars a ++ exprVars b
+  Sub a b   -> exprVars a ++ exprVars b
+  Mul a _   -> exprVars a
+  Div a _   -> exprVars a
+  Mod a _   -> exprVars a
+  Not a     -> exprVars a
+  And a b   -> exprVars a ++ exprVars b
+  Or  a b   -> exprVars a ++ exprVars b
+  Eq  a b   -> exprVars a ++ exprVars b
+  Lt  a b   -> exprVars a ++ exprVars b
+  Gt  a b   -> exprVars a ++ exprVars b
+  Le  a b   -> exprVars a ++ exprVars b
+  Ge  a b   -> exprVars a ++ exprVars b
+  Mux a b c -> exprVars a ++ exprVars b ++ exprVars c
 
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -2,7 +2,9 @@
 module Language.ImProve.Examples
   ( gcd'
   , gcdMain
-  , gcdBuild
+  , buildGCD
+  , counter
+  , verifyCounter
   ) where
 
 import Language.ImProve
@@ -52,6 +54,25 @@
 
 
 -- | Build the gcdMain code (i.e. gcd.c, gcd.h).
-gcdBuild :: IO ()
-gcdBuild = code "gcd" gcdMain
+buildGCD :: IO ()
+buildGCD = code "gcd" gcdMain
+
+
+
+-- | A rolling counter verification example.
+counter :: Stmt ()
+counter = do
+  -- The counter variable.
+  counter <- int "counter" 0
+
+  -- Specification.
+  assert "GreaterThanOrEqualTo0" $ ref counter >=. 0
+  assert "LessThan10"            $ ref counter <.  10
+
+  -- Implementation.
+  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (incr counter)
+
+-- Verify the 'counter' example.
+verifyCounter :: IO ()
+verifyCounter = verify "yices" 20 counter
 
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -1,7 +1,320 @@
 module Language.ImProve.Verify (verify) where
 
+import Control.Monad.State hiding (State)
+import Math.SMT.Yices.Pipe
+import Math.SMT.Yices.Syntax
+import System.IO
+import Text.Printf
+
 import Language.ImProve.Core
 
-verify :: Statement -> IO (Maybe Bool)
-verify _ = putStrLn "verification not implemented yet" >> return Nothing
+-- | 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
+  mapM_ (verifyProgram yices format maxK) $ trimAssertions program
+  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 ]
+
+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 path cond a b -> [ Branch path cond a (removeAssertions b) | a <- trimAssertions' a ]
+                       ++ [ Branch path cond (removeAssertions a) b | b <- trimAssertions' b ]
+  a -> [a]
+
+-- | Remove all assertions.
+removeAssertions :: Statement -> Statement
+removeAssertions a = case a of
+  Assert _ _ -> Null
+  Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)
+  Branch path cond a b -> Branch path cond (removeAssertions a) (removeAssertions b)
+  a -> 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
+  _ -> []
+
+-- | Trim all unneeded stuff from a program.
+trimProgram :: Statement -> Statement
+trimProgram = id --XXX
+
+-- | Verify a trimmed program.
+verifyProgram :: FilePath -> String -> Int -> Statement -> IO ()
+verifyProgram yices format maxK program' = do
+  printf format name
+  hFlush stdout
+  env0 <- initEnv program
+  execStateT (check yices name maxK program env0 1) env0
+  return ()
+  where
+  program = trimProgram program'
+  name = pathName $ head' "a1" $ assertions program
+
+head' msg a = if null a then error msg else head a
+
+data Result = Pass | Fail [ExpY] | Problem
+
+-- | k-induction.
+check :: FilePath -> Name -> Int -> Statement -> Env -> Int -> Y ()
+check yices name maxK program env0 k = do
+  addTrace $ Cycle' $ k - 1
+  inputs program
+  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
+    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
+        Problem -> error "Verify.check2"
+        Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k
+        
+-- | Check induction step.
+checkStep :: FilePath -> Y Result
+checkStep yices = do
+  env <- get
+  r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env) ++ [ASSERT $ NOT $ head' "a2" $ asserts env] ++ [CHECK]
+  return $ result r
+
+-- | Check induction basis.
+checkBasis :: FilePath -> Statement -> Env -> Y Result
+checkBasis yices program env0 = do
+  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 ]
+          ++ [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 ]
+
+result :: ResY -> Result
+result a = case a of
+  Sat a   -> Fail a
+  UnSat _ -> Pass
+  InCon _ -> Problem
+  _ -> error $ "unexpected yices results: " ++ show a
+
+
+evalStmt :: ExpY -> Statement -> Y ()
+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
+  Assert path 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
+    a <- evalExpr a
+    addCmd $ ASSERT (enabled :=> a)
+  Branch path a onTrue onFalse -> do
+    a <- evalExpr a
+    b <- newBoolVar
+    addCmd $ ASSERT (VarE b := a)
+    env0 <- get
+    put env0 { trace = [] }
+    evalStmt (AND [enabled, a]) onTrue
+    env1 <- get
+    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 }
+  where
+  assign :: AllE a => V a -> E a -> Y ()
+  assign a b = do
+    b <- evalExpr b
+    aPrev <- getVar a
+    aNext <- addVar a
+    addCmd $ ASSERT (VarE aNext := IF enabled b (VarE aPrev))
+    addTrace $ Assign' (pathName a) aNext
+
+evalExpr :: AllE a => E a -> Y ExpY
+evalExpr a = case a of
+  Ref a -> getVar a >>= return . VarE
+  Const a -> return $ evalConst a
+  Add a b ->  do
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a :+: b
+  Sub a b ->  do
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a :-: b
+  Mul a b ->  do
+    a <- evalExpr a
+    return $ a :*: evalConst b
+  Div a b -> do
+    a <- evalExpr a
+    return $ op a $ evalConst b
+    where
+    op = case const' b of
+      Bool  _ -> undefined
+      Int   _ -> DIV
+      Float _ -> (:/:)
+  Mod a b -> do
+    a <- evalExpr a
+    return $ MOD a $ evalConst b
+  Not a -> evalExpr a >>= return . NOT
+  And a b -> do
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ AND [a, b]
+  Or a b -> do
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ OR [a, b]
+  Eq a b -> do  
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a := b
+  Lt a b -> do  
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a :< b
+  Gt a b -> do  
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a :> b
+  Le a b -> do  
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a :<= b
+  Ge a b -> do  
+    a <- evalExpr a
+    b <- evalExpr b
+    return $ a :>= b
+  Mux a b c -> do
+    a <- evalExpr a
+    b <- evalExpr b
+    c <- evalExpr c
+    return $ IF a b c
+
+evalConst :: AllE a => a -> ExpY
+evalConst = evalConst' . const'
+
+evalConst' :: Const -> ExpY
+evalConst' a = case a of
+  Bool  a -> LitB a
+  Int   a -> LitI $ fromIntegral a
+  Float a -> LitR $ toRational a
+
+type Y = StateT Env IO
+
+type Var = String
+
+data Env = Env
+  { nextId    :: Int
+  , var       :: VarInfo -> Var
+  , cmds      :: [CmdY]  -- Commands and variable declarations in reverse order.
+  , asserts   :: [ExpY]  -- Assumes 1 assert in a program under verification.
+  , trace     :: [Trace] -- Program trace in reverse order.
+  }
+ 
+initEnv :: Statement -> IO Env
+initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- stmtVars program, not input ]) Env
+  { nextId  = 0
+  , var     = \ v -> error $ "variable not found in environment: " ++ pathName v
+  , cmds    = []
+  , asserts = []
+  , trace   = []
+  }
+
+data Trace
+  = Init'   Name Var
+  | Cycle'  Int
+  | Input'  Name Var
+  | Assign' Name Var
+  | Assert' Name Var
+  | Branch' Name Var [Trace] [Trace] 
+
+addVar' :: VarInfo -> Y String
+addVar' v = do
+  env <- get
+  let name = printf "n%d" $ nextId env
+  put env { nextId = nextId env + 1, var = \ a -> if a == v then name else var env a, cmds = DEFINE (name, VarT typ) Nothing : cmds env }
+  return name
+  where
+  typ = case v of
+    (_, _, Bool  _) -> "bool"
+    (_, _, Int   _) -> "int"
+    (_, _, Float _) -> "real"
+
+addVar :: AllE a => V a -> Y String
+addVar = addVar' . varInfo
+
+-- | Creates a new boolean variable.  Use for assertions.
+newBoolVar :: Y String
+newBoolVar = do
+  env <- get
+  let name = printf "n%d" $ nextId env
+  put env { nextId = nextId env + 1, cmds = DEFINE (name, VarT "bool") Nothing : cmds env }
+  return name
+
+addCmd :: CmdY -> Y ()
+addCmd cmd = do
+  env <- get
+  put env { cmds = cmd : cmds env }
+
+addTrace :: Trace -> Y ()
+addTrace t = do
+  env <- get
+  put env { trace = t : trace env }
+
+getVar :: AllE a => V a -> Y String
+getVar v = do
+  env <- get
+  return $ var env $ varInfo v
+
+writeTrace :: String -> [ExpY] -> Y ()
+writeTrace name table' = do
+  env <- get
+  liftIO $ writeFile (name ++ ".trace") $ concatMap f $ reverse $ trace env
+  where
+  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 :: Trace -> String
+  f a = case a of
+    Init' path var -> case lookup var table of
+      Nothing -> ""
+      Just value -> "initialize " ++ path ++ " := " ++ value ++ "\n"
+    Cycle' n -> "cycle " ++ show n ++ "\n"
+    Input' path var -> case lookup var table of
+      Nothing -> ""
+      Just value -> "input " ++ path ++ " <== " ++ value ++ "\n"
+    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"
+      _ -> ""
+    Branch' path cond onTrue onFalse -> case lookup cond table of
+      Just "true"  -> "branch true: "  ++ path ++ "\n" ++ indent (concatMap f onTrue)
+      Just "false" -> "branch false: " ++ path ++ "\n" ++ indent (concatMap f onFalse)
+      _ -> ""
+
+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.2
+version: 0.0.3
 
 category: Language
 
@@ -21,8 +21,9 @@
 
 library
     build-depends:
-        base       >= 4.2     && < 5,
-        mtl        >= 1.1.0.1 && < 1.2
+        base  >= 4.2     && < 5,
+        mtl   >= 1.1.0.1 && < 1.2,
+        yices >= 0.0.0.7 && < 0.0.1
 
     exposed-modules:
         Language.ImProve
@@ -32,7 +33,7 @@
         Language.ImProve.Tree
         Language.ImProve.Verify
 
-    extensions: GADTs, FlexibleInstances
+    extensions: GADTs, FlexibleInstances, TypeSynonymInstances
 
     ghc-options: -W