diff --git a/RELEASE-NOTES b/RELEASE-NOTES
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -2,3 +2,9 @@
 
 - Initial release.
 
+afv 0.0.1    01/14/10
+
+- Checks for duplicate top-level names.
+- Uses yices new 'quickCheckY'.
+- Fixed bug affecting 'assume'.
+
diff --git a/afv.cabal b/afv.cabal
--- a/afv.cabal
+++ b/afv.cabal
@@ -1,5 +1,5 @@
 name:    afv
-version: 0.0.0
+version: 0.0.1
 
 category: Formal Methods
 
@@ -37,12 +37,12 @@
 
   build-depends:
     base          >= 4       && < 5,
-    bytestring    >= 0.9.1   && < 0.9.2,
+    bytestring    >= 0.9     && < 1.0,
     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
+    language-c    >= 0.3.1.1,
+    yices         >= 0.0.0.6
 
   ghc-options:  -W
   extensions:
diff --git a/src/AFV.hs b/src/AFV.hs
--- a/src/AFV.hs
+++ b/src/AFV.hs
@@ -8,12 +8,15 @@
 import Parse
 import Verify
 
+version = "0.0.1"
+
 main :: IO ()
 main = do
   args <- getArgs
   case args of
     [] -> help
     (a:_) | elem a ["help", "-h", "--help", "-help"] -> help
+          | elem a ["version", "-v", "--version"] -> putStrLn $ "afv " ++ version
     ["example"] -> example
     ["header"]  -> header
     ("verify":function:args) -> do
@@ -23,6 +26,7 @@
       verify (yices a) (k a) model
     _ -> help
 
+
 data Args = Args
   { yices    :: FilePath
   , k        :: Int
@@ -119,6 +123,9 @@
   [ ""
   , "NAME"
   , "  afv - Atom's Formal Verifier"
+  , ""
+  , "VERSION"
+  , "  " ++ version
   , ""
   , "SYNOPSIS"
   , "  afv verify function-name [-k max-k] [--yices=path-to-yices] [--gcc=path-to-gcc] {-Idir} {-Dmacro[=def]} c-file {c-file}"
diff --git a/src/Compile.hs b/src/Compile.hs
--- a/src/Compile.hs
+++ b/src/Compile.hs
@@ -21,16 +21,27 @@
 
 -- | 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
+rewrite name units = if not $ null asms
+  then notSupported (head asms) "inline assembly"
+  else if not $ null duplicateNames
+    then error $ "duplicate top-level names found (hiding names with static is not supported): " ++ show duplicateNames
+    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 ]
+  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
   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.
+  duplicateNames = duplicates $ [ name | f <- funcDefs, let (_, (Ident name _ _), _, _) = functionInfo f ] ++ concat [ [ name | (Just (CDeclr (Just (Ident name _ _)) _ _ _ _), _, _) <- a ] | CDecl _ a _ <- varDefs ]
 
+duplicates :: Eq a => [a] -> [a]
+duplicates [] = []
+duplicates (a:b) | elem a b  = a : duplicates b
+                 | otherwise =     duplicates b
+
 type M = StateT MDB IO
 
 data MDB = MDB
@@ -215,9 +226,9 @@
     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
+    CAndOp -> notSupported a "(&)"
+    CXorOp -> notSupported a "(^)"
+    COrOp  -> notSupported a "(|)"
     CLndOp -> do
       a <- evalExpr env a
       (b, a) <- branch n' a (evalExpr env b) (return a)
@@ -251,7 +262,7 @@
         b <- latch p $ Var a
         assign False p a $ Sub (Var a) one p
         return b
-      (CPlusOp, a) -> return $ Add zero a p
+      (CPlusOp, a) -> return a
       (CMinOp,  a) -> return $ Sub zero a p
       (CNegOp,  a) -> return $ Not a p
       _ -> notSupported n "unary operator"
@@ -284,8 +295,7 @@
   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)
+      (Just (CInitExpr (CConst const) n'), Nothing) | isStatic typInfo && not (isVolatile typInfo) -> addVar env v
         where
         v = State $ VS name typ init $ posOf n
         init = case typ of
@@ -305,6 +315,8 @@
           CFloatConst (CFloat a) _     -> fromIntegral (read a :: Integer)
           _ -> unexpected const "non numeric initialization"
 
+      (Just (CInitExpr c _), Nothing) -> evalDecl' env (a, Nothing, Just c)
+
       (Nothing, Just e') -> do
         e <- evalExpr env e'
         v <- if isVolatile typInfo
@@ -321,7 +333,7 @@
 
 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?)"
+  when (typ /= Void || not (null args)) $ notSupported f "non void f() function (How lame is this?)"
   return env { values = EnvFunction name (Function (length args) func) : values env }
   where
   (specs, (Ident name _ _), args, stat) = functionInfo f
diff --git a/src/Parse.hs b/src/Parse.hs
--- a/src/Parse.hs
+++ b/src/Parse.hs
@@ -4,7 +4,6 @@
 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
diff --git a/src/Utils.hs b/src/Utils.hs
--- a/src/Utils.hs
+++ b/src/Utils.hs
@@ -4,7 +4,6 @@
   , isVisable
   ) where
 
-import Data.List
 import Language.C
 
 import Error
diff --git a/src/Verify.hs b/src/Verify.hs
--- a/src/Verify.hs
+++ b/src/Verify.hs
@@ -1,9 +1,7 @@
 module Verify (verify) where
 
-import Control.Monad
-import Data.IORef
+import Control.Monad.State hiding (State)
 import Data.List
-import Data.Maybe
 import Math.SMT.Yices.Pipe
 import Math.SMT.Yices.Syntax
 import System.IO
@@ -15,12 +13,11 @@
 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
+  mapM_ (verifyModel yices format maxK) models
   where
   assertions = [ a | a@(Assert _ _ _) <- actions m ]
   models = map (trimModel . trimAssertions m) assertions
+  format = "verifying %-" ++ show (maximum [ length (intercalate "." n) | (Assert _ n _) <- actions m ]) ++ "s    "
 
 -- | Remove all assertions except one.
 trimAssertions :: Model -> Action -> Model
@@ -34,113 +31,95 @@
 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
+verifyModel :: FilePath -> String -> Int -> Model -> IO ()
+verifyModel y format maxK m = do
+  printf format (intercalate "." path) >> hFlush stdout
+  env0 <- initEnv y m
+  execStateT (check env0 1) env0
+  return ()
   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)
+  check :: Env -> Int -> Y ()
+  check _ k | k > maxK = liftIO $ printf "inconclusive: unable to proved step up to max k = %d\n" maxK
+  check env0 k = do
+    transition m
+    resultBasis <- checkBasis m env0
     case resultBasis of
-      Fail -> printf "FAILED: disproved basis in k = %d\n" k
+      Fail -> liftIO $ printf "FAILED: disproved basis in k = %d\n" k
       Pass -> do
-        resultStep <- checkStep y assert
+        resultStep <- checkStep
         case resultStep of
-          Fail -> withLogic y $ check initEnv env (assert : asserts) (k + 1)
-          Pass -> printf "passed: proved step in k = %d\n" k
+          Fail -> check env0 (k + 1)
+          Pass -> liftIO $ 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
+checkStep :: Y Result
+checkStep = do
+  Env y _ _ cmds asserts <- get
+  r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ head asserts] ++ cmds
   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
+checkBasis :: Model -> Env -> Y Result
+checkBasis m env0 = do
+  Env y _ _ cmds asserts <- get
+  r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ AND asserts] ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ] ++ cmds
   return $ result r
 
 result :: ResY -> Result
 result a = case a of
   Sat _   -> Fail
   UnSat _ -> Pass
-  InCon _ -> Pass
+  _ -> error $ "unexpected yices results: " ++ show a
 
--- | 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)
+transition :: Model -> Y ()
+transition m = mapM_ action $ actions m
 
-action :: YicesIPC -> (Env, ExpY) -> Action -> IO (Env, ExpY)
-action y (env, assert) a = case a of
+action :: Action -> Y ()
+action 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)
+    e <- expr (typeOf v) e
+    v <- addVar v
+    Env y i table cmds asserts <- get
+    put $ Env y i table (ASSERT (VarE v := e) : cmds) asserts
   Assert a _ _ -> do
-    a <- expr y env Bool a
-    return (env, AND [assert, a])
+    a <- expr Bool a
+    Env y i table cmds asserts <- get
+    put $ Env y i table cmds (a : asserts)
   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
+    a <- expr Bool a
+    Env y i table cmds asserts <- get
+    put $ Env y i table (ASSERT a : cmds) asserts
 
+expr :: Type -> E -> Y ExpY
+expr t a = case a of
+  Var a@(Volatile _ _ _) -> addVar a >>= return . VarE
+  Var a   -> getVar a >>= return . VarE
   Const a -> return $ exprConst t a
-
-  Not a _ -> do
-    a <- expr y env Bool a
-    return $ NOT a
+  Not a _ -> expr Bool a >>= return . NOT
 
   And a b _ -> do
-    a <- expr y env Bool a
-    b <- expr y env Bool b
+    a <- expr Bool a
+    b <- expr Bool b
     return $ AND [a, b]
 
   Or  a b _ -> do
-    a <- expr y env Bool a
-    b <- expr y env Bool b
+    a <- expr Bool a
+    b <- expr Bool b
     return $ OR  [a, b]
 
   Mul a b _ -> do
-    a <- expr y env t a
-    b <- expr y env t b
+    a <- expr t a
+    b <- expr t b
     return $ a :*: b
   
   Div a b _  -> do
-    a <- expr y env t a
-    b <- expr y env t b
+    a <- expr t a
+    b <- expr t b
     return $ op a b
     where
     op = case t of
@@ -148,37 +127,37 @@
       _         -> (:/:)
 
   Mod a b _ -> do
-    a <- expr y env t a
-    b <- expr y env t b
+    a <- expr t a
+    b <- expr t b
     return $ MOD a b
 
   Add a b _ -> do
-    a <- expr y env t a
-    b <- expr y env t b
+    a <- expr t a
+    b <- expr t b
     return $ a :+: b
 
   Sub a b _ -> do
-    a <- expr y env t a
-    b <- expr y env t b
+    a <- expr t a
+    b <- expr 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
+    a <- expr t' a
+    b <- expr 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
+    a <- expr t' a
+    b <- expr 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
+    a <- expr Bool a
+    b <- expr t' b
+    c <- expr t' c
     return $ IF a b c
 
 exprConst :: Type -> Const -> ExpY
@@ -190,23 +169,27 @@
 
 
 
+type Y = StateT Env IO
 
-data Env = Env NextId [(V, String)]  -- Env nextId table
+data Env = Env FilePath Int [(V, String)] [CmdY] [ExpY]  -- Env nextId table cmds assertions
 
-initEnv :: YicesIPC -> Model -> IO Env
-initEnv y m = do
-  nid <- newNextId
-  foldM (addVar y) (Env nid []) $ map State $ variables m
+initEnv :: FilePath -> Model -> IO Env
+initEnv y m = execStateT (mapM_ addVar $ map State $ variables m) (Env y 0 [] [] [])
 
-addVar :: YicesIPC -> Env -> V -> IO Env
-addVar y (Env nid table) v = do
-  i <- nextId nid
+addVar :: V -> Y String
+addVar v = do
+  Env y i table cmds asserts <- get
   let name = printf "n%d" i
-  runCmds y [DEFINE (name, VarT $ typeY v) Nothing]
-  return $ Env nid $ replace (v, name) table
+  put $ Env y (i + 1) (replace (v, name) table) (DEFINE (name, VarT $ typeY v) Nothing : cmds) asserts
+  return name
 
-getVar :: Env -> V -> String
-getVar (Env _ table) v = case lookup v table of
+getVar :: V -> Y String
+getVar v = do
+  env <- get
+  return $ getVar' env v
+
+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)
 
@@ -216,44 +199,11 @@
                               | 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