diff --git a/RELEASE-NOTES b/RELEASE-NOTES
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -8,3 +8,8 @@
 - Uses yices new 'quickCheckY'.
 - Fixed bug affecting 'assume'.
 
+afv 0.0.2    01/17/10
+
+- Support for function arguments.  Still no support for return values.
+- Stronger type checking.
+
diff --git a/afv.cabal b/afv.cabal
--- a/afv.cabal
+++ b/afv.cabal
@@ -1,11 +1,13 @@
 name:    afv
-version: 0.0.1
+version: 0.0.2
 
 category: Formal Methods
 
-synopsis: Model checking Atom generated C.
+synopsis: Infinite state model checking of iterative C programs.
 
-description: A model checker for Atom generated, or similar, C code.
+description: AFV is an infinite state model checker that
+             verifies iterative C programs by k-induction.
+             AFV uses Yices as the backend SMT solver.
 
 author:     Tom Hawkins <tomahawkins@gmail.com>
 maintainer: Tom Hawkins <tomahawkins@gmail.com>
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.1"
+version = "0.0.2"
 
 main :: IO ()
 main = do
diff --git a/src/Compile.hs b/src/Compile.hs
--- a/src/Compile.hs
+++ b/src/Compile.hs
@@ -45,7 +45,7 @@
 type M = StateT MDB IO
 
 data MDB = MDB
-  { nextId  :: Int
+  { nextId' :: Int
   , stack   :: [Ident]
   , enabled :: E
   , model   :: Model
@@ -53,12 +53,17 @@
 
 initMDB :: MDB
 initMDB = MDB
-  { nextId  = 0
+  { nextId' = 0
   , stack   = []
   , enabled = true
   , model   = Model { variables = [], actions = [] }
   }
 
+nextId :: M Int
+nextId = do
+  m <- get
+  put m { nextId' = nextId' m + 1 }
+  return $ nextId' m
 
 
 -- | Environment for resolving identifiers.
@@ -126,13 +131,13 @@
     (s, n) <- callPath
     m <- get
     let x = imply (enabled m) (head a) n
-    newAction $ Assert x s n
+    newAction $ Assert x s
     return x
   assume a = do
     (s, n) <- callPath
     m <- get
     let x = imply (enabled m) (head a) n
-    newAction $ Assume x s n
+    newAction $ Assume x s
     return x
 
 -- | Adds new action.
@@ -265,6 +270,8 @@
       (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"
     where
     p = posOf n
@@ -300,6 +307,7 @@
         v = State $ VS name typ init $ posOf n
         init = case typ of
           Void -> unexpected d "void type for variable declaration"
+          Ptr _ -> notSupported d "pointer types"
           Bool -> CBool (cInt /= 0) $ posOf n'
           Integer _  -> M.CInteger cInt $ posOf n'
           Rational _ -> CRational cRat $ posOf n'
@@ -322,9 +330,8 @@
         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')
+            i <- nextId
+            return $ Local name typ i (posOf e')
         assign True (posOf e') v e
         addVar env v
       _ -> notSupported i "variable declaration"
@@ -333,20 +340,37 @@
 
 evalFunc :: Env -> CFunDef -> M Env
 evalFunc env f =  do
-  when (typ /= Void || not (null args)) $ notSupported f "non void f() function (How lame is this?)"
+  when (typ /= Void) $ notSupported f "non void function"
   return env { values = EnvFunction name (Function (length args) func) : values env }
   where
-  (specs, (Ident name _ _), args, stat) = functionInfo f
+  (specs, (Ident name _ _), args', stat) = functionInfo f
   (_, typ) = typeInfo specs
-  func _ = do --XXX
+  args = concatMap funcArgs args'
+  func args' = do
+    env <- foldM bindArg env $ zip args args'
     evalStat env stat
-    return false
+    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
+  then addVar env (Volatile name typ (posOf n))
+  else do
+    i <- nextId
+    let v = Local name typ i (posOf n)
+    assign True (posOf n) v a
+    addVar env v
 
+funcArgs :: CDecl -> [(Ident, (TypeInfo, Type))]
+funcArgs (CDecl specs decls n) = map f decls
+  where
+  t = typeInfo specs
+  f (Just (CDeclr (Just i) [] Nothing [] _), Nothing, Nothing) = (i, t)
+  f _ = notSupported n "function argument"
 
 
 
 
+
 -- | Assgins a value to a variable.
 assign :: Bool -> Position -> V -> E -> M ()
 assign decl n v a = case v of
@@ -360,9 +384,8 @@
 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 }
+  i <- nextId
+  let v = Tmp (typeOf a) i n
   assign True n v a
   return $ Var v
 
@@ -377,7 +400,7 @@
 
 -- | 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 (CFunDef specs (CDeclr (Just ident) [(CFunDeclr (Right (args, False)) _ _)] Nothing [] _) [] stmt _) = (specs, ident, args, stmt)  --XXX What is the False?
 functionInfo f = notSupported f "function"
 
 
diff --git a/src/Error.hs b/src/Error.hs
--- a/src/Error.hs
+++ b/src/Error.hs
@@ -2,6 +2,7 @@
   ( err
   , notSupported
   , unexpected
+  , position
   , debug
   , debug'
   ) where
@@ -10,12 +11,10 @@
 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
+err a m = error $ position a ++ ": " ++ m
 
 notSupported :: Pos a => a -> String -> b
-notSupported a m = err a $ " not supported: " ++ m
+notSupported a m = err a $ "not supported: " ++ m
 
 unexpected :: Pos a => a -> String -> b
 unexpected a m = err a $ "unexpected: " ++ m
@@ -25,3 +24,8 @@
 
 debug' :: Show a => String -> a -> b -> b
 debug' m a b = unsafePerformIO (putStrLn (m ++ ": " ++ show a) >> return b)
+
+position :: Pos a => a -> String
+position a = f ++ ":" ++ show l ++ ":" ++ show c
+  where
+  Position f l c = posOf a
diff --git a/src/Model.hs b/src/Model.hs
--- a/src/Model.hs
+++ b/src/Model.hs
@@ -1,6 +1,7 @@
 module Model
   ( Type        (..)
   , IntegerType (..)
+  , FloatType   (..)
   , TypeOf      (..)
   , Const       (..)
   , VS          (..)
@@ -12,6 +13,7 @@
   , false
   , isRational
   , isInteger
+  , typeCheckModel
   , unify
   ) where
 
@@ -21,11 +23,14 @@
 
 data IntegerType = U8 | U16 | U32 | U64 | S8 | S16 | S32 | S64 deriving (Show, Eq)
 
+data FloatType = Float | Double deriving (Show, Eq)
+
 data Type
   = Void
+  | Ptr Type
   | Bool
   | Integer  (Maybe IntegerType)
-  | Rational (Maybe Bool)          -- isDouble
+  | Rational (Maybe FloatType)
   deriving Eq
 
 isInteger :: Type -> Bool
@@ -39,6 +44,7 @@
 instance Show Type where
   show a = case a of
     Void -> "void"
+    Ptr a -> show a ++ " *"
     Bool -> "bool"
     Integer Nothing -> "unspecified integer type"
     Integer (Just a) -> case a of
@@ -51,23 +57,23 @@
       S32 -> "signed long"
       S64 -> "signed long long"
     Rational Nothing -> "unspecified floating type"
-    Rational (Just True)  -> "double"
-    Rational (Just False) -> "float"
+    Rational (Just Double) -> "double"
+    Rational (Just Float)  -> "float"
 
 class TypeOf a where typeOf :: a -> Type
 
 instance TypeOf Type where typeOf = id
 
 data Const
-  = CBool Bool Position
-  | CInteger Integer Position
+  = 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
+    CBool     _ _ -> Bool
+    CInteger  _ _ -> Integer  Nothing
     CRational _ _ -> Rational Nothing
 
 instance Pos Const where
@@ -104,14 +110,6 @@
     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
@@ -127,6 +125,8 @@
   | Lt  E E Position
   | Eq  E E Position
   | Mux E E E Position
+  | Ref   E Position
+  | Deref E Position
   deriving (Show, Eq)
 
 instance Pos E where
@@ -144,6 +144,8 @@
     Lt  _ _ a -> a
     Eq  _ _ a -> a
     Mux _ _ _ a -> a
+    Ref _ a -> a
+    Deref _ a -> a
 
 instance TypeOf E where
   typeOf a = case a of
@@ -159,7 +161,11 @@
     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)
+    Mux a b c _ -> seq (unify' Bool (typeOf a)) $ unify' (typeOf b) (typeOf c)
+    Ref a _ -> Ptr $ typeOf a
+    Deref a p -> case typeOf a of
+      Ptr a -> a
+      t -> err p $ "type violation: expecting pointer type, but got " ++ show t
     where
     unify' = unify a
 
@@ -179,8 +185,17 @@
   (Rational Nothing, a@(Rational _)) -> a
   (a@(Rational _), Rational Nothing) -> a
 
-  (a, b) -> unexpected n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b
+  (a, b) -> err n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b
 
+typeCheckModel :: Model -> Model
+typeCheckModel m = m { actions = map typeCheckAction $ actions m }
+
+typeCheckAction :: Action -> Action
+typeCheckAction a = case a of
+  Assign v a -> seq (unify a (typeOf v) (typeOf a)) $ Assign v a
+  Assert a n -> seq (unify a Bool (typeOf a))       $ Assert a n
+  Assume a n -> seq (unify a Bool (typeOf a))       $ Assume a n
+
 true :: E
 true = Const $ CBool True nopos
 
@@ -191,8 +206,8 @@
 
 data Action
   = Assign V E
-  | Assert E [String] Position
-  | Assume E [String] Position
+  | Assert E [String]
+  | Assume E [String]
   deriving (Show, Eq)
 
 data Model = Model
diff --git a/src/Utils.hs b/src/Utils.hs
--- a/src/Utils.hs
+++ b/src/Utils.hs
@@ -77,8 +77,8 @@
     (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
+    (0, 0, 0, 0, 0, 0, 0, 0, 1, 0) -> Rational $ Just Float
+    (0, 0, 0, 0, 0, 0, 0, 0, 0, 1) -> Rational $ Just Double
 
     a -> notSupported (head specs) $ "type signature: " ++ show a
 
diff --git a/src/Verify.hs b/src/Verify.hs
--- a/src/Verify.hs
+++ b/src/Verify.hs
@@ -7,6 +7,7 @@
 import System.IO
 import Text.Printf
 
+import Error
 import Model
 
 -- | Verify a model with k-induction.
@@ -15,15 +16,16 @@
 verify yices maxK m = do
   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    "
+  model = typeCheckModel m
+  assertions = [ a | a@(Assert _ _) <- actions model ]
+  models = map (trimModel . trimAssertions model) assertions
+  format = "verifying %-" ++ show (maximum [ length (intercalate "." n) | (Assert _ n) <- actions model ]) ++ "s    "
 
 -- | 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 b@(Assert _ _) = a == b
   keep _ = True
 
 -- | Trim all unneeded stuff from a model.
@@ -38,21 +40,23 @@
   execStateT (check env0 1) env0
   return ()
   where
-  [path] = [ path | Assert _ path _ <- actions m ]
+  [path] = [ path | Assert _ path <- actions m ]
   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 -> liftIO $ printf "FAILED: disproved basis in k = %d\n" k
+      Fail    -> liftIO $ printf "FAILED: disproved basis in k = %d\n" k
+      Problem -> return ()
       Pass -> do
         resultStep <- checkStep
         case resultStep of
-          Fail -> check env0 (k + 1)
-          Pass -> liftIO $ printf "passed: proved step in k = %d\n" k
+          Fail    -> check env0 (k + 1)
+          Problem -> return ()
+          Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k
         
-data Result = Pass | Fail
+data Result = Pass | Fail | Problem
 
 -- | Check induction step.
 checkStep :: Y Result
@@ -72,6 +76,7 @@
 result a = case a of
   Sat _   -> Fail
   UnSat _ -> Pass
+  InCon _ -> Problem
   _ -> error $ "unexpected yices results: " ++ show a
 
 
@@ -86,11 +91,11 @@
     v <- addVar v
     Env y i table cmds asserts <- get
     put $ Env y i table (ASSERT (VarE v := e) : cmds) asserts
-  Assert a _ _ -> do
+  Assert a _ -> do
     a <- expr Bool a
     Env y i table cmds asserts <- get
     put $ Env y i table cmds (a : asserts)
-  Assume a _ _ -> do
+  Assume a _ -> do
     a <- expr Bool a
     Env y i table cmds asserts <- get
     put $ Env y i table (ASSERT a : cmds) asserts
@@ -160,6 +165,9 @@
     c <- expr t' c
     return $ IF a b c
 
+  Ref _ _ -> notSupported a "address-of operator"
+  Deref _ _ -> notSupported a "indirection operator"
+
 exprConst :: Type -> Const -> ExpY
 exprConst t a = case a of 
   CBool     a _ -> LitB a
@@ -201,7 +209,8 @@
 
 typeY :: TypeOf a => a -> String
 typeY a = case typeOf a of
-  Void       -> error "Verify.typeY: void time"
+  Void       -> error "Verify.typeY: void"
+  Ptr _      -> error "Verify.typeY: ptr"
   Bool       -> "bool"
   Integer  _ -> "int"
   Rational _ -> "real"