diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -216,7 +216,10 @@
   -- * Verification
   , verify
   -- * Code Generation
+  , C.Target (..)
   , code
+  -- * General Analysis
+  , analyze
   ) where
 
 import Control.Monad
@@ -360,17 +363,8 @@
 mux :: AllE a => E Bool -> E a -> E a -> E a
 mux = Mux
 
--- | Array index to a variable.
---(!) :: AllE a => A a -> E Int -> V a
---(!) a i = VArray a i
-
--- | Array index to an expression.
---(!.) :: AllE a => A a -> E Int -> E a
---(!.) a i = ref $ a ! i
-
--- | Labels a statement and creates a variable scope.
---   Labels are used in counter examples to trace the program execution.
---   And assertion names, and hence counter example trace file names, are produce from labels.
+-- | Labels a statement and creates a new variable scope.
+--   Labels are used in counter examples to help trace the program execution.
 (-|) :: Name -> Stmt a -> Stmt a
 name -| stmt = do
   (id, path0, stmt0) <- get
@@ -470,15 +464,17 @@
 instance Assign Int   where a <== b = statement $ Assign a b
 instance Assign Float where a <== b = statement $ Assign a b
 
--- | Declare an assumption condition is true.
---   Assumptions expressions must contain variables directly or indirectly related
---   to the assertion under verification, otherwise they will be ignored.
-assume :: Name -> E Bool -> Stmt ()
-assume name a = statement $ Label name $ Assume a
-
 -- | Theorem to be proven or used as lemmas to assist proofs of other theorems.
 data Theorem = Theorem' Int
 
+-- | Assume a condition is true.
+--   Assumptions are used as lemmas to other theorems.
+assume :: Name -> E Bool -> Stmt Theorem
+assume name a = do
+  (id, path, stmt) <- get
+  put (id + 1, path, Sequence stmt $ Label name $ Assume id a)
+  return $ Theorem' id
+
 -- | Defines a new theorem.
 --
 -- > theorem name k lemmas proposition
@@ -520,13 +516,15 @@
 --
 -- > verify pathToYices program
 verify :: FilePath -> Stmt () -> IO ()
-verify yices program = V.verify yices stmt
-  where
-  (_, _, stmt) = evalStmt 0 [] program
+verify yices program = analyze (V.verify yices) program
 
--- | Generate C and Simulink code.
-code :: Name -> Stmt () -> IO ()
-code name program = C.code name stmt
+-- | Generate code.
+code :: C.Target -> Name -> Stmt () -> IO ()
+code target name program = analyze (C.code target name) program
+
+-- | Generic program analysis.
+analyze :: (Statement -> IO a) -> Stmt () -> IO a
+analyze f program = f stmt
   where
   (_, _, stmt) = evalStmt 0 [] program
 
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -1,436 +1,26 @@
-module Language.ImProve.Code (code) where
-
-import Control.Monad.State
-import Data.List
-import Data.Maybe
-import Text.Printf
+module Language.ImProve.Code
+  ( Target (..)
+  , code
+  ) where
 
+import Language.ImProve.Code.C
+import Language.ImProve.Code.Modelica
+import Language.ImProve.Code.Simulink
 import Language.ImProve.Core
-import Language.ImProve.Tree hiding (Branch)
-import qualified Language.ImProve.Tree as T
 
-infixr 0 :-, :=
-
--- | Generate C and Simulink code.
-code :: Name -> Statement -> IO ()
-code name stmt = do
-  writeFile (name ++ ".c") $
-       "/* Generated by ImProve. */\n\n"
-    ++ "#include <assert.h>\n\n"
-    ++ codeVariables True scope ++ "\n"
-    ++ "void " ++ name ++ "()\n{\n"
-    ++ indent (codeStmt name [] stmt)
-    ++ "}\n\n"
-  writeFile (name ++ ".h") $
-       "/* Generated by ImProve. */\n\n"
-    ++ codeVariables False scope ++ "\n"
-    ++ "void " ++ name ++ "(void);\n\n"
-  codeMdl name stmt
-  where
-  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of
-    [] -> error "program contains no useful statements"
-    a  -> T.Branch (name ++ "_variables") a
-
-instance Show Statement where show = codeStmt "none" []
-
-codeStmt :: Name -> [Name] -> Statement -> String
-codeStmt name path a = case a of
-  Assign a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"
-  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n"
-  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n"
-  Sequence a b -> codeStmt name path a ++ codeStmt name path b
-  Theorem _ _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
-  Assume a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
-  Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)
-  Null -> ""
-  where
-
-  codeExpr :: E a -> String
-  codeExpr a = case a of
-    Ref a     -> name ++ "_variables." ++ pathName a
-    Const a   -> showConst $ const' a
-    Add a b   -> group [codeExpr a, "+", codeExpr b]
-    Sub a b   -> group [codeExpr a, "-", codeExpr b]
-    Mul a b   -> group [codeExpr a, "*", showConst (const' b)]
-    Div a b   -> group [codeExpr a, "/", showConst (const' b)]
-    Mod a b   -> group [codeExpr a, "%", showConst (const' b)]
-    Not a     -> group ["!", codeExpr a]
-    And a b   -> group [codeExpr a, "&&",  codeExpr b]
-    Or  a b   -> group [codeExpr a, "||",  codeExpr b]
-    Eq  a b   -> group [codeExpr a, "==",  codeExpr b]
-    Lt  a b   -> group [codeExpr a, "<",   codeExpr b]
-    Gt  a b   -> group [codeExpr a, ">",   codeExpr b]
-    Le  a b   -> group [codeExpr a, "<=",  codeExpr b]
-    Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]
-    Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] 
-    where
-    group :: [String] -> String
-    group a = "(" ++ intercalate " " a ++ ")"
-
-indent :: String -> String
-indent = unlines . map ("\t" ++) . lines
-
-indent' :: String -> String
-indent' a = case lines a of
-  [] -> []
-  (a:b) -> a ++ "\n" ++ indent (unlines b)
-
-codeVariables :: Bool -> (Tree Name (Bool, Path, Const)) -> String
-codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n    " ++ f2 a else "") ++ ";\n"
-  where
-  f1 a = case a of
-    T.Branch name items -> "struct {  /* " ++ name ++ " */\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"
-    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  /* input */" else "")
-
-  f2 a = case a of
-    T.Branch name items -> indent' $ "{   " ++ (intercalate ",   " $ map f2 items) ++ "}  /* " ++ name ++ " */\n"
-    Leaf name (_, _, init) -> printf "%-15s  /* %s */\n" (showConst init) name
-
-showConst :: Const -> String
-showConst a = case a of
-  Bool  True  -> "1"
-  Bool  False -> "0"
-  Int   a     -> show a
-  Float a     -> show a
-
-showConstType :: Const -> String
-showConstType a = case a of
-  Bool  _ -> "int"
-  Int   _ -> "int"
-  Float _ -> "float"
-
-
-type Net = StateT Netlist IO
-
-data Block
-  = Inport  Const
-  | Outport Const
-  | UnitDelay Const
-  | Cast String
-  | Assertion
-  | Const' Const
-  | Add'
-  | Sub'
-  | Mul'
-  | Div'
-  | Mod'
-  | Not'
-  | And'
-  | Or'
-  | Eq'
-  | Lt'
-  | Gt'
-  | Le'
-  | Ge'
-  | Mux'
-
-data Netlist = Netlist
-  { nextId :: Int
-  , path   :: Path
-  , vars   :: [Path]
-  , env    :: [Name]
-  , blocks :: [(Name, Block)]
-  , nets   :: [(Name, (Name, Int))]
-  }
-
--- Simulink generation.
-codeMdl :: Name -> Statement -> IO ()
-codeMdl name stmt = do
-  net <- execStateT all (Netlist 0 [] paths env [] []) >>= return . removeNullEffect
-  writeFile (name ++ ".mdl") $ show $ mdl name $ (mdlBlocks $ blocks net) ++ (mdlLines $ nets net)
-  where
-  vars = stmtVars stmt
-  paths = [ path | (_, path, _) <- vars ]
-  env = [ error $ "variable " ++ pathName a ++ " does not have a source" | a <- vars ]
-
-  all :: Net ()
-  all = do
-    inputs <- mapM input vars
-    elaborate stmt
-    mapM_ output $ zip vars inputs
-
-  input :: VarInfo -> Net Name
-  input (input, path, const) = if input
-    then do
-      a <- block' (pathName path) (Inport const)
-      updateEnv path a
-      return a
-    else do
-      a <- block $ UnitDelay const
-      b <- block $ Cast $ constType const
-      net a (b, 0)
-      updateEnv path b
-      return a
-  
-  output :: (VarInfo, Name) -> Net ()
-  output ((True, _, _), _) = return ()
-  output ((False, path, const), delay) = do
-    a <- block' (pathName path) $ Outport const
-    src <- getNet path
-    net src (a, 0)
-    net src (delay, 0)
-
-newName :: Net Name
-newName = do
-  net <- get
-  put net { nextId = nextId net + 1 }
-  return $ "b" ++ show (nextId net)
-
--- New unnamed block.
-block :: Block -> Net Name
-block a = do
-  name <- newName
-  modify $ \ net -> net { blocks = (name, a) : blocks net }
-  return name
-
--- New named block.
-block' :: Name -> Block -> Net Name
-block' name a = do
-  modify $ \ net -> net { blocks = (name, a) : blocks net }
-  return name
-
--- New net.
-net :: Name -> (Name, Int) -> Net ()
-net src (dest, port) = modify $ \ net -> net { nets = (src, (dest, port)) : nets net }
-
-updateEnv :: Path -> Name -> Net ()
-updateEnv path name = do
-  net <- get
-  let i = fromJust $ elemIndex path $ vars net
-      pre = take i $ env net
-      post = drop (i + 1) $ env net
-  put net { env = pre ++ [name] ++ post }
-
-getNet :: Path -> Net Name
-getNet path = do
-  net <- get
-  return $ env net !! (fromJust $ elemIndex path $ vars net)
-
-getPathName :: Net Name
-getPathName = do
-  net <- get
-  return $ pathName $ path net
-
--- Elaborate netlist.
-elaborate :: Statement -> Net ()
-elaborate a = case a of 
-
-  Assign (V _ path _) b -> do
-    b <- evalExpr b
-    updateEnv path b
-
-  Branch a b c -> do
-    cond <- evalExpr a
-    net0 <- get
-
-    elaborate b
-    net1 <- get
-    modify $ \ net -> net { env = env net0 }
-
-    elaborate c
-    net2 <- get
-    modify $ \ net -> net { env = env net0 }
-
-    names <- mergeEnvs cond (env net1) (env net2)
-    modify $ \ net -> net { env = names }
-
-    where
-
-    mergeEnvs :: Name -> [Name] -> [Name] -> Net [Name]
-    mergeEnvs _ [] [] = return []
-    mergeEnvs cond (a : as) (b : bs) = do
-      names <- mergeEnvs cond as bs
-      name <- if a == b then return a else do
-        switch <- block Mux'
-        net a    (switch, 0)
-        net cond (switch, 1)
-        net b    (switch, 2)
-        return switch
-      return $ name : names
-    mergeEnvs _ _ _ = error "unbalanced environments"
-
-  Sequence a b    -> elaborate a >> elaborate b
-
-  Theorem _ _ _ a -> do
-    a <- evalExpr a
-    name <- getPathName
-    assert <- block' name Assertion
-    net a (assert, 0)
-
-  Assume a -> do
-    a <- evalExpr a
-    name <- getPathName
-    assert <- block' name Assertion
-    net a (assert, 0)
-
-  Label name a -> do
-    modify $ \ net -> net { path = path net ++ [name] }
-    elaborate a
-    modify $ \ net -> net { path = init $ path net }
-
-  Null            -> return ()
-
-evalExpr :: E a -> Net Name
-evalExpr a = case a of
-  Ref (V _ path _) -> getNet path
-  Const a   -> block $ Const' $ const' a
-  Add a b   -> f2 Add' a b
-  Sub a b   -> f2 Sub' a b
-  Mul a b   -> do
-    b <- block $ Const' $ const' b
-    f2' Mul' a b
-  Div a b   -> do
-    b <- block $ Const' $ const' b
-    f2' Div' a b
-  Mod a b   -> do
-    b <- block $ Const' $ const' b
-    f2' Mod' a b
-  Not a     -> f1 Not' a
-  And a b   -> f2 And' a b
-  Or  a b   -> f2 Or'  a b
-  Eq  a b   -> f2 Eq'  a b
-  Lt  a b   -> f2 Lt'  a b
-  Gt  a b   -> f2 Gt'  a b
-  Le  a b   -> f2 Le'  a b
-  Ge  a b   -> f2 Ge'  a b
-  Mux a b c -> f3 Mux' b a c
-  where
-  f1 :: Block -> E a -> Net Name
-  f1 b a1 = do
-    a1 <- evalExpr a1
-    b  <- block b
-    net a1 (b, 0)
-    return b
-
-  f2 :: Block -> E a -> E b -> Net Name
-  f2 b a1 a2 = do
-    a1 <- evalExpr a1
-    a2 <- evalExpr a2
-    b  <- block b
-    net a1 (b, 0)
-    net a2 (b, 1)
-    return b
-
-  f2' :: Block -> E a -> Name -> Net Name
-  f2' b a1 a2 = do
-    a1 <- evalExpr a1
-    b  <- block b
-    net a1 (b, 0)
-    net a2 (b, 1)
-    return b
-
-  f3 :: Block -> E a -> E b -> E c -> Net Name
-  f3 b a1 a2 a3 = do
-    a1 <- evalExpr a1
-    a2 <- evalExpr a2
-    a3 <- evalExpr a3
-    b  <- block b
-    net a1 (b, 0)
-    net a2 (b, 1)
-    net a3 (b, 2)
-    return b
-
-data Mdl
-  = String :- String
-  | String := [Mdl]
-
-instance Show Mdl where
-  show a = case a of
-    name :- value -> name ++ "\t" ++ show value ++ "\n"
-    name := items -> name ++ " {\n" ++ indent (concatMap show items) ++ "}\n"
-    where
-    indent = unlines . map ('\t' :) . lines
-
-mdl :: Name -> [Mdl] -> Mdl
-mdl name blocks = "Library" :=
-  [ "Name" :- name
-  , "System" :=
-    [ "Name" :- name
-    , "Block" :=
-      [ "BlockType" :- "SubSystem"
-      , "Name" :- name
-      , "TreatAsAtomicUnit" :- "on"
-      , "System" := ("Name" :- name) : blocks
-      ]
-    ]
-  ]
-
-mdlLines :: [(Name, (Name, Int))] -> [Mdl]
-mdlLines nets = map branch branches
-  where
-  branches :: [(Name, [(Name, Int)])]
-  branches = [ (src, [ dest | (src', dest) <- nets, src == src' ]) | src <- nub $ fst $ unzip nets ]
-  branch :: (Name, [(Name, Int)]) -> Mdl
-  branch (src, dests) = "Line" :=
-    [ "SrcBlock" :- src
-    , "SrcPort"  :- "1"
-    ] ++ (if length dests == 1 then head dests' else map ("Branch" :=) dests')
-    where
-    dests' = [ ["DstBlock" :- dest, "DstPort" :- show $ port + 1] | (dest, port) <- dests ]
-
-mdlBlocks :: [(Name, Block)] -> [Mdl]
-mdlBlocks blocks = map (port "Inport") inputs ++ map blk others ++ map (port "Outport") outputs
-  where
-  inputs  = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Inport  init) <- blocks ]
-  outputs = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Outport init) <- blocks ]
-  others  = [ (name, block) | (name, block) <- blocks, not $ isPort block ]
-  port :: String -> (Int, (Name, String)) -> Mdl
-  port direction (port, (name, typ)) = mdlBlock direction name
-    [ "Port" :- show port
-    , "DataType" :- typ
-    ]
-  isPort :: Block -> Bool
-  isPort (Inport  _) = True
-  isPort (Outport _) = True
-  isPort _           = False
-
-mdlBlock :: String -> Name -> [Mdl] -> Mdl
-mdlBlock blockType name fields = "Block" :=
-  [ "BlockType" :- blockType
-  , "Name"      :- name
-  ] ++ fields
-
-constType :: Const -> String
-constType a = case a of
-  Bool  _ -> "boolean"
-  Int   _ -> "int32"
-  Float _ -> "single"
-
-blk :: (Name, Block) -> Mdl
-blk (name, a) = case a of
-  Inport  _ -> undefined
-  Outport _ -> undefined
-  UnitDelay init -> f "UnitDelay"          ["X0" :- showConst init, "SampleTime" :- "-1"]
-  Cast t         -> f "DataTypeConversion" ["OutDataTypeMode" :- t]
-  Assertion      -> f "Assertion"          ["StopWhenAssertionFail" :- "off", "SampleTime" :- "-1", "Enabled" :- "on"]
-  Const' c       -> f "Constant"           ["Value" :- showConst c, "OutDataTypeMode" :- constType c]
-  Add'           -> f "Sum"                ["Inputs" :- "++"]
-  Sub'           -> f "Sum"                ["Inputs" :- "+-"]
-  Mul'           -> f "Product"            ["Inputs" :- "**"]
-  Div'           -> f "Product"            ["Inputs" :- "*/"]
-  Mod'           -> f "Math"               ["Operator" :- "mod"]
-  Not'           -> f "Logic"              ["Operator" :- "NOT", "Inputs" :- "1"]
-  And'           -> f "Logic"              ["Operator" :- "AND", "Inputs" :- "2"]
-  Or'            -> f "Logic"              ["Operator" :- "OR",  "Inputs" :- "2"]
-  Eq'            -> f "RelationalOperator" ["Operator" :- "==", "LogicOutDataTypeMode" :- "boolean"]
-  Lt'            -> f "RelationalOperator" ["Operator" :- "<" , "LogicOutDataTypeMode" :- "boolean"]
-  Gt'            -> f "RelationalOperator" ["Operator" :- ">" , "LogicOutDataTypeMode" :- "boolean"]
-  Le'            -> f "RelationalOperator" ["Operator" :- "<=", "LogicOutDataTypeMode" :- "boolean"]
-  Ge'            -> f "RelationalOperator" ["Operator" :- ">=", "LogicOutDataTypeMode" :- "boolean"]
-  Mux'           -> f "Switch"             ["Criteria" :- "u2 ~= 0"]
-  where
-  f typ args = mdlBlock typ name args
-
-isSrc :: Block -> Bool
-isSrc a = case a of
-  Outport _ -> False
-  Assertion -> False
-  _         -> True
+-- | Code generation targets.
+data Target
+  = C
+  | Modelica
+  | Simulink
+  deriving Eq
 
-removeNullEffect :: Netlist -> Netlist
-removeNullEffect net = if null unused then net else removeNullEffect net { blocks = blocks', nets = nets' }
+-- | Generate target code.
+code :: Target -> Name -> Statement -> IO ()
+code target name stmt = f name stmt
   where
-  unused = [ name | (name, block) <- blocks net, isSrc block, not $ any (\ (n, _) -> name == n) $ nets net ]
-  blocks' = [ (name, block) | (name, block) <- blocks net, not $ elem name unused ]
-  nets' = [ (src, (dest, port)) | (src, (dest, port)) <- nets net, not $ elem dest unused ]
+  f = case target of
+    C        -> codeC
+    Modelica -> codeModelica
+    Simulink -> codeSimulink
 
diff --git a/Language/ImProve/Code/C.hs b/Language/ImProve/Code/C.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Code/C.hs
@@ -0,0 +1,100 @@
+module Language.ImProve.Code.C (codeC) where
+
+import Data.List
+import Text.Printf
+
+import Language.ImProve.Code.Common
+import Language.ImProve.Core
+import Language.ImProve.Tree hiding (Branch)
+import qualified Language.ImProve.Tree as T
+
+-- | Generate C.
+codeC :: Name -> Statement -> IO ()
+codeC name stmt = do
+  writeFile (name ++ ".c") $
+       "/* Generated by ImProve. */\n\n"
+    ++ "#include <assert.h>\n\n"
+    ++ codeVariables True scope ++ "\n"
+    ++ "void " ++ name ++ "()\n{\n"
+    ++ indent (codeStmt name [] stmt)
+    ++ "}\n\n"
+  writeFile (name ++ ".h") $
+       "/* Generated by ImProve. */\n\n"
+    ++ "#ifdef __cplusplus\n"
+    ++ "extern \"C\" {\n"
+    ++ "#endif\n\n"
+    ++ codeVariables False scope ++ "\n"
+    ++ "void " ++ name ++ "(void);\n\n"
+    ++ "#ifdef __cplusplus\n"
+    ++ "}\n"
+    ++ "#endif\n"
+  where
+  scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of
+    [] -> error "program contains no useful statements"
+    a  -> T.Branch (name ++ "_variables") a
+
+instance Show Statement where show = codeStmt "none" []
+
+codeStmt :: Name -> [Name] -> Statement -> String
+codeStmt name path a = case a of
+  Assign a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"
+  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n"
+  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n"
+  Sequence a b -> codeStmt name path a ++ codeStmt name path b
+  Theorem _ _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
+  Assume _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"
+  Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)
+  Null -> ""
+  where
+
+  codeExpr :: E a -> String
+  codeExpr a = case a of
+    Ref a     -> name ++ "_variables." ++ pathName a
+    Const a   -> showConst $ const' a
+    Add a b   -> group [codeExpr a, "+", codeExpr b]
+    Sub a b   -> group [codeExpr a, "-", codeExpr b]
+    Mul a b   -> group [codeExpr a, "*", showConst (const' b)]
+    Div a b   -> group [codeExpr a, "/", showConst (const' b)]
+    Mod a b   -> group [codeExpr a, "%", showConst (const' b)]
+    Not a     -> group ["!", codeExpr a]
+    And a b   -> group [codeExpr a, "&&",  codeExpr b]
+    Or  a b   -> group [codeExpr a, "||",  codeExpr b]
+    Eq  a b   -> group [codeExpr a, "==",  codeExpr b]
+    Lt  a b   -> group [codeExpr a, "<",   codeExpr b]
+    Gt  a b   -> group [codeExpr a, ">",   codeExpr b]
+    Le  a b   -> group [codeExpr a, "<=",  codeExpr b]
+    Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]
+    Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] 
+    where
+    group :: [String] -> String
+    group a = "(" ++ intercalate " " a ++ ")"
+
+indent' :: String -> String
+indent' a = case lines a of
+  [] -> []
+  (a:b) -> a ++ "\n" ++ indent (unlines b)
+
+codeVariables :: Bool -> (Tree Name (Bool, Path, Const)) -> String
+codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n\t" ++ f2 a else "") ++ ";\n"
+  where
+  f1 a = case a of
+    T.Branch name items -> "struct {  /* " ++ name ++ " */\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"
+    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  /* input */" else "")
+
+  f2 a = case a of
+    T.Branch name items -> indent' $ "{   " ++ (intercalate ",   " $ map f2 items) ++ "}  /* " ++ name ++ " */\n"
+    Leaf name (_, _, init) -> printf "%-15s  /* %s */\n" (showConst init) name
+
+showConst :: Const -> String
+showConst a = case a of
+  Bool  True  -> "1"
+  Bool  False -> "0"
+  Int   a     -> show a
+  Float a     -> show a
+
+showConstType :: Const -> String
+showConstType a = case a of
+  Bool  _ -> "int"
+  Int   _ -> "int"
+  Float _ -> "float"
+
diff --git a/Language/ImProve/Code/Common.hs b/Language/ImProve/Code/Common.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Code/Common.hs
@@ -0,0 +1,7 @@
+module Language.ImProve.Code.Common
+  ( indent
+  ) where
+
+indent :: String -> String
+indent = unlines . map ("\t" ++) . lines
+
diff --git a/Language/ImProve/Code/Modelica.hs b/Language/ImProve/Code/Modelica.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Code/Modelica.hs
@@ -0,0 +1,154 @@
+module Language.ImProve.Code.Modelica (codeModelica) where
+
+import Data.Function
+import Data.List
+import Data.Maybe
+import Text.Printf
+
+import Language.ImProve.Code.Simulink
+import Language.ImProve.Core
+
+-- Modelica generation.
+codeModelica :: Name -> Statement -> IO ()
+codeModelica name stmt = do
+  net <- netlist stmt >>= return . moRename
+  writeFile (name ++ ".mo") $ unlines $
+    [ "// Generated by ImProve."
+    , ""
+    , "block " ++ name
+    , "\tparameter Real Period=0.001;"
+    ] ++
+    inputs net ++
+    outputs net ++
+    [ "protected" ] ++
+    states net ++
+    internals net ++
+    [ "equation"
+    , "\twhen sample(0, Period) then"
+    ] ++
+    equations net ++
+    [ "\tend when;"
+    , "end " ++ name ++ ";"
+    ]
+  where
+  inputs    net = [ printf "\tinput %s %s;"                 (constType a) name               | (name, Inport a)    <- sortedBlocks net ]
+  outputs   net = [ printf "\tdiscrete output %s %s;"       (constType a) name               | (name, Outport a)   <- sortedBlocks net ]
+  states    net = [ printf "\tdiscrete %s %s (start = %s);" (constType a) name (showConst a) | (name, UnitDelay a) <- sortedBlocks net ]
+  internals net = [ printf "\tdiscrete %s %s;"           (constType $ netType net name) name | (name, block) <- sortedBlocks net, isInternal block ]
+  equations net = mapMaybe (equation net) $ blocks net
+  sortedBlocks net = sortBy (compare `on` fst) $ blocks net
+
+equation :: Netlist -> (Name, Block) -> Maybe String
+equation net (name, block) = case block of
+  Inport  _      -> Nothing
+  Outport _      -> f $ arg 0
+  UnitDelay _    -> f $ arg 0
+  Cast _         -> f $ printf "pre(%s)" $ arg 0
+  Assertion      -> Just $ printf "\tassert(%s, \"%s\");" (arg 0) name
+  Const' c       -> f $ showConst c
+  Add'           -> f $ printf "%s + %s" (arg 0) (arg 1)
+  Sub'           -> f $ printf "%s - %s" (arg 0) (arg 1)
+  Mul'           -> f $ printf "%s * %s" (arg 0) (arg 1)
+  Div'           -> case netType net name of
+		      Bool  _ -> error "Modelica.equation: invalid netlist (1)"
+                      Int   _ -> f $ printf "div(%s, %s)" (arg 0) (arg 1)
+		      Float _ -> f $ printf "%s / %s"     (arg 0) (arg 1)
+  Mod'           -> f $ printf "mod(%s, %s)" (arg 0) (arg 1)
+  Not'           -> f $ printf "not %s" $ arg 0
+  And'           -> f $ printf "%s and %s" (arg 0) (arg 1)
+  Or'            -> f $ printf "%s or %s" (arg 0) (arg 1)
+  Eq'            -> f $ printf "%s == %s" (arg 0) (arg 1)
+  Lt'            -> f $ printf "%s < %s" (arg 0) (arg 1)
+  Gt'            -> f $ printf "%s > %s" (arg 0) (arg 1)
+  Le'            -> f $ printf "%s <= %s" (arg 0) (arg 1)
+  Ge'            -> f $ printf "%s >= %s" (arg 0) (arg 1)
+  Mux'           -> f $ printf "if %s then %s else %s" (arg 0) (arg 1) (arg 2)
+  where
+  f :: String -> Maybe String
+  f a = Just $ printf "\t%s = %s;" name a
+  arg i = case [ n | (n, (n1, p1)) <- nets net, n1 == name, p1 == i ] of
+    [n] -> n
+    _ -> error "Modelica.equation: invalid netlist (2)"
+
+isInternal :: Block -> Bool
+isInternal a = case a of
+  Inport    _ -> False
+  Outport   _ -> False
+  UnitDelay _ -> False
+  Assertion   -> False
+  _           -> True
+
+moRename :: Netlist -> Netlist
+moRename net = net { env = map f $ env net, blocks = [ (f n, b) | (n, b) <- blocks net ], nets = [ (f a, (f b, i)) | (a, (b, i)) <- nets net ] }
+  where
+  f n = "`" ++ n ++ "`"
+
+showConst :: Const -> String
+showConst a = case a of
+  Bool  True  -> "true"
+  Bool  False -> "false"
+  Int   a     -> show a
+  Float a     -> show a
+
+constType :: Const -> String
+constType a = case a of
+  Bool  _ -> "Boolean"
+  Int   _ -> "Integer"
+  Float _ -> "Real   "
+
+netType :: Netlist -> Name -> Const
+netType net name = case fromJust $ lookup name $ blocks net of
+  Inport    a -> a
+  UnitDelay a -> a
+  Const'    a -> a
+  Outport _ -> error "Modelica.netType: not expecting Outport"
+  Assertion -> error "Modelica.netType: not expecting Assertion"
+  Mod' -> Int 0
+  Not' -> Bool False
+  And' -> Bool False
+  Or'  -> Bool False
+  Eq'  -> Bool False
+  Lt'  -> Bool False
+  Gt'  -> Bool False
+  Le'  -> Bool False
+  Ge'  -> Bool False
+  Mux' -> follow 1
+  _    -> follow 0
+  where
+  follow :: Int -> Const
+  follow p = case [ n | (n, (n1, p1)) <- nets net, n1 == name, p1 == p ] of
+    [n] -> netType net n
+    _   -> error "Modelica.netType: invalid netlist"
+
+{-
+data Block
+  = Inport  Const
+  | Outport Const
+  | UnitDelay Const
+  | Cast String
+  | Assertion
+  | Const' Const
+  | Add'
+  | Sub'
+  | Mul'
+  | Div'
+  | Mod'
+  | Not'
+  | And'
+  | Or'
+  | Eq'
+  | Lt'
+  | Gt'
+  | Le'
+  | Ge'
+  | Mux'
+
+data Netlist = Netlist
+  { nextId :: Int
+  , path   :: Path
+  , vars   :: [Path]
+  , env    :: [Name]
+  , blocks :: [(Name, Block)]
+  , nets   :: [(Name, (Name, Int))]
+  }
+-}
diff --git a/Language/ImProve/Code/Simulink.hs b/Language/ImProve/Code/Simulink.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Code/Simulink.hs
@@ -0,0 +1,371 @@
+module Language.ImProve.Code.Simulink
+  ( codeSimulink
+  , Netlist (..)
+  , Block   (..)
+  , netlist
+  ) where
+
+import Control.Monad.State
+import Data.List
+import Data.Maybe
+
+import Language.ImProve.Code.Common
+import Language.ImProve.Core
+
+infixr 0 :-, :=
+
+showConst :: Const -> String
+showConst a = case a of
+  Bool  True  -> "1"
+  Bool  False -> "0"
+  Int   a     -> show a
+  Float a     -> show a
+
+type Net = StateT Netlist IO
+
+data Block
+  = Inport  Const
+  | Outport Const
+  | UnitDelay Const
+  | Cast String
+  | Assertion
+  | Const' Const
+  | Add'
+  | Sub'
+  | Mul'
+  | Div'
+  | Mod'
+  | Not'
+  | And'
+  | Or'
+  | Eq'
+  | Lt'
+  | Gt'
+  | Le'
+  | Ge'
+  | Mux'
+
+data Netlist = Netlist
+  { nextId :: Int
+  , path   :: Path
+  , vars   :: [Path]
+  , env    :: [Name]
+  , blocks :: [(Name, Block)]
+  , nets   :: [(Name, (Name, Int))]
+  }
+
+-- Simulink generation.
+codeSimulink :: Name -> Statement -> IO ()
+codeSimulink name stmt = do
+  net <- netlist stmt
+  writeFile (name ++ ".mdl") $ show $ mdl name $ (mdlBlocks $ blocks net) ++ (mdlLines $ nets net)
+
+-- | Builds a netlist.
+netlist :: Statement -> IO Netlist
+netlist stmt' = execStateT all (Netlist 0 [] paths env [] []) >>= return . removeNullEffect
+  where
+  stmt = lowerConditionals (Const True) stmt'
+  vars = stmtVars stmt
+  paths = [ path | (_, path, _) <- vars ]
+  env = [ error $ "variable " ++ pathName a ++ " does not have a source" | a <- vars ]
+
+  all :: Net ()
+  all = do
+    inputs <- mapM input vars
+    evalStmt stmt
+    mapM_ output $ zip vars inputs
+
+  input :: VarInfo -> Net Name
+  input (input, path, const) = if input
+    then do
+      a <- block' (pathName path) (Inport const)
+      updateEnv path a
+      return a
+    else do
+      a <- block $ UnitDelay const
+      b <- block $ Cast $ constType const
+      net a (b, 0)
+      updateEnv path b
+      return a
+  
+  output :: (VarInfo, Name) -> Net ()
+  output ((True, _, _), _) = return ()
+  output ((False, path, const), delay) = do
+    a <- block' (pathName path) $ Outport const
+    src <- getNet path
+    net src (a, 0)
+    net src (delay, 0)
+
+-- Pushes conditionals down to theorems and assumptions.
+lowerConditionals :: E Bool -> Statement -> Statement
+lowerConditionals cond a = case a of
+  Assign   a b     -> Assign a b
+  Branch   a b c   -> Branch a (lowerConditionals (And cond a) b) (lowerConditionals (And cond $ Not a) c)
+  Sequence a b     -> Sequence (lowerConditionals cond a) (lowerConditionals cond b)
+  Theorem  a b c d -> Theorem a b c $ Or (Not cond) d
+  Assume   i a     -> Assume i $ Or (Not cond) a
+  Label    a b     -> Label a $ lowerConditionals cond b
+  Null             -> Null
+
+newName :: Net Name
+newName = do
+  net <- get
+  put net { nextId = nextId net + 1 }
+  return $ "b" ++ show (nextId net)
+
+-- New unnamed block.
+block :: Block -> Net Name
+block a = do
+  name <- newName
+  modify $ \ net -> net { blocks = (name, a) : blocks net }
+  return name
+
+-- New named block.
+block' :: Name -> Block -> Net Name
+block' name a = do
+  modify $ \ net -> net { blocks = (name, a) : blocks net }
+  return name
+
+-- New net.
+net :: Name -> (Name, Int) -> Net ()
+net src (dest, port) = modify $ \ net -> net { nets = (src, (dest, port)) : nets net }
+
+updateEnv :: Path -> Name -> Net ()
+updateEnv path name = do
+  net <- get
+  let i = fromJust $ elemIndex path $ vars net
+      pre = take i $ env net
+      post = drop (i + 1) $ env net
+  put net { env = pre ++ [name] ++ post }
+
+getNet :: Path -> Net Name
+getNet path = do
+  net <- get
+  return $ env net !! (fromJust $ elemIndex path $ vars net)
+
+getPathName :: Net Name
+getPathName = do
+  net <- get
+  return $ pathName $ path net
+
+-- Elaborate netlist.
+evalStmt :: Statement -> Net ()
+evalStmt a = case a of 
+
+  Assign (V _ path _) b -> do
+    b <- evalExpr b
+    updateEnv path b
+
+  Branch a b c -> do
+    cond <- evalExpr a
+    net0 <- get
+
+    evalStmt b
+    net1 <- get
+    modify $ \ net -> net { env = env net0 }
+
+    evalStmt c
+    net2 <- get
+    modify $ \ net -> net { env = env net0 }
+
+    names <- mergeEnvs cond (env net1) (env net2)
+    modify $ \ net -> net { env = names }
+
+    where
+
+    mergeEnvs :: Name -> [Name] -> [Name] -> Net [Name]
+    mergeEnvs _ [] [] = return []
+    mergeEnvs cond (a : as) (b : bs) = do
+      names <- mergeEnvs cond as bs
+      name <- if a == b then return a else do
+        switch <- block Mux'
+        net a    (switch, 0)
+        net cond (switch, 1)
+        net b    (switch, 2)
+        return switch
+      return $ name : names
+    mergeEnvs _ _ _ = error "unbalanced environments"
+
+  Sequence a b    -> evalStmt a >> evalStmt b
+
+  Theorem _ _ _ a -> do
+    a <- evalExpr a
+    name <- getPathName
+    assert <- block' name Assertion
+    net a (assert, 0)
+
+  Assume _ a -> do
+    a <- evalExpr a
+    name <- getPathName
+    assert <- block' name Assertion
+    net a (assert, 0)
+
+  Label name a -> do
+    modify $ \ net -> net { path = path net ++ [name] }
+    evalStmt a
+    modify $ \ net -> net { path = init $ path net }
+
+  Null            -> return ()
+
+evalExpr :: E a -> Net Name
+evalExpr a = case a of
+  Ref (V _ path _) -> getNet path
+  Const a   -> block $ Const' $ const' a
+  Add a b   -> f2 Add' a b
+  Sub a b   -> f2 Sub' a b
+  Mul a b   -> do
+    b <- block $ Const' $ const' b
+    f2' Mul' a b
+  Div a b   -> do
+    b <- block $ Const' $ const' b
+    f2' Div' a b
+  Mod a b   -> do
+    b <- block $ Const' $ const' b
+    f2' Mod' a b
+  Not a     -> f1 Not' a
+  And a b   -> f2 And' a b
+  Or  a b   -> f2 Or'  a b
+  Eq  a b   -> f2 Eq'  a b
+  Lt  a b   -> f2 Lt'  a b
+  Gt  a b   -> f2 Gt'  a b
+  Le  a b   -> f2 Le'  a b
+  Ge  a b   -> f2 Ge'  a b
+  Mux a b c -> f3 Mux' b a c
+  where
+  f1 :: Block -> E a -> Net Name
+  f1 b a1 = do
+    a1 <- evalExpr a1
+    b  <- block b
+    net a1 (b, 0)
+    return b
+
+  f2 :: Block -> E a -> E b -> Net Name
+  f2 b a1 a2 = do
+    a1 <- evalExpr a1
+    a2 <- evalExpr a2
+    b  <- block b
+    net a1 (b, 0)
+    net a2 (b, 1)
+    return b
+
+  f2' :: Block -> E a -> Name -> Net Name
+  f2' b a1 a2 = do
+    a1 <- evalExpr a1
+    b  <- block b
+    net a1 (b, 0)
+    net a2 (b, 1)
+    return b
+
+  f3 :: Block -> E a -> E b -> E c -> Net Name
+  f3 b a1 a2 a3 = do
+    a1 <- evalExpr a1
+    a2 <- evalExpr a2
+    a3 <- evalExpr a3
+    b  <- block b
+    net a1 (b, 0)
+    net a2 (b, 1)
+    net a3 (b, 2)
+    return b
+
+data Mdl
+  = String :- String
+  | String := [Mdl]
+
+instance Show Mdl where
+  show a = case a of
+    name :- value -> name ++ "\t" ++ show value ++ "\n"
+    name := items -> name ++ " {\n" ++ indent (concatMap show items) ++ "}\n"
+
+mdl :: Name -> [Mdl] -> Mdl
+mdl name blocks = "Library" :=
+  [ "Name" :- name
+  , "System" :=
+    [ "Name" :- name
+    , "Block" :=
+      [ "BlockType" :- "SubSystem"
+      , "Name" :- name
+      , "TreatAsAtomicUnit" :- "on"
+      , "System" := ("Name" :- name) : blocks
+      ]
+    ]
+  ]
+
+mdlLines :: [(Name, (Name, Int))] -> [Mdl]
+mdlLines nets = map branch branches
+  where
+  branches :: [(Name, [(Name, Int)])]
+  branches = [ (src, [ dest | (src', dest) <- nets, src == src' ]) | src <- nub $ fst $ unzip nets ]
+  branch :: (Name, [(Name, Int)]) -> Mdl
+  branch (src, dests) = "Line" :=
+    [ "SrcBlock" :- src
+    , "SrcPort"  :- "1"
+    ] ++ (if length dests == 1 then head dests' else map ("Branch" :=) dests')
+    where
+    dests' = [ ["DstBlock" :- dest, "DstPort" :- show $ port + 1] | (dest, port) <- dests ]
+
+mdlBlocks :: [(Name, Block)] -> [Mdl]
+mdlBlocks blocks = map (port "Inport") inputs ++ map blk others ++ map (port "Outport") outputs
+  where
+  inputs  = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Inport  init) <- blocks ]
+  outputs = zip [1 ..] $ sortBy (\ (a, _) (b, _) -> compare a b) [ (name, constType init) | (name, Outport init) <- blocks ]
+  others  = [ (name, block) | (name, block) <- blocks, not $ isPort block ]
+  port :: String -> (Int, (Name, String)) -> Mdl
+  port direction (port, (name, typ)) = mdlBlock direction name
+    [ "Port" :- show port
+    , "DataType" :- typ
+    ]
+  isPort :: Block -> Bool
+  isPort (Inport  _) = True
+  isPort (Outport _) = True
+  isPort _           = False
+
+mdlBlock :: String -> Name -> [Mdl] -> Mdl
+mdlBlock blockType name fields = "Block" :=
+  [ "BlockType" :- blockType
+  , "Name"      :- name
+  ] ++ fields
+
+constType :: Const -> String
+constType a = case a of
+  Bool  _ -> "boolean"
+  Int   _ -> "int32"
+  Float _ -> "single"
+
+blk :: (Name, Block) -> Mdl
+blk (name, a) = case a of
+  Inport  _ -> undefined
+  Outport _ -> undefined
+  UnitDelay init -> f "UnitDelay"          ["X0" :- showConst init, "SampleTime" :- "-1"]
+  Cast t         -> f "DataTypeConversion" ["OutDataTypeMode" :- t]
+  Assertion      -> f "Assertion"          ["StopWhenAssertionFail" :- "off", "SampleTime" :- "-1", "Enabled" :- "on"]
+  Const' c       -> f "Constant"           ["Value" :- showConst c, "OutDataTypeMode" :- constType c]
+  Add'           -> f "Sum"                ["Inputs" :- "++"]
+  Sub'           -> f "Sum"                ["Inputs" :- "+-"]
+  Mul'           -> f "Product"            ["Inputs" :- "**"]
+  Div'           -> f "Product"            ["Inputs" :- "*/"]
+  Mod'           -> f "Math"               ["Operator" :- "mod"]
+  Not'           -> f "Logic"              ["Operator" :- "NOT", "Inputs" :- "1"]
+  And'           -> f "Logic"              ["Operator" :- "AND", "Inputs" :- "2"]
+  Or'            -> f "Logic"              ["Operator" :- "OR",  "Inputs" :- "2"]
+  Eq'            -> f "RelationalOperator" ["Operator" :- "==", "LogicOutDataTypeMode" :- "boolean"]
+  Lt'            -> f "RelationalOperator" ["Operator" :- "<" , "LogicOutDataTypeMode" :- "boolean"]
+  Gt'            -> f "RelationalOperator" ["Operator" :- ">" , "LogicOutDataTypeMode" :- "boolean"]
+  Le'            -> f "RelationalOperator" ["Operator" :- "<=", "LogicOutDataTypeMode" :- "boolean"]
+  Ge'            -> f "RelationalOperator" ["Operator" :- ">=", "LogicOutDataTypeMode" :- "boolean"]
+  Mux'           -> f "Switch"             ["Criteria" :- "u2 ~= 0"]
+  where
+  f typ args = mdlBlock typ name args
+
+isSrc :: Block -> Bool
+isSrc a = case a of
+  Outport _ -> False
+  Assertion -> False
+  _         -> True
+
+removeNullEffect :: Netlist -> Netlist
+removeNullEffect net = if null unused then net else removeNullEffect net { blocks = blocks', nets = nets' }
+  where
+  unused = [ name | (name, block) <- blocks net, isSrc block, not $ any (\ (n, _) -> name == n) $ nets net ]
+  blocks' = [ (name, block) | (name, block) <- blocks net, not $ elem name unused ]
+  nets' = [ (src, (dest, port)) | (src, (dest, port)) <- nets net, not $ elem dest unused ]
+
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -108,7 +108,7 @@
   Branch   :: E Bool -> Statement -> Statement -> Statement
   Sequence :: Statement -> Statement -> Statement
   Theorem  :: Int -> Int -> [Int] -> E Bool -> Statement -- Theorem id k lemmas expr
-  Assume   :: E Bool -> Statement
+  Assume   :: Int -> E Bool -> Statement                 -- Assume id expr
   Label    :: Name -> Statement -> Statement
   Null     :: Statement
 
@@ -131,7 +131,7 @@
   Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c
   Sequence a b -> nub $ stmtVars a ++ stmtVars b
   Theorem _ _ _ a -> exprVars a
-  Assume a     -> exprVars a
+  Assume  _ a     -> exprVars a
   Label  _ a   -> stmtVars a
   Null         -> []
 
@@ -162,7 +162,7 @@
   Assign _ _   -> []
   Branch _ a b -> theorems a ++ theorems b
   Sequence a b -> theorems a ++ theorems b
-  Assume _     -> []
+  Assume _ _   -> []
   Label  _ a   -> theorems a
   Null         -> []
 
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -60,7 +60,7 @@
 
 -- | Build the gcdMain code (i.e. gcd.c, gcd.h).
 buildGCD :: IO ()
-buildGCD = code "gcd" gcdMain
+buildGCD = code C "gcd" gcdMain
 
 
 
@@ -176,13 +176,13 @@
 buildArbiters :: IO ()
 buildArbiters = do
   putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."
-  code "arbiter1" $ arbiter "arbiter1" arbiter1
+  code C "arbiter1" $ arbiter "arbiter1" arbiter1
 
   putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."
-  code "arbiter2" $ arbiter "arbiter2" arbiter2
+  code C "arbiter2" $ arbiter "arbiter2" arbiter2
 
   putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."
-  code "arbiter3" $ arbiter "arbiter3" arbiter3
+  code C "arbiter3" $ arbiter "arbiter3" arbiter3
 
 -- | Run all examples.
 runAll :: IO ()
diff --git a/Language/ImProve/Path.hs b/Language/ImProve/Path.hs
new file mode 100644
--- /dev/null
+++ b/Language/ImProve/Path.hs
@@ -0,0 +1,42 @@
+module Language.ImProve.Path
+  ( totalPaths
+  ) where
+
+import Language.ImProve.Core
+
+totalPaths :: Name -> Statement -> IO ()
+totalPaths name stmt = do
+  putStrLn $ "total paths: " ++ show (paths stmt)
+  writeFile (name ++ ".dot") (dot stmt)
+
+paths :: Statement -> Integer
+paths a = case a of
+  Assign _ _      -> 1
+  Branch _ a b    -> paths a + paths b
+  Sequence a b    -> paths a * paths b
+  Theorem _ _ _ _ -> 1
+  Assume  _ _     -> 1
+  Label  _ a      -> paths a
+  Null            -> 1
+
+dot :: Statement -> String
+dot stmt = unlines $ ["digraph {"] ++ links ++ ["}"]
+  where
+  (_, _, links) = d 0 1 stmt
+
+d :: Int -> Int -> Statement -> (Int, Int, [String])
+d src id a = case a of
+  Branch _ a b -> (id2, id2 + 1, link src id ++ a' ++ b' ++ link srcA id2 ++ link srcB id2)
+    where
+    (srcA, id1, a') = d id (id + 1)  a
+    (srcB, id2, b') = d id  id1      b
+  Sequence a b -> (srcB, id2, a' ++ b')
+    where
+    (srcA, id1, a') = d src id  a
+    (srcB, id2, b') = d srcA id1 b
+  Label  _ a -> d src id a
+  _ -> (src, id, [])
+  where
+  link :: Int -> Int -> [String]
+  link a b = ["  " ++ show a ++ " -> " ++ show b]
+
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -122,9 +122,11 @@
       put env { asserts = VarE b : asserts env }
       addTrace $ Assert' b
     | otherwise -> return ()
-  Assume a -> do
-    a <- evalExpr a
-    addCmd $ ASSERT (enabled :=> a)
+  Assume id a
+    | elem id lemmas -> do
+      a <- evalExpr a
+      addCmd $ ASSERT (enabled :=> a)
+    | otherwise -> return ()
   Branch a onTrue onFalse -> do
     a <- evalExpr a
     b <- newBoolVar
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.3.2
+version: 0.3.3
 
 category: Language, Formal Methods, Embedded
 
@@ -9,7 +9,7 @@
   ImProve is an imperative programming language for high assurance applications.
   ImProve uses infinite state, unbounded model checking to verify programs adhere
   to specifications.  Yices (required) is the backend SMT solver.
-  ImProve compiles to C and Simulink.
+  ImProve compiles to C, Simulink, and Modelica.
 
 author:     Tom Hawkins <tomahawkins@gmail.com>
 maintainer: Tom Hawkins <tomahawkins@gmail.com>
@@ -17,7 +17,7 @@
 license:      BSD3
 license-file: LICENSE
 
-homepage: http://tomahawkins.org
+homepage: http://github.com/tomahawkins/improve/wiki/ImProve
 
 build-type:    Simple
 cabal-version: >= 1.6
@@ -31,8 +31,13 @@
     exposed-modules:
         Language.ImProve
         Language.ImProve.Code
+        Language.ImProve.Code.C
+        Language.ImProve.Code.Common
+        Language.ImProve.Code.Modelica
+        Language.ImProve.Code.Simulink
         Language.ImProve.Core
         Language.ImProve.Examples
+        Language.ImProve.Path
         Language.ImProve.Tree
         Language.ImProve.Verify