diff --git a/Language/SMTLib2/Connection.hs b/Language/SMTLib2/Connection.hs
--- a/Language/SMTLib2/Connection.hs
+++ b/Language/SMTLib2/Connection.hs
@@ -12,16 +12,13 @@
 
 import Language.SMTLib2.Internals
 import Control.Concurrent.MVar
-import Control.Monad.State (runStateT)
-import Control.Monad.Reader (runReaderT)
 import Control.Monad.Trans (MonadIO,liftIO)
 import Control.Exception
 import Prelude (($),IO,return)
 
 -- | Represents a connection to an SMT solver.
 --   The SMT solver runs in a seperate thread and communication is handled via handles.
-data SMTConnection b = SMTConnection { backend :: b
-                                     , status :: MVar SMTState
+data SMTConnection b = SMTConnection { backend :: MVar b
                                      }
 
 -- | Create a new connection to a SMT solver by spawning a shell command.
@@ -29,23 +26,21 @@
 open :: (MonadIO m,SMTBackend b m) => b -- ^ The backend for the SMT solver.
         -> m (SMTConnection b)
 open solver = do
-  st <- liftIO $ newMVar emptySMTState
-  return (SMTConnection { backend = solver
-                        , status = st
-                        })
+  st <- liftIO $ newMVar solver
+  return (SMTConnection { backend = st })
 
 -- | Closes an open SMT connection. Do not use the connection afterwards.
 close :: (MonadIO m,SMTBackend b m) => SMTConnection b -> m ()
 close conn = do
-  st <- liftIO $ takeMVar (status conn)
-  smtHandle (backend conn) st SMTExit
+  st <- liftIO $ takeMVar (backend conn)
+  smtHandle st SMTExit
   return ()
 
-withConnection :: MonadIO m => SMTConnection b -> (b -> SMTState -> m (a,SMTState)) -> m a
+withConnection :: MonadIO m => SMTConnection b -> (b -> m (a,b)) -> m a
 withConnection conn f = do
-  st <- liftIO $ takeMVar (status conn)
-  (res,nst) <- f (backend conn) st
-  liftIO $ putMVar (status conn) nst
+  b <- liftIO $ takeMVar (backend conn)
+  (res,nb) <- f b
+  liftIO $ putMVar (backend conn) nb
   return res
 
 -- | Perform an action in the SMT solver associated with this connection and return the result.
@@ -53,18 +48,18 @@
               => SMTConnection b -- ^ The connection to the SMT solver to use
               -> SMT' m a -- ^ The action to perform
               -> m a
-performSMT conn act = withConnection conn (\b st -> runStateT (runReaderT (runSMT act) (AnyBackend b)) st)
+performSMT conn act = withConnection conn (runSMT act)
 
 performSMTExitCleanly :: SMTBackend b IO
                          => SMTConnection b
                          -> SMT' IO a
                          -> IO a
 performSMTExitCleanly conn act = do
-  st <- takeMVar (status conn)
+  b <- takeMVar (backend conn)
   catch (do
-            (res,nst) <- runStateT (runReaderT (runSMT act) (AnyBackend $ backend conn)) st
-            putMVar (status conn) nst
+            (res,nb) <- runSMT act b
+            putMVar (backend conn) nb
             return res)
     (\e -> do
-        smtHandle (backend conn) st SMTExit
+        smtHandle b SMTExit
         throw (e :: SomeException))
diff --git a/Language/SMTLib2/Internals.hs b/Language/SMTLib2/Internals.hs
--- a/Language/SMTLib2/Internals.hs
+++ b/Language/SMTLib2/Internals.hs
@@ -4,8 +4,6 @@
 import Language.SMTLib2.Internals.Operators
 import Language.SMTLib2.Strategy
 
-import Control.Monad.Reader hiding (mapM,mapM_)
-import Control.Monad.State hiding (mapM,mapM_)
 import Data.Typeable
 import Data.Map as Map hiding (assocs,foldl)
 import Data.Ratio
@@ -27,7 +25,9 @@
 
 -- Monad stuff
 import Control.Applicative (Applicative(..))
-import Control.Monad.State.Lazy as Lazy (StateT)
+import Control.Monad.Trans
+import Control.Monad.Fix
+import Control.Monad (ap,when)
 
 data SMTRequest response where
   SMTSetLogic :: String -> SMTRequest ()
@@ -35,12 +35,13 @@
   SMTSetOption :: SMTOption -> SMTRequest ()
   SMTAssert :: SMTExpr Bool -> Maybe InterpolationGroup -> Maybe ClauseId -> SMTRequest ()
   SMTCheckSat :: Maybe Tactic -> CheckSatLimits -> SMTRequest CheckSatResult
+  SMTDeclaredDataTypes :: SMTRequest DataTypeInfo
   SMTDeclareDataTypes :: TypeCollection -> SMTRequest ()
   SMTDeclareSort :: String -> Integer -> SMTRequest ()
   SMTPush :: SMTRequest ()
   SMTPop :: SMTRequest ()
-  SMTDefineFun :: SMTType res => FunInfo -> [FunInfo] -> SMTExpr res -> SMTRequest ()
-  SMTDeclareFun :: FunInfo -> SMTRequest ()
+  SMTDefineFun :: (Args arg,SMTType res) => Maybe String -> Proxy arg -> ArgAnnotation arg -> SMTExpr res -> SMTRequest Integer
+  SMTDeclareFun :: FunInfo -> SMTRequest Integer
   SMTGetValue :: SMTValue t => SMTExpr t -> SMTRequest t
   SMTGetModel :: SMTRequest SMTModel
   SMTGetProof :: SMTRequest (SMTExpr Bool)
@@ -50,6 +51,9 @@
   SMTComment :: String -> SMTRequest ()
   SMTExit :: SMTRequest ()
   SMTApply :: Tactic -> SMTRequest [SMTExpr Bool]
+  SMTNameExpr :: String -> SMTExpr t -> SMTRequest Integer
+  SMTNewInterpolationGroup :: SMTRequest InterpolationGroup
+  SMTNewClauseId :: SMTRequest ClauseId
   deriving Typeable
 
 data SMTModel = SMTModel { modelFunctions :: Map Integer (Integer,[ProxyArg],SMTExpr Untyped)
@@ -68,7 +72,9 @@
   deriving (Show,Eq,Ord,Typeable)
 
 class Monad m => SMTBackend a m where
-  smtHandle :: Typeable response => a -> SMTState -> SMTRequest response -> m response
+  smtHandle :: Typeable response => a -> SMTRequest response -> m (response,a)
+  smtGetNames :: a -> m (Integer -> String)
+  smtNextName :: a -> m (Maybe String -> String)
 
 -- | Haskell types which can be represented in SMT
 class (Ord t,Typeable t,
@@ -92,7 +98,7 @@
 type ArgumentSort = Fix ArgumentSort'
 
 data Unmangling a = PrimitiveUnmangling (Value -> SMTAnnotation a -> Maybe a)
-                  | ComplexUnmangling (forall m. Monad m => (forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b) -> SMTExpr a -> SMTAnnotation a -> m (Maybe a))
+                  | ComplexUnmangling (forall m s. Monad m => (forall b. SMTValue b => s -> SMTExpr b -> SMTAnnotation b -> m (b,s)) -> s -> SMTExpr a -> SMTAnnotation a -> m (Maybe a,s))
 
 data Mangling a = PrimitiveMangling (a -> SMTAnnotation a -> Value)
                 | ComplexMangling (a -> SMTAnnotation a -> SMTExpr a)
@@ -117,64 +123,49 @@
 -- | An array which maps indices of type /i/ to elements of type /v/.
 data SMTArray (i :: *) (v :: *) = SMTArray deriving (Eq,Ord,Typeable)
 
-data FunInfo = forall arg r. (Args arg,SMTType r) => FunInfo { funInfoId :: Integer
-                                                             , funInfoProxy :: Proxy (arg,r)
+data FunInfo = forall arg r. (Args arg,SMTType r) => FunInfo { funInfoProxy :: Proxy (arg,r)
                                                              , funInfoArgAnn :: ArgAnnotation arg
                                                              , funInfoResAnn :: SMTAnnotation r
-                                                             , funInfoName :: Maybe (String,Integer)
+                                                             , funInfoName :: Maybe String
                                                              }
 
-data SMTState = SMTState { nextVar :: Integer
-                         , nextInterpolationGroup :: Integer
-                         , nextClauseId :: Integer
-                         , allVars :: Map Integer FunInfo
-                         , namedVars :: Map (String,Integer) Integer
-                         , nameCount :: Map String Integer
-                         , declaredDataTypes :: DataTypeInfo }
-
 data AnyBackend m = forall b. SMTBackend b m => AnyBackend b
 
 -- | The SMT monad used for communating with the SMT solver
-data SMT' m a = SMT { runSMT :: ReaderT (AnyBackend m) (Lazy.StateT SMTState m) a }
+data SMT' m a = SMT { runSMT :: forall b. SMTBackend b m => b -> m (a,b) }
 
 type SMT = SMT' IO
 
 instance Functor m => Functor (SMT' m) where
-  fmap f = SMT . fmap f . runSMT
+  fmap f (SMT g) = SMT $ \b -> fmap (\(r,b) -> (f r,b)) (g b)
 
 instance Monad m => Monad (SMT' m) where
-  return = SMT . return
-  m >>= f = SMT $ (runSMT m) >>= runSMT . f
+  return x = SMT $ \b -> return (x,b)
+  (SMT f) >>= g = SMT $ \b -> do
+    (r,b1) <- f b
+    case g r of
+     SMT act -> act b1
 
 instance MonadIO m => MonadIO (SMT' m) where
-  liftIO = SMT . liftIO
+  liftIO act = SMT $ \b -> do
+    res <- liftIO act
+    return (res,b)
 
 instance MonadFix m => MonadFix (SMT' m) where
-  mfix f = SMT $ mfix (runSMT . f)
+  mfix f = SMT $ \b -> mfix (\(~(res,_)) -> case f res of
+                              ~(SMT act) -> act b)
 
 instance (Monad m,Functor m) => Applicative (SMT' m) where
   pure = return
   (<*>) = ap
 
---askSMT :: Monad m => SMT' b m b
---askSMT = SMT ask
-
-smtBackend :: Monad m => (forall b. SMTBackend b m => b -> SMT' m a) -> SMT' m a
-smtBackend f = SMT $ do
-  AnyBackend backend <- ask
-  runSMT $ f backend
-
-getSMT :: Monad m => SMT' m SMTState
-getSMT = SMT get
-
-putSMT :: Monad m => SMTState -> SMT' m ()
-putSMT = SMT . put
-
-modifySMT :: Monad m => (SMTState -> SMTState) -> SMT' m ()
-modifySMT f = SMT $ modify f
+smtBackend :: Monad m => (forall b. SMTBackend b m => b -> m (res,b)) -> SMT' m res
+smtBackend f = SMT f
 
 instance MonadTrans SMT' where
-  lift = SMT . lift . lift
+  lift act = SMT $ \b -> do
+    res <- act
+    return (res,b)
 
 data Untyped = forall t. SMTType t => Untyped t deriving Typeable
 
@@ -209,6 +200,7 @@
 data SMTExpr t where
   Var :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t
   QVar :: SMTType t => Integer -> Integer -> SMTAnnotation t -> SMTExpr t
+  FunArg :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t
   Const :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t
   AsArray :: (Args arg,SMTType res) => SMTFunction arg res -> ArgAnnotation arg
              -> SMTExpr (SMTArray arg res)
@@ -406,26 +398,16 @@
 withSMTBackendExitCleanly backend act
   = bracket
     (return backend)
-    (\backend -> smtHandle backend emptySMTState SMTExit)
-    (\backend -> withSMTBackend' (AnyBackend backend) False act)
-
-withSMTBackend :: SMTBackend b m => b -> SMT' m a -> m a
-withSMTBackend backend act = withSMTBackend' (AnyBackend backend) True act
+    (\backend -> smtHandle backend SMTExit)
+    (\backend -> withSMTBackend' backend False act)
 
-emptySMTState :: SMTState
-emptySMTState = SMTState { nextVar = 0
-                         , nextInterpolationGroup = 0
-                         , nextClauseId = 0
-                         , allVars = Map.empty
-                         , namedVars = Map.empty
-                         , nameCount = Map.empty
-                         , declaredDataTypes = emptyDataTypeInfo
-                         }
+withSMTBackend :: SMTBackend a m => a -> SMT' m b -> m b
+withSMTBackend b = withSMTBackend' b True
 
-withSMTBackend' :: AnyBackend m -> Bool -> SMT' m a -> m a
-withSMTBackend' backend@(AnyBackend b) mustExit f = do
-  (res,st) <- runStateT (runReaderT (runSMT f) backend) emptySMTState
-  when mustExit (smtHandle b st SMTExit)
+withSMTBackend' :: SMTBackend a m => a -> Bool -> SMT' m b -> m b
+withSMTBackend' backend mustExit f = do
+  (res,nbackend) <- runSMT f backend
+  when mustExit (smtHandle nbackend SMTExit >> return ())
   return res
 
 funInfoSort :: FunInfo -> Sort
@@ -438,7 +420,7 @@
                          , funInfoArgAnn = ann })
   = getSorts (undefined::a) ann
 
-newVariableId :: (Monad m) => Maybe String -> (Integer -> Maybe Integer -> (r,FunInfo)) -> SMT' m r
+{-newVariableId :: (Monad m) => Maybe String -> (Integer -> Maybe Integer -> (r,FunInfo)) -> SMT' m r
 newVariableId name f = do
   st <- getSMT
   let idx = nextVar st
@@ -501,7 +483,7 @@
 nameVariable var name = do
   st <- getSMT
   let c = Map.findWithDefault 0 name (nameCount st)
-  putSMT $ st { nameCount = Map.insert name (c+1) (nameCount st) }
+  putSMT $ st { nameCount = Map.insert name (c+1) (nameCount st) }-}
 
 argsSignature :: Args a => a -> ArgAnnotation a -> [Sort]
 argsSignature arg ann
@@ -536,13 +518,14 @@
 sortToArgumentSort (Fix s) = Fix (NormalSort (fmap sortToArgumentSort s))
 
 declareType :: (Monad m,SMTType t) => t -> SMTAnnotation t -> SMT' m ()
-declareType (_::t) ann = do
-  st <- getSMT
-  let (colls,ndts) = getNewTypeCollections (Proxy::Proxy t) ann
-                     (declaredDataTypes st)
-      nst = st { declaredDataTypes = ndts }
-  putSMT nst
-  smtBackend $ \backend -> mapM_ (\coll -> lift $ smtHandle backend nst (SMTDeclareDataTypes coll)) colls
+declareType (_::t) ann = smtBackend $ \b0 -> do
+  (dts,b1) <- smtHandle b0 SMTDeclaredDataTypes
+  let (colls,ndts) = getNewTypeCollections (Proxy::Proxy t) ann dts
+  b2 <- foldlM (\backend coll -> do
+                   ((),nbackend) <- smtHandle backend (SMTDeclareDataTypes coll)
+                   return nbackend
+               ) b1 colls
+  return ((),b2)
 
 -- Data type info
 
@@ -550,6 +533,7 @@
                                  , datatypes :: Map String (DataType,TypeCollection)
                                  , constructors :: Map String (Constr,DataType,TypeCollection)
                                  , fields :: Map String (DataField,Constr,DataType,TypeCollection) }
+                  deriving Typeable
 
 data TypeCollection = TypeCollection { argCount :: Integer
                                      , dataTypes :: [DataType]
@@ -622,6 +606,7 @@
                      , construct :: forall r. [Maybe ProxyArg] -> [AnyValue]
                                     -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r)
                                     -> r
+                     , conUndefinedArgs :: forall r. [ProxyArg] -> (forall arg. Args arg => arg -> ArgAnnotation arg -> r) -> r
                      , conTest :: forall t. SMTType t => [ProxyArg] -> t -> Bool
                      }
 
@@ -744,6 +729,44 @@
   return (x:name,nc)
 unescapeName' "" = Just ("",0)
 
+data SMTState = SMTState { nextVar :: Integer
+                         , nextInterpolationGroup :: Integer
+                         , nextClauseId :: Integer
+                         , allVars :: Map Integer (FunInfo,Integer)
+                         , namedVars :: Map (String,Integer) Integer
+                         , nameCount :: Map String Integer
+                         , declaredDataTypes :: DataTypeInfo }
+
+emptySMTState :: SMTState
+emptySMTState = SMTState { nextVar = 0
+                         , nextInterpolationGroup = 0
+                         , nextClauseId = 0
+                         , allVars = Map.empty
+                         , namedVars = Map.empty
+                         , nameCount = Map.empty
+                         , declaredDataTypes = emptyDataTypeInfo
+                         }
+
+smtStateAddFun :: FunInfo -> SMTState -> (Integer,String,SMTState)
+smtStateAddFun finfo st
+  = (v,name',nst)
+  where
+    v = nextVar st
+    nameBase = case funInfoName finfo of
+      Nothing -> "var"
+      Just n -> n
+    nc = case Map.lookup nameBase (nameCount st) of
+      Just n -> n
+      Nothing -> 0
+    name' = if nc==0
+            then nameBase
+            else nameBase++"_"++show nc
+    nst = st { nextVar = v+1
+             , allVars = Map.insert v (finfo,nc) (allVars st)
+             , namedVars = Map.insert (nameBase,nc) v (namedVars st)
+             , nameCount = Map.insert nameBase (nc+1) (nameCount st)
+             }
+
 -- BitVectors
 
 #ifdef SMTLIB2_WITH_DATAKINDS
@@ -999,7 +1022,11 @@
 type BV64 = BitVector (BVTyped N64)
 
 instance Monad m => SMTBackend (AnyBackend m) m where
-  smtHandle (AnyBackend b) = smtHandle b
+  smtHandle (AnyBackend b) req = do
+    (res,nb) <- smtHandle b req
+    return (res,AnyBackend nb)
+  smtGetNames (AnyBackend b) = smtGetNames b
+  smtNextName (AnyBackend b) = smtNextName b
 
 instance Show (SMTExpr t) where
   showsPrec = showExpr
@@ -1017,6 +1044,10 @@
                                                 showsPrec 11 v .
                                                 showChar ' ' .
                                                 showsPrec 11 ann)
+showExpr p (FunArg v ann) = showParen (p>10) (showString "FunArg " .
+                                              showsPrec 11 v .
+                                              showChar ' ' .
+                                              showsPrec 11 ann)
 showExpr p (Const c ann) = showParen (p>10) (showString "Const " .
                                              showsPrec 11 c .
                                              showChar ' ' .
@@ -1059,8 +1090,10 @@
                                                      showsPrec 11 obj .
                                                      showChar ' ' .
                                                      showsPrec 11 ann)
-showExpr p (UntypedExpr e) = showExpr p e
-showExpr p (UntypedExprValue e) = showExpr p e
+showExpr p (UntypedExpr e) = showParen (p>10) (showString "UntypedExpr " .
+                                               showExpr 11 e)
+showExpr p (UntypedExprValue e) = showParen (p>10) (showString "UntypedExprValue " .
+                                                    showExpr 11 e)
 
 instance Show (SMTFunction arg res) where
   showsPrec _ SMTEq = showString "SMTEq"
diff --git a/Language/SMTLib2/Internals/Instances.hs b/Language/SMTLib2/Internals/Instances.hs
--- a/Language/SMTLib2/Internals/Instances.hs
+++ b/Language/SMTLib2/Internals/Instances.hs
@@ -59,6 +59,7 @@
 extractAnnotation :: SMTExpr a -> SMTAnnotation a
 extractAnnotation (Var _ ann) = ann
 extractAnnotation (QVar _ _ ann) = ann
+extractAnnotation (FunArg _ ann) = ann
 extractAnnotation (Const _ ann) = ann
 extractAnnotation (AsArray f arg) = (arg,inferResAnnotation f arg)
 extractAnnotation (Forall _ _ _) = ()
@@ -127,6 +128,8 @@
   = f (Var i ann::SMTExpr t)
 entype f (QVar lvl i (ProxyArg (_::t) ann))
   = f (QVar lvl i ann::SMTExpr t)
+entype f (FunArg i (ProxyArg (_::t) ann))
+  = f (FunArg i ann::SMTExpr t)
 entype f (UntypedExpr x) = f x
 entype f (InternalObj obj (ProxyArg (_::t) ann))
   = f (InternalObj obj ann :: SMTExpr t)
@@ -137,6 +140,8 @@
   = f (Var i ann::SMTExpr t)
 entypeValue f (QVar lvl i (ProxyArgValue (_::t) ann))
   = f (QVar lvl i ann::SMTExpr t)
+entypeValue f (FunArg i (ProxyArgValue (_::t) ann))
+  = f (FunArg i ann::SMTExpr t)
 entypeValue f (Const (UntypedValue v) (ProxyArgValue (_::t) ann))
   = case cast v of
   Just rv -> f (Const (rv::t) ann)
@@ -196,12 +201,12 @@
 
 instance SMTValue UntypedValue where
   unmangle = ComplexUnmangling $
-             \f val (ProxyArgValue _ ann)
+             \f st val (ProxyArgValue _ ann)
              -> entypeValue
                 (\(expr'::SMTExpr t) -> case cast ann of
                   Just ann' -> do
-                    res <- f expr' ann'
-                    return $ Just $ UntypedValue res
+                    (res,nst) <- f st expr' ann'
+                    return (Just $ UntypedValue res,nst)
                 ) val
   mangle = ComplexMangling (\(UntypedValue x) (ProxyArgValue (_::t) ann)
                              -> case cast x of
@@ -930,6 +935,7 @@
            , construct = \[Just prx] [] f
                          -> withProxyArg prx $
                             \(_::t) ann -> f [prx] (Nothing::Maybe t) ann
+           , conUndefinedArgs = \_ f -> f () ()
            , conTest = \args x -> case args of
                                    [s] -> withProxyArg s $
                                           \(_::t) _ -> case cast x of
@@ -946,6 +952,9 @@
                              [v] -> withAnyValue v $
                                     \_ (rv::t) ann
                                     -> f [ProxyArg (undefined::t) ann] (Just rv) ann
+           , conUndefinedArgs = \sorts f -> case sorts of
+                                             [s] -> withProxyArg s $
+                                                    \(_::t) ann -> f (undefined::SMTExpr t) ann
            , conTest = \args x -> case args of
                                    [s] -> withProxyArg s $
                                           \(_::t) _ -> case cast x of
@@ -989,18 +998,18 @@
                                      Nothing -> Nothing
                                _ -> Nothing)
     ComplexUnmangling p
-      -> ComplexUnmangling $ \f (expr::SMTExpr (Maybe t)) ann -> do
-        isNothing <- f (App (SMTConTest
-                             (Constructor [ProxyArg (undefined::t) (extractAnnotation expr)]
-                              dtMaybe conNothing :: Constructor () (Maybe a))) expr
-                       ) ()
+      -> ComplexUnmangling $ \f st (expr::SMTExpr (Maybe t)) ann -> do
+        (isNothing,st1) <- f st (App (SMTConTest
+                                      (Constructor [ProxyArg (undefined::t) (extractAnnotation expr)]
+                                       dtMaybe conNothing :: Constructor () (Maybe a))) expr
+                                ) ()
         if isNothing
-          then return (Just Nothing)
+          then return (Just Nothing,st1)
           else do
-           val <- p f (App (SMTFieldSel (Field [ProxyArg (undefined::t) (extractAnnotation expr)] dtMaybe conJust fieldFromJust)) expr) ann
+           (val,st2) <- p f st1 (App (SMTFieldSel (Field [ProxyArg (undefined::t) (extractAnnotation expr)] dtMaybe conJust fieldFromJust)) expr) ann
            case val of
-            Nothing -> return Nothing
-            Just val' -> return (Just (Just val'))
+            Nothing -> return (Nothing,st2)
+            Just val' -> return (Just (Just val'),st2)
   mangle = case mangle of
     PrimitiveMangling p
       -> PrimitiveMangling $
@@ -1047,6 +1056,7 @@
                 , construct = \[Just sort] args f
                               -> withProxyArg sort $
                                  \(_::t) ann -> f [sort] ([]::[t]) ann
+                , conUndefinedArgs = \_ f -> f () ()
                 , conTest = \args x -> case args of
                 [s] -> withProxyArg s $
                        \(_::t) _ -> case cast x of
@@ -1058,18 +1068,21 @@
 conInsert = Constr { conName = "insert"
                    , conFields = [fieldHead
                                  ,fieldTail]
-                         , construct = \sort args f
-                                       -> case args of
-                                         [h,t] -> withAnyValue h $
-                                                \_ (v::t) ann
-                                                -> case castAnyValue t of
+                   , construct = \sort args f
+                                 -> case args of
+                                     [h,t] -> withAnyValue h $
+                                              \_ (v::t) ann
+                                              -> case castAnyValue t of
                                                   Just (vs,_) -> f [ProxyArg (undefined::t) ann] (v:vs) ann
-                         , conTest = \args x -> case args of
-                           [s] -> withProxyArg s $
-                                \(_::t) _ -> case cast x of
-                                  Just ((_:_)::[t]) -> True
-                                  _ -> False
-                         }
+                   , conUndefinedArgs = \sorts f -> case sorts of
+                   [s] -> withProxyArg s $
+                          \(_::t) ann -> f (undefined::(SMTExpr t,SMTExpr [t])) (ann,ann)
+                   , conTest = \args x -> case args of
+                   [s] -> withProxyArg s $
+                          \(_::t) _ -> case cast x of
+                                        Just ((_:_)::[t]) -> True
+                                        _ -> False
+                   }
 
 insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a,SMTExpr [a]) [a]
 insert' ann = withUndef $
@@ -1118,25 +1131,25 @@
         t' <- pUnmangle p t ann
         return (h':t')
       cUnmangle :: Monad m
-                => ((forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b)
-                    -> SMTExpr a -> SMTAnnotation a -> m (Maybe a))
-                -> (forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b)
-                -> SMTExpr [a] -> SMTAnnotation a -> m (Maybe [a])
-      cUnmangle c f (expr::SMTExpr [t]) ann = do
-        isNil <- f (App (SMTConTest
-                         (Constructor [ProxyArg (undefined::t) ann] dtList conNil
-                          ::Constructor () [t]))
-                    expr) ()
+                => ((forall b. SMTValue b => st -> SMTExpr b -> SMTAnnotation b -> m (b,st))
+                    -> st -> SMTExpr a -> SMTAnnotation a -> m (Maybe a,st))
+                -> (forall b. SMTValue b => st -> SMTExpr b -> SMTAnnotation b -> m (b,st))
+                -> st -> SMTExpr [a] -> SMTAnnotation a -> m (Maybe [a],st)
+      cUnmangle c f st (expr::SMTExpr [t]) ann = do
+        (isNil,st1) <- f st (App (SMTConTest
+                                  (Constructor [ProxyArg (undefined::t) ann] dtList conNil
+                                   ::Constructor () [t]))
+                             expr) ()
         if isNil
-          then return (Just [])
+          then return (Just [],st1)
           else do
-           h <- c f (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldHead))
+           (h,st2) <- c f st1 (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldHead))
                      expr) ann
-           t <- cUnmangle c f (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldTail)) expr) ann
-           return $ do
-             h' <- h
-             t' <- t
-             return $ h':t'
+           (t,st3) <- cUnmangle c f st2 (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldTail)) expr) ann
+           return (do
+                      h' <- h
+                      t' <- t
+                      return $ h':t',st3)
   mangle = case mangle of
     PrimitiveMangling p
       -> PrimitiveMangling $ pMangle p
@@ -1506,6 +1519,9 @@
   r -> r
 compareExprs (QVar _ _ _) _ = LT
 compareExprs _ (QVar _ _ _) = GT
+compareExprs (FunArg i _) (FunArg j _) = compare i j
+compareExprs (FunArg _ _) _ = LT
+compareExprs _ (FunArg _ _) = GT
 compareExprs (Const i _) (Const j _) = case cast j of
       Just j' -> compare i j'
       Nothing -> compare (typeOf i) (typeOf j)
@@ -1571,6 +1587,9 @@
   (QVar l1 v1 _,QVar l2 v2 _) -> if l1==l2 && v1==v2
                                  then Just True
                                  else Nothing
+  (FunArg v1 _,FunArg v2 _) -> if v1==v2
+                               then Just True
+                               else Nothing
   (Const v1 _,Const v2 _) -> Just $ v1 == v2
   (AsArray f1 arg1,AsArray f2 arg2) -> case cast f2 of
     Nothing -> Nothing
diff --git a/Language/SMTLib2/Internals/Interface.hs b/Language/SMTLib2/Internals/Interface.hs
--- a/Language/SMTLib2/Internals/Interface.hs
+++ b/Language/SMTLib2/Internals/Interface.hs
@@ -12,7 +12,6 @@
 import Data.Array
 import Data.Unit
 import Data.List (genericReplicate)
-import Control.Monad.Trans (lift)
 import Data.Proxy
 
 -- | Check if the model is satisfiable (e.g. if there is a value for each variable so that every assertion holds)
@@ -25,9 +24,7 @@
 
 -- | Like 'checkSat', but gives you more options like choosing a tactic (Z3 only) or providing memory/time-limits
 checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult
-checkSat' tactic limits = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTCheckSat tactic limits)
+checkSat' tactic limits = smtBackend $ \b -> smtHandle b (SMTCheckSat tactic limits)
 
 isSat :: CheckSatResult -> Bool
 isSat Sat = True
@@ -36,21 +33,15 @@
 
 -- | Apply the given tactic to the current assertions. (Works only with Z3)
 apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]
-apply t = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTApply t)
+apply t = smtBackend $ \backend -> smtHandle backend (SMTApply t)
 
 -- | Push a new context on the stack
 push :: Monad m => SMT' m ()
-push = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st SMTPush
+push = smtBackend $ \b -> smtHandle b SMTPush
 
 -- | Pop a new context from the stack
 pop :: Monad m => SMT' m ()
-pop = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st SMTPop
+pop = smtBackend $ \b -> smtHandle b SMTPop
 
 -- | Perform a stacked operation, meaning that every assertion and declaration made in it will be undone after the operation.
 stack :: Monad m => SMT' m a -> SMT' m a
@@ -63,9 +54,7 @@
 -- | Insert a comment into the SMTLib2 command stream.
 --   If you aren't looking at the command stream for debugging, this will do nothing.
 comment :: Monad m => String -> SMT' m ()
-comment msg = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTComment msg)
+comment msg = smtBackend $ \b -> smtHandle b (SMTComment msg)
 
 -- | Create a new named variable
 varNamed :: (SMTType t,Typeable t,Unit (SMTAnnotation t),Monad m) => String -> SMT' m (SMTExpr t)
@@ -86,8 +75,8 @@
 -- | Create a fresh untyped variable with a name
 untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped)
 untypedNamedVar name sort = do
-  st <- getSMT
-  withSort (declaredDataTypes st) sort $
+  dts <- smtBackend $ \b -> smtHandle b SMTDeclaredDataTypes
+  withSort dts sort $
     \(_::t) ann -> do
       v <- varNamedAnn name ann
       return $ UntypedExpr (v::SMTExpr t)
@@ -95,8 +84,8 @@
 -- | Create a fresh untyped variable
 untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped)
 untypedVar sort = do
-  st <- getSMT
-  withSort (declaredDataTypes st) sort $
+  dts <- smtBackend $ \b -> smtHandle b SMTDeclaredDataTypes
+  withSort dts sort $
     \(_::t) ann -> do
       v <- varAnn ann
       return $ UntypedExpr (v::SMTExpr t)
@@ -113,15 +102,17 @@
 argVarsAnnNamed' :: (Args a,Monad m) => Maybe String -> ArgAnnotation a -> SMT' m a
 argVarsAnnNamed' name ann = do
   (_,arg) <- foldExprs (\_ (_::SMTExpr t) ann' -> do
-                           (res,info) <- newVariable name ann'
-                           smtBackend $ \backend -> do
-                             declareType (undefined::t) ann'
-                             st <- getSMT
-                             lift $ smtHandle backend st (SMTDeclareFun info)
-                             case additionalConstraints (undefined::t) ann' of
-                               Nothing -> return ()
-                               Just constr -> mapM_ assert $ constr res
-                           return ((),res)
+                           declareType (undefined::t) ann'
+                           let info = FunInfo { funInfoProxy = Proxy::Proxy ((),t)
+                                              , funInfoArgAnn = ()
+                                              , funInfoResAnn = ann'
+                                              , funInfoName = name }
+                           res <- smtBackend $ \b -> smtHandle b (SMTDeclareFun info)
+                           let expr = Var res ann'
+                           case additionalConstraints (undefined::t) ann' of
+                            Nothing -> return ()
+                            Just constr -> mapM_ assert $ constr expr
+                           return ((),expr)
                        ) () undefined ann
   return arg
 
@@ -138,18 +129,14 @@
 constantAnn x ann = Const x ann
 
 getValue :: (SMTValue t,Monad m) => SMTExpr t -> SMT' m t
-getValue expr = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTGetValue expr)
+getValue expr = smtBackend $ \b -> smtHandle b (SMTGetValue expr)
 
 getValues :: (LiftArgs arg,Monad m) => arg -> SMT' m (Unpacked arg)
 getValues args = unliftArgs args getValue
 
 -- | Extract all assigned values of the model
 getModel :: Monad m => SMT' m SMTModel
-getModel = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st SMTGetModel
+getModel = smtBackend $ \b -> smtHandle b SMTGetModel
 
 -- | Extract all values of an array by giving the range of indices.
 unmangleArray :: (Liftable i,LiftArgs i,Ix (Unpacked i),SMTValue v,
@@ -176,12 +163,9 @@
 defConstNamed name = defConstNamed' (Just name)
 
 defConstNamed' :: (SMTType r,Monad m) => Maybe String -> SMTExpr r -> SMT' m (SMTExpr r)
-defConstNamed' name e = smtBackend $ \backend -> do
-  let ann = extractAnnotation e
-  (fun,info) <- newVariable name ann
-  st <- getSMT
-  lift $ smtHandle backend st (SMTDefineFun info [] e)
-  return fun
+defConstNamed' name e = do
+  i <- smtBackend $ \b -> smtHandle b (SMTDefineFun name (Proxy::Proxy ()) () e)
+  return (Var i (extractAnnotation e))
 
 -- | Define a new function with a body and custom type annotations for arguments and result.
 defFunAnnNamed :: (Args a,SMTType r,Monad m)
@@ -189,16 +173,13 @@
 defFunAnnNamed name = defFunAnnNamed' (Just name)
 
 defFunAnnNamed' :: (Args a,SMTType r,Monad m)
-                  => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)
-defFunAnnNamed' name ann_arg f = smtBackend $ \backend -> do
-  (au,tps) <- createArgs' ann_arg
-  let body = f au
-      ann_res = extractAnnotation body
-  
-  (fun,info) <- newFunction name ann_arg ann_res
-  st <- getSMT
-  lift $ smtHandle backend st (SMTDefineFun info tps body)
-  return fun
+                => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r)
+                -> SMT' m (SMTFunction a r)
+defFunAnnNamed' name ann_arg (f::a -> SMTExpr r) = do
+  let (_,rargs) = foldExprsId (\i _ ann -> (i+1,FunArg i ann)) 0 (undefined::a) ann_arg
+      body = f rargs
+  i <- smtBackend $ \b -> smtHandle b (SMTDefineFun name (Proxy::Proxy a) ann_arg body)
+  return (SMTFun i (extractAnnotation body))
 
 -- | Like `defFunAnnNamed`, but defaults the function name to "fun".
 defFunAnn :: (Args a,SMTType r,Monad m)
@@ -230,49 +211,33 @@
 
 -- | Asserts that a boolean expression is true
 assert :: Monad m => SMTExpr Bool -> SMT' m ()
-assert expr = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTAssert expr Nothing Nothing)
+assert expr = smtBackend $ \b -> smtHandle b (SMTAssert expr Nothing Nothing)
 
 -- | Create a new interpolation group
 interpolationGroup :: Monad m => SMT' m InterpolationGroup
-interpolationGroup = do
-  st <- getSMT
-  let intgr = nextInterpolationGroup st
-  putSMT $ st { nextInterpolationGroup = succ intgr }
-  return (InterpolationGroup intgr)
+interpolationGroup = smtBackend $ \b -> smtHandle b SMTNewInterpolationGroup
 
 -- | Assert a boolean expression and track it for an unsat core call later
 assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId
-assertId expr = smtBackend $ \backend -> do
-  st <- getSMT
-  let cid = nextClauseId st
-  putSMT $ st { nextClauseId = succ cid }
-  lift $ smtHandle backend st (SMTAssert expr Nothing (Just $ ClauseId cid))
-  return (ClauseId cid)
+assertId expr = smtBackend $ \b -> do
+  (cid,b1) <- smtHandle b SMTNewClauseId
+  ((),b2) <- smtHandle b1 (SMTAssert expr Nothing (Just cid))
+  return (cid,b2)
 
 -- | Assert a boolean expression to be true and assign it to an interpolation group
 assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()
-assertInterp expr interp = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTAssert expr (Just interp) Nothing)
+assertInterp expr interp = smtBackend $ \b -> smtHandle b (SMTAssert expr (Just interp) Nothing)
 
 getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)
-getInterpolant grps = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTGetInterpolant grps)
+getInterpolant grps = smtBackend $ \b -> smtHandle b (SMTGetInterpolant grps)
 
 -- | Set an option for the underlying SMT solver
 setOption :: Monad m => SMTOption -> SMT' m ()
-setOption opt = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTSetOption opt)
+setOption opt = smtBackend $ \b -> smtHandle b (SMTSetOption opt)
 
 -- | Get information about the underlying SMT solver
 getInfo :: (Monad m,Typeable i) => SMTInfo i -> SMT' m i
-getInfo inf = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTGetInfo inf)
+getInfo inf = smtBackend $ \b -> smtHandle b (SMTGetInfo inf)
 
 -- | Create a new uniterpreted function with annotations for
 --   the argument and the return type.
@@ -285,18 +250,26 @@
 funAnnNamed name = funAnnNamed' (Just name)
 
 funAnnNamed' :: (Liftable a, SMTType r,Monad m) => Maybe String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)
-funAnnNamed' name annArg annRet = smtBackend $ \backend -> do
-  (fun,info) <- newFunction name annArg annRet
-  st <- getSMT
-  lift $ smtHandle backend st (SMTDeclareFun info)
-  case additionalConstraints (undefined::t) annRet of
-    Nothing -> return ()
-    Just constr -> assert $ forAllAnn annArg
-                   (\x -> case constr (fun `app` x) of
-                       [] -> constant True
-                       [x] -> x
-                       xs -> and' `app` xs)
-  return fun
+funAnnNamed' name annArg annRet
+  = withUndef $ \(_::a) (_::r) -> do
+    let finfo = FunInfo { funInfoProxy = Proxy::Proxy (a,r)
+                        , funInfoArgAnn = annArg
+                        , funInfoResAnn = annRet
+                        , funInfoName = name
+                        }
+    i <- smtBackend $ \b -> smtHandle b (SMTDeclareFun finfo)
+    let fun = SMTFun i annRet
+    case additionalConstraints (undefined::t) annRet of
+     Nothing -> return ()
+     Just constr -> assert $ forAllAnn annArg
+                    (\x -> case constr (fun `app` x) of
+                            [] -> constant True
+                            [x] -> x
+                            xs -> and' `app` xs)
+    return fun
+  where
+    withUndef :: (a -> r -> SMT' m (SMTFunction a r)) -> SMT' m (SMTFunction a r)
+    withUndef f = f undefined undefined
 
 -- | funAnn with an annotation only for the return type.
 funAnnRet :: (Liftable a,SMTType r,Unit (ArgAnnotation a),Monad m)
@@ -667,17 +640,14 @@
 
 -- | Sets the logic used for the following program (Not needed for many solvers).
 setLogic :: Monad m => String -> SMT' m ()
-setLogic name = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTSetLogic name)
+setLogic name = smtBackend $ \b -> smtHandle b (SMTSetLogic name)
 
 -- | Given an arbitrary expression, this creates a named version of it and a name to reference it later on.
 named :: (SMTType a,SMTAnnotation a ~ (),Monad m)
          => String -> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a)
 named name expr = do
-  (var,info) <- newVariable (Just name) (extractAnnotation expr)
-  let Just (name,nc) = funInfoName info
-  return (Named expr name nc,var)
+  i <- smtBackend $ \b -> smtHandle b (SMTNameExpr name expr)
+  return (Named expr name i,Var i (extractAnnotation expr))
 
 -- | Like `named`, but defaults the name to "named".
 named' :: (SMTType a,SMTAnnotation a ~ (),Monad m)
@@ -686,23 +656,17 @@
   
 -- | After an unsuccessful 'checkSat' this method extracts a proof from the SMT solver that the instance is unsatisfiable.
 getProof :: Monad m => SMT' m (SMTExpr Bool)
-getProof = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st SMTGetProof
+getProof = smtBackend $ \b -> smtHandle b SMTGetProof
 
 -- | Use the SMT solver to simplify a given expression.
 --   Currently only works with Z3.
 simplify :: (SMTType t,Monad m) => SMTExpr t -> SMT' m (SMTExpr t)
-simplify expr = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st (SMTSimplify expr)
+simplify expr = smtBackend $ \b -> smtHandle b (SMTSimplify expr)
 
 -- | After an unsuccessful 'checkSat', return a list of clauses which make the
 --   instance unsatisfiable.
 getUnsatCore :: Monad m => SMT' m [ClauseId]
-getUnsatCore = smtBackend $ \backend -> do
-  st <- getSMT
-  lift $ smtHandle backend st SMTGetUnsatCore
+getUnsatCore = smtBackend $ \b -> smtHandle b SMTGetUnsatCore
   
 optimizeExpr' :: SMTExpr a -> SMTExpr a
 optimizeExpr' e = case optimizeExpr e of
diff --git a/Language/SMTLib2/Internals/Optimize.hs b/Language/SMTLib2/Internals/Optimize.hs
--- a/Language/SMTLib2/Internals/Optimize.hs
+++ b/Language/SMTLib2/Internals/Optimize.hs
@@ -14,42 +14,50 @@
 data OptimizeBackend b = OptB b
 
 instance SMTBackend b m => SMTBackend (OptimizeBackend b) m where
-  smtHandle (OptB b) st (SMTAssert expr grp cid)
+  smtHandle (OptB b) (SMTAssert expr grp cid)
     = let nexpr = case optimizeExpr expr of
             Just e -> e
             Nothing -> expr
       in case nexpr of
-        Const True _ -> return ()
-        _ -> smtHandle b st (SMTAssert nexpr grp cid)
-  smtHandle (OptB b) st (SMTDefineFun name args body)
-    = let nbody = case optimizeExpr body of
-            Just e -> e
-            Nothing -> body
-      in smtHandle b st (SMTDefineFun name args nbody)
-  smtHandle (OptB b) st (SMTGetValue expr)
-    = let nexpr = case optimizeExpr expr of
-            Just e -> e
-            Nothing -> expr
-      in smtHandle b st (SMTGetValue nexpr)
-  smtHandle (OptB b) st SMTGetProof = do
-    res <- smtHandle b st SMTGetProof
-    case optimizeExpr res of
-      Just e -> return e
-      Nothing -> return res
-  smtHandle (OptB b) st (SMTSimplify expr) = do
+        Const True _ -> return ((),OptB b)
+        _ -> do
+          (res,nb) <- smtHandle b (SMTAssert nexpr grp cid)
+          return (res,OptB nb)
+  smtHandle (OptB b) (SMTDefineFun name prx ann body) = do
+    let nbody = case optimizeExpr body of
+                 Just e -> e
+                 Nothing -> body
+    (res,nb) <- smtHandle b (SMTDefineFun name prx ann nbody)
+    return (res,OptB nb)
+  smtHandle (OptB b) (SMTGetValue expr) = do
     let nexpr = case optimizeExpr expr of
+                 Just e -> e
+                 Nothing -> expr
+    (res,nb) <- smtHandle b (SMTGetValue nexpr)
+    return (res,OptB nb)
+  smtHandle (OptB b) SMTGetProof = do
+    (res,nb) <- smtHandle b SMTGetProof
+    return (case optimizeExpr res of
+             Just e -> e
+             Nothing -> res,OptB nb)
+  smtHandle (OptB b) (SMTSimplify expr) = do
+    let nexpr = case optimizeExpr expr of
           Just e -> e
           Nothing -> expr
-    simp <- smtHandle b st (SMTSimplify nexpr)
-    case optimizeExpr simp of
-      Nothing -> return simp
-      Just simp' -> return simp'
-  smtHandle (OptB b) st (SMTGetInterpolant grps) = do
-    inter <- smtHandle b st (SMTGetInterpolant grps)
-    case optimizeExpr inter of
-      Nothing -> return inter
-      Just e -> return e
-  smtHandle (OptB b) st req = smtHandle b st req
+    (simp,nb) <- smtHandle b (SMTSimplify nexpr)
+    return (case optimizeExpr simp of
+             Nothing -> simp
+             Just simp' -> simp',OptB nb)
+  smtHandle (OptB b) (SMTGetInterpolant grps) = do
+    (inter,nb) <- smtHandle b (SMTGetInterpolant grps)
+    return (case optimizeExpr inter of
+             Nothing -> inter
+             Just e -> e,OptB nb)
+  smtHandle (OptB b) req = do
+    (res,nb) <- smtHandle b req
+    return (res,OptB nb)
+  smtGetNames (OptB b) = smtGetNames b
+  smtNextName (OptB b) = smtNextName b
 
 optimizeExpr :: SMTExpr t -> Maybe (SMTExpr t)
 optimizeExpr (App fun x) = let (opt,x') = foldExprsId (\opt expr ann -> case optimizeExpr expr of
@@ -61,7 +69,6 @@
                                         then Just $ App fun x'
                                         else Nothing
                              Just res -> Just res
-
 optimizeExpr _ = Nothing
 
 optimizeCall :: SMTFunction arg res -> arg -> Maybe (SMTExpr res)
diff --git a/Language/SMTLib2/Pipe.hs b/Language/SMTLib2/Pipe.hs
--- a/Language/SMTLib2/Pipe.hs
+++ b/Language/SMTLib2/Pipe.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE ViewPatterns #-}
 module Language.SMTLib2.Pipe
        (SMTPipe(),
-        FunctionParser(),
+        FunctionParser(..),
         createSMTPipe,
         withPipe,
         exprToLisp,
@@ -13,7 +13,9 @@
         renderSMTRequest,
         renderSMTResponse,
         commonFunctions,
-        commonTheorems) where
+        commonTheorems,
+        simpleParser,
+        FunctionParser'(..)) where
 
 import Language.SMTLib2.Internals as SMT
 import Language.SMTLib2.Internals.Instances
@@ -33,7 +35,6 @@
 import qualified Data.ByteString.Char8 as BS8
 import Blaze.ByteString.Builder
 import Data.Typeable
-import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Fix
 import Data.Proxy
@@ -51,46 +52,64 @@
      process. -}
 data SMTPipe = SMTPipe { channelIn :: Handle
                        , channelOut :: Handle
-                       , processHandle :: ProcessHandle }
+                       , processHandle :: ProcessHandle
+                       , smtState :: SMTState }
 
 renderExpr :: (SMTType t,Monad m) => SMTExpr t -> SMT' m String
-renderExpr expr = do
-  st <- getSMT
-  return $ renderExpr' st expr
-  
-renderExpr' :: SMTType t => SMTState -> SMTExpr t -> String
-renderExpr' st expr
-  = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st)
+renderExpr expr = smtBackend $ \b -> do
+  getName <- smtGetNames b
+  (dts,nb) <- smtHandle b SMTDeclaredDataTypes
+  return (renderExpr' getName dts expr,nb)
+
+renderExpr' :: SMTType t => (Integer -> String) -> DataTypeInfo -> SMTExpr t -> String
+renderExpr' getName dts expr
+  = let lexpr = exprToLisp expr getName dts
     in show lexpr
 
 instance MonadIO m => SMTBackend SMTPipe m where
-  smtHandle pipe st req@(SMTGetValue (expr::SMTExpr t))
+  smtHandle pipe req@(SMTGetValue (expr::SMTExpr t))
     = case unmangle :: Unmangling t of
-       PrimitiveUnmangling _ -> handleNormal pipe st req
+       PrimitiveUnmangling _ -> handleNormal pipe req
        ComplexUnmangling f -> do
-         res <- f (\expr' ann -> smtHandle pipe st (SMTGetValue expr')) expr (extractAnnotation expr)
+         (res,npipe) <- f (\pipe expr' ann -> smtHandle pipe (SMTGetValue expr')
+                          ) pipe expr (extractAnnotation expr)
          case res of
-          Just x -> return x
+          Just x -> return (x,npipe)
           Nothing -> error $ "smtlib2: Error while unmangling expression "++show expr++" to type "++show (typeOf (undefined::t))
-  smtHandle pipe st req = handleNormal pipe st req
+  smtHandle pipe req = handleNormal pipe req
+  --smtGetState pipe = return $ smtState pipe
+  smtGetNames pipe = return (\idx -> case Map.lookup idx (allVars (smtState pipe)) of
+                              Just (info,nc) -> case funInfoName info of
+                                Nothing -> escapeName (Right idx)
+                                Just name -> escapeName (Left (name,nc)))
+  smtNextName pipe = return (\name -> case name of
+                              Nothing -> let nxt = nextVar (smtState pipe)
+                                         in escapeName (Right nxt)
+                              Just name' -> case Map.lookup name' (nameCount (smtState pipe)) of
+                                Just nc -> escapeName (Left (name',nc))
+                                Nothing -> escapeName (Left (name',0)))
 
-handleNormal :: (MonadIO m,Typeable a) => SMTPipe -> SMTState -> SMTRequest a -> m a
-handleNormal pipe st req = do
+handleNormal :: (MonadIO m,Typeable a) => SMTPipe -> SMTRequest a -> m (a,SMTPipe)
+handleNormal pipe req = do
   case cast req of
    Just (_::SMTRequest ()) -> return ()
    _ -> clearInput pipe
-  case renderSMTRequest st req of
+  getName <- smtGetNames pipe
+  nxtName <- smtNextName pipe
+  case renderSMTRequest nxtName getName (declaredDataTypes $ smtState pipe) req of
    Left l -> putRequest pipe l
+   Right "" -> return ()
    Right msg -> liftIO $ IO.hPutStr (channelIn pipe) $ Prelude.unlines (fmap (';':) (Prelude.lines msg))
-  handleRequest pipe st req
+  handleRequest pipe req
 
-renderSMTRequest :: SMTState -> SMTRequest r -> Either L.Lisp String
-renderSMTRequest st (SMTGetInfo SMTSolverName)
+renderSMTRequest :: (Maybe String -> String) -> (Integer -> String) -> DataTypeInfo
+                 -> SMTRequest r -> Either L.Lisp String
+renderSMTRequest _ _ _ (SMTGetInfo SMTSolverName)
   = Left $ L.List [L.Symbol "get-info",L.Symbol ":name"]
-renderSMTRequest st (SMTGetInfo SMTSolverVersion)
+renderSMTRequest _ _ _ (SMTGetInfo SMTSolverVersion)
   = Left $ L.List [L.Symbol "get-info",L.Symbol ":version"]
-renderSMTRequest st (SMTAssert expr interp cid)
-  = let expr1 = exprToLisp expr (allVars st) (declaredDataTypes st)
+renderSMTRequest _ getName dts (SMTAssert expr interp cid)
+  = let expr1 = exprToLisp expr getName dts
         expr2 = case interp of
           Nothing -> expr1
           Just (InterpolationGroup gr)
@@ -106,7 +125,7 @@
                       ,L.Symbol ":named"
                       ,L.Symbol (T.pack $ "_cid"++show cid)]
     in Left $ L.List [L.Symbol "assert",expr3]
-renderSMTRequest st (SMTCheckSat tactic limits)
+renderSMTRequest _ _ _ (SMTCheckSat tactic limits)
   = Left $ L.List (if extendedCheckSat
                    then [L.Symbol "check-sat-using"
                         ,case tactic of
@@ -129,7 +148,8 @@
         _ -> case limitMemory limits of
           Just _ -> True
           _ -> False
-renderSMTRequest st (SMTDeclareDataTypes dts)
+renderSMTRequest _ _ _ SMTDeclaredDataTypes = Right ""
+renderSMTRequest _ _ _ (SMTDeclareDataTypes dts)
   = let param x = L.Symbol $ T.pack $ "arg"++show x
     in Left $
        L.List [L.Symbol "declare-datatypes"
@@ -147,109 +167,127 @@
                     | con <- dataTypeConstructors dt ]
                | dt <- dataTypes dts ]
               ]
-renderSMTRequest st (SMTDeclareSort name arity)
+renderSMTRequest _ _ _ (SMTDeclareSort name arity)
   = Left $ L.List [L.Symbol "declare-sort",L.Symbol $ T.pack name,L.toLisp arity]
-renderSMTRequest st (SMTDeclareFun name)
-  = let tps = funInfoArgSorts name
-        rtp = funInfoSort name
+renderSMTRequest nextName _ _ (SMTDeclareFun finfo)
+  = let tps = funInfoArgSorts finfo
+        rtp = funInfoSort finfo
     in Left $ L.List [L.Symbol "declare-fun"
-                     ,L.Symbol $ T.pack $ getSMTName name
+                     ,L.Symbol $ T.pack (nextName (funInfoName finfo))
                      ,args (fmap sortToLisp tps)
                      ,sortToLisp rtp
                      ]
-renderSMTRequest st (SMTDefineFun name arg definition)
-  = let ann = extractAnnotation definition
-        retSort = getSort (getUndef definition) ann
+renderSMTRequest nextName getName dts (SMTDefineFun name (_::Proxy arg) argAnn (body::SMTExpr res))
+  = let tpLst = zip [0..] (getTypes (undefined::arg) argAnn)
+        annRes = extractAnnotation body
+        name' = nextName name
+        retSort = getSort (undefined::res) annRes
     in Left $ L.List [L.Symbol "define-fun"
-                     ,L.Symbol $ T.pack $ getSMTName name
-                     ,args [ L.List [ L.Symbol $ T.pack $ getSMTName n, sortToLisp $ funInfoSort n ]
-                           | n <- arg ]
+                     ,L.Symbol $ T.pack name'
+                     ,args [ L.List [ L.Symbol $ T.pack $ "farg_"++show (j::Integer)
+                                    , sortToLisp $ getSort u ann ]
+                           | (j,ProxyArg u ann) <- tpLst ]
                      ,sortToLisp retSort
-                     ,exprToLisp definition (allVars st) (declaredDataTypes st)]
-renderSMTRequest st (SMTComment msg) = Right msg
-renderSMTRequest st SMTExit = Left $ L.List [L.Symbol "exit"]
-renderSMTRequest st (SMTGetInterpolant grps)
+                     ,exprToLisp body getName dts]
+renderSMTRequest _ _ _ (SMTComment msg) = Right msg
+renderSMTRequest _ _ _ SMTExit = Left $ L.List [L.Symbol "exit"]
+renderSMTRequest _ _ _ (SMTGetInterpolant grps)
   = Left $ L.List [L.Symbol "get-interpolant"
                   ,L.List [ L.Symbol $ T.pack ("i"++show g) | InterpolationGroup g <- grps ]
                   ]
-renderSMTRequest st (SMTSetOption opt)
+renderSMTRequest _ _ _ (SMTSetOption opt)
   = Left $ L.List $ [L.Symbol "set-option"]
     ++(case opt of
-          PrintSuccess v -> [L.Symbol ":print-success"
-                            ,L.Symbol $ if v then "true" else "false"]
-          ProduceModels v -> [L.Symbol ":produce-models"
-                             ,L.Symbol $ if v then "true" else "false"]
-          SMT.ProduceProofs v -> [L.Symbol ":produce-proofs"
-                                 ,L.Symbol $ if v then "true" else "false"]
-          SMT.ProduceUnsatCores v -> [L.Symbol ":produce-unsat-cores"
-                                     ,L.Symbol $ if v then "true" else "false"]
-          ProduceInterpolants v -> [L.Symbol ":produce-interpolants"
+        PrintSuccess v -> [L.Symbol ":print-success"
+                          ,L.Symbol $ if v then "true" else "false"]
+        ProduceModels v -> [L.Symbol ":produce-models"
+                           ,L.Symbol $ if v then "true" else "false"]
+        SMT.ProduceProofs v -> [L.Symbol ":produce-proofs"
+                               ,L.Symbol $ if v then "true" else "false"]
+        SMT.ProduceUnsatCores v -> [L.Symbol ":produce-unsat-cores"
                                    ,L.Symbol $ if v then "true" else "false"]
+        ProduceInterpolants v -> [L.Symbol ":produce-interpolants"
+                                 ,L.Symbol $ if v then "true" else "false"]
       )
-renderSMTRequest st (SMTSetLogic name)
+renderSMTRequest _ _ _ (SMTSetLogic name)
   = Left $ L.List [L.Symbol "set-logic"
                   ,L.Symbol $ T.pack name]
-renderSMTRequest st SMTGetProof
+renderSMTRequest _ _ _ SMTGetProof
   = Left $ L.List [L.Symbol "get-proof"]
-renderSMTRequest st SMTGetUnsatCore
+renderSMTRequest _ _ _ SMTGetUnsatCore
   = Left $ L.List [L.Symbol "get-unsat-core"]
-renderSMTRequest st (SMTSimplify expr)
-  = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st)
+renderSMTRequest _ getName dts (SMTSimplify expr)
+  = let lexpr = exprToLisp expr getName dts
     in Left $ L.List [L.Symbol "simplify"
                      ,lexpr]
-renderSMTRequest st SMTPush = Left $ L.List [L.Symbol "push",L.toLisp (1::Integer)]
-renderSMTRequest st SMTPop = Left $ L.List [L.Symbol "pop",L.toLisp (1::Integer)]
-renderSMTRequest st (SMTGetValue expr)
-  = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st)
+renderSMTRequest _ _ _ SMTPush = Left $ L.List [L.Symbol "push",L.toLisp (1::Integer)]
+renderSMTRequest _ _ _ SMTPop = Left $ L.List [L.Symbol "pop",L.toLisp (1::Integer)]
+renderSMTRequest _ getName dts (SMTGetValue expr)
+  = let lexpr = exprToLisp expr getName dts
     in Left $ L.List [L.Symbol "get-value"
                      ,L.List [lexpr]]
-renderSMTRequest st SMTGetModel = Left $ L.List [L.Symbol "get-model"]
-renderSMTRequest st (SMTApply tactic)
+renderSMTRequest _ _ _ SMTGetModel = Left $ L.List [L.Symbol "get-model"]
+renderSMTRequest _ _ _ (SMTApply tactic)
   = Left $ L.List [L.Symbol "apply"
                   ,tacticToLisp tactic]
+renderSMTRequest _ _ _ (SMTNameExpr _ _) = Right ""
+renderSMTRequest _ _ _ SMTNewInterpolationGroup = Right ""
+renderSMTRequest _ _ _ SMTNewClauseId = Right ""
 
-handleRequest :: MonadIO m => SMTPipe -> SMTState -> SMTRequest response -> m response
-handleRequest pipe _ (SMTGetInfo SMTSolverName) = do
+handleRequest :: MonadIO m => SMTPipe -> SMTRequest response -> m (response,SMTPipe)
+handleRequest pipe (SMTGetInfo SMTSolverName) = do
   res <- parseResponse pipe
   case res of
-    L.List [L.Symbol ":name",L.String name] -> return $ T.unpack name
+    L.List [L.Symbol ":name",L.String name] -> return (T.unpack name,pipe)
     _ -> error "Invalid solver response to 'get-info' name query"
-handleRequest pipe _ (SMTGetInfo SMTSolverVersion) = do
+handleRequest pipe (SMTGetInfo SMTSolverVersion) = do
   res <- parseResponse pipe
   case res of
-    L.List [L.Symbol ":version",L.String name] -> return $ T.unpack name
+    L.List [L.Symbol ":version",L.String name] -> return (T.unpack name,pipe)
     _ -> error "Invalid solver response to 'get-info' version query"
-handleRequest pipe st (SMTAssert _ _ _) = return ()
-handleRequest pipe _ (SMTCheckSat tactic limits) = do
+handleRequest pipe (SMTAssert _ _ _) = return ((),pipe)
+handleRequest pipe (SMTCheckSat tactic limits) = do
   res <- liftIO $ BS.hGetLine (channelOut pipe)
-  case res of
-    "sat" -> return Sat
-    "sat\r" -> return Sat
-    "unsat" -> return Unsat
-    "unsat\r" -> return Unsat
-    "unknown" -> return Unknown
-    "unknown\r" -> return Unknown
-    _ -> error $ "smtlib2: unknown check-sat response: "++show res
-handleRequest pipe _ (SMTDeclareDataTypes dts) = return ()
-handleRequest pipe _ (SMTDeclareSort name arity) = return ()
-handleRequest pipe _ (SMTDeclareFun name) = return ()
-handleRequest _ _ (SMTDefineFun name arg definition) = return ()
-handleRequest _ _ (SMTComment msg) = return ()
-handleRequest pipe _ SMTExit = do
+  return (case res of
+           "sat" -> Sat
+           "sat\r" -> Sat
+           "unsat" -> Unsat
+           "unsat\r" -> Unsat
+           "unknown" -> Unknown
+           "unknown\r" -> Unknown
+           _ -> error $ "smtlib2: unknown check-sat response: "++show res,pipe)
+handleRequest pipe SMTDeclaredDataTypes = return (declaredDataTypes $ smtState pipe,pipe)
+handleRequest pipe (SMTDeclareDataTypes dts) = do
+  let ndts = addDataTypeStructure dts (declaredDataTypes $ smtState pipe)
+  return ((),pipe { smtState = (smtState pipe) { declaredDataTypes = ndts } })
+handleRequest pipe (SMTDeclareSort name arity) = return ((),pipe)
+handleRequest pipe (SMTDeclareFun info)
+  = let (v,name,nst) = smtStateAddFun info (smtState pipe)
+    in return (v,pipe { smtState = nst })
+handleRequest pipe (SMTDefineFun name (_::Proxy arg) argAnn (body::SMTExpr res)) = do
+  let finfo = FunInfo { funInfoProxy = Proxy::Proxy (arg,res)
+                      , funInfoArgAnn = argAnn
+                      , funInfoResAnn = extractAnnotation body
+                      , funInfoName = name }
+      (i,_,nst) = smtStateAddFun finfo (smtState pipe)
+  return (i,pipe { smtState = nst })
+handleRequest pipe (SMTComment msg) = return ((),pipe)
+handleRequest pipe SMTExit = do
   liftIO $ hClose (channelIn pipe)
   liftIO $ hClose (channelOut pipe)
   liftIO $ terminateProcess (processHandle pipe)
   _ <- liftIO $ waitForProcess (processHandle pipe)
-  return ()
-handleRequest pipe st (SMTGetInterpolant grps) = do
+  return ((),pipe)
+handleRequest pipe (SMTGetInterpolant grps) = do
   val <- parseResponse pipe
   case lispToExpr commonFunctions
-       (findName st) (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 val of
-    Just (Just x) -> return x
+       (findName $ smtState pipe) (declaredDataTypes $ smtState pipe)
+       gcast (Just $ Fix BoolSort) 0 val of
+    Just (Just x) -> return (x,pipe)
     _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val
-handleRequest _ _ (SMTSetOption opt) = return ()
-handleRequest _ _ (SMTSetLogic name) = return ()
-handleRequest pipe st SMTGetProof = do
+handleRequest pipe (SMTSetOption opt) = return ((),pipe)
+handleRequest pipe (SMTSetLogic name) = return ((),pipe)
+handleRequest pipe SMTGetProof = do
   res <- parseResponse pipe
   let proof = case res of
         L.List items -> case findProof items of
@@ -257,36 +295,37 @@
           Just p -> p
         _ -> res
   case lispToExpr (commonFunctions `mappend` commonTheorems)
-       (findName st)
-       (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 proof of
-    Just (Just x) -> return x
+       (findName $ smtState pipe)
+       (declaredDataTypes $ smtState pipe) gcast (Just $ Fix BoolSort) 0 proof of
+    Just (Just x) -> return (x,pipe)
     _ -> error $ "smtlib2: Couldn't parse proof "++show res
   where
     findProof [] = Nothing
     findProof ((L.List [L.Symbol "proof",proof]):_) = Just proof
     findProof (x:xs) = findProof xs
-handleRequest pipe _ SMTGetUnsatCore = do
+handleRequest pipe SMTGetUnsatCore = do
   res <- parseResponse pipe
   case res of
-    L.List names -> return $
-                    fmap (\name -> case name of
-                             L.Symbol s -> case T.unpack s of
-                               '_':'c':'i':'d':cid
-                                 | all isDigit cid -> ClauseId (read cid)
-                               str -> error $ "Language.SMTLib2.getUnsatCore: Unknown clause id "++str
-                             _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown expression "
-                                  ++show name++" in core list."
-                         ) names
+    L.List names -> return
+                    (fmap (\name -> case name of
+                            L.Symbol s -> case T.unpack s of
+                              '_':'c':'i':'d':cid
+                                | all isDigit cid -> ClauseId (read cid)
+                              str -> error $ "Language.SMTLib2.getUnsatCore: Unknown clause id "++str
+                            _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown expression "
+                                 ++show name++" in core list."
+                          ) names,pipe)
     _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown response "++show res++" to query."
-handleRequest pipe st (SMTSimplify (expr::SMTExpr t)) = do
+handleRequest pipe (SMTSimplify (expr::SMTExpr t)) = do
   val <- parseResponse pipe
   case lispToExpr commonFunctions
-       (findName st) (declaredDataTypes st) gcast (Just $ getSort (undefined::t) (extractAnnotation expr)) 0 val of
-    Just (Just x) -> return x
+       (findName $ smtState pipe) (declaredDataTypes $ smtState pipe)
+       gcast (Just $ getSort (undefined::t) (extractAnnotation expr)) 0 val of
+    Just (Just x) -> return (x,pipe)
     _ -> error $ "smtlib2: Failed to parse simplify result: "++show val
-handleRequest _ _ SMTPush = return ()
-handleRequest _ _ SMTPop = return ()
-handleRequest pipe st (SMTGetValue (expr::SMTExpr t)) = do
+handleRequest pipe SMTPush = return ((),pipe)
+handleRequest pipe SMTPop = return ((),pipe)
+handleRequest pipe (SMTGetValue (expr::SMTExpr t)) = do
   let ann = extractAnnotation expr
       sort = getSort (undefined::t) ann
       PrimitiveUnmangling unm = unmangle :: Unmangling t
@@ -294,16 +333,16 @@
   case val of
     L.List [L.List [_,res]]
       -> let res' = removeLets res
-         in case lispToValue' (declaredDataTypes st) (Just sort) res' of
+         in case lispToValue' (declaredDataTypes $ smtState pipe) (Just sort) res' of
            Just val' -> case unm val' ann of
-             Just val'' -> return val''
+             Just val'' -> return (val'',pipe)
              Nothing -> error $ "smtlib2: Failed to unmangle value "++show val'++" to type "++show (typeOf (undefined::t))
            Nothing -> error $ "smtlib2: Failed to parse value from "++show res
     _ -> error $ "smtlib2: Unexpected get-value response: "++show val
-handleRequest pipe st SMTGetModel = do
+handleRequest pipe SMTGetModel = do
   val <- parseResponse pipe
   case val of
-   L.List (L.Symbol "model":mdl) -> return $ foldl parseModel (SMTModel Map.empty) mdl
+   L.List (L.Symbol "model":mdl) -> return (foldl parseModel (SMTModel Map.empty) mdl,pipe)
    _ -> error $ "smtlib2: Unexpected get-model response: "++show val
   where
     parseModel cur (L.List [L.Symbol "define-fun",
@@ -313,7 +352,7 @@
                             fun]) = case mapM (\arg -> case arg of
                                                 L.List [L.Symbol argName,
                                                         argTp] -> case lispToSort argTp of
-                                                  Just argTp' -> withSort (declaredDataTypes st) argTp' $
+                                                  Just argTp' -> withSort (declaredDataTypes $ smtState pipe ) argTp' $
                                                                  \u ann -> Just (argName,ProxyArg u ann)
                                                   _ -> Nothing
                                                 _ -> Nothing
@@ -324,13 +363,13 @@
                          funId = case unescapeName (T.unpack fname) of
                            Nothing -> Nothing
                            Just (Right idx) -> Just idx
-                           Just (Left name) -> case Map.lookup name (namedVars st) of
+                           Just (Left name) -> case Map.lookup name (namedVars $ smtState pipe) of
                              Just idx -> Just idx
                              Nothing -> Nothing
                      in case lispToExpr commonFunctions (\n -> do
                                                             (i,tp) <- Map.lookup n argMp
                                                             return $ QVar 0 i tp)
-                             (declaredDataTypes st)
+                             (declaredDataTypes $ smtState pipe)
                              UntypedExpr
                              (Just rtp')
                              1
@@ -343,45 +382,62 @@
         Nothing -> error $ "smtlib2: Failed to parse return type: "++show rtp
       Nothing -> error $ "smtlib2: Failed to parse argument specification "++show args
     parseModel _ def = error $ "smtlib2: Failed to parse model entry: "++show def
-handleRequest pipe st (SMTApply tactic) = do
+handleRequest pipe (SMTApply tactic) = do
   val <- parseResponse pipe
   case val of
     L.List (L.Symbol "goals":goals)
-      -> return $
-         fmap (\goal -> case goal of
-                  L.List ((L.Symbol "goal"):expr:_)
-                    -> case lispToExpr (commonFunctions `mappend` commonTheorems)
-                            (findName st)
-                            (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 expr of
-                         Just (Just x) -> x
-                         _ -> error $ "smtlib2: Couldn't parse goal "++show expr
-                  _ -> error $ "smtlib2: Couldn't parse goal description "++show val
-              ) goals
+      -> return
+         (fmap (\goal -> case goal of
+                 L.List ((L.Symbol "goal"):expr:_)
+                   -> case lispToExpr (commonFunctions `mappend` commonTheorems)
+                           (findName $ smtState pipe)
+                           (declaredDataTypes $ smtState pipe) gcast (Just $ Fix BoolSort) 0 expr of
+                       Just (Just x) -> x
+                       _ -> error $ "smtlib2: Couldn't parse goal "++show expr
+                 _ -> error $ "smtlib2: Couldn't parse goal description "++show val
+               ) goals,pipe)
+handleRequest pipe (SMTNameExpr name expr) = do
+  return (nc,pipe { smtState = nst })
+  where
+    nc = case Map.lookup name (nameCount $ smtState pipe) of
+      Just n -> n
+      Nothing -> 0
+    nst = (smtState pipe) { nameCount = Map.insert name (nc+1) (nameCount $ smtState pipe) }
+handleRequest pipe SMTNewInterpolationGroup = do
+  return (InterpolationGroup igrp,pipe { smtState = nst })
+  where
+    igrp = nextInterpolationGroup (smtState pipe)
+    nst = (smtState pipe) { nextInterpolationGroup = igrp+1 }
+handleRequest pipe SMTNewClauseId = do
+  return (ClauseId icl,pipe { smtState = nst })
+  where
+    icl = nextClauseId (smtState pipe)
+    nst = (smtState pipe) { nextClauseId = icl+1 }
 
-renderSMTResponse :: SMTState -> SMTRequest response -> response -> Maybe String
-renderSMTResponse _ (SMTGetInfo SMTSolverName) name
+renderSMTResponse :: (Integer -> String) -> DataTypeInfo -> SMTRequest response -> response -> Maybe String
+renderSMTResponse _ _ (SMTGetInfo SMTSolverName) name
   = Just $ show $ L.List [L.Symbol ":name",L.String $ T.pack name]
-renderSMTResponse _ (SMTGetInfo SMTSolverVersion) vers
+renderSMTResponse _ _ (SMTGetInfo SMTSolverVersion) vers
   = Just $ show $ L.List [L.Symbol ":version",L.String $ T.pack vers]
-renderSMTResponse _ (SMTCheckSat _ _) res = case res of
+renderSMTResponse _ _ (SMTCheckSat _ _) res = case res of
   Sat -> Just "sat"
   Unsat -> Just "unsat"
   Unknown -> Just "unknown"
-renderSMTResponse st (SMTGetInterpolant grps) expr
-  = Just $ renderExpr' st expr
-renderSMTResponse st SMTGetProof proof
-  = Just $ renderExpr' st proof
-renderSMTResponse st (SMTSimplify _) expr
-  = Just $ renderExpr' st expr
-renderSMTResponse _ (SMTGetValue _) v = Just $ show v
-renderSMTResponse st (SMTApply _) goals
+renderSMTResponse getName dts (SMTGetInterpolant grps) expr
+  = Just $ renderExpr' getName dts expr
+renderSMTResponse getName dts SMTGetProof proof
+  = Just $ renderExpr' getName dts proof
+renderSMTResponse getName dts (SMTSimplify _) expr
+  = Just $ renderExpr' getName dts expr
+renderSMTResponse _ _ (SMTGetValue _) v = Just $ show v
+renderSMTResponse getName dts (SMTApply _) goals
   = Just $ show $
     L.List $ [L.Symbol "goals"]++
-    [exprToLisp goal (allVars st) (declaredDataTypes st)
+    [exprToLisp goal getName dts
     | goal <- goals ]
-renderSMTResponse _ SMTGetUnsatCore core = Just (show core)
-renderSMTResponse _ SMTGetModel mdl = Just (show mdl)
-renderSMTResponse _ _ _ = Nothing
+renderSMTResponse _ _ SMTGetUnsatCore core = Just (show core)
+renderSMTResponse _ _ SMTGetModel mdl = Just (show mdl)
+renderSMTResponse _ _ _ _ = Nothing
 
 -- | Spawn a new SMT solver process and create a pipe to communicate with it.
 createSMTPipe :: String -- ^ Path to the binary of the SMT solver
@@ -403,7 +459,8 @@
   (Just hin,Just hout,_,handle) <- createProcess cmd
   return $ SMTPipe { channelIn = hin
                    , channelOut = hout
-                   , processHandle = handle }
+                   , processHandle = handle
+                   , smtState = emptySMTState }
 
 sortToLisp :: Sort -> L.Lisp
 sortToLisp s = sortToLisp' sortToLisp (unFix s)
@@ -452,10 +509,10 @@
   return $ Fix $ NamedSort (T.unpack x) argSorts
 lispToSort _ = Nothing
 
-getSMTName :: FunInfo -> String
+{-getSMTName :: FunInfo -> String
 getSMTName info = escapeName (case funInfoName info of
   Nothing -> Right (funInfoId info)
-  Just name -> Left name)
+  Just name -> Left name)-}
 
 findName :: SMTState -> T.Text -> Maybe (SMTExpr Untyped)
 findName st name = case unescapeName (T.unpack name) of
@@ -464,18 +521,18 @@
     Nothing -> Nothing
     Just (FunInfo { funInfoProxy = _::Proxy (a,t)
                   , funInfoResAnn = ann
-                  }) -> let expr :: SMTExpr t
-                            expr = Var idx ann
-                        in Just $ mkUntyped expr
+                  },nc) -> let expr :: SMTExpr t
+                               expr = Var idx ann
+                           in Just $ mkUntyped expr
   Just (Left name') -> case Map.lookup name' (namedVars st) of
     Nothing -> Nothing
     Just idx -> case Map.lookup idx (allVars st) of
       Nothing -> Nothing
       Just (FunInfo { funInfoProxy = _::Proxy (a,t)
                     , funInfoResAnn = ann
-                    }) -> let expr :: SMTExpr t
-                              expr = Var idx ann
-                          in Just $ mkUntyped expr
+                    },_) -> let expr :: SMTExpr t
+                                expr = Var idx ann
+                            in Just $ mkUntyped expr
 
 mkUntyped :: SMTType t => SMTExpr t -> SMTExpr Untyped
 mkUntyped e = case cast e of
@@ -484,20 +541,18 @@
     Just e' -> entypeValue UntypedExpr e'
     Nothing -> UntypedExpr e
 
-exprToLisp :: SMTExpr t -> Map Integer FunInfo -> DataTypeInfo -> L.Lisp
+exprToLisp :: SMTExpr t -> (Integer -> String) -> DataTypeInfo -> L.Lisp
 exprToLisp
   = exprToLispWith
     (\obj -> error $ "smtlib2: Can't translate internal object "++
              show obj++" to s-expression.")
 
-exprToLispWith :: (forall a. (Typeable a,Ord a,Show a) => a -> L.Lisp) -> SMTExpr t -> Map Integer FunInfo -> DataTypeInfo -> L.Lisp
-exprToLispWith _ (Var idx _) mp _ = case Map.lookup idx mp of
-  Just info -> L.Symbol $ T.pack $
-               escapeName (case funInfoName info of
-                            Nothing -> Right (funInfoId info)
-                            Just name -> Left name)
-  Nothing -> L.Symbol $ T.pack $ escapeName (Right idx)
+exprToLispWith :: (forall a. (Typeable a,Ord a,Show a) => a -> L.Lisp) -> SMTExpr t
+                  -> (Integer -> String)
+                  -> DataTypeInfo -> L.Lisp
+exprToLispWith _ (Var idx _) mp _ = L.Symbol $ T.pack $ mp idx
 exprToLispWith _ (QVar lvl idx _) _ _ = L.Symbol $ T.pack $ "q_"++show lvl++"_"++show idx
+exprToLispWith _ (FunArg i _) _ _ = L.Symbol $ T.pack $ "farg_"++show i
 exprToLispWith objs (Const x ann) mp dts = case mangle of
   PrimitiveMangling f -> valueToLisp dts $ f x ann
   ComplexMangling f -> exprToLispWith objs (f x ann) mp dts
@@ -511,19 +566,19 @@
                                                 else f']
 exprToLispWith objs (Forall lvl tps body) mp dts
   = L.List [L.Symbol "forall"
-           ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,sortToLisp sort]
+           ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show (i::Integer),sortToLisp sort]
                    | (i,tp) <- Prelude.zip [0..] tps
                    , let sort = withProxyArg tp getSort ]
            ,exprToLispWith objs body mp dts]
 exprToLispWith objs (Exists lvl tps body) mp dts
   = L.List [L.Symbol "exists"
-           ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,sortToLisp sort]
+           ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show (i::Integer),sortToLisp sort]
                    | (i,tp) <- Prelude.zip [0..] tps
                    , let sort = withProxyArg tp getSort ]
            ,exprToLispWith objs body mp dts]
 exprToLispWith objs (Let lvl args body) mp dts
   = L.List [L.Symbol "let"
-           ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,
+           ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show (i::Integer),
                             exprToLispWith objs def mp dts]
                    | (i,def) <- Prelude.zip [0..] args ]
            ,exprToLispWith objs body mp dts]
@@ -574,7 +629,7 @@
     withUndef :: SMTFunction a b -> (a -> b -> r) -> r
     withUndef _ f = f undefined undefined
 
-functionGetSymbol :: Map Integer FunInfo -> SMTFunction a b -> ArgAnnotation a -> L.Lisp
+functionGetSymbol :: (Integer -> String) -> SMTFunction a b -> ArgAnnotation a -> L.Lisp
 functionGetSymbol _ SMTEq _ = L.Symbol "="
 functionGetSymbol mp fun@(SMTMap f) ann
   = L.List [L.Symbol "_",
@@ -595,8 +650,7 @@
                        L.List (fmap sortToLisp sigArg),
                        sortToLisp sigRes]
           else sym'     
-functionGetSymbol mp (SMTFun name _) _ = case Map.lookup name mp of
-  Just info -> L.Symbol (T.pack $ getSMTName info)
+functionGetSymbol mp (SMTFun i _) _ = L.Symbol (T.pack $ mp i)
 functionGetSymbol _ (SMTBuiltIn name _) _ = L.Symbol $ T.pack name
 functionGetSymbol _ (SMTOrd op) _ = L.Symbol $ case op of
   Ge -> ">="
@@ -688,7 +742,7 @@
 putRequest pipe expr = do
   clearInput pipe
   liftIO $ toByteStringIO (BS.hPutStr $ channelIn pipe) (mappend (L.fromLispExpr expr) flush)
-  liftIO $ BS.hPutStrLn (channelIn pipe) ""
+  liftIO $ BS8.hPutStrLn (channelIn pipe) ""
   liftIO $ hFlush (channelIn pipe)
 
 parseResponse :: MonadIO m => SMTPipe -> m L.Lisp
@@ -828,6 +882,7 @@
   Just res -> Just res
   Nothing -> case sort of
     Just (Fix (NamedSort name argSorts)) -> lispToConstr dts (Just (name,argSorts)) l
+    _ -> error $ "smtlib2: Cannot translate "++show l++" to value"
 
 lispToConstr :: DataTypeInfo -> Maybe (String,[Sort]) -> L.Lisp -> Maybe Value
 lispToConstr dts sort (L.List [L.Symbol "as",
@@ -1589,7 +1644,7 @@
 withPipe :: MonadIO m => String -> [String] -> SMT' m a -> m a
 withPipe prog args act = do
   pipe <- liftIO $ createSMTPipe prog args
-  withSMTBackend pipe act
+  withSMTBackend' pipe True act
 
 tacticToLisp :: Tactic -> L.Lisp
 tacticToLisp Skip = L.Symbol "skip"
diff --git a/Language/SMTLib2/Strategy.hs b/Language/SMTLib2/Strategy.hs
--- a/Language/SMTLib2/Strategy.hs
+++ b/Language/SMTLib2/Strategy.hs
@@ -2,8 +2,6 @@
 
 import Language.SMTLib2.Internals.Operators
 
-import Text.Show
-
 data Tactic
   = Skip
   | AndThen [Tactic]
diff --git a/smtlib2.cabal b/smtlib2.cabal
--- a/smtlib2.cabal
+++ b/smtlib2.cabal
@@ -1,5 +1,5 @@
 Name:           smtlib2
-Version:        0.1
+Version:        0.2
 Author:         Henning Günther <guenther@forsyte.at>
 Maintainer:     guenther@forsyte.at
 Synopsis:       A type-safe interface to communicate with an SMT solver.
@@ -23,12 +23,13 @@
 
 Library
   Build-Depends:        base >= 4 && < 5,text,mtl,process,blaze-builder,bytestring,
-                        attoparsec,atto-lisp >= 0.2,array,
+                        attoparsec,atto-lisp >= 0.2 && < 0.3,array,
                         containers, transformers, data-fix, tagged
   Extensions: GADTs,RankNTypes,CPP,ScopedTypeVariables,
               MultiParamTypeClasses,FlexibleContexts,OverloadedStrings,
               DeriveFunctor,FlexibleInstances,DeriveTraversable,DeriveFoldable,
               DeriveDataTypeable
+  GHC-Options: -fcontext-stack=100
   if flag(WithConstraints)
     Build-Depends:      constraints
     CPP-Options: -DSMTLIB2_WITH_CONSTRAINTS