diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) Tom Hawkins 2009, 2010
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
new file mode 100644
--- /dev/null
+++ b/RELEASE-NOTES
@@ -0,0 +1,4 @@
+afv 0.0.0    01/12/10
+
+- Initial release.
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,8 @@
+#! /usr/bin/env runhaskell
+
+> module Main (main) where
+>
+> import Distribution.Simple (defaultMain)
+>
+> main :: IO ()
+> main = defaultMain
diff --git a/afv.cabal b/afv.cabal
new file mode 100644
--- /dev/null
+++ b/afv.cabal
@@ -0,0 +1,52 @@
+name:    afv
+version: 0.0.0
+
+category: Formal Methods
+
+synopsis: Model checking Atom generated C.
+
+description: A model checker for Atom generated, or similar, C code.
+
+author:     Tom Hawkins <tomahawkins@gmail.com>
+maintainer: Tom Hawkins <tomahawkins@gmail.com>
+
+stability: experimental
+
+license:      BSD3
+license-file: LICENSE
+
+homepage: http://tomahawkins.org
+
+build-type:    Simple
+cabal-version: >= 1.6
+
+extra-source-files:
+  RELEASE-NOTES
+
+executable afv
+  hs-source-dirs:   src
+
+  main-is:          AFV.hs
+
+  other-modules:    Compile,
+                    Error,
+                    Model,
+                    Parse,
+                    Utils,
+                    Verify
+
+  build-depends:
+    base          >= 4       && < 5,
+    bytestring    >= 0.9.1   && < 0.9.2,
+    mtl           >= 1.1     && < 1.2,
+    directory     >= 1.0     && < 1.1,
+    process       >= 1.0     && < 1.1,
+    language-c    >= 0.3     && < 0.4,
+    yices         >= 0.0.0.4 && < 0.1
+
+  ghc-options:  -W
+  extensions:
+
+source-repository head
+  type:     darcs
+  location: http://patch-tag.com/r/tomahawkins/afv/pullrepo
diff --git a/src/AFV.hs b/src/AFV.hs
new file mode 100644
--- /dev/null
+++ b/src/AFV.hs
@@ -0,0 +1,150 @@
+module Main (main) where
+
+import Data.List
+import System.Environment
+import System.IO
+
+import Compile
+import Parse
+import Verify
+
+main :: IO ()
+main = do
+  args <- getArgs
+  case args of
+    [] -> help
+    (a:_) | elem a ["help", "-h", "--help", "-help"] -> help
+    ["example"] -> example
+    ["header"]  -> header
+    ("verify":function: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
+      verify (yices a) (k a) model
+    _ -> help
+
+data Args = Args
+  { yices    :: FilePath
+  , k        :: Int
+  , gcc      :: FilePath
+  , defines  :: [(String, String)]
+  , includes :: [FilePath]
+  , inputs   :: [FilePath]
+  } deriving Show
+
+parseArgs :: Args -> [String] -> Args
+parseArgs a b = case b of
+  [] -> a
+  arg : args | isYices   -> parseArgs a { gcc = pathYices } args
+             | isGCC     -> parseArgs a { gcc = pathGCC   } args
+             | isInclude -> parseArgs a { includes = includes a ++ [drop 2 arg]    } args
+             | isDefine  -> parseArgs a { defines  = defines a  ++ [(name, value)] } args
+    where
+    isYices = isPrefixOf "--yices=" arg
+    pathYices = drop 8 arg
+    isGCC   = isPrefixOf "--gcc="   arg
+    pathGCC = drop 6 arg
+    isInclude = length arg > 2 && take 2 arg == "-I"
+    isDefine  = length arg > 2 && take 2 arg == "-D"
+    (name, value') = span (/= '=') $ drop 2 arg
+    value = if length value' <= 1 then "1" else tail value'
+  "-k" : k : args -> parseArgs a { k = read k } args
+  files -> a { inputs = files }
+ 
+
+header :: IO ()
+header = do
+  putStrLn "writing AFV header file (afv.h) ..."
+  writeFile "afv.h" $ unlines
+    [ "#ifndef AFV"
+    , "#include <assert.h>"
+    , "#define assume assert"
+    , "#endif"
+    ]
+
+example :: IO ()
+example = do
+  header
+  putStrLn "writing example design (example.c) ..."
+  putStrLn "verify with:  afv verify example -k 15 example.c"
+  writeFile "example.c" $ unlines
+    [ "// Provides assert and assume functions."
+    , "#include \"afv.h\""
+    , ""
+    , "// Periodic function for verification.  Implements a simple rolling counter."
+    , "void example () {"
+    , ""
+    , "  // The rolling counter."
+    , "  static int counter = 0;"
+    , ""
+    , "  // Assertions."
+    , "  GreaterThanOrEqualTo0: assert(counter >= 0);    // The 'counter' must always be greater than or equal to 0."
+    , "  LessThan10:            assert(counter < 10);    // The 'counter' must always be less than 10."
+    , ""
+    , "  // Implementation 1."
+    , "  if (counter == 10)"
+    , "    counter = 0;"
+    , "  else"
+    , "    counter++;"
+    , ""
+    , "  // Implementation 2."
+    , "  // if (counter == 9)"
+    , "  //   counter = 0;"
+    , "  // else"
+    , "  //   counter = counter + 1;"
+    , ""
+    , "  // Implementation 3."
+    , "  // if (counter >= 9)"
+    , "  //   counter = 0;"
+    , "  // else"
+    , "  //   counter++;"
+    , ""
+    , "  // Implementation 4."
+    , "  // if (counter >= 9 || counter < 0)"
+    , "  //   counter = 0;"
+    , "  // else"
+    , "  //   counter++;"
+    , ""
+    , "  // Implementation 5."
+    , "  // counter = (counter + 1) % 10;"
+    , ""
+    , "}"
+    , ""
+    ]
+
+
+
+help :: IO ()
+help = putStrLn $ unlines
+  [ ""
+  , "NAME"
+  , "  afv - Atom's Formal Verifier"
+  , ""
+  , "SYNOPSIS"
+  , "  afv verify function-name [-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."
+  , "  Requires GCC for C preprocessing and the Yices SMT solver."
+  , ""
+  , "COMMANDS"
+  , "  verify function-name [options] c-files ..."
+  , "    Runs verification on the specified periodic function."
+  , ""
+  , "    -k n          : Max k-induction depth."
+  , "    --yices=path  : Path to Yices solver."
+  , "    --gcc=path    : Path to GCC."
+  , "    -Idir         : Add directory to includes search path."
+  , "    -Dmacro       : Define a macro."
+  , "    -Dmacro=def   : Define a macro with a value."
+  , ""
+  , "  header"
+  , "    Writes AFV's header file (afv.h), which provides the 'assert' and 'assume' functions."
+  , ""
+  , "  example"
+  , "    Writes an example design (example.c).  Verify with:"
+  , "      afv verify example -k 15 example.c"
+  , ""
+  ]
diff --git a/src/Compile.hs b/src/Compile.hs
new file mode 100644
--- /dev/null
+++ b/src/Compile.hs
@@ -0,0 +1,457 @@
+module Compile (compile) where
+
+import Control.Monad.State hiding (State)
+import Data.List
+import Language.C
+import Language.C.Data.Ident
+
+import Error
+import Model hiding (CInteger)
+import qualified Model as M
+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) }
+
+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 then notSupported (head asms) "inline assembly" else CCompound [] (vars ++ funcs ++ [CBlockStmt call]) none
+  where
+  items = [ a | CTranslUnit items _ <- units, a <- items ]
+  vars  = [ CBlockDecl (CDecl (CStorageSpec (CStatic none) : specs) a b) | CDeclExt (CDecl specs a b) <- items ]  -- Make top level vars static.
+  funcs = map CNestedFunDef $ sortFunctions [ a | CFDefExt a <- items ]
+  asms  = [ a | CAsmExt  a <- items ]
+  call :: CStat
+  call = CExpr (Just $ CCall (CVar (Ident name 0 none) none) [] none) none
+  -- XXX Need to check for top level name conflicts.
+
+type M = StateT MDB IO
+
+data MDB = MDB
+  { nextId  :: Int
+  , stack   :: [Ident]
+  , enabled :: E
+  , model   :: Model
+  }
+
+initMDB :: MDB
+initMDB = MDB
+  { nextId  = 0
+  , stack   = []
+  , enabled = true
+  , model   = Model { variables = [], actions = [] }
+  }
+
+
+
+-- | Environment for resolving identifiers.
+data Env = Env
+  { values  :: [Value]
+  }
+
+data Value
+  = EnvFunction String Function
+  | EnvVariable String V
+
+data Function = Function Int ([E] -> M E)
+
+-- | 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 ]
+
+-- | 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 ]
+
+-- | Creates a branch.
+branch :: Position -> E -> M a -> M a -> M (a, a)
+branch n a onTrue onFalse = do
+  m1 <- get
+  put m1 { enabled = And (enabled m1) a n }
+  r1 <- onTrue
+  m2 <- get
+  put m2 { enabled = And (enabled m1) (Not a n) n }
+  r2 <- onFalse
+  m3 <- get
+  put m3 { enabled = enabled m1 }
+  return (r1, r2)
+
+-- | Push an identifier onto the call stack, do something, then pop it off.
+callStack :: Ident -> M a -> M a
+callStack id a = do
+  m <- get
+  put m { stack = id : stack m }
+  a <- a
+  m <- get
+  put m { stack = tail $ stack m }
+  return a
+
+callPath :: M ([String], Position)
+callPath = do
+  m <- get
+  let s = stack m
+  return ([ n | Ident n _ _ <- reverse s ], posOf $ head s)
+
+-- | The initial environment defines the assert and assume functions.
+initEnv :: Env
+initEnv = Env
+  { values =
+    [ EnvFunction "assert" $ Function 1 assert
+    , EnvFunction "assume" $ Function 1 assume
+    ]
+  }
+  where
+  assert a = do
+    (s, n) <- callPath
+    m <- get
+    let x = imply (enabled m) (head a) n
+    newAction $ Assert x s n
+    return x
+  assume a = do
+    (s, n) <- callPath
+    m <- get
+    let x = imply (enabled m) (head a) n
+    newAction $ Assume x s n
+    return x
+
+-- | Adds new action.
+newAction :: Action -> M ()
+newAction a = do
+  m <- get
+  put m { model = (model m) { actions = a : actions (model m) }}
+
+-- | 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 }
+  where
+  name = case a of
+    State (VS a _ _ _)  -> a
+    Volatile a _ _   -> a
+    Local    a _ _ _ -> a
+    Tmp      _ _ _   -> error "Compile.addVar: should not call addVar with Tmp"
+
+
+
+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
+    branch (posOf n) a (evalStat env b) (evalStat env c)
+    return ()
+  _ -> 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
+evalExpr env a = latch (posOf 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'
+        _ -> 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
+    (b, c) <- branch (posOf n) a (evalExpr env b) (evalExpr env c)
+    return $ Mux 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)
+    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
+    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
+    CAndOp -> f And
+    CXorOp -> f $ \ a b n -> Or (And a (Not b n) n) (And (Not a n) b n) n
+    COrOp  -> f Or
+    CLndOp -> do
+      a <- evalExpr env a
+      (b, a) <- branch n' a (evalExpr env b) (return a)
+      return $ Mux a b a n'
+    CLorOp -> do
+      a <- evalExpr env a
+      (a, b) <- branch n' a (return a) (evalExpr env b)
+      return $ Mux a a b n'
+    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'
+
+  CUnary op a n -> do
+    a <- evalExpr env a
+    case (op, a) of
+      (CPreIncOp, Var a) -> do
+        assign False p a $ Add (Var a) one p
+        return $ Var a
+      (CPreDecOp, Var a) -> do
+        assign False 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
+      (CPostDecOp, Var a) -> do
+        b <- latch p $ Var a
+        assign False p a $ Sub (Var a) one p
+        return b
+      (CPlusOp, a) -> return $ Add zero a p
+      (CMinOp,  a) -> return $ Sub zero a p
+      (CNegOp,  a) -> return $ Not a p
+      _ -> notSupported n "unary operator"
+    where
+    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
+  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
+    _ -> notSupported a "char or string constant"
+  _ -> notSupported a "expression"
+    
+evalDecl :: Env -> CDecl -> M Env
+evalDecl env d@(CDecl specs decls _) = if isExtern typInfo then return env else foldM evalDecl' env decls
+  where
+  (typInfo, typ) = typeInfo specs
+  evalDecl' :: Env -> (Maybe CDeclr, Maybe CInit, Maybe CExpr) -> M Env
+  evalDecl' env (a, b, c) = case a of
+    Just (CDeclr (Just i@(Ident name _ n)) [] Nothing [] _) -> case (b, c) of
+      (Nothing, Nothing) -> evalDecl' env (a, Just $ CInitExpr (CConst (CIntConst (cInteger 0) n)) n, Nothing)
+      (Just (CInitExpr c@(CConst const) n'), Nothing) | isStatic typInfo && not (isVolatile typInfo) -> addVar env v
+                                                      | otherwise -> evalDecl' env (a, Nothing, Just c)
+        where
+        v = State $ VS name typ init $ posOf n
+        init = case typ of
+          Void -> unexpected d "void type for variable declaration"
+          Bool -> CBool (cInt /= 0) $ posOf n'
+          Integer _  -> M.CInteger cInt $ posOf n'
+          Rational _ -> CRational cRat $ posOf n'
+
+        cInt :: Integer
+        cInt = case const of
+          CIntConst (CInteger a _ _) _ -> a
+          _ -> unexpected const "non integer initialization"
+
+        cRat :: Rational
+        cRat = case const of
+          CIntConst (CInteger a _ _) _ -> fromIntegral a
+          CFloatConst (CFloat a) _     -> fromIntegral (read a :: Integer)
+          _ -> unexpected const "non numeric initialization"
+
+      (Nothing, Just e') -> do
+        e <- evalExpr env e'
+        v <- if isVolatile typInfo
+          then return $ Volatile name typ $ posOf n
+          else do
+            m <- get
+            put m { nextId = nextId m + 1 }
+            return $ Local name typ (nextId m) (posOf e')
+        assign True (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?)"
+      
+
+evalFunc :: Env -> CFunDef -> M Env
+evalFunc env f =  do
+  when (typ /= Void || not (null args)) $ notSupported f "non void f(void) function (How lame is this?)"
+  return env { values = EnvFunction name (Function (length args) func) : values env }
+  where
+  (specs, (Ident name _ _), args, stat) = functionInfo f
+  (_, typ) = typeInfo specs
+  func _ = do --XXX
+    evalStat env stat
+    return false
+
+
+
+
+
+
+-- | Assgins a value to a variable.
+assign :: Bool -> Position -> V -> E -> M ()
+assign decl 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?
+
+-- | 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 n a = do
+  m <- get
+  let v = Tmp (typeOf a) (nextId m) n
+  put m { nextId = nextId m + 1 }
+  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
+
+
+
+
+
+
+-- | Extract relavent info from a function declaration.
+functionInfo :: CFunDef -> ([CDeclSpec], Ident, [CDecl], CStat)
+functionInfo (CFunDef specs (CDeclr (Just ident) [(CFunDeclr (Right (args, False)) _ _)] Nothing [] _) [] stmt _) = (specs, ident, args, stmt)
+functionInfo f = notSupported f "function"
+
+
+
+
+-- | Topologically sorts functions based on dependencies.
+sortFunctions :: [CFunDef] -> [CFunDef]
+sortFunctions fs = case topo $ map functionDeps fs of
+  Left a -> notSupported none $ "recursive functions somewhere among: " ++ show a
+  Right a -> [ f | a <- a, f <- fs, functionName f == a ]
+
+topo :: Eq a => [(a, [a])] -> Either [a] [a]
+topo a = topo' [] a
+  where
+  topo' a [] = Right a
+  topo' done waiting = if null next then Left $ fst $ unzip waiting else topo' (done ++ next) stillWaiting
+    where
+    next = [ a | (a, deps) <- waiting, all (flip elem done) deps ]
+    stillWaiting = [ (a, deps) | (a, deps) <- waiting, notElem a next ]
+
+
+functionName :: CFunDef -> String
+functionName f = name where (_, Ident name _ _, _, _) = functionInfo f
+
+afvFunctionNames :: [String]
+afvFunctionNames = ["assert", "assume"]
+
+-- | Analyzes a function for dependencies.
+functionDeps :: CFunDef -> (String, [String])
+functionDeps f = (functionName f, filter (flip notElem afvFunctionNames) $ nub $ fb [] [CNestedFunDef f])
+  where
+  rewrite :: CFunDef -> CStat
+  rewrite f = CCompound [] (map CBlockDecl args ++ [CBlockStmt stat]) none where (_, _, args, stat) = functionInfo f
+  fs :: [String] -> CStat -> [String]
+  fs env a = case a of
+    CLabel _ a _ _ -> fs env a
+    CCase a b _ -> fe env a ++ fs env b
+    CCases a b c _ -> fe env a ++ fe env b ++ fs env c
+    CDefault a _ -> fs env a
+    CExpr (Just a ) _ -> fe env a
+    CExpr Nothing _ -> []
+    CCompound _ a _ -> fb env a
+    CIf a b Nothing _ -> fe env a ++ fs env b
+    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 _ _ _ _ _ -> notSupported a "for loops"
+    CGoto _ _ -> []
+    CGotoPtr a _ -> fe env a
+    CCont _ -> []
+    CBreak _ -> []
+    CReturn Nothing _ -> []
+    CReturn (Just a) _ -> fe env a
+    CAsm _ _ -> []
+  fe :: [String] -> CExpr -> [String]
+  fe env a = case a of
+    CComma a _ -> fe' a
+    CAssign _ a b _ -> fe' [a, b]
+    CCond a (Just b) c _ ->  fe' [a, b, c]
+    CCond a Nothing b _ ->  fe' [a, b]
+    CBinary _ a b _ -> fe' [a, b]
+    CCast _ a _ -> fe env a --XXX does not check cast declaration.
+    CUnary _ a _ -> fe env a
+    --CSizeofExpr CExpr NodeInfo
+    --CSizeofType CDecl NodeInfo
+    --CAlignofExpr CExpr NodeInfo
+    --CAlignofType CDecl NodeInfo
+    --CComplexReal CExpr NodeInfo
+    --CComplexImag CExpr NodeInfo
+    CIndex a b _ -> fe' [a, b]
+    CCall (CVar (Ident n _ _) _) args _ -> (if elem n env then [] else [n]) ++ fe' args
+    CCall _ _ _ -> notSupported a "non-named function references"
+    CMember a _ _ _ -> fe env a
+    CVar _ _ -> []
+    CConst _ -> []
+    --CCompoundLit CDecl CInitList NodeInfo
+    CStatExpr a _ -> fs env a
+    CLabAddrExpr _ _ -> []
+    --CBuiltinExpr CBuiltin
+    _ -> notSupported a "expression"
+    where
+    fe' = concatMap $ fe env
+  fb :: [String] -> [CBlockItem] -> [String]
+  fb _ [] = []
+  fb env (a:b) = case a of
+    CBlockStmt a -> fs env a ++ fb env b
+    CBlockDecl _ -> fb env b
+    CNestedFunDef f -> fs env' (rewrite f) ++ fb env' b where env' = functionName f : env
+
diff --git a/src/Error.hs b/src/Error.hs
new file mode 100644
--- /dev/null
+++ b/src/Error.hs
@@ -0,0 +1,27 @@
+module Error
+  ( err
+  , notSupported
+  , unexpected
+  , debug
+  , debug'
+  ) where
+
+import Language.C
+import System.IO.Unsafe
+
+err :: Pos a => a -> String -> b
+err a m = error $ format (posOf a) ++ ": " ++ m
+  where
+  format (Position name line col) = name ++ ":" ++ show line ++ ":" ++ show col
+
+notSupported :: Pos a => a -> String -> b
+notSupported a m = err a $ " not supported: " ++ m
+
+unexpected :: Pos a => a -> String -> b
+unexpected a m = err a $ "unexpected: " ++ m
+
+debug :: Show a => String -> a -> a
+debug m a = debug' m a a
+
+debug' :: Show a => String -> a -> b -> b
+debug' m a b = unsafePerformIO (putStrLn (m ++ ": " ++ show a) >> return b)
diff --git a/src/Model.hs b/src/Model.hs
new file mode 100644
--- /dev/null
+++ b/src/Model.hs
@@ -0,0 +1,202 @@
+module Model
+  ( Type        (..)
+  , IntegerType (..)
+  , TypeOf      (..)
+  , Const       (..)
+  , VS          (..)
+  , V           (..)
+  , E           (..)
+  , Action      (..)
+  , Model       (..)
+  , true
+  , false
+  , isRational
+  , isInteger
+  , unify
+  ) where
+
+import Language.C.Data.Position
+
+import Error
+
+data IntegerType = U8 | U16 | U32 | U64 | S8 | S16 | S32 | S64 deriving (Show, Eq)
+
+data Type
+  = Void
+  | Bool
+  | Integer  (Maybe IntegerType)
+  | Rational (Maybe Bool)          -- isDouble
+  deriving Eq
+
+isInteger :: Type -> Bool
+isInteger (Integer _) = True
+isInteger _ = False
+
+isRational :: Type -> Bool
+isRational (Rational _) = True
+isRational _ = False
+
+instance Show Type where
+  show a = case a of
+    Void -> "void"
+    Bool -> "bool"
+    Integer Nothing -> "unspecified integer type"
+    Integer (Just a) -> case a of
+      U8  -> "unsigned char"
+      U16 -> "unsigned short"
+      U32 -> "unsigned long"
+      U64 -> "unsigned long long"
+      S8  -> "signed char"
+      S16 -> "signed short"
+      S32 -> "signed long"
+      S64 -> "signed long long"
+    Rational Nothing -> "unspecified floating type"
+    Rational (Just True)  -> "double"
+    Rational (Just False) -> "float"
+
+class TypeOf a where typeOf :: a -> Type
+
+instance TypeOf Type where typeOf = id
+
+data Const
+  = CBool Bool Position
+  | CInteger Integer Position
+  | CRational Rational Position
+  deriving (Show, Eq)
+
+instance TypeOf Const where
+  typeOf a = case a of
+    CBool _ _     -> Bool
+    CInteger  _ _ -> Integer Nothing
+    CRational _ _ -> Rational Nothing
+
+instance Pos Const where
+  posOf a = case a of
+    CBool     _ a -> a
+    CInteger  _ a -> a
+    CRational _ a -> a
+
+-- | User defined state variable (non-volatile top level variables or non-volatile static variables in functions).
+data VS = VS String Type Const Position deriving (Show, Eq)
+
+instance TypeOf VS where typeOf (VS _ t _ _) = t
+instance Pos VS where posOf (VS _ _ _ n) = n
+
+-- | Variables.
+data V
+  = State VS
+  | Volatile String Type       Position
+  | Local    String Type Int   Position
+  | Tmp             Type Int   Position
+  deriving (Show, Eq)
+     
+instance TypeOf V where
+  typeOf a = case a of
+    State a -> typeOf a
+    Volatile _ a _   -> a
+    Local    _ a _ _ -> a
+    Tmp      a _ _   -> a
+
+instance Pos V where
+  posOf a = case a of
+    State a -> posOf a
+    Volatile _ _ n -> n
+    Local _ _ _ n -> n
+    Tmp _ _ n -> n
+
+{-
+instance Pos V where
+  posOf a = case a of
+    V        _ _ a   -> a
+    Volatile _ _ a   -> a
+    Local    _ _ a _ -> a
+-}   
+
+-- | Expressions.
+data E
+  = Var V
+  | Const Const
+  | Not E Position
+  | And E E Position
+  | Or  E E Position
+  | Mul E E Position
+  | Div E E Position
+  | Mod E E Position
+  | Add E E Position
+  | Sub E E Position
+  | Lt  E E Position
+  | Eq  E E Position
+  | Mux E E E Position
+  deriving (Show, Eq)
+
+instance Pos E where
+  posOf a = case a of
+    Var a -> posOf a
+    Const a -> posOf a
+    Not _ a -> a
+    And _ _ a -> a
+    Or  _ _ a -> a
+    Mul _ _ a -> a
+    Div _ _ a -> a
+    Mod _ _ a -> a
+    Add _ _ a -> a
+    Sub _ _ a -> a
+    Lt  _ _ a -> a
+    Eq  _ _ a -> a
+    Mux _ _ _ a -> a
+
+instance TypeOf E where
+  typeOf a = case a of
+    Var a       -> typeOf a
+    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)
+    Mul a b _   -> unify' (typeOf a) (typeOf b)
+    Div a b _   -> unify' (typeOf a) (typeOf b)
+    Mod a b _   -> unify' (typeOf a) (typeOf b)
+    Add a b _   -> unify' (typeOf a) (typeOf b)
+    Sub a b _   -> unify' (typeOf a) (typeOf b)
+    Lt  a b _   -> seq (unify' (typeOf a) (typeOf b)) Bool
+    Eq  a b _   -> seq (unify' (typeOf a) (typeOf b)) Bool
+    Mux a b c _ -> seq (unify' (typeOf b) (typeOf c)) $ unify' Bool (typeOf a)
+    where
+    unify' = unify a
+
+unify :: Pos a => a -> Type -> Type -> Type
+unify n a b = case (a, b) of
+  (a, b) | a == b -> a
+
+  (Bool, Integer Nothing) -> Bool
+  (Integer Nothing, Bool) -> Bool
+
+  (Integer Nothing, a@(Integer _)) -> a
+  (a@(Integer _), Integer Nothing) -> a
+
+  (Integer Nothing, a@(Rational _)) -> a
+  (a@(Rational _), Integer Nothing) -> a
+
+  (Rational Nothing, a@(Rational _)) -> a
+  (a@(Rational _), Rational Nothing) -> a
+
+  (a, b) -> unexpected n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b
+
+true :: E
+true = Const $ CBool True nopos
+
+false :: E
+false = Const $ CBool False nopos
+
+instance Pos Position where posOf = id
+
+data Action
+  = Assign V E
+  | Assert E [String] Position
+  | Assume E [String] Position
+  deriving (Show, Eq)
+
+data Model = Model
+  { variables :: [VS]
+  , actions   :: [Action]
+  } deriving Show
+
diff --git a/src/Parse.hs b/src/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Parse.hs
@@ -0,0 +1,28 @@
+module Parse (parse) where
+
+import Language.C
+import Language.C.System.GCC
+import Language.C.System.Preprocess
+import System.Exit
+import System.IO
+
+parse :: FilePath -> [FilePath] -> [(String,String)] -> FilePath -> IO CTranslUnit
+parse gcc includes defines file = do
+  a <- preprocess gcc includes defines file
+  case parseC a (initPos file) of
+    Left e  -> putStrLn ("parsing error: " ++ show e) >> exitFailure
+    Right a -> return a
+
+preprocess :: FilePath -> [FilePath] -> [(String,String)] -> FilePath -> IO InputStream
+preprocess gcc includes defines file = do
+  a <- runPreprocessor (newGCC gcc) CppArgs
+    { cppOptions = map IncludeDir includes ++ map (\ (a,b) -> Define a b) defines
+    , extraOptions = []
+    , cppTmpDir = Nothing
+    , inputFile = file
+    , outputFile = Nothing
+    }
+  case a of
+    Left e  -> putStrLn "preprocessing error" >> exitWith e
+    Right a -> return a
+    
diff --git a/src/Utils.hs b/src/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Utils.hs
@@ -0,0 +1,85 @@
+module Utils
+  ( TypeInfo (..)
+  , typeInfo
+  , isVisable
+  ) where
+
+import Data.List
+import Language.C
+
+import Error
+import Model
+
+data TypeInfo = TypeInfo
+  { isConst
+  , isVolatile
+  , isStatic
+  , isExtern    :: Bool
+  }
+
+isVisable :: TypeInfo -> Bool
+isVisable t = not (isStatic t) && not (isExtern t)
+
+typeInfo :: [CDeclSpec] -> (TypeInfo, Type)
+typeInfo specs = (info, typ)
+  where
+  info = foldl f TypeInfo { isConst = False, isVolatile = False, isStatic = False, isExtern = False } specs
+  f :: TypeInfo -> CDeclSpec -> TypeInfo
+  f t a = case a of
+    CStorageSpec a -> case a of
+      CStatic _ -> t { isStatic = True }
+      CExtern _ -> t { isExtern = True }
+      _         -> notSupported a "storage class"
+    CTypeQual a -> case a of
+      CConstQual _ -> t { isConst    = True }
+      CVolatQual _ -> t { isVolatile = True }
+      _         -> notSupported a "type qualifier"
+    CTypeSpec _ -> t
+  voids    = [ a | CTypeSpec a@(CVoidType _) <- specs ]
+  signed   = [ a | CTypeSpec a@(CSignedType _) <- specs ]
+  unsigned = [ a | CTypeSpec a@(CUnsigType  _) <- specs ]
+  bools    = [ a | CTypeSpec a@(CBoolType _) <- specs ]
+  chars    = [ a | CTypeSpec a@(CCharType _) <- specs ]
+  shorts   = [ a | CTypeSpec a@(CShortType _) <- specs ]
+  longs    = [ a | CTypeSpec a@(CLongType _) <- specs ]
+  ints     = [ a | CTypeSpec a@(CIntType _) <- specs ]
+  floats   = [ a | CTypeSpec a@(CFloatType _) <- specs ]
+  doubles  = [ a | CTypeSpec a@(CDoubleType _) <- specs ]
+  typ = case (length voids, length signed, length unsigned, length bools, length chars, length shorts, length longs, length ints, length floats, length doubles) of
+    (1, 0, 0, 0, 0, 0, 0, 0, 0, 0) -> Void
+
+    (0, 0, 0, 1, 0, 0, 0, 0, 0, 0) -> Bool
+
+    (0, 0, 0, 0, 1, 0, 0, 0, 0, 0) -> Integer $ Just S8
+    (0, 1, 0, 0, 1, 0, 0, 0, 0, 0) -> Integer $ Just S8
+    (0, 0, 1, 0, 1, 0, 0, 0, 0, 0) -> Integer $ Just U8
+
+    (0, 0, 0, 0, 0, 1, 0, 0, 0, 0) -> Integer $ Just S16
+    (0, 1, 0, 0, 0, 1, 0, 0, 0, 0) -> Integer $ Just S16
+    (0, 0, 1, 0, 0, 1, 0, 0, 0, 0) -> Integer $ Just U16
+    (0, 0, 0, 0, 0, 1, 0, 1, 0, 0) -> Integer $ Just S16
+    (0, 1, 0, 0, 0, 1, 0, 1, 0, 0) -> Integer $ Just S16
+    (0, 0, 1, 0, 0, 1, 0, 1, 0, 0) -> Integer $ Just U16
+
+    (0, 0, 0, 0, 0, 0, 0, 1, 0, 0) -> Integer $ Just S32
+    (0, 1, 0, 0, 0, 0, 0, 1, 0, 0) -> Integer $ Just S32
+    (0, 0, 1, 0, 0, 0, 0, 1, 0, 0) -> Integer $ Just U32
+    (0, 0, 0, 0, 0, 0, 1, 0, 0, 0) -> Integer $ Just S32
+    (0, 1, 0, 0, 0, 0, 1, 0, 0, 0) -> Integer $ Just S32
+    (0, 0, 1, 0, 0, 0, 1, 0, 0, 0) -> Integer $ Just U32
+    (0, 0, 0, 0, 0, 0, 1, 1, 0, 0) -> Integer $ Just S32
+    (0, 1, 0, 0, 0, 0, 1, 1, 0, 0) -> Integer $ Just S32
+    (0, 0, 1, 0, 0, 0, 1, 1, 0, 0) -> Integer $ Just U32
+
+    (0, 0, 0, 0, 0, 0, 2, 0, 0, 0) -> Integer $ Just S64
+    (0, 1, 0, 0, 0, 0, 2, 0, 0, 0) -> Integer $ Just S64
+    (0, 0, 1, 0, 0, 0, 2, 0, 0, 0) -> Integer $ Just U64
+    (0, 0, 0, 0, 0, 0, 2, 1, 0, 0) -> Integer $ Just S64
+    (0, 1, 0, 0, 0, 0, 2, 1, 0, 0) -> Integer $ Just S64
+    (0, 0, 1, 0, 0, 0, 2, 1, 0, 0) -> Integer $ Just U64
+
+    (0, 0, 0, 0, 0, 0, 0, 0, 1, 0) -> Rational $ Just False
+    (0, 0, 0, 0, 0, 0, 0, 0, 0, 1) -> Rational $ Just True
+
+    a -> notSupported (head specs) $ "type signature: " ++ show a
+
diff --git a/src/Verify.hs b/src/Verify.hs
new file mode 100644
--- /dev/null
+++ b/src/Verify.hs
@@ -0,0 +1,259 @@
+module Verify (verify) where
+
+import Control.Monad
+import Data.IORef
+import Data.List
+import Data.Maybe
+import Math.SMT.Yices.Pipe
+import Math.SMT.Yices.Syntax
+import System.IO
+import Text.Printf
+
+import Model
+
+-- | 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
+  y <- createYicesPipe yices []
+  mapM_ (verifyModel y maxK) models
+  exitY y
+  where
+  assertions = [ a | a@(Assert _ _ _) <- actions m ]
+  models = map (trimModel . trimAssertions m) assertions
+
+-- | 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
+
+-- | Trim all unneeded stuff from a model.
+trimModel :: Model -> Model
+trimModel = id  --XXX
+
+-- | Verify a trimmed model.
+verifyModel :: YicesIPC -> Int -> Model -> IO ()
+verifyModel y maxK m = do
+  printf "verifying assertion %s ...\n" (intercalate "." path) >> hFlush stdout
+  withLogic y $ do
+    initEnv <- initEnv y m
+    check initEnv initEnv [] 1
+  where
+  [path] = [ path | Assert _ path _ <- actions m ]
+  check :: Env -> Env -> [ExpY] -> Int -> IO ()
+  check _ _ _ k | k > maxK = printf "inconclusive: unable to proved step up to max k = %d\n" maxK
+  check initEnv env asserts k = do
+    (env, assert) <- transition y m env
+    resultBasis <- checkBasis y m initEnv (assert : asserts)
+    case resultBasis of
+      Fail -> printf "FAILED: disproved basis in k = %d\n" k
+      Pass -> do
+        resultStep <- checkStep y assert
+        case resultStep of
+          Fail -> withLogic y $ check initEnv env (assert : asserts) (k + 1)
+          Pass -> printf "passed: proved step in k = %d\n" k
+        
+data Result = Pass | Fail
+
+-- | Check induction step.
+checkStep :: YicesIPC -> ExpY -> IO Result
+checkStep y assert = do
+  r <- withLogic y $ do
+    runCmds y [ASSERT $ NOT assert]
+    checkLogic y
+  return $ result r
+
+-- | Check induction basis.
+checkBasis :: YicesIPC -> Model -> Env -> [ExpY] -> IO Result
+checkBasis y m env asserts = do
+  r <- withLogic y $ do
+    runCmds y [ ASSERT $ VarE (getVar env (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ]
+    runCmds y [ASSERT $ NOT $ AND asserts]
+    checkLogic y
+  return $ result r
+
+result :: ResY -> Result
+result a = case a of
+  Sat _   -> Fail
+  UnSat _ -> Pass
+  InCon _ -> Pass
+
+-- | Does operation in a new stack.
+withLogic :: YicesIPC -> IO a -> IO a
+withLogic y a = do
+  runCmds y [PUSH]
+  a <- a
+  runCmds y [POP]
+  return a
+
+-- | Transition relation.  Returns assertion.
+transition :: YicesIPC -> Model -> Env -> IO (Env, ExpY)  -- (new env, assertion)
+transition y m env = do
+  (env', assert) <- foldM (action y) (env, LitB True) (actions m)
+  --runCmds y [ ASSERT (VarE (getVar env $ State a) := VarE (getVar env' $ State a)) | a <- variables m ]
+  return (env', assert)
+
+action :: YicesIPC -> (Env, ExpY) -> Action -> IO (Env, ExpY)
+action y (env, assert) a = case a of
+  Assign v e -> do
+    e <- expr y env (typeOf v) e
+    env <- addVar y env v
+    runCmds y [ASSERT $ VarE (getVar env v) := e]
+    return (env, assert)
+  Assert a _ _ -> do
+    a <- expr y env Bool a
+    return (env, AND [assert, a])
+  Assume a _ _ -> do
+    a <- expr y env Bool a
+    runCmds y [ASSERT a]
+    return (env, assert)
+
+expr :: YicesIPC -> Env -> Type -> E -> IO ExpY
+expr y env t a = case a of
+  Var a@(Volatile _ _ _) -> do
+    env <- addVar y env a
+    return $ VarE $ getVar env a
+  Var a -> return $ VarE $ getVar env a
+
+  Const a -> return $ exprConst t a
+
+  Not a _ -> do
+    a <- expr y env Bool a
+    return $ NOT a
+
+  And a b _ -> do
+    a <- expr y env Bool a
+    b <- expr y env Bool b
+    return $ AND [a, b]
+
+  Or  a b _ -> do
+    a <- expr y env Bool a
+    b <- expr y env Bool b
+    return $ OR  [a, b]
+
+  Mul a b _ -> do
+    a <- expr y env t a
+    b <- expr y env t b
+    return $ a :*: b
+  
+  Div a b _  -> do
+    a <- expr y env t a
+    b <- expr y env t b
+    return $ op a b
+    where
+    op = case t of
+      Integer _ -> DIV
+      _         -> (:/:)
+
+  Mod a b _ -> do
+    a <- expr y env t a
+    b <- expr y env t b
+    return $ MOD a b
+
+  Add a b _ -> do
+    a <- expr y env t a
+    b <- expr y env t b
+    return $ a :+: b
+
+  Sub a b _ -> do
+    a <- expr y env t a
+    b <- expr y env t b
+    return $ a :-: b
+
+  Lt  a b n -> do
+    let t' = unify n (typeOf a) (typeOf b)
+    a <- expr y env t' a
+    b <- expr y env t' b
+    return $ a :< b
+
+  Eq  a b n -> do
+    let t' = unify n (typeOf a) (typeOf b)
+    a <- expr y env t' a
+    b <- expr y env t' b
+    return $ a := b
+
+  Mux a b c n -> do
+    let t' = unify n (typeOf b) (typeOf c)
+    a <- expr y env Bool a
+    b <- expr y env t' b
+    c <- expr y env t' c
+    return $ IF a b c
+
+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
+
+
+
+
+data Env = Env NextId [(V, String)]  -- Env nextId table
+
+initEnv :: YicesIPC -> Model -> IO Env
+initEnv y m = do
+  nid <- newNextId
+  foldM (addVar y) (Env nid []) $ map State $ variables m
+
+addVar :: YicesIPC -> Env -> V -> IO Env
+addVar y (Env nid table) v = do
+  i <- nextId nid
+  let name = printf "n%d" i
+  runCmds y [DEFINE (name, VarT $ typeY v) Nothing]
+  return $ Env nid $ replace (v, name) table
+
+getVar :: Env -> V -> String
+getVar (Env _ table) v = case lookup v table of
+  Just a -> a
+  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (fst $ unzip table)
+
+replace :: Eq a => (a, b) -> [(a, b)] -> [(a, b)]
+replace a [] = [a]
+replace (a, b) ((a', b') : c) | a == a'   = (a, b) : c
+                              | otherwise = (a', b') : replace (a, b) c
+
+
+
+
+
+
+typeY :: TypeOf a => a -> String
+typeY a = case typeOf a of
+  Void       -> error "Verify.typeY: void time"
+  Bool       -> "bool"
+  Integer  _ -> "int"
+  Rational _ -> "real"
+
+
+
+newtype NextId = NextId (IORef Int)
+
+newNextId :: IO NextId
+newNextId = newIORef 0 >>= (return . NextId)
+
+nextId :: NextId -> IO Int
+nextId (NextId a) = do
+  i <- readIORef a
+  writeIORef a $ i + 1
+  return i
+
+
+verbose :: Bool
+verbose = False
+
+runCmds :: YicesIPC -> [CmdY] -> IO ()
+runCmds y cmds = do
+  when verbose $ mapM_ (putStrLn . show) cmds
+  runCmdsY' y cmds
+
+checkLogic :: YicesIPC -> IO ResY
+checkLogic y = do
+  when verbose $ do
+    putStrLn "(check)"
+    hFlush stdout
+  checkY y
+
+