diff --git a/example/Switch-coinduction.smt b/example/Switch-coinduction.smt
new file mode 100644
index 0000000..31a3a2f
--- /dev/null
+++ b/example/Switch-coinduction.smt
@@ -0,0 +1,156 @@
+;; Implementation of Switch.lm by hand for exploration
+;; Proves the 3 given properties using (0-)coinduction.
+;; There are slight variants (commented) of those
+;; properties which are incorrect. Those give the
+;; expected counterexamples.
+
+;; node Switch
+(define-fun Switch_s_def ((on Bool) (off Bool) (s_1 Bool) (s Bool)) Bool
+  (= s
+     (ite s_1 (not off) on)))
+(define-fun Switch_s_1_def ((s Bool) (s_1_next Bool)) Bool
+  (= s_1_next
+     s ))
+(define-fun Switch_so_def ((so Bool) (s Bool)) Bool
+  (= so
+     s))
+
+;; Global flow
+(define-fun Switch_on_def ((Switch_on Bool) (on Bool)) Bool
+  (= Switch_on
+     on))
+(define-fun Switch_off_def ((Switch_off Bool) (off Bool)) Bool
+  (= Switch_off
+     off))
+(define-fun s_def ((Switch_so Bool) (s Bool)) Bool
+  (= s
+     Switch_so))
+(define-fun s_1_def ((s_1_next Bool) (s Bool)) Bool
+  (= s_1_next
+     s))
+
+;; properties
+(define-fun prop1 ((off Bool) (on Bool) (s Bool)) Bool
+;  (=> on s))
+  (=> (and on (not off)) s))
+(define-fun prop2 ((off Bool) (on Bool) (s Bool)) Bool
+;  (=> off (not s)))
+  (=> (and off (not on)) (not s)))
+(define-fun prop3 ((off Bool) (on Bool) (s Bool) (s_1 Bool)) Bool
+  (=> (and (not off) (not on)) (= s s_1)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Prove that initial state fulfils property
+
+(push)
+
+;; declarations
+(declare-fun Switch_on_0 () Bool)
+(declare-fun Switch_off_0 () Bool)
+(declare-fun Switch_so_0 () Bool)
+(declare-fun Switch_s_0 () Bool)
+(declare-fun Switch_s_1_0 () Bool)
+
+(declare-fun on_0 () Bool)
+(declare-fun off_0 () Bool)
+(declare-fun s_0 () Bool)
+(declare-fun s_1_0 () Bool)
+
+(declare-fun Switch_s_1_1 () Bool)
+(declare-fun s_1_1 () Bool)
+
+;; initialisation
+(assert (= Switch_s_1_0 false))
+(assert (= s_1_0 false))
+
+(assert (Switch_on_def Switch_on_0 on_0))
+(assert (Switch_off_def Switch_off_0 off_0))
+
+(assert (Switch_so_def Switch_so_0 Switch_s_0))
+(assert (Switch_s_def Switch_on_0 Switch_off_0 Switch_s_1_0 Switch_s_0))
+(assert (Switch_s_1_def Switch_s_0 Switch_s_1_1))
+
+(assert (s_def s_0 Switch_so_0))
+(assert (s_1_def s_1_1 s_0))
+
+;(assert (not (prop1 off_0 on_0 s_0)))
+(assert (not (prop2 off_0 on_0 s_0)))
+;(assert (not (prop3 off_0 on_0 s_0 s_1_0)))
+
+(check-sat)
+(get-model)
+(pop)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Prove that property is an invariant
+
+;; declarations
+(declare-fun Switch_on () Bool)
+(declare-fun Switch_off () Bool)
+(declare-fun Switch_so () Bool)
+(declare-fun Switch_s () Bool)
+(declare-fun Switch_s_1 () Bool)
+
+(declare-fun on () Bool)
+(declare-fun off () Bool)
+(declare-fun s () Bool)
+(declare-fun s_1 () Bool)
+
+(declare-fun Switch_s_1_n1 () Bool)
+(declare-fun s_1_n1 () Bool)
+
+(declare-fun Switch_on_n1 () Bool)
+(declare-fun Switch_off_n1 () Bool)
+(declare-fun Switch_so_n1 () Bool)
+(declare-fun Switch_s_n1 () Bool)
+
+(declare-fun on_n1 () Bool)
+(declare-fun off_n1 () Bool)
+(declare-fun s_n1 () Bool)
+
+(declare-fun Switch_s_1_n2 () Bool)
+(declare-fun s_1_n2 () Bool)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Assume that we start in a state in which the invariant holds
+
+;(assert (prop1 off on s))
+(assert (prop2 off on s))
+;(assert (prop3 off on s s_1))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Set up variables in starting state
+
+(assert (Switch_on_def Switch_on on))
+(assert (Switch_off_def Switch_off off))
+
+(assert (Switch_so_def Switch_so Switch_s))
+(assert (Switch_s_def Switch_on Switch_off Switch_s_1 Switch_s))
+(assert (Switch_s_1_def Switch_s Switch_s_1_n1))
+
+(assert (s_def s Switch_so))
+(assert (s_1_def s_1_n1 s))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Make transition
+
+(assert (Switch_on_def Switch_on_n1 on_n1))
+(assert (Switch_off_def Switch_off_n1 off_n1))
+
+(assert (Switch_so_def Switch_so_n1 Switch_s_n1))
+(assert (Switch_s_def Switch_on_n1 Switch_off_n1 Switch_s_1_n1 Switch_s_n1))
+(assert (Switch_s_1_def Switch_s_n1 Switch_s_1_n2))
+
+(assert (s_def s_n1 Switch_so_n1))
+(assert (s_1_def s_1_n2 s_n1))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Try to prove that property holds after transition
+(push)
+;(assert (not (prop1 off_n1 on_n1 s_n1)))
+(assert (not (prop2 off_n1 on_n1 s_n1)))
+;(assert (not (prop3 off_n1 on_n1 s_n1 s_1_n1)))
+
+(check-sat)
+(get-model)
+(pop)
\ No newline at end of file
diff --git a/interpreter/LAMA.cabal b/interpreter/LAMA.cabal
index 566ed20..1b05040 100644
--- a/interpreter/LAMA.cabal
+++ b/interpreter/LAMA.cabal
@@ -8,7 +8,7 @@ Description:
 Executable test-lama
   default-language: Haskell2010
   build-depends: base, containers, mtl, bytestring, natural-numbers,
-    transformers, pretty, array, HUnit, language-lama
+    transformers, pretty, array, HUnit, language-lama, fgl >= 5.5.0.0
   hs-source-dirs: test lib
   GHC-Options: -Wall
   other-modules:
diff --git a/interpreter/Main.hs b/interpreter/Main.hs
index 7408bce..0c0e41b 100644
--- a/interpreter/Main.hs
+++ b/interpreter/Main.hs
@@ -18,7 +18,6 @@ import Data.Foldable (forM_, foldlM, foldl)
 import Lang.LAMA.Identifier
 import qualified Data.Map as Map
 import Data.Map (Map)
-import Data.Graph.Inductive.GenShow ()
 import Control.Monad (void, when, MonadPlus(..))
 import Control.Monad.Trans.Maybe
 import Control.Monad.IO.Class
diff --git a/lamaSMT/LamaSMT.cabal b/lamaSMT/LamaSMT.cabal
index eeb0587..bf48018 100644
--- a/lamaSMT/LamaSMT.cabal
+++ b/lamaSMT/LamaSMT.cabal
@@ -1,5 +1,5 @@
 Name:           LamaSMT
-Version:        0.1
+Version:        0.3
 Build-Type:     Simple
 Cabal-Version:  >= 1.10
 Description:
@@ -15,4 +15,4 @@ Executable lamasmt
   GHC-Options: -Wall -rtsopts
   other-modules:
     Transform
-  Main-Is: Main.hs
\ No newline at end of file
+  Main-Is: Main.hs
diff --git a/lamaSMT/Main.hs b/lamaSMT/Main.hs
index 65d4e4e..440c3df 100644
--- a/lamaSMT/Main.hs
+++ b/lamaSMT/Main.hs
@@ -5,10 +5,8 @@ module Main (main) where
 
 import qualified Data.ByteString.Lazy.Char8 as BL
 
-import Text.PrettyPrint (render)
+import Text.PrettyPrint (Doc, render, vcat, text, ($$))
 import Data.List.Split (splitOn)
-import Data.List (intercalate)
-import Data.Natural
 
 import System.IO (stdin)
 import System.Environment (getArgs)
@@ -170,7 +168,7 @@ run opts@Options{..} file inp = do
   model <- runCheck opts
     ( (liftSMT $ mapM_ setOption optSMTOpts) >>
       lamaSMT optNatImpl optEnumImpl p >>=
-      (uncurry $ checkWithModel optNatImpl optStrategy) )
+      (uncurry $ checkWithModel optStrategy) )
   liftIO $ checkModel opts p model
 
 checkErrors :: Either Error a -> MaybeT IO a
@@ -204,11 +202,36 @@ runCheck progOpts = chooseSolver progOpts . checkError
                       -- ++ solverBase
   -- withPipe solverCmd []
 
-checkModel :: Ident i => Options -> Program i -> Maybe (Natural, Model i) -> IO ()
-checkModel _ _ Nothing = putStrLn "42"
-checkModel opts prog (Just (lastIndex, m)) =
+checkModel :: Ident i =>
+           Options
+           -> Program i
+           -> (StrategyResult i)
+           -> IO ()
+checkModel _ _ Success = putStrLn "42"
+checkModel opts prog (Failure lastIndex m) =
   do putStrLn ":-("
+     putStrLn $ "Found counterexample at depth " ++ show lastIndex
      when (optDumpModel opts) (putStrLn . render $ prettyModel m)
      case optScenarioFile opts of
        Nothing -> return ()
-       Just f -> writeFile f $ render $ scadeScenario prog (optTopNodePath opts) lastIndex m
+       Just f -> writeFile f $ render $ scadeScenario prog (optTopNodePath opts) m
+checkModel opts prog (Unknown what hints) =
+  do putStrLn ":-("
+     putStrLn what
+     when (optDumpModel opts)
+          (putStrLn . render . prettyHints $ hints)
+     case optScenarioFile opts of
+       Nothing -> return ()
+       Just f ->
+         mapM_ (\h ->
+                 writeFile (f ++ "_" ++ hintDescr h)
+                 . render
+                 $ scadeScenario prog (optTopNodePath opts) (hintModel h))
+               hints
+
+prettyHints :: Ident i => Hints i -> Doc
+prettyHints = vcat . map prettyHint
+  where
+    prettyHint h
+      = text ("Hint for " ++ (hintDescr h))
+        $$ prettyModel (hintModel h)
diff --git a/lamaSMT/lib/Check.hs b/lamaSMT/lib/Check.hs
index ff1ecc4..3ce8c96 100644
--- a/lamaSMT/lib/Check.hs
+++ b/lamaSMT/lib/Check.hs
@@ -3,4 +3,4 @@ module Check where
 import Strategy
 
 check :: Strategy s => 
-check = undefined
\ No newline at end of file
+check = undefined
diff --git a/lamaSMT/lib/Definition.hs b/lamaSMT/lib/Definition.hs
index 873ecf4..0c4c41c 100644
--- a/lamaSMT/lib/Definition.hs
+++ b/lamaSMT/lib/Definition.hs
@@ -1,31 +1,36 @@
 module Definition where
 
-import Data.Array as Arr
-
 import Language.SMTLib2 as SMT
 
+import Data.Array as Arr
+
 import LamaSMTTypes
 import Internal.Monads
 
 data Definition =
-  SingleDef (Stream Bool)
+  SingleDef [Int] Bool (SMTFunction [TypedExpr] Bool)
   | ProdDef (Array Int Definition)
---  deriving Show
+  deriving Show
 
-ensureDefinition :: TypedStream i -> Definition
-ensureDefinition (BoolStream s) = SingleDef s
-ensureDefinition (ProdStream ps) = ProdDef $ fmap ensureDefinition ps
-ensureDefinition _
-  = error $ "ensureDefinition: not a boolean stream" -- : " ++ show s
+ensureDefinition :: [Int] -> Bool -> TypedFunc -> Definition
+ensureDefinition argN succ (BoolFunc s) = SingleDef argN succ s
+ensureDefinition argN succ (ProdFunc ps) = ProdDef $ fmap (ensureDefinition argN succ) ps
+ensureDefinition _ _ _
+  = error $ "ensureDefinition: not a boolean function"
 
 assertDefinition :: MonadSMT m =>
                     (SMTExpr Bool -> SMTExpr Bool)
-                    -> StreamPos
+                    -> ([TypedExpr], [TypedExpr])
                     -> Definition
                     -> m ()
-assertDefinition f i (SingleDef s) = liftSMT $ assert (f $ s `app` i)
+assertDefinition f i (SingleDef argN succ s) = liftSMT $ assert (f $ s `app` (lookupArgs argN succ i))
 assertDefinition f i (ProdDef ps) = mapM_ (assertDefinition f i) $ Arr.elems ps
 
+lookupArgs :: [Int] -> Bool -> ([TypedExpr], [TypedExpr])
+               -> [TypedExpr]
+lookupArgs argN True vars = [(snd vars) !! (head argN)] ++ (map ((!!) (fst vars)) $ tail argN)
+lookupArgs argN False vars = map ((!!) (fst vars)) argN
+
 data ProgDefs = ProgDefs
                 { flowDef :: [Definition]
                 , precondition :: Definition
diff --git a/lamaSMT/lib/Internal/Monads.hs b/lamaSMT/lib/Internal/Monads.hs
index 79837fb..16917aa 100644
--- a/lamaSMT/lib/Internal/Monads.hs
+++ b/lamaSMT/lib/Internal/Monads.hs
@@ -6,6 +6,7 @@ import Control.Monad.Error
 import Control.Monad.State.Lazy as Lazy
 import Control.Monad.State.Strict as Strict
 import Control.Monad.Reader
+import Control.Monad.Writer
 
 -- | Lift an SMT action into an arbitrary monad (like liftIO).
 class Monad m => MonadSMT m where
@@ -25,3 +26,6 @@ instance MonadSMT m => MonadSMT (Strict.StateT s m) where
 
 instance MonadSMT m => MonadSMT (ReaderT r m) where
   liftSMT = lift . liftSMT
+
+instance (Monoid w, MonadSMT m) => MonadSMT (WriterT w m) where
+  liftSMT = lift . liftSMT
diff --git a/lamaSMT/lib/LamaSMTTypes.hs b/lamaSMT/lib/LamaSMTTypes.hs
index 599fb1d..459342e 100644
--- a/lamaSMT/lib/LamaSMTTypes.hs
+++ b/lamaSMT/lib/LamaSMTTypes.hs
@@ -2,62 +2,172 @@
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
 module LamaSMTTypes where
 
 import Data.Natural
 import NatInstance ()
 import Data.Array as Arr
+import Data.Typeable
+import Data.Foldable (foldlM)
+import Data.List (mapAccumL)
+
+import Text.Show
 
 import Control.Arrow ((&&&))
 
 import Language.SMTLib2 as SMT
 import SMTEnum
 
-data TypedExpr i
+data TypedExpr
   = BoolExpr { unBool :: SMTExpr Bool }
   | IntExpr { unInt :: SMTExpr Integer }
   | RealExpr { unReal :: SMTExpr Rational }
   | EnumExpr { unEnum :: SMTExpr SMTEnum }
-  | ProdExpr { unProd :: Array Int (TypedExpr i) }
-  deriving (Eq, Show)
-
-unBool' :: TypedExpr i -> SMTExpr Bool
+  | ProdExpr { unProd :: Array Int (TypedExpr) }
+  deriving (Ord, Typeable, Eq, Show)
+
+data TypedAnnotation
+  = BoolAnnotation { anBool :: ArgAnnotation (SMTExpr Bool) }
+  | IntAnnotation { anInt :: ArgAnnotation (SMTExpr Integer) }
+  | RealAnnotation { anReal :: ArgAnnotation (SMTExpr Rational) }
+  | EnumAnnotation { anEnum :: ArgAnnotation (SMTExpr SMTEnum) }
+  | ProdAnnotation { anProd :: Array Int TypedAnnotation }
+  deriving (Ord, Typeable, Eq, Show)
+
+unBool' :: TypedExpr -> SMTExpr Bool
 unBool' (BoolExpr e) = e
 unBool' e = error $ "Cannot unBool: " ++ show e
 
-unProd' :: TypedExpr i -> Array Int (TypedExpr i)
+unProd' :: TypedExpr -> Array Int (TypedExpr)
 unProd' (ProdExpr e) = e
 unProd' e = error $ "Cannot unProd: " ++ show e
 
-type StreamPos = SMTExpr Natural
-type Stream t = SMTFunction StreamPos t
-data TypedStream i
-  = BoolStream (Stream Bool)
-  | IntStream (Stream Integer)
-  | RealStream (Stream Rational)
-  | EnumStream EnumAnn (Stream SMTEnum)
-  | ProdStream (Array Int (TypedStream i))
---  deriving Show
-
-mkProdStream :: [TypedStream i] -> TypedStream i
-mkProdStream [] = error "Cannot create empty product stream"
-mkProdStream [s] = s
-mkProdStream sts = ProdStream . uncurry listArray $ ((0,) . pred . length &&& id) sts
-
-appStream :: TypedStream i -> StreamPos -> TypedExpr i
-appStream (BoolStream s) n = BoolExpr $ s `app` n
-appStream (IntStream s) n = IntExpr $ s `app` n
-appStream (RealStream s) n = RealExpr $ s `app` n
-appStream (EnumStream _ s) n = EnumExpr $ s `app` n
-appStream (ProdStream s) n = ProdExpr $ fmap (`appStream` n) s
-
-liftAssert :: TypedExpr i -> SMT ()
+data TypedFunc
+  = BoolFunc (SMTFunction [TypedExpr] Bool)
+  | IntFunc (SMTFunction [TypedExpr] Integer)
+  | RealFunc (SMTFunction [TypedExpr] Rational)
+  | EnumFunc EnumAnn (SMTFunction [TypedExpr] SMTEnum)
+  | ProdFunc (Array Int (TypedFunc))
+  deriving Show
+
+mkProdExpr :: [TypedExpr] -> TypedExpr
+mkProdExpr [] = error "Cannot create empty product expression"
+mkProdExpr [s] = s
+mkProdExpr sts = ProdExpr . uncurry listArray $ ((0,) . pred . length &&& id) sts
+
+appFunc :: TypedFunc -> [TypedExpr] -> TypedExpr
+appFunc (BoolFunc f) arg = BoolExpr $ f `app` arg
+appFunc (IntFunc f) arg = IntExpr $ f `app` arg
+appFunc (RealFunc f) arg = RealExpr $ f `app` arg
+appFunc (EnumFunc _ f) arg = EnumExpr $ f `app` arg
+appFunc (ProdFunc f) arg = ProdExpr $ fmap (`appFunc` arg) f
+
+instance Args (TypedExpr) where
+  type ArgAnnotation TypedExpr = TypedAnnotation
+  foldExprs f s ~(BoolExpr x) (BoolAnnotation ann) = do
+    (ns, res) <- foldExprs f s x ann
+    return (ns, BoolExpr res)
+  foldExprs f s ~(IntExpr x) (IntAnnotation ann) = do
+    (ns, res) <- foldExprs f s x ann
+    return (ns, IntExpr res)
+  foldExprs f s ~(RealExpr x) (RealAnnotation ann) = do
+    (ns, res) <- foldExprs f s x ann
+    return (ns, RealExpr res)
+  foldExprs f s ~(EnumExpr x) (EnumAnnotation ann) = do
+    (ns, res) <- foldExprs f s x ann
+    return (ns, EnumExpr res)
+  foldExprs f s ~(ProdExpr x) (ProdAnnotation y) =
+    foldlM (\(s',ProdExpr cmp) (k,ann) -> do
+      let el = x ! k
+      (s'',el') <- foldExprs f s' el ann
+      return (s'', ProdExpr $ cmp Arr.// [(k,el')])
+      ) (s,ProdExpr $ Arr.array (bounds y) []) (Arr.assocs y)
+  foldsExprs f s lst (BoolAnnotation ann) = do
+    (ns, ress, res) <- foldsExprs f s (fmap (\(x,p) -> (case x of BoolExpr x' -> x',p)) lst) ann
+    return (ns, fmap BoolExpr ress, BoolExpr res)
+  foldsExprs f s lst (IntAnnotation ann) = do
+    (ns, ress, res) <- foldsExprs f s (fmap (\(x,p) -> (case x of IntExpr x' -> x',p)) lst) ann
+    return (ns, fmap IntExpr ress, IntExpr res)
+  foldsExprs f s lst (RealAnnotation ann) = do
+    (ns, ress, res) <- foldsExprs f s (fmap (\(x,p) -> (case x of RealExpr x' -> x',p)) lst) ann
+    return (ns, fmap RealExpr ress, RealExpr res)
+  foldsExprs f s lst (EnumAnnotation ann) = do
+    (ns, ress, res) <- foldsExprs f s (fmap (\(x,p) -> (case x of EnumExpr x' -> x',p)) lst) ann
+    return (ns, fmap EnumExpr ress, EnumExpr res)
+  foldsExprs f s args (ProdAnnotation ann) = do
+    let lst_ann = Arr.assocs ann
+        lst = fmap (\(ProdExpr mp,extra) -> ([ mp ! k | (k,_) <- lst_ann ],extra)
+                   ) args
+    (ns,lst',lst_merged) <- foldsExprs f s lst (fmap snd lst_ann)
+    return (ns,fmap (\lst'' -> ProdExpr $ Arr.array (bounds ann) $ zip (fmap fst lst_ann) lst''
+                    ) lst',ProdExpr $ Arr.array (bounds ann)  $ zip (fmap fst lst_ann) lst_merged)
+  extractArgAnnotation (BoolExpr x) = BoolAnnotation $ extractArgAnnotation x
+  extractArgAnnotation (IntExpr x) = IntAnnotation $ extractArgAnnotation x
+  extractArgAnnotation (RealExpr x) = RealAnnotation $ extractArgAnnotation x
+  extractArgAnnotation (EnumExpr x) = EnumAnnotation $ extractArgAnnotation x
+  extractArgAnnotation (ProdExpr x) = ProdAnnotation $ fmap extractArgAnnotation x
+  toArgs (BoolAnnotation ann) exprs = do
+    (res, rest) <- toArgs ann exprs
+    return (BoolExpr res, rest)
+  toArgs (IntAnnotation ann) exprs = do
+    (res, rest) <- toArgs ann exprs
+    return (IntExpr res, rest)
+  toArgs (RealAnnotation ann) exprs = do
+    (res, rest) <- toArgs ann exprs
+    return (RealExpr res, rest)
+  toArgs (EnumAnnotation ann) exprs = do
+    (res, rest) <- toArgs ann exprs
+    return (EnumExpr res, rest)
+  toArgs (ProdAnnotation mp_ann) exprs =
+    case mapAccumL (\cst (k,ann) -> case cst of
+        Nothing -> (Nothing,undefined)
+        Just rest -> case toArgs ann rest of
+          Nothing -> (Nothing,undefined)
+          Just (res,rest') -> (Just rest', (k,res))
+                   ) (Just exprs) (Arr.assocs mp_ann) of
+      (Nothing,_) -> Nothing
+      (Just rest,mp) -> Just (ProdExpr $ Arr.array (bounds mp_ann) mp,rest)
+  fromArgs (BoolExpr xs) = fromArgs xs
+  fromArgs (IntExpr  xs) = fromArgs xs
+  fromArgs (RealExpr xs) = fromArgs xs
+  fromArgs (EnumExpr xs) = fromArgs xs
+  fromArgs (ProdExpr xs) = concat $ fmap fromArgs $ Arr.elems xs
+  getSorts (_::TypedExpr) (BoolAnnotation _) = error "lamasmt: no getSorts for TypedExpr"
+  getArgAnnotation _ _ = error "lamasmt: getArgAnnotation undefined for TypedExpr"
+  showsArgs n p (BoolExpr x) = let (showx,nn) = showsArgs n 11 x
+                               in (showParen (p>10) $
+                                   showString "BoolExpr " . showx,nn)
+  showsArgs n p (IntExpr x) = let (showx,nn) = showsArgs n 11 x
+                               in (showParen (p>10) $
+                                   showString "IntExpr " . showx,nn)
+  showsArgs n p (RealExpr x) = let (showx,nn) = showsArgs n 11 x
+                               in (showParen (p>10) $
+                                   showString "RealExpr " . showx,nn)
+  showsArgs n p (EnumExpr x) = let (showx,nn) = showsArgs n 11 x
+                               in (showParen (p>10) $
+                                   showString "EnumExpr " . showx,nn)
+  showsArgs n p (ProdExpr x) =
+    let (ni,lst') = mapAccumL (\ci (key,arg)
+                               -> let (str,ci') = showsArgs ci 0 arg
+                                  in (ci',(key,str))
+                              ) n (Arr.assocs x)
+    in (showString "fromList " . showListWith (\(key,str)
+                                               -> showChar '(' .
+                                                  showsPrec 0 key .
+                                                  showChar ',' .
+                                                  str . showChar ')') lst',ni)
+
+liftAssert :: TypedExpr -> SMT ()
 liftAssert (BoolExpr e) = assert e
 liftAssert (ProdExpr es) = mapM_ liftAssert $ Arr.elems es
 liftAssert e = error $ "liftAssert: cannot assert non-boolean expression: " ++ show e
 
 liftRel :: (forall a. SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool)
-           -> TypedExpr i -> TypedExpr i -> TypedExpr i
+           -> TypedExpr -> TypedExpr -> TypedExpr
 liftRel r (BoolExpr e1) (BoolExpr e2) = BoolExpr $ r e1 e2
 liftRel r (IntExpr e1) (IntExpr e2) = BoolExpr $ r e1 e2
 liftRel r (RealExpr e1) (RealExpr e2) = BoolExpr $ r e1 e2
@@ -68,33 +178,33 @@ liftRel _ _ _ = error "liftRel: argument types don't match"
 -- | Only for boolean product streams. Ensures that all fields of
 -- a product hold simultaniuosly. Useful for elementwise
 -- extended relatations.
-prodAll :: TypedExpr i -> TypedExpr i
+prodAll :: TypedExpr -> TypedExpr
 prodAll (BoolExpr e) = BoolExpr e
 prodAll (ProdExpr e) = liftBoolL and' $ Arr.elems e
 prodAll e = error $ "prodAll: not a product or boolean expr: " ++ show e
 
 liftOrd :: (forall a. (SMTType a, SMTOrd a) => SMTExpr a -> SMTExpr a -> SMTExpr Bool)
-           -> TypedExpr i -> TypedExpr i -> TypedExpr i
+           -> TypedExpr -> TypedExpr -> TypedExpr
 liftOrd r (IntExpr e1) (IntExpr e2) = BoolExpr $ r e1 e2
 liftOrd r (RealExpr e1) (RealExpr e2) = BoolExpr $ r e1 e2
 liftOrd _ _ _ = error "liftRel: argument types don't match or are not ordered"
 
 
-lift1Bool :: (SMTExpr Bool -> SMTExpr Bool) -> TypedExpr i -> TypedExpr i
+lift1Bool :: (SMTExpr Bool -> SMTExpr Bool) -> TypedExpr -> TypedExpr
 lift1Bool f (BoolExpr e) = BoolExpr $ f e
 lift1Bool _ _ = error "lift1Bool: argument is not boolean"
 
 liftBool2 :: (SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool)
-             -> TypedExpr i -> TypedExpr i -> TypedExpr i
+             -> TypedExpr -> TypedExpr -> TypedExpr
 liftBool2 f (BoolExpr e1) (BoolExpr e2) = BoolExpr $ f e1 e2
 liftBool2 _ e1 e2 = error $ "liftBool2: arguments are not boolean: " ++ show e1 ++ "; " ++ show e2
 
-liftBoolL :: SMTFunction [SMTExpr Bool] Bool -> [TypedExpr i] -> TypedExpr i
+liftBoolL :: SMTFunction [SMTExpr Bool] Bool -> [TypedExpr] -> TypedExpr
 liftBoolL f es@((BoolExpr _):_) = BoolExpr . app f $ map unBool es
 liftBoolL _ es = error $ "Cannot lift bool expr for" ++ show es
 
 lift2 :: (forall a. SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr a)
-         -> TypedExpr i -> TypedExpr i -> TypedExpr i
+         -> TypedExpr -> TypedExpr -> TypedExpr
 lift2 f (BoolExpr e1) (BoolExpr e2) = BoolExpr $ f e1 e2
 lift2 f (IntExpr e1) (IntExpr e2) = IntExpr $ f e1 e2
 lift2 f (RealExpr e1) (RealExpr e2) = RealExpr $ f e1 e2
@@ -102,33 +212,33 @@ lift2 f (EnumExpr e1) (EnumExpr e2) = EnumExpr $ f e1 e2
 lift2 f (ProdExpr e1) (ProdExpr e2) = ProdExpr $ accum (lift2 f) e1 (Arr.assocs e2)
 lift2 _ _ _ = error "lift2: argument types don't match"
 
-liftIte :: TypedExpr i -> TypedExpr i -> TypedExpr i -> TypedExpr i
+liftIte :: TypedExpr -> TypedExpr -> TypedExpr -> TypedExpr
 liftIte (BoolExpr c) = lift2 (ite c)
 liftIte _ = error "liftIte: condition is not boolean"
 
 liftArith :: (forall a. SMTArith a => SMTFunction (SMTExpr a, SMTExpr a) a)
-             -> TypedExpr i
-             -> TypedExpr i
-             -> TypedExpr i
+             -> TypedExpr
+             -> TypedExpr
+             -> TypedExpr
 liftArith f (IntExpr e1)  (IntExpr e2)  = IntExpr  $ app f (e1, e2)
 liftArith f (RealExpr e1) (RealExpr e2) = RealExpr $ app f (e1, e2)
 liftArith _ _ _
   = error "liftArith: argument types don't match or are not aritemetic types"
 
 liftArithL :: (forall a. SMTArith a => SMTFunction [SMTExpr a] a)
-              -> [TypedExpr i]
-              -> TypedExpr i
+              -> [TypedExpr]
+              -> TypedExpr
 liftArithL f es@((IntExpr _):_)  = IntExpr  . app f $ map unInt  es
 liftArithL f es@((RealExpr _):_) = RealExpr . app f $ map unReal es
 liftArithL _ _
   = error "liftArithL: argument types don't match or are not arithmetic types"
 
 liftInt2 :: (SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer)
-              -> TypedExpr i -> TypedExpr i -> TypedExpr i
+              -> TypedExpr -> TypedExpr -> TypedExpr
 liftInt2 f (IntExpr e1) (IntExpr e2) = IntExpr $ f e1 e2
 liftInt2 _ _ _ = error "liftInt2: argument types are not integers"
 
 liftReal2 :: (SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational)
-              -> TypedExpr i -> TypedExpr i -> TypedExpr i
+              -> TypedExpr -> TypedExpr -> TypedExpr
 liftReal2 f (RealExpr e1) (RealExpr e2) = RealExpr $ f e1 e2
 liftReal2 _ _ _ = error "liftReal2: argument types are not rational"
diff --git a/lamaSMT/lib/Model.hs b/lamaSMT/lib/Model.hs
index f9b88b5..5b9123f 100644
--- a/lamaSMT/lib/Model.hs
+++ b/lamaSMT/lib/Model.hs
@@ -8,6 +8,8 @@ import Data.Natural
 import Text.PrettyPrint hiding ((<>))
 import Data.Array as Arr
 import Data.Monoid
+import Data.Maybe (fromJust)
+import qualified Data.List as List
 
 import Control.Monad.Reader (MonadReader(..), ReaderT(..))
 import Control.Applicative (Applicative(..), (<$>))
@@ -61,20 +63,23 @@ prettyNodeModel m = braces . nest 2 $
 
 prettyStream :: ValueStream -> Doc
 prettyStream (BoolVStream s) = prettyStreamVals s
-prettyStream (IntVStream s) = prettyStreamVals s
+prettyStream (IntVStream s)  = prettyStreamVals s
 prettyStream (RealVStream s) = prettyStreamVals s
 prettyStream (EnumVStream s) = prettyStreamVals s
-prettyStream (ProdVStream s) = parens . hcat . punctuate comma . fmap prettyStream $ Arr.elems s
+prettyStream (ProdVStream s)
+             = parens . hcat . punctuate comma . fmap prettyStream $ Arr.elems s
 
 prettyStreamVals :: Show t => ValueStreamT t -> Doc
-prettyStreamVals = cat . punctuate (char ',')
-               . map (\(n, v) -> (integer $ toInteger n) <+> text "->" <+> text (show v))
-               . Map.toList
+prettyStreamVals
+        = cat . punctuate (char ',')
+          . map (\(n, v) ->
+                (integer $ toInteger n) <+> text "->" <+> text (show v))
+          . Map.toList
 
-getModel :: VarEnv i -> Map Natural StreamPos -> SMT (Model i)
-getModel env = runReaderT (getModel' env)
+getModel :: VarEnv i -> Map Natural [TypedExpr] -> SMT (Model i)
+getModel env m = runReaderT (getModel' env) m
 
-type ModelM = ReaderT (Map Natural StreamPos) SMT
+type ModelM = ReaderT (Map Natural [TypedExpr]) SMT
 
 getModel' :: VarEnv i -> ModelM (Model i)
 getModel' env =
@@ -82,33 +87,66 @@ getModel' env =
 
 getNodeModel :: NodeEnv i -> ModelM (NodeModel i)
 getNodeModel (NodeEnv i o e) =
-  NodeModel <$> mapM getVarModel i <*> mapM getVarModel o <*> getModel' e
+  NodeModel <$> mapM getVarModel i <*> mapM (getVarModel . snd) o <*> getModel' e
 
-getVarsModel :: Map i (TypedStream i) -> ModelM (Map i ValueStream)
+getVarsModel :: Map i (TypedExpr) -> ModelM (Map i ValueStream)
 getVarsModel = mapM getVarModel
 
-getVarModel :: TypedStream i -> ModelM ValueStream
-getVarModel (BoolStream   s) = BoolVStream <$> getStreamValue s
-getVarModel (IntStream    s) = IntVStream <$> getStreamValue s
-getVarModel (RealStream   s) = RealVStream <$> getStreamValue s
-getVarModel (EnumStream _ s) = EnumVStream <$> getStreamValue s
-getVarModel (ProdStream   s) = ProdVStream <$> mapM getVarModel s
-
-getStreamValue :: SMTValue t => Stream t -> ModelM (ValueStreamT t)
-getStreamValue s
-  = ask >>=
-    liftSMT . mapM (\i -> getValue $ s `app` i)
-
-scadeScenario :: Ident i => Program i -> [String] -> Natural -> Model i -> Doc
-scadeScenario p varPath lastIndex m =
+getVarModel :: TypedExpr -> ModelM ValueStream
+getVarModel (BoolExpr s) = do varMap   <- ask
+                              let i = fromJust $ List.elemIndex (BoolExpr s) (varMap Map.! 0)
+                              stream <- liftSMT $ mapM (\l -> getValue $ unBool $ l !! i) varMap
+                              return $ BoolVStream stream
+getVarModel (IntExpr s)  = do varMap   <- ask
+                              let i = fromJust $ List.elemIndex (IntExpr s) (varMap Map.! 0)
+                              stream <- liftSMT $ mapM (\l -> getValue $ unInt $ l !! i) varMap
+                              return $ IntVStream stream
+getVarModel (RealExpr s) = do varMap   <- ask
+                              let i = fromJust $ List.elemIndex (RealExpr s) (varMap Map.! 0)
+                              stream <- liftSMT $ mapM (\l -> getValue $ unReal $ l !! i) varMap
+                              return $ RealVStream stream
+getVarModel (EnumExpr s) = do varMap   <- ask
+                              let i = fromJust $ List.elemIndex (EnumExpr s) (varMap Map.! 0)
+                              stream <- liftSMT $ mapM (\l -> getValue $ unEnum $ l !! i) varMap
+                              return $ EnumVStream stream
+getVarModel (ProdExpr s) = do varMap <- ask
+                              let i = fromJust $ List.elemIndex (ProdExpr s) (varMap Map.! 0)
+                                  newArg = Map.map (\l -> Arr.elems $ unProd $ l !! i) varMap
+                              stream <- liftSMT $ mapM (\a -> runReaderT (getVarModel a) newArg) s
+                              return $ ProdVStream stream
+
+scadeScenario :: Ident i =>
+              Program i -> [String] -> Model i -> Doc
+scadeScenario p varPath m =
   let progInputNames = map varIdent . declsInput $ progDecls p
       progInputs = (Map.fromList $ zip progInputNames (repeat ()))
+      lastIndex = case fmap fst . Map.minView . modelVars $ m of
+        Nothing -> 0
+        Just s -> getLastIndex s
       inputTraces = Map.toList $ (modelVars m) `Map.intersection` progInputs
       path = case varPath of
         [] -> mempty
         _ -> (hcat $ punctuate (text "::") $ map text varPath) <> text ("/")
   in scenario inputTraces path lastIndex 0
   where
+    -- | Retrieves the last defined index of a given stream
+    getLastIndex :: ValueStream -> Natural
+    getLastIndex (BoolVStream s) = highestIndex s
+    getLastIndex (IntVStream s)  = highestIndex s
+    getLastIndex (RealVStream s) = highestIndex s
+    getLastIndex (EnumVStream s) = highestIndex s
+     -- abuses that products are non-empty
+    getLastIndex (ProdVStream a) = getLastIndex (a ! 0)
+
+    -- | Usese that streams are given by maps and so we can use findMax to
+    -- get the highest defined index.
+    highestIndex :: ValueStreamT t -> Natural
+    highestIndex s
+      | Map.null s = 0
+      | otherwise  = fst $ Map.findMax s
+
+    -- | Creates a Doc for all indices i..n from inp, setting the variables
+    -- under path.
     scenario inp path n i
       | i <= n =
         let setOp = text "SSM::set"
diff --git a/lamaSMT/lib/Posets.hs b/lamaSMT/lib/Posets.hs
new file mode 100644
index 0000000..62a13ef
--- /dev/null
+++ b/lamaSMT/lib/Posets.hs
@@ -0,0 +1,152 @@
+module Posets where
+
+import Lang.LAMA.Types
+
+import Language.SMTLib2 as SMT
+
+import qualified Data.Set as Set
+import Data.Set (Set)
+import qualified Data.List as List
+import qualified Data.Map as Map
+import Data.Map (Map)
+import Data.List ((\\))
+import Control.Monad.State
+import Control.Arrow ((***))
+
+import LamaSMTTypes
+import Internal.Monads
+import Definition
+
+data Term = BoolTerm Int | IntTerm Int
+  deriving (Show, Ord, Eq)
+
+type GraphNode = [Term]
+type GraphEdge = (Int, Int)
+type ChainNode = ([Integer], [Term])
+type Chain     = [ChainNode]
+
+data Poset =
+  PosetGraph [GraphNode] [GraphEdge]
+  | PosetChains [Chain] (Map Term [Term])
+  deriving (Show, Ord, Eq)
+
+type GraphM = State [GraphEdge]
+
+initGraph :: GraphNode -> Maybe Poset
+initGraph instSet = Just $ PosetGraph [instSet] []
+
+initChains :: [Term] -> Maybe Poset
+initChains instSet = Just $ PosetChains [[([], instSet)]] $ Map.singleton (head instSet) []
+
+getPosetStats :: Poset -> String
+getPosetStats (PosetGraph ns es) = (show $ sum (map (\i -> (List.length i) - 1) ns)) ++ " equalities and " ++ (show $ List.length es) ++  " inequalities"
+getPosetStats (PosetChains cs m) = (show $ sum $ Set.toList (Set.map (\(_,i) -> (List.length i) - 1) $ getChainNodeSet cs)) ++ " equalities and " ++ (show $ (sum (map (\i -> (List.length i) - 1) cs)) + (List.length $ concat $ Map.elems m)) ++  " inequalities"
+
+getChainNodeSet :: [Chain] -> Set ChainNode
+getChainNodeSet cs = foldl (\s t -> Set.insert t s) Set.empty $ concat cs
+
+buildNextGraph :: ([GraphNode], [GraphNode]) -> [GraphEdge] -> Poset
+buildNextGraph (v0, v1) e = let leaves = getLeaves e
+                                i = length v0
+                                firstEdges = [(a, a+i) | a <- [0..i-1]] ++ e
+                                otherEdges = evalState (traverseGraph i leaves) e
+                                in removeUnreachableNodes $ removeEmptyNodes $ PosetGraph (v0 ++ v1) (firstEdges ++ otherEdges)
+  where
+    getLeaves ed = [snd $ head ed]
+
+removeEmptyNodes :: Poset -> Poset
+removeEmptyNodes (PosetGraph vs es) = PosetGraph (map snd vs') $ newEdges es
+  where
+    vs' = filter (\(_,v) -> not $ null v) $ zip [0..] vs
+    newEdges ((a,b):eds) = case List.elemIndex a (map fst vs') of
+                           Nothing -> newEdges eds
+                           Just i -> case List.elemIndex b (map fst vs') of
+                                       Nothing -> newEdges eds
+                                       Just j -> [(i,j)] ++ newEdges eds
+    newEdges [] = []
+removeEmptyNodes _ = error "Poset is not a graph"
+
+removeUnreachableNodes :: Poset -> Poset
+removeUnreachableNodes (PosetGraph vs es) = PosetGraph (map snd vs') $ newEdges es
+  where
+    vs' = filter (\a -> (elem (fst a) nodesWithEdges) || (length (snd a) > 1)) $ zip [0..] vs
+    nodesWithEdges = (fst $ unzip es) ++ (snd $ unzip es)
+    newEdges ((a,b):eds) = case List.elemIndex a (map fst vs') of
+                           Nothing -> newEdges eds
+                           Just i -> case List.elemIndex b (map fst vs') of
+                                       Nothing -> newEdges eds
+                                       Just j -> [(i,j)] ++ newEdges eds
+    newEdges [] = []
+removeUnreachableNodes _ = error "Poset is not a graph"
+
+traverseGraph :: Int -> [Int] -> GraphM [GraphEdge]
+traverseGraph i (l:ls) = do edgesLeft <- get
+                            let p = getPredecessors l edgesLeft
+                            put $ edgesLeft \\ p
+                            top <- traverseGraph i (map fst p)
+                            rest <- traverseGraph i ls
+                            return $ map ((+i) *** (+i)) p ++ top ++ rest
+  where
+    getPredecessors a e = [(x,y) | (x,y) <- e, y == a]
+
+traverseGraph _ [] = return []
+
+type SortM = State ([Chain], Map Term [Term])
+
+buildNextChain :: [ChainNode] -> Poset
+buildNextChain ns = let s = execState (mapM insertChain ns) ([], Map.empty)
+                    in PosetChains (fst s) (snd s)
+
+insertChain :: ChainNode -> SortM ()
+insertChain node = do chains <- get
+                      let res = unzip $ map (tryChain node) $ fst chains
+                          newChains = if fst chains == fst res then [[node]] else []
+                      put (fst res ++ newChains, Map.unions $ snd res ++ [snd chains, Map.singleton (head $ snd node) []])
+  where
+    tryChain :: ChainNode -> Chain -> (Chain, Map Term [Term])
+    tryChain n@(is,ts) c = let gB = List.findIndices (\a -> and $ map (\(b,c) -> b < c) $ zip (fst a) is) c
+                               i  = if List.length gB == 0 then 0 else (maximum gB) + 1
+                               lA = List.findIndices (\a -> and $ map (\(b,c) -> b > c) $ zip (fst a) is) c
+                               j  = if List.length lA == 0 then 0 else (minimum lA) + 1
+                           in if j == 1
+                             then ([n] ++ c, Map.empty)
+                             else if i == j - 1
+                               then let (cl,cr) = List.splitAt i c
+                                    in (cl ++ [n] ++ cr, Map.empty)
+                               else if i == List.length c
+                                 then (c ++ [n], Map.empty)
+                                 else let m1 = if i > 0 then Map.singleton (head $ snd (c !! (i - 1))) [head ts] else Map.empty
+                                          m2 = if j > 0 then Map.singleton (head ts) [head $ snd (c !! (j - 1))] else Map.empty
+                                      in (c, m1 `Map.union` m2)
+
+assertPoset :: MonadSMT m => (SMTExpr Bool -> SMTExpr Bool) -> ([TypedExpr], [TypedExpr]) -> Poset -> m ()
+assertPoset f i (PosetChains cs m) = do let eq = concat $ map (assertEquality . snd) $ Set.toList $ getChainNodeSet cs
+                                            rep = map (map (head . snd)) cs
+                                            cc = concat $ map assertChain rep
+                                            c  = foldl (.&&.) (constant True) $ cc ++ eq
+                                        liftSMT $ assert $ f c
+  where
+    assertEquality (_:[]) = [constant True]
+    assertEquality (t:ts) = map (\a -> mkIntRelation (fst i) (a, t) (.==.)) ts
+    assertChain [] = [constant True]
+    assertChain (_:[]) = [constant True]
+    assertChain (t:ts) = [mkIntRelation (fst i) (t, head ts) (.<=.)] ++ assertChain (m Map.! t) ++ assertChain ts
+    assertChain x = error $ "ha: " ++ show x
+assertPoset f i (PosetGraph vs es) = do let vcs = map assertPosetGraphVs vs
+                                            vc = foldl (.&&.) (constant True) $ vcs ++ assertPosetGraphEs es
+                                        liftSMT $ assert (f vc)
+  where
+    assertPosetGraphVs (_:[]) = constant True
+    assertPosetGraphVs (vc:vcs) = let c = map (\a -> mkBoolRelation (fst i) (a, vc) (.==.)) vcs in
+                                  foldl (.&&.) (head c) $ tail c
+    assertPosetGraphVs [] = constant True
+    assertPosetGraphEs ecs = map (\(a,b) -> mkBoolRelation (fst i) (head (vs !! a), head (vs !! b)) (.=>.)) ecs
+
+
+mkBoolRelation :: [TypedExpr] -> (Term, Term) -> (SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool) -> SMTExpr Bool
+mkBoolRelation i (BoolTerm f, BoolTerm g) r =
+  (unBool $ head $ lookupArgs [f] False (i,i)) `r` (unBool $ head $ lookupArgs [g] False (i,i))
+
+mkIntRelation :: [TypedExpr] -> (Term, Term) -> (SMTExpr Integer -> SMTExpr Integer -> SMTExpr Bool) -> SMTExpr Bool
+mkIntRelation i (IntTerm f, IntTerm g) r =
+  (unInt $ head $ lookupArgs [f] False (i,i)) `r` (unInt $ head $ lookupArgs [g] False (i,i))
diff --git a/lamaSMT/lib/Strategies/BMC.hs b/lamaSMT/lib/Strategies/BMC.hs
index fb2c724..4457654 100644
--- a/lamaSMT/lib/Strategies/BMC.hs
+++ b/lamaSMT/lib/Strategies/BMC.hs
@@ -1,21 +1,24 @@
 {-# LANGUAGE ViewPatterns #-}
-module Strategies.BMC (BMC, assumeTrace, checkInvariant, bmcStep, assertPrecond) where
+{-# LANGUAGE FlexibleContexts #-}
+module Strategies.BMC (BMC, assumeTrace, checkInvariant, bmcStep, assertPrecond, freshVars) where
 
 import Data.Natural
-import NatInstance
 import Data.List (stripPrefix)
 import qualified Data.Map as Map
 import Data.Map (Map)
+import qualified Data.Array as Array
 
 import Control.Monad.IO.Class
-import Control.Monad (when, liftM)
+import Control.Monad.State
 
 import Language.SMTLib2
+import Language.SMTLib2.Internals (SMTExpr(Var))
 
 import Strategy
 import LamaSMTTypes
 import Definition
-import Model (Model)
+import TransformEnv
+import Model (Model, getModel)
 import Internal.Monads
 
 data BMC = BMC
@@ -33,64 +36,99 @@ instance StrategyClass BMC where
     s { bmcPrintProgress = True }
   readOption o _ = error $ "Invalid BMC option: " ++ o
 
-  check natAnn s getModel defs =
+  check s env defs =
     let base = 0
-    in do baseDef <- liftSMT . defConst $ constantAnn base natAnn
-          check' natAnn s getModel defs (Map.singleton base baseDef) base baseDef
-
-assumeTrace :: MonadSMT m => ProgDefs -> StreamPos -> m ()
-assumeTrace defs iDef =
-  assertDefs iDef (flowDef defs) >>
-  assertPrecond iDef (precondition defs)
-
-bmcStep :: MonadSMT m
-             => (Map Natural StreamPos -> SMT (Model i))
-             -> ProgDefs -> Map Natural StreamPos -> StreamPos -> m (Maybe (Model i))
-bmcStep getModel defs pastIndices iDef =
-  do assumeTrace defs iDef
+        vars = varList env
+    in do fresh <- freshVars vars
+          check' s (getModel $ varEnv env) defs (Map.singleton base vars) base (vars, fresh)
+
+assumeTrace :: MonadSMT m => ProgDefs -> ([TypedExpr], [TypedExpr]) -> m ()
+assumeTrace defs args =
+  assertDefs args (flowDef defs) >>
+  assertPrecond args (precondition defs)
+
+bmcStep :: MonadSMT m =>
+        (Map Natural [TypedExpr] -> SMT (Model i))
+        -> ProgDefs
+        -> Map Natural [TypedExpr]
+        -> ([TypedExpr], [TypedExpr])
+        -> m (Maybe (Model i))
+bmcStep getModel defs pastVars vars =
+  do assumeTrace defs vars
      let invs = invariantDef defs
      liftSMT . stack
-       $ checkInvariant iDef invs >>=
-       checkGetModel getModel pastIndices
-
-check' :: SMTAnnotation Natural -> BMC -> (Map Natural StreamPos -> SMT (Model i))
-          -> ProgDefs -> Map Natural StreamPos -> Natural -> StreamPos -> SMTErr (Maybe (Natural, Model i))
-check' natAnn s getModel defs pastIndices i iDef =
+       $ checkInvariant vars invs >>=
+       checkGetModel getModel pastVars
+
+check' :: BMC
+       -> (Map Natural [TypedExpr] -> SMT (Model i))
+       -> ProgDefs
+       -> Map Natural [TypedExpr]
+       -> Natural
+       -> ([TypedExpr], [TypedExpr])
+       -> SMTErr (StrategyResult i)
+check' s getModel defs pastVars i vars =
   do liftIO $ when (bmcPrintProgress s) (putStrLn $ "Depth " ++ show i)
-     r <- bmcStep getModel defs pastIndices iDef
+     r <- bmcStep getModel defs pastVars vars
      case r of
-       Nothing -> next (check' natAnn s getModel defs) natAnn s pastIndices i iDef
-       Just m -> return $ Just (i, m)
+       Nothing -> next (check' s getModel defs) s pastVars i vars
+       Just m -> return $ Failure i m
 
-assertDefs :: MonadSMT m => SMTExpr Natural -> [Definition] -> m ()
+assertDefs :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> [Definition] -> m ()
 assertDefs i = mapM_ (assertDef i)
 
-assertDef :: MonadSMT m => SMTExpr Natural -> Definition -> m ()
+assertDef :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> Definition -> m ()
 assertDef = assertDefinition id
 
-assertPrecond :: MonadSMT m => SMTExpr Natural -> Definition -> m ()
+assertPrecond :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> Definition -> m ()
 assertPrecond = assertDefinition id
 
 -- | Returns true, if the invariant holds
-checkInvariant :: MonadSMT m => SMTExpr Natural -> Definition -> m Bool
+checkInvariant :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> Definition -> m Bool
 checkInvariant i p = liftSMT $ assertDefinition not' i p >> liftM not checkSat
 
-checkGetModel :: MonadSMT m
-                 => (Map Natural StreamPos -> SMT (Model i)) -> Map Natural StreamPos
-                 -> Bool -> m (Maybe (Model i))
+checkGetModel :: MonadSMT m =>
+              (Map Natural [TypedExpr] -> SMT (Model i))
+              -> Map Natural [TypedExpr]
+              -> Bool
+              -> m (Maybe (Model i))
 checkGetModel getModel indices r = liftSMT $
   if r then return Nothing else fmap Just $ getModel indices
 
-next :: (Map Natural StreamPos -> Natural -> SMTExpr Natural -> SMTErr (Maybe (Natural, Model i)))
-        -> SMTAnnotation Natural
-        -> BMC -> Map Natural StreamPos -> Natural -> SMTExpr Natural -> SMTErr (Maybe (Natural, Model i))
-next checkCont natAnn s pastIndices i iDef =
-  do let i' = succ i
-     iDef' <- liftSMT . defConst$ succ' natAnn iDef
-     let pastIndices' = Map.insert i' iDef' pastIndices
-     case bmcDepth s of
-       Nothing -> checkCont pastIndices' i' iDef'
+next :: (Map Natural [TypedExpr]
+             -> Natural
+             -> ([TypedExpr], [TypedExpr])
+             -> SMTErr (StrategyResult i)
+        )
+        -> BMC
+        -> Map Natural [TypedExpr]
+        -> Natural
+        -> ([TypedExpr], [TypedExpr])
+        -> SMTErr (StrategyResult i)
+next checkCont s pastVars i vars =
+  let i' = succ i
+      pastVars' = Map.insert i' (snd vars) pastVars
+  in case bmcDepth s of
+       Nothing -> do vars' <- freshVars $ snd vars
+                     checkCont pastVars' i' (snd vars, vars')
        Just l ->
          if i' < l
-         then checkCont pastIndices' i' iDef'
-         else return Nothing
+         then do vars' <- freshVars $ snd vars
+                 checkCont pastVars' i' (snd vars, vars')
+         else return Success
+
+freshVars :: MonadSMT m => [TypedExpr] -> m [TypedExpr]
+freshVars vars = liftSMT $ mapM newVar vars
+  where
+    newVar (BoolExpr _)          = do new <- var
+                                      return $ BoolExpr new
+    newVar (IntExpr _)           = do new <- var
+                                      return $ IntExpr new
+    newVar (RealExpr _)          = do new <- var
+                                      return $ RealExpr new
+    newVar (EnumExpr (Var _ k))  = do new <- varAnn k
+                                      return $ EnumExpr new
+    newVar (ProdExpr arr)        =
+      do newList <- mapM newVar (Array.elems arr)
+         let newProd = mkProdExpr newList
+         return newProd
diff --git a/lamaSMT/lib/Strategies/Factory.hs b/lamaSMT/lib/Strategies/Factory.hs
index e4b6e7e..e3b440c 100644
--- a/lamaSMT/lib/Strategies/Factory.hs
+++ b/lamaSMT/lib/Strategies/Factory.hs
@@ -6,6 +6,7 @@ import Text.PrettyPrint
 import Strategy
 import Strategies.BMC
 import Strategies.KInduction
+import Strategies.Invariant
 
 defaultStrategy :: Strategy
 defaultStrategy = Strategy (defaultStrategyOpts :: BMC)
@@ -45,4 +46,5 @@ getStrategyHelp lineLength = renderStyle (style { lineLength }) $
 getStrategy :: String -> Strategy
 getStrategy "bmc" = Strategy (defaultStrategyOpts :: BMC)
 getStrategy "kinduct" = Strategy (defaultStrategyOpts :: KInduct)
-getStrategy _ = error "Unknown strategy"
\ No newline at end of file
+getStrategy "kinduct-inv" = Strategy (defaultStrategyOpts :: Invar)
+getStrategy _ = error "Unknown strategy"
diff --git a/lamaSMT/lib/Strategies/Invariant.hs b/lamaSMT/lib/Strategies/Invariant.hs
new file mode 100644
index 0000000..4efd238
--- /dev/null
+++ b/lamaSMT/lib/Strategies/Invariant.hs
@@ -0,0 +1,261 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
+module Strategies.Invariant where
+
+import Data.Natural
+import qualified Data.List as List
+import Data.List (stripPrefix)
+import qualified Data.Map as Map
+import Data.Map (Map)
+import Data.Maybe (fromMaybe, isJust, fromJust)
+
+import Control.Monad.State (MonadState(..), StateT, evalStateT, modify)
+import Control.Monad.Writer (MonadWriter(..), WriterT, runWriterT)
+import Control.Monad.IO.Class
+import Control.Monad (when, filterM)
+import Control.Arrow ((&&&))
+
+import Language.SMTLib2
+
+import Strategy
+import LamaSMTTypes
+import Definition
+import Posets
+import TransformEnv
+import Model (Model, getModel)
+import Strategies.BMC
+import Internal.Monads
+
+data GenerateHints =
+     NoHints
+     | LastInductionStep
+     | AllInductionSteps
+data Invar = Invar
+               { depth :: Maybe Natural
+               , printProgress  :: Bool
+               , printInvStats  :: Bool
+               , boolInvariants :: Bool
+               , intInvariants  :: Bool
+               , generateHints  :: GenerateHints }
+
+instance StrategyClass Invar where
+  defaultStrategyOpts = Invar Nothing False False True True NoHints
+
+  readOption (stripPrefix "depth=" -> Just d) indOpts =
+    case d of
+      "inf" -> indOpts { depth = Nothing }
+      _     -> indOpts { depth = Just $ read d }
+  readOption "progress" indOpts =
+    indOpts { printProgress = True }
+  readOption "invariant-stats" indOpts =
+    indOpts { printInvStats = True }
+  readOption "only-bool-inv" indOpts =
+    indOpts { intInvariants = False }
+  readOption "only-int-inv" indOpts =
+    indOpts { boolInvariants = False }
+  readOption (stripPrefix "hints" -> Just r) indOpts =
+    case (stripPrefix "=" r) of
+         Nothing    -> indOpts { generateHints = LastInductionStep }
+         Just which -> case which of
+              "all"  -> indOpts { generateHints = AllInductionSteps }
+              "last" -> indOpts { generateHints = LastInductionStep }
+              _      -> error $ "Invalid hint option: " ++ which
+  readOption o _ = error $ "Invalid invariant option: " ++ o
+
+  check indOpts env defs =
+    let baseK = 0
+        vars  = varList env
+    in do k1  <- freshVars vars
+          n0  <- freshVars vars
+          n1  <- freshVars vars
+          assumeTrace defs (n0, n1)
+          let s0 = InductState baseK (vars, k1) (n0, n1) (initGraph $ instSetBool env) Nothing (initChains $ instSetInt env) Nothing
+          (r, hints) <- runWriterT
+                $ (flip evalStateT s0)
+                $ check' indOpts (getModel $ varEnv env) defs (Map.singleton baseK vars) [n0]
+          case r of
+               Unknown what h -> return $ Unknown what (h ++ hints)
+               _ -> return r
+
+-- | Checks the induction step and returns true if the invariant could be
+-- proven
+checkStep :: ProgDefs -> ([TypedExpr], [TypedExpr]) -> SMT Bool
+checkStep defs vars =
+  do assumeTrace defs vars
+     let invs = invariantDef defs
+     checkInvariant vars invs
+
+-- | Holds current depth k and definitions of last k and n
+data InductState = InductState
+                   { kVal     :: Natural
+                   , kDefs    :: ([TypedExpr], [TypedExpr])
+                   , nDefs    :: ([TypedExpr], [TypedExpr])
+                   , binPoset :: Maybe Poset
+                   , binInv   :: Maybe Poset
+                   , intPoset :: Maybe Poset
+                   , intInv   :: Maybe Poset }
+type KInductM i = StateT InductState (WriterT (Hints i) SMTErr)
+
+-- | Checks the program against its invariant. If the invariant
+-- does not hold in the base case, then a model is returned.
+-- If the base case is fine, but the induction step is not, we
+-- call next, which increases k. Finally, if also the induction
+-- step can be proven, Nothing is returned.
+check' :: Invar
+       -> (Map Natural [TypedExpr] -> SMT (Model i))
+       -> ProgDefs
+       -> Map Natural [TypedExpr]
+       -> [[TypedExpr]]
+       -> KInductM i (StrategyResult i)
+check' indOpts getModel defs pastVars pastNs =
+  do InductState{..} <- get
+     liftIO $ when (printProgress indOpts) (putStrLn $ "Depth " ++ show kVal)
+     when (printInvStats indOpts) $ do invStats <- showInvStats
+                                       liftIO $ putStr invStats
+     rBMC <- bmcStep getModel defs pastVars kDefs
+     case rBMC of
+       Just m -> return $ Failure kVal m
+       Nothing ->
+         do let n0 = fst nDefs
+                n1 = snd nDefs
+                pastNs' = pastNs ++ [n1]
+            n2 <- freshVars n1
+            assertPrecond (n0, n1) $ invariantDef defs
+            modify $ \indSt -> indSt { nDefs = (n1, n2) }
+            heuristicInvariants indOpts defs pastNs
+            (indSuccess, hints) <- liftSMT . stack $
+              do r <- checkStep defs (n1, n2)
+                 h <- retrieveHints (getModel pastVars) indOpts kVal r
+                 return (r, h)
+            tell hints
+            let k' = succ kVal
+            if indSuccess
+               then return Success
+               else case depth indOpts of
+                      Nothing -> cont k' pastVars pastNs'
+                      Just l  ->
+                        if k' > l
+                          then return $ Unknown ("Cancelled induction. Found no"
+                                                   ++" proof within given depth")
+                                         []
+                          else cont k' pastVars pastNs'
+  where
+    cont k' pastVars pNs =
+      do indState@InductState{..} <- get
+         let k1 = snd kDefs
+             pastVars' = Map.insert k' k1 pastVars
+         k2 <- freshVars k1
+         put $ indState { kVal = k', kDefs = (k1, k2) }
+         check' indOpts getModel defs pastVars' pNs
+    showInvStats = do
+      InductState{..} <- get
+      let boolStat = getPosetStats $ fromMaybe (fromJust binInv) binPoset
+          intStat  = getPosetStats $ fromMaybe (fromJust intInv) intPoset
+          boolText = if isJust binPoset then "Possible boolean invariants: " ++ boolStat else "Boolean invariants: " ++ boolStat
+          intText  = if isJust intPoset then "Possible integer invariants: " ++ intStat else "Integer invariants: " ++ intStat
+      return $ (if boolInvariants indOpts then boolText ++ "\n" else "") ++ (if intInvariants indOpts then intText ++ "\n" else "")
+
+heuristicInvariants :: Invar -> ProgDefs -> [[TypedExpr]] -> KInductM i ()
+heuristicInvariants indOpts defs pastNs = do
+  InductState{..} <- get
+  when (boolInvariants indOpts) $ if (isJust binPoset)
+  then
+    do binPoset' <- filterC (fromJust binPoset) kDefs
+       case binPoset' of
+         Just b  -> modify $ \indSt -> indSt { binPoset = Just b }
+         Nothing -> do liftIO $ when (printInvStats indOpts) $ putStrLn "Trying to prove inductive boolean invariants..."
+                       binInv' <- checkInvariantStep (fromJust binPoset) nDefs pastNs defs
+
+                       assertPoset id nDefs binInv'
+                       modify $ \indSt -> indSt { binPoset = Nothing, binInv = Just binInv' }
+  else
+    assertPoset id nDefs $ fromJust binInv
+  when (intInvariants indOpts) $ if (isJust intPoset)
+  then
+    do intPoset' <- filterC (fromJust intPoset) kDefs
+       case intPoset' of
+         Just i  -> modify $ \indSt -> indSt { intPoset = Just i }
+         Nothing -> do liftIO $ when (printInvStats indOpts) $ putStrLn "Trying to prove inductive integer invariants..."
+                       intInv' <- checkInvariantStep (fromJust intPoset) nDefs pastNs defs
+                       assertPoset id nDefs intInv'
+                       modify $ \indSt -> indSt { intPoset = Nothing, intInv = Just intInv' }
+  else
+    assertPoset id nDefs $ fromJust intInv
+
+filterC :: MonadSMT m => Poset -> ([TypedExpr], [TypedExpr]) -> m (Maybe Poset)
+filterC g@(PosetGraph v e) args =
+  liftSMT $ do push
+               assertPoset not' args g
+               r  <- checkSat
+               if r
+                 then do v0' <- mapM (filterM (\a -> evalBoolTerm args a >>= return . not)) v
+                         v1' <- mapM (filterM $ evalBoolTerm args) v
+                         pop
+                         return $ Just $ buildNextGraph (v0', v1') e
+                  else pop >> return Nothing
+filterC i@(PosetChains cs m) args =
+  liftSMT $ do push
+               assertPoset not' args i
+               r  <- checkSat
+               if r
+                 then do let nodes = concat cs
+                         part <- mapM (partitionChainNode args) nodes
+                         pop
+                         return $ Just $ buildNextChain $ concat part
+                  else pop >> return Nothing
+
+partitionChainNode :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> ChainNode -> m [ChainNode]
+partitionChainNode args node = do values <- mapM (evalIntTerm args) $ snd node
+                                  let comb = zip values (snd node)
+                                      part = List.groupBy (\(a,_) (b,_) -> a == b) $ List.sort comb
+                                  return $ map (\n -> (fst node ++ [fst (head n)], map snd n)) part
+
+checkInvariantStep :: MonadSMT m => Poset -> ([TypedExpr], [TypedExpr]) -> [[TypedExpr]] -> ProgDefs -> m Poset
+
+checkInvariantStep g args pastVars defs = liftSMT $ do
+  push
+  mapM (\a -> assertPoset id (a,a) g) $ pastVars
+  assumeTrace defs args
+  g' <- checkInvariantStep' g
+  pop
+  return g'
+  where
+    checkInvariantStep' graph@(PosetGraph v e) = do
+      push
+      assertPoset not' args graph
+      r <- checkSat
+      if r
+        then do v0' <- mapM (filterM (\a -> evalBoolTerm args a >>= return . not)) v
+                v1' <- mapM (filterM $ evalBoolTerm args) v
+                pop
+                graph' <- checkInvariantStep' $ buildNextGraph (v0', v1') e
+                return graph'
+         else pop >> return graph
+    checkInvariantStep' chains@(PosetChains cs m) = do
+      push
+      assertPoset not' args chains
+      r <- checkSat
+      if r
+        then do let nodes = concat cs
+                part <- mapM (partitionChainNode args) nodes
+                pop
+                chains' <- checkInvariantStep' $ buildNextChain $ concat part
+                return chains'
+        else pop >> return chains
+
+-- | If requested, gets a model for the induction step
+retrieveHints :: SMT (Model i)
+              -> Invar
+              -> Natural
+              -> Bool
+              -> SMT [(Hint i)]
+retrieveHints getModel indOpts k success =
+  case (generateHints  &&& depth) indOpts of
+       (NoHints          , _      ) -> return []
+       (LastInductionStep, Nothing) -> return []
+       (LastInductionStep, Just l ) ->
+         if not success && succ k > l
+         then getModel >>= \m -> return [Hint (show k) m]
+         else return []
+       (AllInductionSteps, _      ) ->
+         getModel >>= \m -> return [Hint (show k) m]
diff --git a/lamaSMT/lib/Strategies/KInduction.hs b/lamaSMT/lib/Strategies/KInduction.hs
index a3d0faa..6572d7d 100644
--- a/lamaSMT/lib/Strategies/KInduction.hs
+++ b/lamaSMT/lib/Strategies/KInduction.hs
@@ -3,88 +3,143 @@
 module Strategies.KInduction where
 
 import Data.Natural
-import NatInstance
 import Data.List (stripPrefix)
 import qualified Data.Map as Map
 import Data.Map (Map)
 
 import Control.Monad.State (MonadState(..), StateT, evalStateT, modify)
+import Control.Monad.Writer (MonadWriter(..), WriterT, runWriterT)
 import Control.Monad.IO.Class
 import Control.Monad (when)
-import Control.Monad.Error (throwError)
+import Control.Arrow ((&&&))
 
 import Language.SMTLib2
 
 import Strategy
 import LamaSMTTypes
 import Definition
-import Model (Model)
+import TransformEnv
+import Model (Model, getModel)
 import Strategies.BMC
 import Internal.Monads
 
+data GenerateHints =
+     NoHints
+     | LastInductionStep
+     | AllInductionSteps
 data KInduct = KInduct
                { depth :: Maybe Natural
-               , printProgress :: Bool }
+               , printProgress :: Bool
+               , generateHints :: GenerateHints }
 
 instance StrategyClass KInduct where
-  defaultStrategyOpts = KInduct Nothing False
+  defaultStrategyOpts = KInduct Nothing False NoHints
 
-  readOption (stripPrefix "depth=" -> Just d) s =
+  readOption (stripPrefix "depth=" -> Just d) indOpts =
     case d of
-      "inf" -> s { depth = Nothing }
-      _ -> s { depth = Just $ read d }
-  readOption "progress" s =
-    s { printProgress = True }
+      "inf" -> indOpts { depth = Nothing }
+      _     -> indOpts { depth = Just $ read d }
+  readOption "progress" indOpts =
+    indOpts { printProgress = True }
+  readOption (stripPrefix "hints" -> Just r) indOpts =
+    case (stripPrefix "=" r) of
+         Nothing    -> indOpts { generateHints = LastInductionStep }
+         Just which -> case which of
+              "all"  -> indOpts { generateHints = AllInductionSteps }
+              "last" -> indOpts { generateHints = LastInductionStep }
+              _      -> error $ "Invalid hint option: " ++ which
   readOption o _ = error $ "Invalid k-induction option: " ++ o
 
-  check natAnn s getModel defs =
+  check indOpts env defs =
     let baseK = 0
-    in do baseKDef <- liftSMT . defConst $ constantAnn baseK natAnn
-          baseNDef <- liftSMT $ varAnn natAnn
-          assumeTrace defs baseNDef
-          let s0 = InductState baseK baseKDef baseNDef (Map.singleton baseK baseKDef)
-          (flip evalStateT s0) $ check' natAnn s getModel defs
+        vars  = varList env
+    in do k1  <- freshVars vars
+          n0  <- freshVars vars
+          n1  <- freshVars vars
+          assumeTrace defs (n0, n1)
+          let s0 = InductState baseK (vars, k1) (n0, n1)
+          (r, hints) <- runWriterT
+                $ (flip evalStateT s0)
+                $ check' indOpts (getModel $ varEnv env) defs (Map.singleton baseK vars)
+          case r of
+               Unknown what h -> return $ Unknown what (h ++ hints)
+               _ -> return r
 
-checkStep :: MonadSMT m => ProgDefs -> StreamPos -> m Bool
-checkStep defs iDef =
-  do assumeTrace defs iDef
+-- | Checks the induction step and returns true if the invariant could be
+-- proven
+checkStep :: ProgDefs -> ([TypedExpr], [TypedExpr]) -> SMT Bool
+checkStep defs vars =
+  do assumeTrace defs vars
      let invs = invariantDef defs
-     liftSMT . stack $ checkInvariant iDef invs
+     checkInvariant vars invs
 
 -- | Holds current depth k and definitions of last k and n
 data InductState = InductState
-                   { kVal :: Natural
-                   , kDef :: StreamPos -- ^ SMT expression for k
-                   , nDef :: StreamPos -- ^ SMT expression for n
-                   , pastKs :: Map Natural StreamPos }
-type KInductM = StateT InductState SMTErr
+                   { kVal  :: Natural
+                   , kDefs :: ([TypedExpr], [TypedExpr])
+                   , nDefs :: ([TypedExpr], [TypedExpr]) }
+type KInductM i = StateT InductState (WriterT (Hints i) SMTErr)
 
-check' :: SMTAnnotation Natural
-          -> KInduct -> (Map Natural StreamPos -> SMT (Model i))
-          -> ProgDefs -> KInductM (Maybe (Natural, Model i))
-check' natAnn s getModel defs =
+-- | Checks the program against its invariant. If the invariant
+-- does not hold in the base case, then a model is returned.
+-- If the base case is fine, but the induction step is not, we
+-- call next, which increases k. Finally, if also the induction
+-- step can be proven, Nothing is returned.
+check' :: KInduct
+       -> (Map Natural [TypedExpr] -> SMT (Model i))
+       -> ProgDefs
+       -> Map Natural [TypedExpr]
+       -> KInductM i (StrategyResult i)
+check' indOpts getModel defs pastVars =
   do InductState{..} <- get
-     liftIO $ when (printProgress s) (putStrLn $ "Depth " ++ show kVal)
-     rBMC <- bmcStep getModel defs pastKs kDef
+     liftIO $ when (printProgress indOpts) (putStrLn $ "Depth " ++ show kVal)
+     rBMC <- bmcStep getModel defs pastVars kDefs
      case rBMC of
-       Just m -> return $ Just (kVal, m)
+       Just m -> return $ Failure kVal m
        Nothing ->
-         do n1 <- liftSMT . defConst $ succ' natAnn nDef
-            modify $ \indSt -> indSt { nDef = n1 }
-            assertPrecond nDef $ invariantDef defs
-            r <- checkStep defs n1
-            if r then return Nothing else next (check' natAnn s getModel defs) natAnn s
+         do let n0 = fst nDefs
+                n1 = snd nDefs
+            n2 <- freshVars n1
+            assertPrecond (n0, n1) $ invariantDef defs
+            modify $ \indSt -> indSt { nDefs = (n1, n2) }
+            (indSuccess, hints) <- liftSMT . stack $
+              do r <- checkStep defs (n1, n2)
+                 h <- retrieveHints (getModel pastVars) indOpts kVal r
+                 return (r, h)
+            tell hints
+            let k' = succ kVal
+            if indSuccess
+               then return Success
+               else case depth indOpts of
+                    Nothing -> cont k' pastVars
+                    Just l  ->
+                      if k' > l
+                      then return $ Unknown ("Cancelled induction. Found no"
+                                              ++" proof within given depth")
+                                    []
+                      else cont k' pastVars
+  where
+    cont k' pastVars =
+      do indState@InductState{..} <- get
+         let k1 = snd kDefs
+             pastVars' = Map.insert k' k1 pastVars
+         k2 <- freshVars k1
+         put $ indState { kVal = k', kDefs = (k1, k2) }
+         check' indOpts getModel defs pastVars'
 
-next :: KInductM (Maybe (Natural, Model i)) -> SMTAnnotation Natural -> KInduct -> KInductM (Maybe (Natural, Model i))
-next checkCont natAnn s =
-  do indState@InductState {..} <- get
-     let k' = succ kVal
-     kDef' <- liftSMT . defConst $ succ' natAnn kDef
-     let pastKs' = Map.insert k' kDef' pastKs
-     put $ indState { kVal = k', kDef = kDef', pastKs = pastKs' }
-     case depth s of
-       Nothing -> checkCont
-       Just l ->
-         if k' < l
-         then checkCont
-         else throwError $ "Cancelled induction. Found no proof within given depth"
+-- | If requested, gets a model for the induction step
+retrieveHints :: SMT (Model i)
+              -> KInduct
+              -> Natural
+              -> Bool
+              -> SMT [(Hint i)]
+retrieveHints getModel indOpts k success =
+  case (generateHints  &&& depth) indOpts of
+       (NoHints          , _      ) -> return []
+       (LastInductionStep, Nothing) -> return []
+       (LastInductionStep, Just l ) ->
+         if not success && succ k > l
+         then getModel >>= \m -> return [Hint (show k) m]
+         else return []
+       (AllInductionSteps, _      ) ->
+         getModel >>= \m -> return [Hint (show k) m]
diff --git a/lamaSMT/lib/Strategy.hs b/lamaSMT/lib/Strategy.hs
index 1946cc7..c88f427 100644
--- a/lamaSMT/lib/Strategy.hs
+++ b/lamaSMT/lib/Strategy.hs
@@ -4,31 +4,38 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 module Strategy where
 
-import Data.Map (Map)
 import Data.Natural
 import Control.Monad.Error
 
 import Language.SMTLib2
 
-import LamaSMTTypes
 import Definition
 import TransformEnv
 import Model
 
 type SMTErr = ErrorT String SMT
+data Hint i = Hint { hintDescr :: String, hintModel :: Model i }
+type Hints i = [Hint i]
+data StrategyResult i =
+     Success
+     | Failure Natural (Model i)
+     | Unknown String (Hints i)
 
 data Strategy = forall s. StrategyClass s => Strategy s
 
 class StrategyClass s where
   defaultStrategyOpts :: s
   readOption :: String -> s -> s
-  check :: SMTAnnotation Natural
-           -> s
-           -> (Map Natural StreamPos -> SMT (Model i))
-           -> ProgDefs -> SMTErr (Maybe (Natural, Model i))
+  check :: s
+           -> Env i
+           -> ProgDefs
+           -> SMTErr (StrategyResult i)
 
-checkWithModel :: SMTAnnotation Natural -> Strategy -> ProgDefs -> VarEnv i -> SMTErr (Maybe (Natural, Model i))
-checkWithModel natAnn (Strategy s) d env = check natAnn s (getModel env) d
+checkWithModel :: Strategy
+               -> ProgDefs
+               -> Env i
+               -> SMTErr (StrategyResult i)
+checkWithModel (Strategy s) d env = check s env d
 
 readOptions' :: String -> Strategy -> Strategy
-readOptions' o (Strategy s) = Strategy $ readOption o s
\ No newline at end of file
+readOptions' o (Strategy s) = Strategy $ readOption o s
diff --git a/lamaSMT/lib/Transform.hs b/lamaSMT/lib/Transform.hs
index a083b8f..74faf36 100644
--- a/lamaSMT/lib/Transform.hs
+++ b/lamaSMT/lib/Transform.hs
@@ -21,8 +21,7 @@ import Lang.LAMA.Identifier
 import Lang.LAMA.Typing.TypedStructure
 import Lang.LAMA.Types
 import Language.SMTLib2 as SMT
-import Language.SMTLib2.Internals (declareType)
-import Data.Unit
+import Language.SMTLib2.Internals (declareType, SMTExpr(Var))
 import Data.String (IsString(..))
 import Data.Array as Arr
 
@@ -32,15 +31,17 @@ import qualified Data.Set as Set
 import Data.Set (Set)
 import qualified Data.Map as Map
 import Data.Map (Map)
+import Data.List (zip4)
 import Prelude hiding (mapM)
 import Data.Traversable
 import Data.Foldable (foldlM, foldrM)
 import Data.Monoid
+import Data.Maybe
 
 import Control.Monad.Trans.Class
 import Control.Monad.State (StateT(..), MonadState(..), gets)
 import Control.Monad.Error (ErrorT(..), MonadError(..))
-import Control.Monad.Reader (ReaderT(..), asks)
+import Control.Monad.Reader (ReaderT(..), ask, asks)
 import Control.Applicative (Applicative(..), (<$>))
 import Control.Arrow ((&&&), second)
 
@@ -50,18 +51,6 @@ import Definition
 import TransformEnv
 import Internal.Monads
 
--- | Gets an "undefined" value for a given type of stream.
--- The stream itself is not further analysed.
--- FIXME: Make behaviour configurable, i.e. bottom can be some
--- default value or a left open stream
--- (atm it does the former).
-getBottom :: TypedStream i -> TypedExpr i
-getBottom (BoolStream _)     = BoolExpr $ constant False
-getBottom (IntStream _)      = IntExpr  $ constant 0xdeadbeef
-getBottom (RealStream _)     = RealExpr . constant $ fromInteger 0xdeadbeef
-getBottom (EnumStream ann _) = EnumExpr $ constantAnn (enumBottom ann) ann
-getBottom (ProdStream strs)  = ProdExpr $ fmap getBottom strs
-
 -- | Transforms a LAMA program into a set of formulas which is
 -- directly declared and a set of defining functions. Those functions
 -- can be used to define a cycle by giving it the point in time.
@@ -71,10 +60,9 @@ getBottom (ProdStream strs)  = ProdExpr $ fmap getBottom strs
 -- gets a value at that time (after getting the model).
 lamaSMT :: Ident i =>
            NatImplementation -> EnumImplementation -> Program i
-           -> ErrorT String SMT (ProgDefs, VarEnv i)
+           -> ErrorT String SMT (ProgDefs, Env i)
 lamaSMT natImpl' enumImpl' =
-  fmap (second varEnv)
-  . flip runStateT (emptyEnv natImpl' enumImpl')
+  flip runStateT (emptyEnv natImpl' enumImpl')
   . declProgram
 
 -- | Declare the formulas which define a LAMA program.
@@ -117,7 +105,7 @@ declareEnum (t, EnumDef cs) =
         liftSMT (declareType (undefined :: SMTEnum) ann) >> return (t, ann)
 
 declareDecls :: Ident i =>
-                Maybe (Stream Bool)
+                Maybe (i, TypedExpr)
                 -> Set i
                 -> Declarations i
                 -> DeclM i ([Definition], Map i (Node i))
@@ -132,48 +120,36 @@ declareDecls activeCond excludeNodes d =
      modifyVars $ mappend (inp `mappend` locs `mappend` states)
      return (concat defs, excluded)
 
-declareVars :: Ident i => [Variable i] -> DeclM i (Map i (TypedStream i))
+declareVars :: Ident i => [Variable i] -> DeclM i (Map i (TypedExpr))
 declareVars = fmap (Map.fromList) . declareVarList
 
-declareVarList :: Ident i => [Variable i] -> DeclM i ([(i, TypedStream i)])
+declareVarList :: Ident i => [Variable i] -> DeclM i ([(i, TypedExpr)])
 declareVarList = mapM declareVar
 
-declareVar :: Ident i => Variable i -> DeclM i ((i, TypedStream i))
+declareVar :: Ident i => Variable i -> DeclM i ((i, TypedExpr))
 declareVar (Variable x t) =
-  do natAnn <- gets natImpl
-     (x,) <$> typedVar (identString x) natAnn t
+  do v    <- typedVar (identString x) t
+     putVar v
+     putTerm v
+     return (x, v)
   where
     typedVar :: Ident i =>
                 String
-                -> SMTAnnotation Natural
                 -> Type i
-                -> DeclM i (TypedStream i)
-    typedVar v ann (GroundType BoolT)
-      = liftSMT $ fmap BoolStream $ funAnnNamed v ann unit
-    typedVar v ann (GroundType IntT)
-      = liftSMT $ fmap IntStream $ funAnnNamed v ann unit
-    typedVar v ann (GroundType RealT)
-      = liftSMT $ fmap RealStream $ funAnnNamed v ann unit
-    typedVar v ann (GroundType _) = $notImplemented
-    typedVar v ann (EnumType et)
+                -> DeclM i (TypedExpr)
+    typedVar v (GroundType BoolT)
+      = liftSMT $ fmap BoolExpr $ varNamed v
+    typedVar v (GroundType IntT)
+      = liftSMT $ fmap IntExpr $ varNamed v
+    typedVar v (GroundType RealT)
+      = liftSMT $ fmap RealExpr $ varNamed v
+    typedVar v (GroundType _) = $notImplemented
+    typedVar v (EnumType et)
       = do etAnn <- lookupEnumAnn et
-           liftSMT $ fmap (EnumStream etAnn) $ funAnnNamed v ann etAnn
-    typedVar v ann (ProdType ts) =
-      do vs <- mapM (typedVar (v ++ "_comp") ann) ts
-         return (ProdStream $ listArray (0, (length vs) - 1) vs)
-{-
--- | Declares a stream of type Enum, including possible extra constraints on it.
-enumVar :: MonadSMT m
-           => SMTAnnotation Natural -> SMTAnnotation SMTEnum
-           -> m (Stream SMTEnum, [Definition])
-enumVar argAnn ann@(EnumTypeAnn _ _ _) = liftSMT (funAnn argAnn ann) >>= return . (, [])
-enumVar argAnn ann@(EnumBitAnn size _ biggestCons) =
-  do v <- liftSMT (funAnn argAnn ann)
-     constr <- liftSMT $
-               defFunAnn argAnn unit $
-               \t -> bvule (toBVExpr (v `app` t)) (constantAnn biggestCons size)
-     return (v, [SingleDef constr])
--}
+           liftSMT $ fmap EnumExpr $ varNamedAnn v etAnn
+    typedVar v (ProdType ts) =
+      do vs <- mapM (typedVar (v ++ "_comp")) ts
+         return (ProdExpr $ listArray (0, (length vs) - 1) vs)
 
 -- | Declares a node and puts the interface variables into the environment.
 -- Here it becomes crucial that a node is used at most once in a program, since
@@ -185,15 +161,15 @@ enumVar argAnn ann@(EnumBitAnn size _ biggestCons) =
 -- declared. The other nodes are deferred to be declared in the corresponding
 -- location (see declareAutomaton and declareLocations).
 declareNode :: Ident i =>
-               Maybe (Stream Bool) -> i -> Node i -> DeclM i [Definition]
-declareNode active nName nDecl =
+               Maybe (i, TypedExpr) -> i -> Node i -> DeclM i [Definition]
+declareNode active nName nDecl = 
   do (interface, defs) <- localVarEnv (const emptyVarEnv) $
                           declareNode' active nDecl
      modifyNodes $ Map.insert nName interface
      return defs
   where
     declareNode' :: Ident i =>
-                    Maybe (Stream Bool) -> Node i
+                    Maybe (i, TypedExpr) -> Node i
                     -> DeclM i (NodeEnv i, [Definition])
     declareNode' activeCond n =
       do let automNodes =
@@ -202,7 +178,7 @@ declareNode active nName nDecl =
            declareDecls activeCond automNodes $ nodeDecls n
          outDecls <- declareVarList $ nodeOutputs n
          ins <- mapM (lookupVar . varIdent) . declsInput $ nodeDecls n
-         let outs = map snd outDecls
+         let outs = outDecls
          modifyVars $ Map.union (Map.fromList outDecls)
          flowDefs <- declareFlow activeCond $ nodeFlow n
          automDefs <-
@@ -227,99 +203,131 @@ getNodesInLocations = mconcat . map getUsedLoc . automLocations
 -- | Creates definitions for instant definitions. In case of a node usage this
 -- may produce multiple definitions. If 
 declareInstantDef :: Ident i =>
-                     Maybe (Stream Bool)
+                     Maybe (i, TypedExpr)
                      -> InstantDefinition i
                      -> DeclM i [Definition]
-declareInstantDef activeCond inst@(InstantExpr x _) =
+declareInstantDef activeCond inst@(InstantExpr x e) =
   do (res, []) <- trInstant (error "no activation condition") inst
-     xStream <- lookupVar x
+     xVar <- lookupVar x
+     let args = getArgList e
+     argsE <- mapM lookupVar args
+     argsN <- mapM getN argsE
      def <- declareConditionalAssign
-            activeCond id (const $ getBottom xStream) xStream res
+            activeCond (const $ const $ getBottom xVar) xVar args argsN False res
      return [def]
-declareInstantDef activeCond inst@(NodeUsage x _ _) =
+declareInstantDef activeCond inst@(NodeUsage x n _) =
   do (outp, inpDefs) <- trInstant activeCond inst
-     xStream         <- lookupVar x
+     xVar            <- lookupVar x
+     nEnv            <- lookupNode n
+     outN            <- mapM (\(_, e) -> getN e) $ nodeEnvOut nEnv
      outpDef         <- declareConditionalAssign
-                        activeCond id (const $ getBottom xStream) xStream outp
+                        activeCond (const $ const $ getBottom xVar) xVar (map fst $ nodeEnvOut nEnv) outN False outp
      return $ inpDefs ++ [outpDef]
 
 -- | Translates an instant definition into a function which can be
 -- used to further refine this instant (e.g. wrap it into an ite).
 -- This may also return definitions of the parameters of a node.
 -- The activation condition is only used for the inputs of a node.
-trInstant :: Ident i => Maybe (Stream Bool) -> InstantDefinition i ->
-             DeclM i (Env i -> StreamPos -> TypedExpr i, [Definition])
+trInstant :: Ident i => Maybe (i, TypedExpr) -> InstantDefinition i -> DeclM i (Env i -> [(i, TypedExpr)] -> TypedExpr, [Definition])
 trInstant _ (InstantExpr _ e) = return (runTransM $ trExpr e, [])
 trInstant inpActive (NodeUsage _ n es) =
   do nEnv <- lookupNode n
      let esTr = map (runTransM . trExpr) es
-         y    = mkProdStream (nodeEnvOut nEnv)
-     inpDefs  <- mapM (\(x, e) ->
+         y    = runTransM $ trOutput $ nodeEnvOut nEnv
+         ins = map getArgList es
+     insE <- mapM (mapM lookupVar) ins
+     insN <- mapM (mapM getN) insE
+     inpDefs  <- mapM (\(x, n, e, eTr) ->
                         declareConditionalAssign
-                        inpActive id (const $ getBottom x) x e)
-                 $ zip (nodeEnvIn nEnv) esTr
-     return (const $ appStream y, inpDefs)
+                        inpActive (const $ const $ getBottom x) x (getArgList e) n False eTr)
+                 $ zip4 (nodeEnvIn nEnv) insN es esTr
+     return (y, inpDefs)
+
+trOutput :: Ident i => [(i, TypedExpr)] -> TransM i (TypedExpr)
+trOutput m = do
+                 s <- ask
+                 outList <- mapM (trOutput' s) m
+                 return $ mkProdExpr outList
+               where
+                 trOutput' s (i, _) = case lookup i (fst s) of
+                                       Nothing -> throwError $ "No argument (output) binding for " ++ identPretty i
+                                       Just n -> return n
 
 -- | Creates a declaration for a state transition.
 -- If an activation condition c is given, the declaration boils down to
 -- x' = (ite c e x) where e is the defining expression. Otherwise it is just
 -- x' = e.
 declareTransition :: Ident i =>
-                     Maybe (Stream Bool)
+                     Maybe (i, TypedExpr)
                      -> StateTransition i
                      -> DeclM i Definition
 declareTransition activeCond (StateTransition x e) =
-  do xStream     <- lookupVar x
-     natAnn      <- gets natImpl
-     let succAnn = succ' natAnn
-         xApp    = appStream xStream
-         e'      = runTransM $ trExpr e
-     declareConditionalAssign activeCond succAnn xApp xStream e'
+  do xVar     <- lookupVar x
+     let e'      = runTransM $ trExpr e
+         defExpr = mkTyped (AtExpr (AtomVar x)) $ varDefType xVar
+         args    = getArgList defExpr ++ getArgList e
+     argsE <- mapM lookupVar args
+     argsN <- mapM getN argsE
+     declareConditionalAssign activeCond (runTransM $ trExpr defExpr) xVar args argsN True e'
 
 -- | Creates a declaration for an assignment. Depending on the
 -- activation condition the given expression or a default expression
--- is used (generated by genDefault). Additionally the position in the
--- stream of /x/ which will be defined, can be specified by modPos
--- (see declareDef).
+-- is used (generated by genDefault). Additionally the cycle of the
+-- variable which will be defined, can be specified by succ.
 declareConditionalAssign :: Ident i =>
-                            Maybe (Stream Bool)
-                            -> (StreamPos -> StreamPos)
-                            -> (StreamPos -> TypedExpr i)
-                            -> TypedStream i
-                            -> (Env i -> StreamPos -> TypedExpr i)
+                            Maybe (i, TypedExpr)
+                            -> (Env i -> [(i, TypedExpr)] -> TypedExpr)
+                            -> TypedExpr
+                            -> [i]
+                            -> [Int]
+                            -> Bool
+                            -> (Env i -> [(i, TypedExpr)] -> TypedExpr)
                             -> DeclM i Definition
-declareConditionalAssign activeCond modPos defaultStream x ef =
+declareConditionalAssign activeCond defaultExpr x as ns succ ef =
   case activeCond of
-    Nothing -> declareDef modPos x ef
-    Just c  ->
-      declareDef modPos x (\env t ->
-                            mkConditionalStream t c (ef env) defaultStream)
-  where
-    -- | Takes a condition and the corresponding branches which may depend
-    -- on the current time and builds an expression which takes the corresponding
-    -- branch depending on the condition (if c then s_1(n) else s_2(n)).
-    mkConditionalStream n c s1 s2 =
-      let c' = BoolExpr $ c `app` n
-      in liftIte c' (s1 n) (s2 n)
-
--- | Creates a definition for a given variable. Whereby a function to
--- manipulate the stream position at which it is defined is used (normally
--- id or succ' to define instances or state transitions).
--- The second argument /x/ is the stream to be defined and the last
+    Nothing -> declareDef x as ns succ ef
+    Just (ident, c)  -> do
+      condN <- getN c
+      let condExpr = mkTyped (AtExpr (AtomVar (ident))) $ varDefType c
+          arg      = getArgList condExpr
+          condVar  = runTransM $ trExpr condExpr
+      declareDef x (arg ++ as) ([condN] ++ ns) succ (\env t -> liftIte (condVar env t) (ef env t) (defaultExpr env t))
+
+-- | Creates a definition for a given variable. 
+-- The first argument /x/ is the variable to be defined and the last
 -- argument (/ef/) is a function that generates the defining expression.
-declareDef :: Ident i => (StreamPos -> StreamPos) -> TypedStream i ->
-              (Env i -> StreamPos -> TypedExpr i) -> DeclM i Definition
-declareDef f x ef =
+declareDef :: Ident i => TypedExpr -> [i] -> [Int] -> Bool ->
+              (Env i -> [(i, TypedExpr)] -> TypedExpr) -> DeclM i Definition
+declareDef x as ns succ ef =
   do env         <- get
-     let defType = streamDefType x
-     d           <- defStream defType
-                    $ \t -> liftRel (.==.) (x `appStream` (f t)) (ef env t)
-     return $ ensureDefinition d
+     let defType = varDefType x
+     xN          <- getN x
+     ann         <- getTypedAnnotation $ [xN] ++ ns
+     d           <- defFunc defType ann
+                    $ \a -> liftRel (.==.) (head a) $ ef env $ zip (as ++ [error "Last argument must not be evaluated!"]) (tail a)
+     let argsN   = ([xN] ++ ns)
+     return $ ensureDefinition argsN succ d
+
+varDefType :: TypedExpr -> Type i
+varDefType (ProdExpr ts) = ProdType . fmap varDefType $ Arr.elems ts
+varDefType _               = boolT
+
+getTypedAnnotation :: Ident i => [Int] -> DeclM i [TypedAnnotation]
+getTypedAnnotation ns = mapM getTypedAnnotation' ns
   where
-    streamDefType (ProdStream ts) = ProdType . fmap streamDefType $ Arr.elems ts
-    streamDefType _               = boolT
-
-declareFlow :: Ident i => Maybe (Stream Bool) -> Flow i -> DeclM i [Definition]
+    getTypedAnnotation' n =
+      do vars    <- gets varList
+         eAnn <- gets enumAnn
+         return $ getTypedAnnCases $ vars !! n
+           where getTypedAnnCases var =
+                   case var of
+                     BoolExpr _ -> BoolAnnotation ()
+                     IntExpr _ -> IntAnnotation ()
+                     RealExpr _ -> RealAnnotation ()
+                     EnumExpr (Var _ k) -> EnumAnnotation k
+                     ProdExpr k -> ProdAnnotation $ fmap getTypedAnnCases k
+
+declareFlow :: Ident i => Maybe (i, TypedExpr) -> Flow i -> DeclM i [Definition]
 declareFlow activeCond f =
   do defDefs        <- fmap concat
                        . mapM (declareInstantDef activeCond)
@@ -337,13 +345,14 @@ declareFlow activeCond f =
 --    conditions (mkTransitionEq)
 -- * asserting the initial location
 declareAutomaton :: Ident i =>
-                    Maybe (Stream Bool)
+                    Maybe (i, TypedExpr)
                     -> Map i (Node i)
                     -> (Int, Automaton i)
                     -> DeclM i [Definition]
 declareAutomaton activeCond localNodes (_, a) =
   do automIndex <- nextAutomatonIndex
      let automName = "Autom" ++ show automIndex
+         condName  = automName ++ "_active"
          enumName  = fromString $ automName ++ "States"
          stateT    = EnumType enumName
          locNames  =
@@ -357,17 +366,18 @@ declareAutomaton activeCond localNodes (_, a) =
          selName   = "sel" ++ automName
          selId     = fromString selName
      declareEnums $ Map.singleton enumName enum
-     (act, sel, eAnn) <- mkStateVars actName selName enumName
+     (act, sel) <- mkStateVars actName selName enumName
      modifyVars ( `Map.union` Map.fromList
-                  [(actId, EnumStream eAnn act),
-                   (selId, EnumStream eAnn sel)
+                  [(actId, act),
+                   (selId, sel)
                   ]
                 )
-     locDefs <- (flip runReaderT (locCons, localNodes))
+     locDefs <- (flip runReaderT ((locCons, localNodes), condName))
                 $ declareLocations activeCond act
                 (automDefaults a) (automLocations a)
-     edgeDefs <- mkTransitionEq activeCond stateT locCons actId selId
-                 $ automEdges a
+     enumAnn <- lookupEnumAnn enumName
+     let bottom = EnumExpr $ constantAnn (enumBottom enumAnn) enumAnn
+     edgeDefs <- mkTransitionEq activeCond stateT locCons actId selId (automEdges a) bottom
      assertInit (selId, locConsConstExpr locCons stateT $ automInitial a)
      return $ locDefs ++ edgeDefs
 
@@ -397,13 +407,14 @@ mkStateVars :: Ident i =>
                String
                -> String
                -> i
-               -> DeclM i (Stream SMTEnum, Stream SMTEnum, EnumAnn)
+               -> DeclM i (TypedExpr, TypedExpr)
 mkStateVars actName selName stateEnum =
   do stEnumAnn <- lookupEnumAnn stateEnum
-     natAnn <- gets natImpl
-     act <- liftSMT $ funAnnNamed actName natAnn stEnumAnn
-     sel <- liftSMT $ funAnnNamed selName natAnn stEnumAnn
-     return (act, sel, stEnumAnn)
+     act <- liftSMT $ fmap EnumExpr $ varNamedAnn actName stEnumAnn
+     putVar act
+     sel <- liftSMT $ fmap EnumExpr $ varNamedAnn selName stEnumAnn
+     putVar sel
+     return (act, sel)
 
 -- | Extracts the the expressions for each variable seperated into
 -- local definitons and state transitions.
@@ -431,20 +442,20 @@ extractAssigns = foldl addLocExprs (Map.empty, Map.empty)
 -- beforehand and the undeclared nodes which are used in one of the
 -- locations of the automata to be defined.
 type AutomTransM i =
-  ReaderT (Map (LocationId i) (EnumConstr i), Map i (Node i)) (DeclM i)
+  ReaderT ((Map (LocationId i) (EnumConstr i), Map i (Node i)), String) (DeclM i)
 
 lookupLocName :: Ident i => LocationId i -> AutomTransM i (EnumConstr i)
 lookupLocName l
-  = asks fst >>= lookupErr ("Unknown location " ++ identPretty l) l
+  = asks (fst . fst) >>= lookupErr ("Unknown location " ++ identPretty l) l
 
 lookupLocalNode :: Ident i => i -> AutomTransM i (Node i)
 lookupLocalNode n
-  = asks snd >>= lookupErr ("Unknow local node " ++ identPretty n) n
+  = asks (snd .fst) >>= lookupErr ("Unknow local node " ++ identPretty n) n
 
 -- | Declares the data flow inside the locations of an automaton.
 declareLocations :: Ident i =>
-                    Maybe (Stream Bool)
-                    -> Stream SMTEnum
+                    Maybe (i, TypedExpr)
+                    -> TypedExpr
                     -> Map i (Expr i)
                     -> [Location i]
                     -> AutomTransM i [Definition]
@@ -460,31 +471,49 @@ declareLocations activeCond s defaultExprs locations =
         return $ instDefs ++ transDefs
   where
     declareLocDefs :: Ident i =>
-                      Maybe (Stream Bool)
+                      Maybe (i, TypedExpr)
                       -> Map i (Expr i)
                       -> (i, [(LocationId i, InstantDefinition i)])
                       -> AutomTransM i [Definition]
     declareLocDefs active defaults (x, locs) =
       do defaultExpr    <- getDefault defaults x locs
          (res, inpDefs) <- declareLocDef active s defaultExpr locs
-         xStream        <- lookupVar x
-         let xBottom    = const $ getBottom xStream
+         xVar           <- lookupVar x
+         argss          <- lift $ mapM locArgList locs
+         let xBottom    = const $ const $ getBottom xVar
+             argDefault  = maybe [] getArgList defaultExpr
+         argDefaultE    <- mapM lookupVar argDefault
+         argDefaultN    <- lift $ mapM getN argDefaultE
+         let args       = concat $ map fst argss ++ [argDefault]
+             argsN      = concat $ map snd argss ++ [argDefaultN]
+         argsNs         <- lift $ getN s
          def            <-
-           lift $ declareConditionalAssign active id xBottom xStream res
+           lift $ declareConditionalAssign active xBottom xVar (args ++ [fromString "dummyForLocEnum"]) (argsN ++ [argsNs]) False res
          return $ inpDefs ++ [def]
+      where
+        locArgList (_,InstantExpr _ e) = do 
+                                          let args = getArgList e
+                                          argsE <- mapM lookupVar args
+                                          argsN <- mapM getN argsE
+                                          return (args, argsN)
+        locArgList (_,NodeUsage _ n _) = do nEnv  <- lookupNode n
+                                            let args = map fst $ nodeEnvOut nEnv
+                                            argsN <- mapM (getN . snd) $ nodeEnvOut nEnv
+                                            return (args, argsN)
 
     declareLocTransitions :: Ident i =>
-                             Maybe (Stream Bool)
+                             Maybe (i, TypedExpr)
                              -> (i, [(LocationId i, StateTransition i)])
                              -> AutomTransM i Definition
     declareLocTransitions active (x, locs) =
       do res         <- trLocTransition s locs
-         xStream     <- lookupVar x
-         natAnn      <- gets natImpl
-         let succAnn = succ' natAnn
-             xApp    = appStream xStream
+         xVar     <- lookupVar x
+         let defExpr    = mkTyped (AtExpr (AtomVar x)) $ varDefType xVar
+             args       = concat $ (map (\(_,StateTransition _ e) -> getArgList e) locs) ++ [getArgList defExpr]
+         argsE          <- mapM lookupVar args
+         argsN          <- lift $ mapM getN (argsE ++ [s])
          def         <-
-           lift $ declareConditionalAssign active succAnn xApp xStream res
+           lift $ declareConditionalAssign active (runTransM $ trExpr defExpr) xVar (args ++ [fromString "dummyForLocEnum"]) argsN True res
          return def
 
     getDefault defaults x locs =
@@ -495,15 +524,15 @@ declareLocations activeCond s defaultExprs locations =
                 $ lookupErr (identPretty x ++ " not fully defined") x defaults
 
     isFullyDefined locDefs =
-      do locNames <- asks fst
+      do locNames <- asks (fst . fst)
          return $ (Map.keysSet locNames) == (Set.fromList $ map fst locDefs)
 
 declareLocDef :: Ident i =>
-                 Maybe (Stream Bool)
-                 -> Stream SMTEnum
+                 Maybe (i, TypedExpr)
+                 -> TypedExpr
                  -> Maybe (Expr i)
                  -> [(LocationId i, InstantDefinition i)]
-                 -> AutomTransM i (Env i -> StreamPos -> TypedExpr i, [Definition])
+                 -> AutomTransM i (Env i -> [(i, TypedExpr)] -> TypedExpr, [Definition])
 declareLocDef activeCond s defaultExpr locs =
   do (innerPat, locs') <- case defaultExpr of
        Nothing -> case locs of
@@ -517,23 +546,23 @@ declareLocDef activeCond s defaultExpr locs =
        innerPat locs'
   where
     trLocInstant :: Ident i =>
-                    Maybe (Stream Bool)
+                    Maybe (i, TypedExpr)
                     -> LocationId i
                     -> InstantDefinition i
-                    -> AutomTransM i (Env i -> StreamPos -> TypedExpr i, [Definition])
+                    -> AutomTransM i (Env i -> [(i, TypedExpr)] -> TypedExpr, [Definition])
     trLocInstant _ _ inst@(InstantExpr _ _) =
       lift $ trInstant (error "no activation condition required") inst
     trLocInstant active l inst@(NodeUsage _ n _) =
-      do (locActive, activeDef) <- mkLocationActivationCond active s l
+      do (identActive, locActive, activeDef) <- mkLocationActivationCond active s l
          node                   <- lookupLocalNode n
-         nodeDefs               <- lift $ declareNode (Just locActive) n node
-         (r, inpDefs)           <- lift $ trInstant (Just locActive) inst
+         nodeDefs               <- lift $ declareNode (Just (identActive, locActive)) n node
+         (r, inpDefs)           <- lift $ trInstant (Just (identActive, locActive)) inst
          return (r, [activeDef] ++ nodeDefs ++ inpDefs)
 
 trLocTransition :: Ident i =>
-                   Stream SMTEnum
+                   TypedExpr
                    -> [(LocationId i, StateTransition i)]
-                   -> AutomTransM i (Env i -> StreamPos -> TypedExpr i)
+                   -> AutomTransM i (Env i -> [(i, TypedExpr)] -> TypedExpr)
 trLocTransition s locs =
   let (innerPat, locs') = case locs of
         (l:ls) -> (trLocTrans $ snd l, ls)
@@ -545,67 +574,77 @@ trLocTransition s locs =
     trLocTrans (StateTransition _ e) = runTransM $ trExpr e
 
 mkLocationMatch :: Ident i =>
-                   Stream SMTEnum
-                   -> (Env i -> StreamPos -> TypedExpr i)
+                   TypedExpr
+                   -> (Env i -> [(i, TypedExpr)] -> TypedExpr)
                    -> LocationId i
-                   -> (Env i -> StreamPos -> TypedExpr i)
-                   -> AutomTransM i (Env i -> StreamPos -> TypedExpr i)
-mkLocationMatch s f l lExpr =
+                   -> (Env i -> [(i, TypedExpr)] -> TypedExpr)
+                   -> AutomTransM i (Env i -> [(i, TypedExpr)] -> TypedExpr)
+mkLocationMatch (EnumExpr s) f l lExpr =
   do lCons <- lookupLocName l
      lEnum <- lift $ trEnumConsAnn lCons <$> lookupEnumConsAnn lCons
      return
        (\env t -> liftIte
-                  (BoolExpr $ (s `app` t) .==. lEnum)
+                  (BoolExpr $ (unEnum $ snd $ last t) .==. lEnum)
                   (lExpr env t)
                   (f env t))
 
 -- | Creates a variable which is true iff the given activation
 -- condition is true and the the given location is active.
 mkLocationActivationCond :: Ident i =>
-                            Maybe (Stream Bool)
-                            -> Stream SMTEnum
+                            Maybe (i, TypedExpr)
+                            -> TypedExpr
                             -> LocationId i
-                            -> AutomTransM i (Stream Bool, Definition)
-mkLocationActivationCond activeCond s l =
-  do lCons <- lookupLocName l
+                            -> AutomTransM i (i, TypedExpr, Definition)
+mkLocationActivationCond activeCond e l =
+  do condName <- asks snd
+     lCons <- lookupLocName l
      lEnum <- lift $ trEnumConsAnn lCons <$> lookupEnumConsAnn lCons
-     natAnn <- gets natImpl
-     let cond = \_env t -> BoolExpr $ (s `app` t) .==. lEnum
-     activeVar <- liftSMT $ funAnn natAnn unit
-     def <- lift $ declareConditionalAssign activeCond id
-            (const . BoolExpr $ constant False) (BoolStream activeVar) cond
-     return (activeVar, def)
+     let cond = \_env t -> BoolExpr $ (unEnum $ snd $ last t) .==. lEnum
+     activeVar <- liftSMT $ fmap BoolExpr $ varNamed condName
+     lift $ putVar activeVar
+     lift $ putTerm activeVar
+     argN <- lift $ getN e
+     def <- lift $ declareConditionalAssign activeCond
+            (const $ const $ BoolExpr $ constant False) activeVar [] [argN] False cond
+     return (fromString condName, activeVar, def)
 
 -- | Creates two equations for the edges. The first calculates
 -- the next location (act). This is a chain of ite for each state surrounded
 -- by a match on the last location (sel). The definition of sel is just
 -- the saving of act for the next cycle.
 mkTransitionEq :: Ident i =>
-                  Maybe (Stream Bool)
+                  Maybe (i, TypedExpr)
                   -> Type i
                   -> Map (LocationId i) (EnumConstr i)
                   -> i
                   -> i
                   -> [Edge i]
+                  -> TypedExpr
                   -> DeclM i [Definition]
-mkTransitionEq activeCond locationEnumTy locationEnumConstrs act sel es =
-  -- we reuse the translation machinery by building a match expression and
-  -- translating that.
+mkTransitionEq activeCond locationEnumTy locationEnumConstrs act sel es bot =
   -- We use foldr to enforce that transition that occur later in the
   -- source get a lower priority.
-  do stateDef <- declareInstantDef activeCond
-                 . InstantExpr act
-                 . mkMatch
-                   locationEnumConstrs
-                   locationEnumTy
-                   sel
-                   (mkTyped (AtExpr $ AtomVar sel) locationEnumTy)
-                 . Map.toList
-                 $ foldr addEdge Map.empty es
-     stateTr <- declareTransition activeCond
-                $ StateTransition
-                  sel
-                  (mkTyped (AtExpr $ AtomVar act) locationEnumTy)
+  do stateDef <- do 
+                   let e = mkMatch locationEnumConstrs
+                           locationEnumTy sel (mkTyped (AtExpr $
+                           AtomVar sel) locationEnumTy) . Map.toList
+                           $ foldr addEdge Map.empty es
+                       inst = InstantExpr act e
+                       args = getArgList e
+                   (res, []) <- trInstant (error "no activation condition") inst
+                   xVar <- lookupVar act
+                   argsE <- mapM lookupVar args
+                   argsN <- mapM getN argsE
+                   def <- declareConditionalAssign activeCond (const $ const $ bot) xVar args argsN False res
+                   return [def]
+     stateTr <- do 
+       xVar     <- lookupVar sel
+       let e'      = runTransM $ trExpr (mkTyped (AtExpr $ AtomVar act) locationEnumTy)
+           defExpr = mkTyped (AtExpr (AtomVar sel)) $ varDefType xVar
+           args    = (getArgList defExpr) ++ (getArgList (mkTyped (AtExpr $ AtomVar act) locationEnumTy))
+       argsE <- mapM lookupVar args
+       argsN <- mapM getN argsE
+       declareConditionalAssign activeCond (runTransM $ trExpr defExpr) xVar args argsN True e'
      return $ stateDef ++ [stateTr]
   where
      addEdge (Edge h t c) m =
@@ -661,30 +700,33 @@ assertInits = mapM_ assertInit . Map.toList
 
 assertInit :: Ident i => (i, ConstExpr i) -> DeclM i ()
 assertInit (x, e) =
-  do natAnn <- gets natImpl
-     x' <- lookupVar x
+  do x' <- lookupVar x
      e' <- trConstExpr e
-     let def = liftRel (.==.) (x' `appStream` (zero' natAnn)) e'
+     let def = liftRel (.==.) x' e'
      liftSMT $ liftAssert def
 
 -- | Creates a definition for a precondition p. If an activation condition c
 -- is given, the resulting condition is (=> c p).
-declarePrecond :: Ident i => Maybe (Stream Bool) -> Expr i -> DeclM i Definition
+declarePrecond :: Ident i => Maybe (i, TypedExpr) -> Expr i -> DeclM i Definition
 declarePrecond activeCond e =
-  do env <- get
-     d <- case activeCond of
-       Nothing -> defStream boolT $ \t -> runTransM (trExpr e) env t
-       Just c -> defStream boolT $
-                 \t -> (flip (flip runTransM env) t)
-                       (trExpr e >>= \e' ->
-                         return $ liftBool2 (.=>.) (BoolExpr $ c `app` t) e')
-     return $ ensureDefinition d
+  do env      <- get
+     let args = getArgList e
+     argsE    <- mapM lookupVar args
+     argsN    <- mapM getN argsE
+     ann      <- getTypedAnnotation argsN
+     d        <- case activeCond of
+       Nothing -> defFunc boolT ann $ \a -> runTransM (trExpr e) env $ zip args a
+       Just (ident, c) -> defFunc boolT ann $
+                 \a -> (flip (flip runTransM env) (zip args a))
+		       (trExpr e >>= \e' ->
+                         return $ liftBool2 (.=>.) c e')
+     return $ ensureDefinition argsN False d
 
 declareInvariant :: Ident i =>
-                    Maybe (Stream Bool) -> Expr i -> DeclM i Definition
+                    Maybe (i, TypedExpr) -> Expr i -> DeclM i Definition
 declareInvariant = declarePrecond
 
-trConstExpr :: Ident i => ConstExpr i -> DeclM i (TypedExpr i)
+trConstExpr :: Ident i => ConstExpr i -> DeclM i (TypedExpr)
 trConstExpr (untyped -> Const c)
   = return $ trConstant c
 trConstExpr (untyped -> ConstEnum x)
@@ -692,18 +734,15 @@ trConstExpr (untyped -> ConstEnum x)
 trConstExpr (untyped -> ConstProd (Prod cs)) =
   ProdExpr . listArray (0, length cs - 1) <$> mapM trConstExpr cs
 
-type TransM i = ReaderT (StreamPos, Env i) (Either String)
-
-doAppStream :: TypedStream i -> TransM i (TypedExpr i)
-doAppStream s = askStreamPos >>= return . appStream s
+type TransM i = ReaderT ([(i, TypedExpr)], Env i) (Either String)
 
 -- beware: uses error
-runTransM :: TransM i a -> Env i -> StreamPos -> a
-runTransM m e n = case runReaderT m (n, e) of
+runTransM :: TransM i a -> Env i -> [(i, TypedExpr)] -> a
+runTransM m e a = case runReaderT m (a, e) of
   Left err -> error err
   Right r -> r
 
-lookupVar' :: Ident i => i -> TransM i (TypedStream i)
+lookupVar' :: Ident i => i -> TransM i (TypedExpr)
 lookupVar' x =
   do vs <- asks $ vars . varEnv . snd
      case Map.lookup x vs of
@@ -716,18 +755,28 @@ lookupEnumConsAnn' t
   = asks (enumConsAnn . snd)
     >>= lookupErr ("Unknown enum constructor " ++ identPretty t) t
 
-askStreamPos :: TransM i StreamPos
-askStreamPos = asks fst
+getArgList :: Ident i => Expr i ->  [i]
+getArgList expr = case untyped expr of
+  AtExpr (AtomConst c)  -> []
+  AtExpr (AtomVar x)    -> [x]
+  AtExpr (AtomEnum x)   -> []
+  LogNot e              -> getArgList e
+  Expr2 op e1 e2        -> getArgList e2 ++ getArgList e1
+  Ite c e1 e2           -> getArgList e2 ++ getArgList e1 ++ getArgList c
+  ProdCons (Prod es)    -> foldr ((++) . getArgList) [] es
+  Project x i           -> [x]
+  Match e pats -> concat $ [getArgList e] ++ map (\(Pattern _ x) -> getArgList x) pats
 
 -- we do no further type checks since this
 -- has been done beforehand.
-trExpr :: Ident i => Expr i -> TransM i (TypedExpr i)
+trExpr :: Ident i => Expr i -> TransM i (TypedExpr)
 trExpr expr = case untyped expr of
   AtExpr (AtomConst c) -> return $ trConstant c
-  AtExpr (AtomVar x)   ->
-    do s <- lookupVar' x
-       n <- askStreamPos
-       return $ s `appStream` n
+  AtExpr (AtomVar x)   -> do
+                            s <- ask
+                            case lookup x (fst s) of
+                              Nothing -> throwError $ "No argument binding for " ++ identPretty x
+                              Just n  -> return n
   AtExpr (AtomEnum x)  -> EnumExpr <$> trEnumCons x
   LogNot e             -> lift1Bool not' <$> trExpr e
   Expr2 op e1 e2       -> applyOp op <$> trExpr e1 <*> trExpr e2
@@ -735,16 +784,18 @@ trExpr expr = case untyped expr of
   ProdCons (Prod es)   -> (ProdExpr . listArray (0, (length es) - 1))
                           <$> mapM trExpr es
   Project x i          ->
-    do (ProdStream s) <- lookupVar' x
-       n <- askStreamPos
-       return $ (s ! fromEnum i) `appStream` n
+    do s <- ask
+       (ProdExpr e) <- case lookup x (fst s) of
+                         Nothing -> throwError $ "No argument binding for " ++ identPretty x
+                         Just n  -> return n
+       return $ (e ! fromEnum i)
   Match e pats         -> trExpr e >>= flip trPattern pats
 
-trPattern :: Ident i => TypedExpr i -> [Pattern i] -> TransM i (TypedExpr i)
+trPattern :: Ident i => TypedExpr -> [Pattern i] -> TransM i (TypedExpr)
 trPattern e@(EnumExpr _) = trEnumMatch e
 trPattern _ = error "Cannot match on non enum expression"
 
-trEnumMatch :: Ident i => TypedExpr i -> [Pattern i] -> TransM i (TypedExpr i)
+trEnumMatch :: Ident i => TypedExpr -> [Pattern i] -> TransM i (TypedExpr)
 trEnumMatch x pats =
   -- respect order of patterns here by putting the last in the default match
   -- and bulding the expression bottom-up:
@@ -769,7 +820,7 @@ trEnumConsAnn x = constantAnn (SMTEnum . fromString $ identString x)
 trEnumCons :: Ident i => EnumConstr i -> TransM i (SMTExpr SMTEnum)
 trEnumCons x = lookupEnumConsAnn' x >>= return . trEnumConsAnn x
 
-applyOp :: BinOp -> TypedExpr i -> TypedExpr i -> TypedExpr i
+applyOp :: BinOp -> TypedExpr -> TypedExpr -> TypedExpr
 applyOp Or      e1 e2 = liftBoolL or'  [e1, e2]
 applyOp And     e1 e2 = liftBoolL and' [e1, e2]
 applyOp Xor     e1 e2 = liftBoolL xor  [e1, e2]
diff --git a/lamaSMT/lib/TransformEnv.hs b/lamaSMT/lib/TransformEnv.hs
index 61388f0..2c579ef 100644
--- a/lamaSMT/lib/TransformEnv.hs
+++ b/lamaSMT/lib/TransformEnv.hs
@@ -11,6 +11,7 @@ import Lang.LAMA.Types
 import Language.SMTLib2 as SMT
 
 import Data.Array as Arr
+import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.Map (Map)
 import Prelude hiding (mapM)
@@ -22,35 +23,53 @@ import Control.Monad.Error (ErrorT(..), MonadError(..))
 import SMTEnum
 import NatInstance
 import LamaSMTTypes
+import Definition
+import Posets
 import Internal.Monads
 
 data NodeEnv i = NodeEnv
-                 { nodeEnvIn :: [TypedStream i]
-                 , nodeEnvOut :: [TypedStream i]
+                 { nodeEnvIn :: [TypedExpr]
+                 , nodeEnvOut :: [(i, TypedExpr)]
                  , nodeEnvVars :: VarEnv i
                  }
 
 data VarEnv i = VarEnv
                 { nodes :: Map i (NodeEnv i)
-                  -- | Maps names of variables to a SMT expression for using that variable
-                , vars :: Map i (TypedStream i)
+                , vars :: Map i (TypedExpr)
+                  -- ^ Maps names of variables to a SMT expression for using
+                  -- that variable
                 }
 
 data Env i = Env
-           { constants :: Map i (TypedExpr i)
+           { constants :: Map i (TypedExpr)
            , enumAnn :: Map i (SMTAnnotation SMTEnum)
            , enumConsAnn :: Map (EnumConstr i) (SMTAnnotation SMTEnum)
            , varEnv :: VarEnv i
            , currAutomatonIndex :: Integer
+           , varList :: [TypedExpr]
+           , instSetBool :: [Term]
+           , instSetInt :: [Term]
            , natImpl :: NatImplementation
            , enumImpl :: EnumImplementation
            }
 
+-- | Gets an "undefined" value for a given type of expression.
+-- The expression itself is not further analysed.
+-- FIXME: Make behaviour configurable, i.e. bottom can be some
+-- default value or a left open stream
+-- (atm it does the former).
+getBottom :: TypedExpr -> TypedExpr
+getBottom (BoolExpr _)     = BoolExpr $ constant False
+getBottom (IntExpr _)      = IntExpr  $ constant 0xdeadbeef
+getBottom (RealExpr _)     = RealExpr . constant $ fromInteger 0xdeadbeef
+getBottom (EnumExpr e) = EnumExpr e --evtl. TODO
+getBottom (ProdExpr strs)  = ProdExpr $ fmap getBottom strs
+
 emptyVarEnv :: VarEnv i
 emptyVarEnv = VarEnv Map.empty Map.empty
 
 emptyEnv :: NatImplementation -> EnumImplementation -> Env i
-emptyEnv = Env Map.empty Map.empty Map.empty emptyVarEnv 0
+emptyEnv = Env Map.empty Map.empty Map.empty emptyVarEnv 0 [] [] []
 
 type DeclM i = StateT (Env i) (ErrorT String SMT)
 
@@ -59,6 +78,36 @@ putConstants cs =
   let cs' = fmap trConstant cs
   in modify $ \env -> env { constants = cs' }
 
+putVar :: Ident i => TypedExpr -> DeclM i ()
+putVar var =
+  modify $ \env -> env { varList = (varList env) ++ [var] }
+
+getN :: TypedExpr -> DeclM i Int
+getN x = do vars <- gets varList
+            return $ case List.elemIndex x vars of
+                          Nothing -> error $ "Could not be found in list of variables: " ++ show x
+                          Just n -> n
+
+putTerm :: Ident i => TypedExpr -> DeclM i ()
+putTerm e@(BoolExpr s) = do
+  n <- getN e
+  modify $ \env -> env { instSetBool = instSetBool env ++ [BoolTerm n] }
+putTerm e@(IntExpr s) = do
+  n <- getN e
+  modify $ \env -> env { instSetInt = instSetInt env ++ [IntTerm n] }
+putTerm _ = return ()
+
+getTypedValue :: MonadSMT m => TypedExpr -> m (TypedExpr)
+getTypedValue (BoolExpr s) = liftSMT $ getValue s >>= return . BoolExpr . constant
+getTypedValue (IntExpr s) = liftSMT $ getValue s >>= return . IntExpr . constant
+getTypedValue e = liftSMT $ return $ getBottom e
+
+evalBoolTerm :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> Term -> m Bool
+evalBoolTerm i (BoolTerm f) = liftSMT $ getValue $ unBool $ head $ lookupArgs [f] False i
+
+evalIntTerm :: MonadSMT m => ([TypedExpr], [TypedExpr]) -> Term -> m Integer
+evalIntTerm i (IntTerm f) = liftSMT $ getValue $ unInt $ head $ lookupArgs [f] False i
+
 putEnumAnn :: Ident i => Map i (SMTAnnotation SMTEnum) -> DeclM i ()
 putEnumAnn eAnns =
   modify $ \env -> env { enumAnn = (enumAnn env) `Map.union` eAnns }
@@ -73,7 +122,7 @@ modifyVarEnv f = modify $ \env -> env { varEnv = f $ varEnv env }
 modifyNodes :: (Map i (NodeEnv i) -> Map i (NodeEnv i)) -> DeclM i ()
 modifyNodes f = modifyVarEnv $ (\env -> env { nodes = f $ nodes env })
 
-modifyVars :: (Map i (TypedStream i) -> Map i (TypedStream i)) -> DeclM i ()
+modifyVars :: (Map i (TypedExpr) -> Map i (TypedExpr)) -> DeclM i ()
 modifyVars f = modifyVarEnv $ (\env -> env { vars = f $ vars env })
 
 lookupErr :: (MonadError e m, Ord k) => e -> k -> Map k v -> m v
@@ -81,7 +130,7 @@ lookupErr err k m = case Map.lookup k m of
   Nothing -> throwError err
   Just v -> return v
 
-lookupVar :: (MonadState (Env i) m, MonadError String m, Ident i) => i -> m (TypedStream i)
+lookupVar :: (MonadState (Env i) m, MonadError String m, Ident i) => i -> m (TypedExpr)
 lookupVar x = gets (vars . varEnv) >>= lookupErr ("Unknown variable " ++ identPretty x) x
 
 lookupNode :: Ident i => i -> DeclM i (NodeEnv i)
@@ -113,39 +162,27 @@ nextAutomatonIndex = state $ \env ->
   let i = currAutomatonIndex env
   in (i, env { currAutomatonIndex = i+1 })
 
--- | Defines a stream analogous to defFun.
-defStream :: Ident i =>
-             Type i -> (StreamPos -> TypedExpr i) -> DeclM i (TypedStream i)
-defStream ty sf = gets natImpl >>= \natAnn -> defStream' natAnn ty sf
-  where
-    defStream' :: Ident i =>
-                  NatImplementation -> Type i -> (StreamPos -> TypedExpr i)
-                  -> DeclM i (TypedStream i)
-    defStream' natAnn (GroundType BoolT) f
-      = liftSMT . fmap BoolStream $ defFunAnn natAnn (unBool' . f)
-    defStream' natAnn (GroundType IntT) f
-      = liftSMT . fmap IntStream $ defFunAnn natAnn (unInt . f)
-    defStream' natAnn (GroundType RealT) f
-      = liftSMT . fmap RealStream $ defFunAnn natAnn (unReal . f)
-    defStream' natAnn (GroundType _) f = $notImplemented
-    defStream' natAnn (EnumType alias) f
-      = do ann <- lookupEnumAnn alias
-           liftSMT $ fmap (EnumStream ann) $ defFunAnn natAnn (unEnum . f)
-    -- We have to pull the product out of a stream.
-    -- If we are given a function f : StreamPos -> (Ix -> TE) = TypedExpr as above,
-    -- we would like to have as result something like:
-    -- g : Ix -> (StreamPos -> TE)
-    -- g(i)(t) = defStream(λt'.f(t')(i))(t)
-    -- Here i is the index into the product and t,t' are time variables.
-    defStream' natAnn (ProdType ts) f =
-      do let u = length ts - 1
-         x <- mapM defParts $ zip ts [0..u]
-         return . ProdStream $ listArray (0,u) x
-      where defParts (ty2, i) = defStream' natAnn ty2 ((! i) . unProd' . f)
-
--- stream :: Ident i => Type i -> DeclM i (Stream t)
-
-trConstant :: Ident i => Constant i -> TypedExpr i
+-- | Defines a function instead of streams
+defFunc :: Ident i =>
+            Type i -> [TypedAnnotation] -> ([TypedExpr] -> TypedExpr) -> DeclM i (TypedFunc)
+defFunc (GroundType BoolT) ann f = liftSMT . fmap BoolFunc $
+                                defFunAnn ann (unBool' . f)
+defFunc (GroundType IntT) ann f = liftSMT . fmap IntFunc $
+                                defFunAnn ann (unInt . f)
+defFunc (GroundType RealT) ann f = liftSMT . fmap RealFunc $
+                               defFunAnn ann (unReal . f)
+defFunc (GroundType _) ann f = $notImplemented
+defFunc (EnumType alias) ann f = do eann <- lookupEnumAnn alias
+                                    liftSMT $ fmap (EnumFunc eann) $
+                                      defFunAnn ann (unEnum . f)
+-- We have to pull the product out of a function
+defFunc (ProdType ts) ann f =
+  do let u = length ts - 1
+     x <- mapM defParts $ zip ts [0..u]
+     return . ProdFunc $ listArray (0,u) x
+  where defParts (ty2, i) = defFunc ty2 ann ((! i) . unProd' . f)
+
+trConstant :: Ident i => Constant i -> TypedExpr
 trConstant (untyped -> BoolConst c) = BoolExpr $ constant c
 trConstant (untyped -> IntConst c) = IntExpr $ constant c
 trConstant (untyped -> RealConst c) = RealExpr $ constant c
diff --git a/lamaSMT/lib/TypeInstances.hs b/lamaSMT/lib/TypeInstances.hs
index e8b4d36..72c82f0 100644
--- a/lamaSMT/lib/TypeInstances.hs
+++ b/lamaSMT/lib/TypeInstances.hs
@@ -20,4 +20,4 @@ instance SMTValue Natural where
   unmangle _ _ = return Nothing
 
   mangle (view -> Zero) _ = L.Symbol "zero"
-  mangle (view -> Succ n) a = L.List [L.Symbol "succ", mangle n a]
\ No newline at end of file
+  mangle (view -> Succ n) a = L.List [L.Symbol "succ", mangle n a]
diff --git a/lamaSMT/lib/Wrapping.hs b/lamaSMT/lib/Wrapping.hs
index 990f201..03e013e 100644
--- a/lamaSMT/lib/Wrapping.hs
+++ b/lamaSMT/lib/Wrapping.hs
@@ -28,4 +28,4 @@ firstM :: Monad m => (a -> m b) -> (a, c) -> m (b, c)
 firstM = ala Kleisli first
 
 fanoutM :: Monad m => (a -> m b) -> (a -> m b') -> a -> m (b, b')
-fanoutM f = ala Kleisli ((Kleisli f) &&&)
\ No newline at end of file
+fanoutM f = ala Kleisli ((Kleisli f) &&&)
diff --git a/lamaSMT/smt_stream.py b/lamaSMT/smt_stream.py
new file mode 100755
index 0000000..be783e2
--- /dev/null
+++ b/lamaSMT/smt_stream.py
@@ -0,0 +1,13 @@
+#!/usr/bin/python2
+
+import subprocess
+import re
+import sys
+
+pattern = re.compile(r"write\(4, \"(\(.*?)\\n")
+
+proc = subprocess.Popen("strace -s 5000 " + " ".join(sys.argv[1:]), stdout=subprocess.PIPE, stderr=subprocess.PIPE, shell=True)
+for line in proc.communicate()[1].splitlines():
+    match = pattern.search(line)
+    if match:
+        print match.group(1)
diff --git a/language/LAMA.cabal b/language/LAMA.cabal
index 9691d39..01e6704 100644
--- a/language/LAMA.cabal
+++ b/language/LAMA.cabal
@@ -5,15 +5,14 @@ Cabal-Version:  >= 1.10
 Description:
   Parser, type checker and dependency analysis for LAMA
 
-Library 
+Library
   default-language: Haskell2010
   Build-Depends: base, containers, mtl, bytestring, natural-numbers,
-    transformers, pretty, array, fgl, text, filepath, placeholders,
+    transformers, pretty, array, fgl >= 5.5.0.0, text, filepath, placeholders,
     prelude-extras
   Hs-Source-Dirs: . lib
   GHC-Options: -Wall -O2
   exposed-modules:
-    Data.Graph.Inductive.GenShow
     Data.Bits.Size
     Lang.LAMA.Identifier
     Lang.LAMA.Types
diff --git a/language/lib/Data/Graph/Inductive/GenShow.hs b/language/lib/Data/Graph/Inductive/GenShow.hs
deleted file mode 100644
index 7c6a971..0000000
--- a/language/lib/Data/Graph/Inductive/GenShow.hs
+++ /dev/null
@@ -1,14 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-
-module Data.Graph.Inductive.GenShow where
-
-import Data.Graph.Inductive.Graph
-import Data.Graph.Inductive.PatriciaTree
-import qualified Data.Graph.Inductive.Tree as GTree
-
-instance forall a b. (Show a, Show b) => Show (Gr a b) where
-  show g =
-    let n = labNodes g
-        e = labEdges g
-        g' = mkGraph n e :: GTree.Gr a b
-    in show g'
diff --git a/language/lib/Lang/LAMA/Dependencies.hs b/language/lib/Lang/LAMA/Dependencies.hs
index 1f4b768..7c1230d 100644
--- a/language/lib/Lang/LAMA/Dependencies.hs
+++ b/language/lib/Lang/LAMA/Dependencies.hs
@@ -36,8 +36,6 @@ import Lang.LAMA.Identifier
 import Lang.LAMA.Types
 import Lang.LAMA.Typing.TypedStructure
 
-import Data.Graph.Inductive.GenShow ()
-
 -- fromSet :: Ord k => (k -> a) -> Set k -> Map k a
 -- fromSet f = Map.fromList . map (id &&& f) . Set.toList
 
diff --git a/language/lib/Lang/LAMA/Parser/ErrM.hs b/language/lib/Lang/LAMA/Parser/ErrM.hs
index 84ff334..27c1d33 100644
--- a/language/lib/Lang/LAMA/Parser/ErrM.hs
+++ b/language/lib/Lang/LAMA/Parser/ErrM.hs
@@ -6,7 +6,8 @@ module Lang.LAMA.Parser.ErrM where
 
 -- the Error monad: like Maybe type with error msgs
 
-import Control.Monad (MonadPlus(..), liftM)
+import Control.Monad (MonadPlus(..), liftM, ap)
+import Control.Applicative
 
 data Err a = Ok a | Bad String
   deriving (Read, Show, Eq, Ord)
@@ -17,6 +18,14 @@ instance Monad Err where
   Ok a  >>= f = f a
   Bad s >>= f = Bad s
 
+instance Applicative Err where
+    pure  = return
+    (<*>) = ap
+
+instance Alternative Err where
+    (<|>) = mplus
+    empty = mzero
+
 instance Functor Err where
   fmap = liftM
 
diff --git a/scade2lama/Scade2Lama.cabal b/scade2lama/Scade2Lama.cabal
index 2ee03c1..985cb57 100644
--- a/scade2lama/Scade2Lama.cabal
+++ b/scade2lama/Scade2Lama.cabal
@@ -9,7 +9,7 @@ Executable scade2lama
   default-language: Haskell2010
   Build-Depends: base, containers, language-scade, language-lama,
     transformers, placeholders, mtl, bytestring, split, pretty,
-    natural-numbers, syb, fgl
+    natural-numbers, syb, fgl >= 5.5.0.0
   Hs-Source-Dirs: . lib
   GHC-Options: -Wall
   other-modules:
diff --git a/scade2lama/lib/TransformAutomata.hs b/scade2lama/lib/TransformAutomata.hs
index 0fcaa2e..6078e26 100644
--- a/scade2lama/lib/TransformAutomata.hs
+++ b/scade2lama/lib/TransformAutomata.hs
@@ -9,7 +9,6 @@ import Development.Placeholders
 
 import Data.Graph.Inductive.Graph as Gr
 import Data.Graph.Inductive.PatriciaTree
-import Data.Graph.Inductive.GenShow ()
 import qualified Data.Map as Map
 import Data.Map (Map, (!))
 import qualified Data.Set as Set
@@ -558,4 +557,4 @@ mkAutomaton gr defaultExprs =
           S.ActionEmission [] -> L.Edge hName tName cond
           S.ActionEmission _ -> $notImplemented
           S.ActionDef (S.DataDef [] [] []) -> L.Edge hName tName cond
-          S.ActionDef _ -> $notImplemented
\ No newline at end of file
+          S.ActionDef _ -> $notImplemented