diff --git a/RELEASE-NOTES b/RELEASE-NOTES
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,3 +1,10 @@
+afv 0.1.0    01/24/10
+
+- Moved functon calls and assignments to statement position only.
+- Added checks for static top-level declarations, which are not supported.
+- Checks start from 'main' function.  Automatically detects infinite loop.
+- Disallows state modifying expressions.
+
 afv 0.0.4    01/21/10
 
 - Moved branches into model.
diff --git a/afv.cabal b/afv.cabal
--- a/afv.cabal
+++ b/afv.cabal
@@ -1,5 +1,5 @@
 name:    afv
-version: 0.0.4
+version: 0.1.0
 
 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.4"
+version = "0.1.0"
 
 main :: IO ()
 main = do
@@ -19,10 +19,10 @@
           | elem a ["version", "-v", "--version"] -> putStrLn $ "afv " ++ version
     ["example"] -> example
     ["header"]  -> header
-    ("verify":function:args) -> do
+    ("verify":args) -> do
       let a = parseArgs Args { yices = "yices", gcc = "gcc", k = 20, defines = [("AFV", "")], includes = ["."], inputs = [] } args
       units <- sequence [ putStrLn ("parsing " ++ f ++ " ...") >> hFlush stdout >> parse (gcc a) (includes a) (defines a) f | f <- inputs a ]
-      model <- compile function units
+      model <- compile units
       verify (yices a) (k a) model
     _ -> help
 
@@ -70,7 +70,7 @@
 example = do
   header
   putStrLn "writing example design (example.c) ..."
-  putStrLn "verify with:  afv verify example -k 15 example.c"
+  putStrLn "verify with:  afv verify -k 15 example.c"
   writeFile "example.c" $ unlines
     [ "// Provides assert and assume functions."
     , "#include \"afv.h\""
@@ -114,6 +114,10 @@
     , ""
     , "}"
     , ""
+    , "void main() {"
+    , "  while (1) example();"
+    , "}"
+    , ""
     ]
 
 
@@ -128,17 +132,17 @@
   , "  " ++ version
   , ""
   , "SYNOPSIS"
-  , "  afv verify function-name [-k max-k] [--yices=path-to-yices] [--gcc=path-to-gcc] {-Idir} {-Dmacro[=def]} c-file {c-file}"
+  , "  afv verify [-k max-k] [--yices=path-to-yices] [--gcc=path-to-gcc] {-Idir} {-Dmacro[=def]} c-file {c-file}"
   , "  afv header"
   , "  afv example"
   , ""
   , "DESCRIPTION"
-  , "  Afv performs bounded model checking and k-induction on a repetitively called C function."
+  , "  Afv performs bounded model checking and k-induction on C code with a signle infinite loop."
   , "  Requires GCC for C preprocessing and the Yices SMT solver."
   , ""
   , "COMMANDS"
-  , "  verify function-name [options] c-files ..."
-  , "    Runs verification on the specified periodic function."
+  , "  verify [options] c-files ..."
+  , "    Runs verification."
   , ""
   , "    -k n          : Max k-induction depth."
   , "    --yices=path  : Path to Yices solver."
@@ -152,6 +156,6 @@
   , ""
   , "  example"
   , "    Writes an example design (example.c).  Verify with:"
-  , "      afv verify example -k 15 example.c"
+  , "      afv verify -k 15 example.c"
   , ""
   ]
diff --git a/src/Compile.hs b/src/Compile.hs
--- a/src/Compile.hs
+++ b/src/Compile.hs
@@ -11,31 +11,35 @@
 import Utils
 
 -- | Compiles a program to a model for analysis.
-compile :: String -> [CTranslUnit] -> IO Model
-compile function units = do
-  m <- execStateT (evalStat initEnv $ rewrite function units) initMDB
-  return (model m) { actions = reverse $ actions (model m) }
+compile :: [CTranslUnit] -> IO Model
+compile units = do
+  m <- execStateT (evalStat initEnv $ rewrite units) initMDB
+  return (model m) { initActions = reverse $ initActions (model m), loopActions = reverse $ loopActions (model m) }
 
 none :: NodeInfo
 none = internalNode
 
 -- | Rewrites a program to a single statement.  Requires no recursive functions and unique declarations for all top level declarations.
-rewrite :: String -> [CTranslUnit] -> CStat
-rewrite name units = if not $ null asms
+rewrite :: [CTranslUnit] -> CStat
+rewrite 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  --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
+    then error $ "duplicate top-level names found: " ++ intercalate ", " duplicateNames
+    else if not $ null staticFuncDefs
+      then notSupported (head staticFuncDefs) "top-level static declarations"
+      else if not $ null staticVarDefs
+        then notSupported (head staticVarDefs) "top-level static declarations"
+        else CCompound [] (varDefs ++ funcDefs ++ [CBlockStmt call]) none
   where
   items = [ a | CTranslUnit items _ <- units, a <- items ]
-  varDefs  = [ a | CDeclExt a <- items ]
-  vars  = [ CBlockDecl (CDecl (CStorageSpec (CStatic none) : specs) a b) | CDecl specs a b <- varDefs ]  -- Make top level vars static.
-  funcDefs = [ a | CFDefExt a <- items ]
-  funcs = map CNestedFunDef $ sortFunctions funcDefs
+  varDefs  = [ CBlockDecl a | CDeclExt a@(CDecl specs _ _) <- items, not $ isExtern $ fst $ typeInfo specs ]
+  funcDefs = map CNestedFunDef $ sortFunctions [ a | CFDefExt a@(CFunDef specs _ _ _ _) <- items, not $ isExtern $ fst $ typeInfo specs ]
   asms  = [ a | CAsmExt  a <- items ]
   call :: CStat
-  call = CExpr (Just $ CCall (CVar (Ident name 0 none) none) [] none) none
-  duplicateNames = duplicates $ [ name | f <- funcDefs, let (_, (Ident name _ _), _, _) = functionInfo f ] ++ concat [ [ name | (Just (CDeclr (Just (Ident name _ _)) _ _ _ _), _, _) <- a ] | CDecl _ a _ <- varDefs ]
+  call = CExpr (Just $ CCall (CVar (Ident "main" 0 none) none) [] none) none
+  duplicateNames = duplicates $ [ name | CNestedFunDef f <- funcDefs, let (_, (Ident name _ _), _, _) = functionInfo f ] ++ concat [ [ name | (Just (CDeclr (Just (Ident name _ _)) _ _ _ _), _, _) <- a ] | CBlockDecl (CDecl _ a _) <- varDefs ]
+  staticFuncDefs = [ a | CFDefExt a@(CFunDef specs _ _ _ _) <- items, isStatic $ fst $ typeInfo specs ]
+  staticVarDefs  = [ a | CDeclExt a@(CDecl specs _ _) <- items, isStatic $ fst $ typeInfo specs ]
 
 duplicates :: Eq a => [a] -> [a]
 duplicates [] = []
@@ -46,15 +50,19 @@
 
 data MDB = MDB
   { nextId' :: Int
+  , stage   :: Stage
   , stack   :: [Ident]
   , model   :: Model
   }
 
+data Stage = Init | Loop | Done deriving Eq
+
 initMDB :: MDB
 initMDB = MDB
   { nextId' = 0
+  , stage   = Init
   , stack   = []
-  , model   = Model { variables = [], actions = [] }
+  , model   = Model { initActions = [], loopActions = [] }
   }
 
 nextId :: M Int
@@ -63,43 +71,59 @@
   put m { nextId' = nextId' m + 1 }
   return $ nextId' m
 
+setStage :: Stage -> M ()
+setStage a = do
+  m <- get
+  put m { stage = a }
 
+getStage :: M Stage
+getStage = do
+  m <- get
+  return $ stage m
+
 -- | Environment for resolving identifiers.
-data Env = Env
-  { values  :: [Value]
-  }
+type Env = [Value]
 
-data Value
-  = EnvFunction String Function
-  | EnvVariable String V
+data Value = EnvFunction String Function | EnvVariable String V
 
-data Function = Function Int ([E] -> M E)
+data Function = Function Int ([E] -> M ())
 
 -- | Looks of a variable in the environment.
 variable :: Env -> Ident -> V
 variable env i@(Ident name _ _) = if null m then err i $ "variable \"" ++ name ++ "\" not found" else head m
   where
-  m = [ a | EnvVariable n a <- values env, n == name ]
+  m = [ a | EnvVariable n a <- env, n == name ]
 
 -- | Looks of a function in the environment.
 function :: Env -> Ident -> Function
 function env i@(Ident name _ _) = if null m then err i $ "function \"" ++ name ++ "\" not found" else head m
   where
-  m = [ a | EnvFunction n a <- values env, n == name ]
+  m = [ a | EnvFunction n a <- env, n == name ]
 
 -- | Creates a branch.
-branch :: Position -> V -> M a -> M a -> M (a, a)
-branch n a onTrue onFalse = do
+branch :: Position -> V -> M () -> M () -> M ()
+branch p a onTrue onFalse = do   --XXX What happens if infinite loop is called within branch?
   m1 <- get
-  put m1 { model = (model m1) { actions = [] } }
-  r1 <- onTrue
+  case stage m1 of
+    Init -> put m1 { model = (model m1) { initActions = [] } }
+    Loop -> put m1 { model = (model m1) { loopActions = [] } }
+    Done -> unexpected p "statements after infinite loop"
+  onTrue
   m2 <- get
-  put m1 { model = (model m2) { actions = [] } }
-  r2 <- onFalse
+  case stage m2 of
+    Init | stage m1 == Init -> put m1 { model = (model m2) { initActions = [] } }
+    Loop | stage m1 == Loop -> put m1 { model = (model m2) { loopActions = [] } }
+    _ -> unexpected p "infinite loop in branch"
+  onFalse
   m3 <- get
-  put m3 { model = (model m3) { actions = actions $ model m1 } }
-  newAction $ Branch a (reverse $ actions $ model m2) (reverse $ actions $ model m3) n
-  return (r1, r2)
+  case stage m3 of
+    Init | stage m1 == Init && stage m2 == Init -> do
+      put m3 { model = (model m3) { initActions = initActions $ model m1 } }
+      newAction $ Branch a (reverse $ initActions $ model m2) (reverse $ initActions $ model m3) p
+    Loop | stage m1 == Loop && stage m2 == Loop -> do
+      put m3 { model = (model m3) { loopActions = loopActions $ model m1 } }
+      newAction $ Branch a (reverse $ loopActions $ model m2) (reverse $ loopActions $ model m3) p
+    _ -> unexpected p "infinite loop in branch"
 
 -- | Push an identifier onto the call stack, do something, then pop it off.
 callStack :: Ident -> M a -> M a
@@ -119,41 +143,31 @@
 
 -- | The initial environment defines the assert and assume functions.
 initEnv :: Env
-initEnv = Env
-  { values =
-    [ EnvFunction "assert" $ Function 1 assert
-    , EnvFunction "assume" $ Function 1 assume
-    ]
-  }
+initEnv = [EnvFunction "assert" $ Function 1 assert, EnvFunction "assume" $ Function 1 assume]
   where
   assert a' = do
     let a = head a'
     s <- callPath
-    x <- latch (posOf a) a
+    x <- latchBool (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
+    x <- latchBool (posOf a) a
     newAction $ Assume x s (posOf a)
-    return $ Var x
 
 -- | Adds new action.
 newAction :: Action -> M ()
 newAction a = do
   m <- get
-  put m { model = (model m) { actions = a : actions (model m) }}
+  case stage m of
+    Init -> put m { model = (model m) { initActions = a : initActions (model m) }}
+    Loop -> put m { model = (model m) { loopActions = a : loopActions (model m) }}
+    Done -> error "Compile.newAction"
 
 -- | Adds new variable.
 addVar :: Env -> V -> M Env
-addVar env a = do
-  case a of
-    State a -> do
-      m <- get
-      put m { model = (model m) { variables = if elem a (variables $ model m) then variables $ model m else a : variables (model m) }}
-    _ -> return ()
-  return env { values = EnvVariable name a : values env }
+addVar env a = return $ EnvVariable name a : env
   where
   name = case a of
     State (VS a _ _ _)  -> a
@@ -164,132 +178,109 @@
 
 
 evalStat :: Env -> CStat -> M ()
-evalStat env a = case a of
-  CLabel i a [] _ -> callStack i $ evalStat env a
-  CExpr Nothing _ -> return ()
-  CExpr (Just a) _ -> evalExpr env a >> return ()
-  CCompound ids items _ -> f ids
-    where
-    f :: [Ident] -> M ()
-    f [] = foldM evalBlockItem env items >> return ()
-    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 >>= latch (posOf n)
-    branch (posOf n) a (evalStat env b) (evalStat env c)
-    return ()
-  _ -> notSupported a "statement"
+evalStat env a = do
+  stage <- getStage
+  when (stage == Done) $ unexpected a "statements after infinite loop"
+  case a of
+    CFor (Left Nothing) Nothing Nothing a _              | stage == Init -> do setStage Loop >> evalStat env a >> setStage Done
+    CWhile (CConst (CIntConst (CInteger 1 _ _) _)) a _ _ | stage == Init -> do setStage Loop >> evalStat env a >> setStage Done
+    CLabel i a [] _ -> callStack i $ evalStat env a
+    CCompound ids items _ -> f ids
+      where
+      f :: [Ident] -> M ()
+      f [] = foldM evalBlockItem env items >> return ()
+      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 <- latchBool (posOf n) $ evalExpr env a
+      branch (posOf n) a (evalStat env b) (evalStat env c)
+      return ()
 
+    CExpr Nothing _ -> return ()
+    CExpr (Just (CAssign op a b n)) _ -> case op of
+      CAssignOp -> case evalExpr env a of
+        Var v -> assign (posOf n) v $ evalExpr env b
+        _ -> unexpected a "non variable in left hand of assignment"
+      CMulAssOp -> f CMulOp
+      CDivAssOp -> f CDivOp
+      CRmdAssOp -> f CRmdOp
+      CAddAssOp -> f CAddOp
+      CSubAssOp -> f CSubOp
+      CShlAssOp -> f CShlOp
+      CShrAssOp -> f CShrOp
+      CAndAssOp -> f CAndOp
+      CXorAssOp -> f CXorOp
+      COrAssOp  -> f COrOp
+      where
+      f :: CBinaryOp -> M ()
+      f op = evalStat env (CExpr (Just (CAssign CAssignOp a (CBinary op a b n) n)) n)
+
+    CExpr (Just (CCall (CVar f _) args _)) _ -> do
+      when (arity /= length args) $ unexpected f $ "function called with " ++ show (length args) ++ " arguments, but defined with " ++ show arity ++ " arguments"
+      callStack f $ func $ map (evalExpr env) args
+      where
+      Function arity func = function env f
+
+    CExpr (Just (CCall _ _ _)) _ -> notSupported a "non named function references"
+
+    CExpr (Just (CUnary op a n1)) n2 | elem op [CPreIncOp, CPostIncOp] -> evalStat env (CExpr (Just (CAssign CAddAssOp a one n1)) n2)
+                                     | elem op [CPreDecOp, CPostDecOp] -> evalStat env (CExpr (Just (CAssign CSubAssOp a one n1)) n2)
+      where
+      one = CConst $ CIntConst (cInteger 1) n1
+
+    _ -> notSupported a "statement"
+
 evalBlockItem :: Env -> CBlockItem -> M Env
 evalBlockItem env a = case a of
   CBlockStmt a    -> evalStat env a >> return env
   CBlockDecl a    -> evalDecl env a
   CNestedFunDef a -> evalFunc env a
 
-evalExpr :: Env -> CExpr -> M E
+-- No stateful operations for expressions.
+evalExpr :: Env -> CExpr -> E
 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 (posOf n) v b' >> return a'
-        _ -> unexpected a "non variable in left hand of assignment"
-    CMulAssOp -> f CMulOp
-    CDivAssOp -> f CDivOp
-    CRmdAssOp -> f CRmdOp
-    CAddAssOp -> f CAddOp
-    CSubAssOp -> f CSubOp
-    CShlAssOp -> f CShlOp
-    CShrAssOp -> f CShrOp
-    CAndAssOp -> f CAndOp
-    CXorAssOp -> f CXorOp
-    COrAssOp  -> f COrOp
-    where
-    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 >>= latch (posOf a)
-    (b, c) <- branch (posOf n) a (evalExpr env b) (evalExpr env c)
-    return $ Mux (Var a) b c $ posOf n
-  CCond a Nothing b n -> do
-    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
-    CDivOp -> f Div
-    CRmdOp -> f Mod
-    CAddOp -> f Add
-    CSubOp -> f Sub
+  CCond a (Just b) c n -> Mux (evalExpr env a) (evalExpr env b) (evalExpr env c) $ posOf n
+  CCond a Nothing  b n -> Or (evalExpr env a) (evalExpr env b) $ posOf n
+  CBinary op a' b' n -> case op of
+    CMulOp -> Mul a b p
+    CDivOp -> Div a b p
+    CRmdOp -> Mod a b p
+    CAddOp -> Add a b p
+    CSubOp -> Sub a b p
     CShlOp -> notSupported a "(<<)"
     CShrOp -> notSupported a "(>>)"
-    CLeOp  -> f Lt
-    CGrOp  -> f $ \ a b n -> Lt b a n
-    CLeqOp -> f $ \ a b n -> Not (Lt b a n) n
-    CGeqOp -> f $ \ a b n -> Not (Lt a b n) n
-    CEqOp  -> f Eq
-    CNeqOp -> f $ \ a b n -> Not (Eq a b n) n
+    CLeOp  -> Lt a b p
+    CGrOp  -> Lt b a p
+    CLeqOp -> Not (Lt b a p) p
+    CGeqOp -> Not (Lt a b p) p
+    CEqOp  -> Eq a b p
+    CNeqOp -> Not (Eq a b p) p
     CAndOp -> notSupported a "(&)"
     CXorOp -> notSupported a "(^)"
     COrOp  -> notSupported a "(|)"
-    CLndOp -> do
-      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 >>= latch (posOf a)
-      (a, b) <- branch n' a (return $ Var a) (evalExpr env b)
-      return $ Mux a a b n'
+    CLndOp -> And a b p
+    CLorOp -> Or a b p
     where
-    n' = posOf n
-    f :: (E -> E -> Position -> E) -> M E
-    f op = do
-      a <- evalExpr env a
-      b <- evalExpr env b
-      return $ op a b n'
+    a = evalExpr env a'
+    b = evalExpr env b'
+    p = posOf n
 
-  CUnary op a n -> do
-    a <- evalExpr env a
-    case (op, a) of
-      (CPreIncOp, Var a) -> do
-        assign p a $ Add (Var a) one p
-        return $ Var a
-      (CPreDecOp, Var a) -> do
-        assign p a $ Sub (Var a) one p
-        return $ Var a
-      (CPostIncOp, Var a) -> do
-        b <- latch p $ Var a
-        assign p a $ Add (Var a) one p
-        return $ Var b
-      (CPostDecOp, Var a) -> do
-        b <- latch p $ Var a
-        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
-      --(CAdrOp,  a) -> return $ Ref a p
-      --(CIndOp,  a) -> return $ Deref a p
-      _ -> notSupported n "unary operator"
+  CUnary op a' n -> case op of
+    CPlusOp -> a
+    CMinOp  -> Sub zero a p
+    CNegOp  -> Not a p
+    --(CAdrOp,  a) -> return $ Ref a p
+    --(CIndOp,  a) -> return $ Deref a p
+    _ -> notSupported n "unary operator"
     where
+    a = evalExpr env a'
     p = posOf n
-    one  = Const $ M.CInteger 1 p
     zero = Const $ M.CInteger 0 p
 
-  CCall (CVar f _) args _ -> do
-    args <- mapM (evalExpr env) args
-    when (arity /= length args) $ unexpected f $ "function called with " ++ show (length args) ++ " arguments, but defined with " ++ show arity ++ " arguments"
-    callStack f $ func args
-    where
-    Function arity func = function env f
-
-  CCall _ _ _ -> notSupported a "non named function references"
-
-  CVar i _ -> return $ Var $ variable env i
+  CVar i _ -> Var $ variable env i
   CConst a -> case a of
-    CIntConst (CInteger a _ _) n -> return $ Const $ M.CInteger a $ posOf n
-    CFloatConst (CFloat a) n -> return $ Const $ CRational (toRational (read a :: Double)) $ posOf n
+    CIntConst (CInteger a _ _) n -> Const $ M.CInteger a $ posOf n
+    CFloatConst (CFloat a) n -> Const $ CRational (toRational (read a :: Double)) $ posOf n
     _ -> notSupported a "char or string constant"
   _ -> notSupported a "expression"
     
@@ -324,15 +315,16 @@
 
       (Just (CInitExpr c _), Nothing) -> evalDecl' env (a, Nothing, Just c)
 
-      (Nothing, Just e') -> do
-        e <- evalExpr env e'
+      (Nothing, Just e) -> do
         v <- if isVolatile typInfo
           then return $ Volatile name typ $ posOf n
           else do
             i <- nextId
-            return $ Local name typ i (posOf e')
-        declare (posOf e') v e
+            return $ Local name typ i p
+        declare p v $ evalExpr env e
         addVar env v
+        where
+        p = posOf e
       _ -> notSupported i "variable declaration"
     _ -> notSupported d "arrays, pointers, or functional pointers (So what good is this tool anyway?)"
       
@@ -340,7 +332,7 @@
 evalFunc :: Env -> CFunDef -> M Env
 evalFunc env f =  do
   when (typ /= Void) $ notSupported f "non void function"
-  return env { values = EnvFunction name (Function (length args) func) : values env }
+  return $ EnvFunction name (Function (length args) func) : env
   where
   (specs, (Ident name _ _), args', stat) = functionInfo f
   (_, typ) = typeInfo specs
@@ -348,7 +340,6 @@
   func args' = do
     env <- foldM bindArg env $ zip args args'
     evalStat env stat
-    return false --XXX No support for 'return'.
 
 bindArg :: Env -> ((Ident, (TypeInfo, Type)), E) -> M Env
 bindArg env ((Ident name _ n, (typInfo, typ)), a) = if isVolatile typInfo
@@ -382,17 +373,12 @@
   _ -> newAction $ Assign v a n
 
 -- | 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
+latchBool :: Position -> E -> M V
+latchBool n a = do
   i <- nextId
-  let v = Tmp (typeOf a) i n
-  case typeOf a of
-    Integer  Nothing -> error "Compile.latch1"
-    Rational Nothing -> error "Compile.latch2"
-    _ -> do
-      declare n v a
-      return v
+  let v = Tmp Bool i n
+  declare n v a
+  return v
 
 
 
@@ -445,6 +431,7 @@
     CIf a b (Just c) _ -> fe env a ++ fs env b ++ fs env c
     CSwitch a b _ -> fe env a ++ fs env b
     CWhile a b _ _ -> fe env a ++ fs env b
+    CFor (Left Nothing) Nothing Nothing a _ -> fs env a
     CFor _ _ _ _ _ -> notSupported a "for loops"
     CGoto _ _ -> []
     CGotoPtr a _ -> fe env a
diff --git a/src/Model.hs b/src/Model.hs
--- a/src/Model.hs
+++ b/src/Model.hs
@@ -15,8 +15,11 @@
   , isInteger
   , typeCheckModel
   , unify
+  , eVars
+  , variables
   ) where
 
+import Data.List
 import Language.C.Data.Position
 
 import Error
@@ -188,7 +191,7 @@
   (a, b) -> err n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b
 
 typeCheckModel :: Model -> Model
-typeCheckModel m = m { actions = map typeCheckAction $ actions m }
+typeCheckModel m = m { initActions = map typeCheckAction $ initActions m, loopActions = map typeCheckAction $ loopActions m }
 
 typeCheckAction :: Action -> Action
 typeCheckAction a = case a of
@@ -204,6 +207,24 @@
 false :: E
 false = Const $ CBool False nopos
 
+eVars :: E -> [V]
+eVars a = case a of
+  Var a -> [a]
+  Const _ -> []
+  Not a _ -> eVars a
+  And a b _ -> eVars a ++ eVars b
+  Or  a b _ -> eVars a ++ eVars b
+  Mul a b _ -> eVars a ++ eVars b
+  Div a b _ -> eVars a ++ eVars b
+  Mod a b _ -> eVars a ++ eVars b
+  Add a b _ -> eVars a ++ eVars b
+  Sub a b _ -> eVars a ++ eVars b
+  Lt  a b _ -> eVars a ++ eVars b
+  Eq  a b _ -> eVars a ++ eVars b
+  Mux a b c _ -> eVars a ++ eVars b ++ eVars c
+  Ref a _ -> eVars a
+  Deref a _ -> eVars a
+
 instance Pos Position where posOf = id
 
 data Action
@@ -222,8 +243,22 @@
     Assume  _ _ a -> a
     Branch  _ _ _ a -> a
 
+variables :: Model -> [VS]
+variables m = nub $ concatMap vars $ initActions m ++ loopActions m
+  where
+  vars :: Action -> [VS]
+  vars a = case a of
+    Declare v e _ -> var v ++ [ a | State a <- eVars e ]
+    Assign  v e _ -> var v ++ [ a | State a <- eVars e ]
+    Assert  v _ _ -> var v
+    Assume  v _ _ -> var v
+    Branch  v a b _ -> var v ++ concatMap vars a ++ concatMap vars b
+  var :: V -> [VS]
+  var (State a) = [a]
+  var _         = []
+    
 data Model = Model
-  { variables :: [VS]
-  , actions   :: [Action]
+  { initActions :: [Action]
+  , loopActions :: [Action]
   } deriving Show
 
diff --git a/src/Verify.hs b/src/Verify.hs
--- a/src/Verify.hs
+++ b/src/Verify.hs
@@ -13,12 +13,13 @@
 -- | Verify a model with k-induction.
 verify :: FilePath -> Int -> Model -> IO ()
 verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"
-verify yices maxK m = do
-  mapM_ (verifyModel yices format maxK) models
+verify yices maxK m' = mapM_ (verifyModel yices format maxK) models
   where
-  model = typeCheckModel m
-  models = [ (name, trimModel model { actions = actions }) | (name, actions) <- trimAssertions (actions model) ]
-  format = "verifying %-" ++ show (maximum [ length n | (n, _) <- models ]) ++ "s    "
+  m = typeCheckModel m'
+  initPlain = removeAssertions $ initActions m
+  models = [ (name, m { initActions = actions,   loopActions = []      }) | (name, actions) <- trimAssertions $ initActions m ]
+        ++ [ (name, m { initActions = initPlain, loopActions = actions }) | (name, actions) <- trimAssertions $ loopActions m ]
+  format = "verifying %-" ++ show (maximum $ map length $ fst $ unzip models) ++ "s    "
 
 -- | Remove all assertions except one.
 trimAssertions :: [Action] -> [(String, [Action])]
@@ -40,29 +41,32 @@
 
 -- | Trim all unneeded stuff from a model.
 trimModel :: Model -> Model
-trimModel = id  --XXX
+trimModel = id --XXX
 
+
 -- | Verify a trimmed model.
 verifyModel :: FilePath -> String -> Int -> (String, Model) -> IO ()
-verifyModel y format maxK (name, m) = do
+verifyModel y format maxK (name, m') = do
   printf format name
   hFlush stdout
   env0 <- initEnv y m
-  execStateT (check env0 1) env0
+  execStateT (actions (initActions m) >> doLoop >> check env0 1) env0
   return ()
   where
+  m = trimModel m'
   check :: Env -> Int -> Y ()
   check env0 k = do
-    transition m
+    actions $ loopActions m
     resultBasis <- checkBasis m 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 trace)\n" k) >> writeTrace True name a
       Problem -> error "Verify.check1"
-      Pass -> do
+      Pass | null $ loopActions m -> liftIO $ printf "passed: assertion in initialization\n"
+           | otherwise -> 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) >> writeTrace name a
+                 | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace False name a
           Problem -> error "Verify.check2"
           Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k
         
@@ -72,16 +76,21 @@
 checkStep :: Y Result
 checkStep = do
   env <- get
-  let cmds' = reverse $ [CHECK] ++ [ASSERT $ NOT $ head $ asserts env] ++ cmds env
-  r <- liftIO $ quickCheckY' (yices env) [] $ cmds'
-  return $ result r
+  if null $ asserts env
+    then return Pass
+    else do
+      let cmds = vars env ++ loopCmds env ++ [ASSERT $ NOT $ head $ asserts env] ++ [CHECK]
+      r <- liftIO $ quickCheckY' (yices env) [] cmds
+      return $ result r
 
 -- | Check induction basis.
 checkBasis :: Model -> Env -> Y Result
 checkBasis m env0 = do
   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'
+  let cmds = vars env ++ initCmds env ++ loopCmds env ++ [ASSERT $ NOT $ AND $ asserts env]
+          ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ]
+          ++ [CHECK]
+  r <- liftIO $ quickCheckY' (yices env) [] cmds
   return $ result r
 
 result :: ResY -> Result
@@ -92,16 +101,14 @@
   _ -> error $ "unexpected yices results: " ++ show a
 
 
--- | Transition relation.  Returns assertion.
-transition :: Model -> Y ()
-transition m = mapM_ (action $ LitB True) $ actions m
+actions :: [Action] -> Y ()
+actions a = mapM_ (action $ LitB True) a
 
 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 }
+    State (VS name _ _ _) -> addTrace $ Assign' p name n
+    Local name _ _ _      -> addTrace $ Assign' p name n
     _ -> return ()
     
 action :: ExpY -> Action -> Y ()
@@ -109,34 +116,38 @@
   Declare v e p -> do
     e <- expr (typeOf v) e
     v' <- addVar v
-    env <- get
-    put env { cmds = ASSERT (VarE v' := e) : cmds env }
+    addCmd $ ASSERT (VarE v' := e)
     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 }
+    addCmd $ ASSERT (VarE v' := IF enabled e (VarE vLast))
     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 }
+    put env { asserts = (enabled :=> VarE a) : asserts env }
+    addTrace $ Assert' p n a
   Assume a _ _ -> do
     a <- getVar a
-    env <- get
-    put env { cmds = ASSERT (enabled :=> VarE a) : cmds env }
+    addCmd $ ASSERT (enabled :=> VarE a)
   Branch a onTrue onFalse p -> do
     a' <- getVar a
     env0 <- get
-    put env0 { trace = [] }
+    if inLoop env0
+      then put env0 { loopTrace = [] }
+      else put env0 { initTrace = [] }
     mapM_ (action $ AND [enabled,       VarE a']) onTrue
     env1 <- get
-    put env1 { trace = [] }
+    if inLoop env1
+      then put env1 { loopTrace = [] }
+      else put env1 { initTrace = [] }
     mapM_ (action $ AND [enabled, NOT $ VarE a']) onFalse
     env2 <- get
-    put env2 { trace = Branch' p a' (reverse $ trace env1) (reverse $ trace env2) : trace env0 }
+    if inLoop env2
+      then put env2 { loopTrace = Branch' p a' (reverse $ loopTrace env1) (reverse $ loopTrace env2) : loopTrace env0 }
+      else put env2 { initTrace = Branch' p a' (reverse $ initTrace env1) (reverse $ initTrace env2) : initTrace env0 }
   
 
 
@@ -223,19 +234,38 @@
 type Y = StateT Env IO
 
 data Env = Env
-  { yices   :: FilePath
-  , nextId  :: Int
-  , vars    :: [(V, String)]
-  , cmds    :: [CmdY]
-  , asserts :: [ExpY]
-  , trace   :: [Trace]
+  { yices     :: FilePath
+  , nextId    :: Int
+  , inLoop    :: Bool
+  , names     :: [(V, String)]
+  , vars      :: [CmdY]
+  , initCmds  :: [CmdY]
+  , loopCmds  :: [CmdY]
+  , asserts   :: [ExpY]
+  , initTrace :: [Trace]
+  , loopTrace :: [Trace]
   }
  
-data Trace = Assign' Position String String | Assert' Position String String | Branch' Position String [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_ f $ variables m) (Env y 0 [] [] [] [])
+initEnv y m = execStateT (mapM_ f $ variables m) env
   where
+  env = Env
+    { yices     = y
+    , nextId    = 0
+    , inLoop    = False
+    , names     = []
+    , vars      = []
+    , initCmds  = []
+    , loopCmds  = []
+    , asserts   = []
+    , initTrace = []
+    , loopTrace = []
+    }
   f :: VS -> Y ()
   f a = do
     n <- addVar v
@@ -243,22 +273,41 @@
     where
     v = State a
 
+doLoop :: Y ()
+doLoop = do
+  env <- get
+  put env { inLoop = True }
+
 addVar :: V -> Y String
 addVar v = do
   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 }
+  put env { nextId = nextId env + 1, names = (v, name) : names env, vars = DEFINE (name, VarT $ typeY v) Nothing : vars env }
   return name
 
+addCmd :: CmdY -> Y ()
+addCmd cmd = do
+  env <- get
+  if inLoop env
+    then put env { loopCmds = cmd : loopCmds env }
+    else put env { initCmds = cmd : initCmds env }
+
+addTrace :: Trace -> Y ()
+addTrace t = do
+  env <- get
+  if inLoop env
+    then put env { loopTrace = t : loopTrace env }
+    else put env { initTrace = t : initTrace env }
+
 getVar :: V -> Y String
 getVar v = do
   env <- get
   return $ getVar' env v
 
 getVar' :: Env -> V -> String
-getVar' env v = case lookup v $ vars env of
+getVar' env v = case lookup v $ names env of
   Just a -> a
-  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (vars env)
+  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (names env)
 
 typeY :: TypeOf a => a -> String
 typeY a = case typeOf a of
@@ -268,12 +317,14 @@
   Integer  _ -> "int"
   Rational _ -> "real"
 
-writeTrace :: String -> [ExpY] -> Y ()
-writeTrace name table' = do
+writeTrace :: Bool -> String -> [ExpY] -> Y ()
+writeTrace withInit 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
+  let format p = printf ("%-" ++ show (maximum $ map maxPosWidth $ (if withInit then initTrace env else []) ++ loopTrace env) ++ "s    ") $ position p
+  liftIO $ writeFile (name ++ ".trace") $ (if withInit then trace format "init" (initTrace env) else "") ++ trace format "loop" (loopTrace env)
   where
+  trace :: (Position -> String) -> String -> [Trace] -> String
+  trace format n t = n ++ ":\n" ++ concatMap (f format) (reverse t)
   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' ]