diff --git a/Makefile b/Makefile
index d0b2ef7f..b4b2667e 100644
--- a/Makefile
+++ b/Makefile
@@ -43,7 +43,7 @@ postcondition_pass=$(wildcard tests/postconditions/pass/*.act) $(typing_pass)
 postcondition_fail=$(wildcard tests/postconditions/fail/*.act)
 
 # supposed to pass, but timeout
-hevm_buggy=tests/hevm/pass/transfer/transfer.act
+hevm_buggy=tests/hevm/pass/transfer/transfer.act tests/hevm/pass/multi3/multi3.act
 # supposed to pass
 hevm_pass=$(filter-out $(hevm_buggy), $(wildcard tests/hevm/pass/*/*.act))
 # supposed to fail
@@ -53,7 +53,7 @@ hevm_fail=$(wildcard tests/hevm/fail/*/*.act)
 failing_typing=tests/frontend/pass/array/array.act tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
 
 
-coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20 tests/coq/multi
+coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20 tests/coq/multi tests/coq/multi
 
 .PHONY: test-coq $(coq-examples)
 test-coq: compiler $(coq-examples)
@@ -104,11 +104,11 @@ tests/%.postcondition.fail:
 
 tests/hevm/pass/%.act.hevm.pass:
 	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
-	./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --contract $(CONTRACT)
+	./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol
 
 tests/hevm/fail/%.act.hevm.fail:
 	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/fail/$*.sol))
-	./bin/act hevm --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol --contract $(CONTRACT) && exit 1 || echo 0
+	./bin/act hevm --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol && exit 1 || echo 0
 
 test-ci: test-parse test-type test-invariant test-postcondition test-coq test-hevm
 test: test-ci test-cabal
diff --git a/src/CLI.hs b/src/CLI.hs
index b9c29702..e03a53df 100644
--- a/src/CLI.hs
+++ b/src/CLI.hs
@@ -19,6 +19,7 @@ import System.IO (hPutStrLn, stderr)
 import Data.Text (unpack)
 import Data.List
 import qualified Data.Map as Map
+import Data.Map (Map)
 import Data.Maybe
 import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
@@ -77,7 +78,6 @@ data Command w
                     , sol        :: w ::: Maybe String         <?> "Path to .sol"
                     , code       :: w ::: Maybe ByteString     <?> "Runtime code"
                     , initcode   :: w ::: Maybe ByteString     <?> "Initial code"
-                    , contract   :: w ::: String               <?> "Contract name"
                     , solver     :: w ::: Maybe Text           <?> "SMT solver: cvc5 (default) or z3"
                     , smttimeout :: w ::: Maybe Integer        <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
                     , debug      :: w ::: Bool                 <?> "Print verbose SMT output (default: False)"
@@ -109,9 +109,9 @@ main = do
       Coq f solver' smttimeout' debug' -> do
         solver'' <- parseSolver solver'
         coq' f solver'' smttimeout' debug'
-      HEVM spec' sol' code' initcode' contract' solver' smttimeout' debug' -> do
+      HEVM spec' sol' code' initcode' solver' smttimeout' debug' -> do
         solver'' <- parseSolver solver'
-        hevm spec' (Text.pack contract') sol' code' initcode' solver'' smttimeout' debug'
+        hevm spec' sol' code' initcode' solver'' smttimeout' debug'
 
 
 ---------------------------------
@@ -207,29 +207,32 @@ coq' f solver' smttimeout' debug' = do
     TIO.putStr $ coq claims
 
 
-hevm :: FilePath -> Text -> Maybe FilePath -> Maybe ByteString -> Maybe ByteString -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
-hevm actspec cid sol' code' initcode' solver' timeout debug' = do
-  let opts = if debug' then debugVeriOpts else defaultVeriOpts
-  (initcode'', bytecode) <- getBytecode
+hevm :: FilePath -> Maybe FilePath -> Maybe ByteString -> Maybe ByteString -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
+hevm actspec sol' code' initcode' solver' timeout debug' = do
   specContents <- readFile actspec
-  proceed specContents (enrich <$> compile specContents) $ \act -> do
-    checkCases act solver' timeout debug'
-    Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers -> do
-      -- Constructor check
-      checkConstructors solvers opts initcode'' bytecode act
-      -- Behavours check
-      checkBehaviours solvers opts bytecode act
-      -- ABI exhaustiveness sheck
-      checkAbi solvers opts act bytecode
+  proceed specContents (enrich <$> compile specContents) $ \ (Act store contracts) -> do
+    cmap <- createContractMap contracts
+    let opts = if debug' then debugVeriOpts else defaultVeriOpts
 
+    Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers ->
+      checkContracts solvers opts store cmap
   where
-    getBytecode :: IO (BS.ByteString, BS.ByteString)
-    getBytecode =
+
+    createContractMap :: [Contract] -> IO (Map Id (Contract, BS.ByteString, BS.ByteString))
+    createContractMap contracts = do
+      foldM (\cmap spec'@(Contract cnstr _) -> do
+                let cid =  _cname cnstr
+                (initcode'', runtimecode') <- getBytecode cid -- TODO do not reread the file each time
+                pure $ Map.insert cid (spec', initcode'', runtimecode') cmap
+            ) mempty contracts
+
+    getBytecode :: Id -> IO (BS.ByteString, BS.ByteString)
+    getBytecode cid =
       case (sol', code', initcode') of
         (Just f, Nothing, Nothing) -> do
           solContents  <- TIO.readFile f
-          bytecodes cid solContents
-        (Nothing, Just c, Just i) -> pure (i, c)
+          bytecodes (Text.pack cid) solContents
+        (Nothing, Just _, Just _) -> render (text "Only Solidity file supported") >> exitFailure -- pure (i, c)
         (Nothing, Nothing, _) -> render (text "No runtime code is given" <> line) >> exitFailure
         (Nothing, _, Nothing) -> render (text "No initial code is given" <> line) >> exitFailure
         (Just _, Just _, _) -> render (text "Both Solidity file and runtime code are given. Please specify only one." <> line) >> exitFailure
diff --git a/src/HEVM.hs b/src/HEVM.hs
index 11ec795d..6cfbf66b 100644
--- a/src/HEVM.hs
+++ b/src/HEVM.hs
@@ -11,10 +11,13 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE TypeApplications #-}
 
 
 module HEVM where
 
+import Prelude hiding (GT, LT)
+
 import qualified Data.Map as M
 import Data.List
 import Data.Containers.ListUtils (nubOrd)
@@ -30,6 +33,7 @@ import Data.DoubleWord
 import Data.Maybe
 import System.Exit ( exitFailure )
 import Control.Monad.ST (stToIO)
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
 
 import Syntax.Annotated
 import Syntax.Untyped (makeIface)
@@ -44,19 +48,25 @@ import EVM.Solvers
 import qualified EVM.Format as Format
 import qualified EVM.Fetch as Fetch
 
+
 type family ExprType a where
   ExprType 'AInteger  = EVM.EWord
   ExprType 'ABoolean  = EVM.EWord
   ExprType 'AByteStr  = EVM.Buf
   ExprType 'AContract = EVM.EWord -- address?
 
-type Layout = M.Map Id (M.Map Id (EVM.Expr EVM.EAddr, Integer))
+type Layout = M.Map Id (M.Map Id Integer)
 
 -- TODO move this to HEVM
 type Calldata = (EVM.Expr EVM.Buf, [EVM.Prop])
 
 type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract)
 
+-- | For each contract in the Act spec, put in a codemap its Act
+-- specification, init code, and runtimecode. This is being looked up
+-- when we encounter a constructor call.
+type CodeMap = M.Map Id (Contract, BS.ByteString, BS.ByteString)
+
 type EquivResult = ProofResult () (T.Text, SMTCex) ()
 
 abstRefineDefault :: EVM.AbstRefineConfig
@@ -70,7 +80,7 @@ initAddr = EVM.SymAddr "entrypoint"
 
 slotMap :: Store -> Layout
 slotMap store =
-  M.map (M.map (\(_, slot) -> (initAddr, slot))) store
+  M.map (M.map (\(_, slot) -> slot)) store
 
 -- Create a calldata that matches the interface of a certain behaviour
 -- or constructor. Use an abstract txdata buffer as the base.
@@ -114,19 +124,17 @@ combineFragments' fragments start base = go (EVM.Lit start) fragments (base, [])
 
 -- * Act translation
 
-translateActBehvs :: Act -> BS.ByteString -> [(Id, [EVM.Expr EVM.End], Calldata)]
-translateActBehvs (Act store contracts) bytecode =
-  let slots = slotMap store in
-  concatMap (\(Contract _ behvs) -> translateBehvs slots bytecode behvs) contracts
+translateActBehvs :: CodeMap -> Store -> [Behaviour] -> BS.ByteString -> [(Id, [EVM.Expr EVM.End], Calldata)]
+translateActBehvs codemap store behvs bytecode =
+  translateBehvs codemap (slotMap store) bytecode behvs
 
-translateActConstr :: Act -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata)
-translateActConstr (Act store [Contract ctor _]) bytecode = translateConstructor (slotMap store) ctor bytecode
-translateActConstr (Act _ _) _ = error "TODO multiple contracts"
+translateActConstr :: CodeMap -> Store -> Contract -> BS.ByteString -> ([EVM.Expr EVM.End], Calldata)
+translateActConstr codemap store (Contract ctor _) bytecode = translateConstructor codemap (slotMap store) ctor bytecode
 
-translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata)
-translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode =
-  (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)],
-  calldata)
+translateConstructor :: CodeMap -> Layout -> Constructor -> BS.ByteString -> ([EVM.Expr EVM.End], Calldata)
+translateConstructor codemap layout (Constructor cid iface preconds _ _ upds _) bytecode =
+  ([EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds) <> symAddrCnstr) mempty (EVM.ConcreteBuf bytecode) cmap],
+   calldata)
   where
     calldata = makeCtrCalldata iface
     initcontract = EVM.C { EVM.code  = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
@@ -135,11 +143,22 @@ translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode
                          , EVM.nonce = Just 1
                          }
     initmap = M.fromList [(initAddr, initcontract)]
+    symAddrCnstr = fmap (\i -> EVM.PNeg (EVM.PEq (EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show i))) (EVM.Lit 0))) [1..nonce-1]
+    (cmap, _) = updatesToExpr codemap layout cid initAddr upds (initmap, []) -- TODO remove caller preconditions from the return type if not needed
+
+    nonce :: Integer
+    nonce = case M.lookup initAddr cmap of
+                 Just (EVM.C _ _ _ n') -> case n' of
+                                            Just n -> fromIntegral n
+                                            Nothing -> error "Internal error: expecing nonce"
+                 Just (EVM.GVar _) -> error "Internal error: unexpected GVar"
+                 Nothing -> error "Internal error: init contract not found"
 
-translateBehvs :: Layout -> BS.ByteString -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)]
-translateBehvs layout bytecode behvs =
+
+translateBehvs :: CodeMap -> Layout -> BS.ByteString -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)]
+translateBehvs codemap layout bytecode behvs =
   let groups = (groupBy sameIface behvs) :: [[Behaviour]] in
-  fmap (\behvs' -> (behvName behvs', fmap (translateBehv layout bytecode) behvs', behvCalldata behvs')) groups
+  fmap (\behvs' -> (behvName behvs', fmap (translateBehv codemap layout bytecode) behvs', behvCalldata behvs')) groups
   where
 
     behvCalldata (Behaviour _ _ iface _ _ _ _ _:_) = makeCalldata iface
@@ -152,12 +171,12 @@ translateBehvs layout bytecode behvs =
     behvName (Behaviour _ _ (Interface name _) _ _ _ _ _:_) = name
     behvName [] = error "Internal error: behaviour groups cannot be empty"
 
-translateBehv :: Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End
-translateBehv layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) =
-  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds bytecode)
+translateBehv :: CodeMap -> Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End
+translateBehv codemap layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) =
+  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr codemap layout cid upds bytecode)
 
-rewritesToExpr :: Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap
-rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout cid) initmap rewrites
+rewritesToExpr :: CodeMap -> Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap
+rewritesToExpr codemap layout cid rewrites bytecode = foldl (flip $ rewriteToExpr codemap layout cid initAddr) initmap rewrites
   where
     initcontract = EVM.C { EVM.code  = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
                          , EVM.storage = EVM.AbstractStore initAddr
@@ -166,30 +185,137 @@ rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout
                          }
     initmap = M.fromList [(initAddr, initcontract)]
 
-rewriteToExpr :: Layout -> Id -> Rewrite -> ContractMap -> ContractMap
-rewriteToExpr _ _ (Constant _) cmap = cmap
-rewriteToExpr layout cid (Rewrite upd) cmap = updateToExpr layout cid upd cmap
+rewriteToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> Rewrite -> ContractMap -> ContractMap
+rewriteToExpr _ _ _ _ (Constant _) cmap = cmap
+rewriteToExpr codemap layout cid caddr (Rewrite upd) cmap = fst $ updateToExpr codemap layout cid caddr upd (cmap, [])
 
-updatesToExpr :: Layout -> Id -> [StorageUpdate] -> ContractMap -> ContractMap
-updatesToExpr layout cid upds initmap = foldl (flip $ updateToExpr layout cid) initmap upds
+updatesToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> [StorageUpdate] -> (ContractMap, [EVM.Prop]) -> (ContractMap, [EVM.Prop])
+updatesToExpr codemap layout cid caddr upds initmap = foldl (flip $ updateToExpr codemap layout cid caddr) initmap upds
 
-updateToExpr :: Layout -> Id -> StorageUpdate -> ContractMap -> ContractMap
-updateToExpr layout cid (Update typ i@(Item _ _ ref) e) cmap =
+updateToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> StorageUpdate -> (ContractMap, [EVM.Prop]) -> (ContractMap, [EVM.Prop])
+updateToExpr codemap layout cid caddr (Update typ i@(Item _ _ ref) e) (cmap, conds) =
   case typ of
-    SInteger -> M.insert addr (updateStorage (EVM.SStore offset e') contract) cmap
-    SBoolean -> M.insert addr (updateStorage (EVM.SStore offset e') contract) cmap
+    SInteger -> (M.insert caddr (updateStorage (EVM.SStore offset e') contract) cmap, conds)
+    SBoolean -> (M.insert caddr (updateStorage (EVM.SStore offset e') contract) cmap, conds)
     SByteStr -> error "Bytestrings not supported"
-    SContract -> error "Contracts not supported"
+    SContract -> let (cmap', preconds) = createContract codemap layout freshAddr cmap e in
+      (M.insert caddr (updateNonce (updateStorage (EVM.SStore offset (EVM.WAddr freshAddr)) contract)) cmap', conds <> preconds)
   where
-    (addr, slot) = getSlot layout cid (idFromItem i)
+    slot = getSlot layout cid (idFromItem i)
     offset = offsetFromRef layout slot ref
+
     e' = toExpr layout e
-    contract = fromMaybe (error "Internal error: contract not found") $ M.lookup addr cmap
+    contract = fromMaybe (error "Internal error: contract not found") $ M.lookup caddr cmap
 
     updateStorage :: (EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage) -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract
-    updateStorage upd c'@(EVM.C _ _ _ _) = c' { EVM.storage = upd c'.storage }
+    updateStorage updfun c'@(EVM.C _ _ _ _) = c' { EVM.storage = updfun c'.storage }
     updateStorage _ (EVM.GVar _) = error "Internal error: contract cannot be a global variable"
 
+    nonce :: Integer
+    nonce = case contract of
+      EVM.C _ _ _ (Just n) -> fromIntegral n
+      EVM.C _ _ _ _ -> error "Internal error: nonce must be a number"
+      EVM.GVar _ -> error "Internal error: contract cannot be a global variable"
+
+    freshAddr = EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show nonce)
+
+    updateNonce :: EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract
+    updateNonce c'@(EVM.C _ _ _ (Just n)) = c' { EVM.nonce = Just (n + 1) }
+    updateNonce (EVM.C _ _ _ Nothing) = error "Internal error: nonce must be a number"
+    updateNonce (EVM.GVar _) = error "Internal error: contract cannot be a global variable"
+
+createContract :: CodeMap -> Layout -> EVM.Expr EVM.EAddr -> ContractMap -> Exp AContract -> (ContractMap, [EVM.Prop])
+createContract codemap layout freshAddr cmap (Create _ cid args) =
+  case M.lookup cid codemap of
+    Just (Contract (Constructor _ iface preconds _ _ upds _) _, _, bytecode) ->
+      let contract = EVM.C { EVM.code  = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
+                           , EVM.storage = EVM.ConcreteStore mempty
+                           , EVM.balance = EVM.Lit 0
+                           , EVM.nonce = Just 1
+                           } in
+      let subst = makeSubstMap iface args in
+      let preconds' = fmap (toProp layout) $ fmap (substExp subst) preconds in
+      let upds' = substUpds subst upds in
+      -- trace "Before" $
+      -- traceShow preconds $
+      -- trace "After" $
+      -- traceShow (fmap (substExp subst) preconds) $
+      updatesToExpr codemap layout cid freshAddr upds' (M.insert freshAddr contract cmap, preconds')
+    Nothing -> error "Internal error: constructor not found"
+createContract _ _ _ _ _ = error "Internal error: constructor call expected"
+
+-- | Substitutions
+
+makeSubstMap :: Interface -> [TypedExp] -> M.Map Id TypedExp
+makeSubstMap (Interface _ decls) args =
+  M.fromList $ zipWith (\(Decl _ x) texp -> (x, texp)) decls args
+
+substUpds :: M.Map Id TypedExp -> [StorageUpdate] -> [StorageUpdate]
+substUpds subst upds = fmap (substUpd subst) upds
+
+substUpd :: M.Map Id TypedExp -> StorageUpdate -> StorageUpdate
+substUpd subst (Update s item expr) = Update s (substItem subst item) (substExp subst expr)
+
+substItem :: M.Map Id TypedExp -> TStorageItem a -> TStorageItem a
+substItem subst (Item st vt sref) = Item st vt (substStorageRef subst sref)
+
+substStorageRef :: M.Map Id TypedExp -> StorageRef -> StorageRef
+substStorageRef _ var@(SVar _ _ _) = var
+substStorageRef subst (SMapping pn sref args) = SMapping pn (substStorageRef subst sref) (substArgs subst args)
+substStorageRef subst (SField pn sref x y) = SField pn (substStorageRef subst sref) x y
+
+substArgs :: M.Map Id TypedExp -> [TypedExp] -> [TypedExp]
+substArgs subst exps = fmap (substTExp subst) exps
+
+substTExp :: M.Map Id TypedExp -> TypedExp -> TypedExp
+substTExp subst (TExp st expr) = TExp st (substExp subst expr)
+
+substExp :: M.Map Id TypedExp -> Exp a -> Exp a
+substExp subst expr = case expr of
+  And pn a b -> And pn (substExp subst a) (substExp subst b)
+  Or pn a b -> Or pn (substExp subst a) (substExp subst b)
+  Impl pn a b -> Impl pn (substExp subst a) (substExp subst b)
+  Neg pn a -> Neg pn (substExp subst a)
+  LT pn a b -> LT pn (substExp subst a) (substExp subst b)
+  LEQ pn a b -> LEQ pn (substExp subst a) (substExp subst b)
+  GEQ pn a b -> GEQ pn (substExp subst a) (substExp subst b)
+  GT pn a b -> GT pn (substExp subst a) (substExp subst b)
+  LitBool _ _ -> expr
+
+  Add pn a b -> Add pn (substExp subst a) (substExp subst b)
+  Sub pn a b -> Sub pn (substExp subst a) (substExp subst b)
+  Mul pn a b -> Mul pn (substExp subst a) (substExp subst b)
+  Div pn a b -> Div pn (substExp subst a) (substExp subst b)
+  Mod pn a b -> Mod pn (substExp subst a) (substExp subst b)
+  Exp pn a b -> Exp pn (substExp subst a) (substExp subst b)
+  LitInt _ _ -> expr
+  IntEnv _ _ -> expr
+
+  IntMin _ _ -> expr
+  IntMax _ _ -> expr
+  UIntMin _ _ -> expr
+  UIntMax _ _ -> expr
+  InRange pn t a -> InRange pn t (substExp subst a)
+
+  Cat pn a b -> Cat pn (substExp subst a) (substExp subst b)
+  Slice pn a b c -> Slice pn (substExp subst a) (substExp subst b) (substExp subst c)
+  ByStr _ _ -> expr
+  ByLit _ _ -> expr
+  ByEnv _ _ -> expr
+
+  Eq pn st a b -> Eq pn st (substExp subst a) (substExp subst b)
+  NEq pn st a b -> NEq pn st (substExp subst a) (substExp subst b)
+
+  ITE pn a b c -> ITE pn (substExp subst a) (substExp subst b) (substExp subst c)
+  TEntry _ _ _ -> expr
+  Var _ st _ x -> case M.lookup x subst of
+    Just (TExp st' exp') -> maybe (error "Internal error: type missmatch") (\Refl -> exp') $ testEquality st st'
+    Nothing -> expr
+
+  Create pn a b -> Create pn a (substArgs subst b)
+
+
+
 returnsToExpr :: Layout -> Maybe TypedExp -> EVM.Expr EVM.Buf
 returnsToExpr _ Nothing = EVM.ConcreteBuf ""
 returnsToExpr layout (Just r) = typedExpToBuf layout r
@@ -219,7 +345,7 @@ expToBuf layout styp e =
     SByteStr -> toExpr layout e
     SContract -> error "Internal error: expecting primitive type"
 
-getSlot :: Layout -> Id -> Id -> (EVM.Expr EVM.EAddr, Integer)
+getSlot :: Layout -> Id -> Id -> Integer
 getSlot layout cid name =
   case M.lookup cid layout of
     Just m -> case M.lookup name m of
@@ -227,15 +353,13 @@ getSlot layout cid name =
       Nothing -> error $ "Internal error: invalid variable name: " <> show name
     Nothing -> error "Internal error: invalid contract name"
 
-refOffset :: Layout -> StorageRef -> (EVM.Expr EVM.EAddr, EVM.Expr EVM.EWord)
+refOffset :: Layout -> StorageRef -> EVM.Expr EVM.EWord
 refOffset layout (SVar _ cid name) =
-  let (addr, slot) = getSlot layout cid name in
-  (addr, EVM.Lit $ fromIntegral slot)
+  let slot = getSlot layout cid name in
+  EVM.Lit $ fromIntegral slot
 refOffset layout (SMapping _ ref ixs) =
-  let (addr, slot) = refOffset layout ref in
-  (addr,
-   foldl (\slot' i -> EVM.keccak ((typedExpToBuf layout i) <> (wordToBuf slot'))) slot ixs)
-
+  let slot = refOffset layout ref in
+  foldl (\slot' i -> EVM.keccak ((typedExpToBuf layout i) <> (wordToBuf slot'))) slot ixs
 refOffset _ _ = error "TODO"
 
 ethEnvToWord :: EthEnv -> EVM.Expr EVM.EWord
@@ -243,7 +367,7 @@ ethEnvToWord Callvalue = EVM.TxValue
 ethEnvToWord Caller = EVM.WAddr $ EVM.SymAddr "caller"
 ethEnvToWord Origin = EVM.Origin
 ethEnvToWord Blocknumber = EVM.BlockNumber
-ethEnvToWord Blockhash = error "TODO" -- TODO argument of EVM.BlockHash ??
+ethEnvToWord Blockhash = EVM.BlockHash $ EVM.Lit 0
 ethEnvToWord Chainid = EVM.ChainId
 ethEnvToWord Gaslimit = EVM.GasLimit
 ethEnvToWord Coinbase = EVM.Coinbase
@@ -340,8 +464,9 @@ toExpr layout = \case
     fromCalldataFramgment $ symAbiArg (T.pack x) typ
 
   (TEntry _ _ (Item SInteger _ ref)) ->
-    let (addr, slot) = refOffset layout ref in
-    EVM.SLoad slot (EVM.AbstractStore addr)
+    let slot = refOffset layout ref in
+    EVM.SLoad slot (EVM.AbstractStore initAddr) -- TODO fix address
+
   e ->  error $ "TODO: " <> show e
 
   where
@@ -393,13 +518,16 @@ checkEquiv solvers opts l1 l2 =
     toEquivRes (Timeout b) = Timeout b
 
 
-checkConstructors :: SolverGroup -> VeriOpts -> ByteString -> ByteString -> Act -> IO ()
-checkConstructors solvers opts initcode runtimecode act = do
-  let (_, actbehvs, calldata) = translateActConstr act runtimecode
+checkConstructors :: SolverGroup -> VeriOpts -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> IO ()
+checkConstructors solvers opts initcode runtimecode store contract codemap = do
+  let (actbehvs, calldata) = translateActConstr codemap store contract runtimecode
   initVM <- stToIO $ abstractVM calldata initcode Nothing True
   expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr
   let simpl = if True then (simplify expr) else expr
+  -- traceM (T.unpack $ Format.formatExpr simpl)
   let solbehvs = removeFails $ flattenExpr simpl
+  -- mapM_ (traceM . T.unpack . Format.formatExpr) solbehvs
+  -- mapM_ (traceM . T.unpack . Format.formatExpr) actbehvs
   putStrLn "\x1b[1mChecking if constructor results are equivalent.\x1b[m"
   checkResult =<< checkEquiv solvers opts solbehvs actbehvs
   putStrLn "\x1b[1mChecking if constructor input spaces are the same.\x1b[m"
@@ -408,18 +536,18 @@ checkConstructors solvers opts initcode runtimecode act = do
     removeFails branches = filter isSuccess $ branches
 
 
-checkBehaviours :: SolverGroup -> VeriOpts -> ByteString -> Act -> IO ()
-checkBehaviours solvers opts bytecode act = do
-  let actbehvs = translateActBehvs act bytecode
-  flip mapM_ actbehvs $ \(name,behvs,calldata) -> do
+checkBehaviours :: SolverGroup -> VeriOpts -> ByteString -> Store -> Contract -> CodeMap -> IO ()
+checkBehaviours solvers opts bytecode store (Contract _ behvs) codemap = do
+  let actbehvs = translateActBehvs codemap store behvs bytecode
+  flip mapM_ actbehvs $ \(name,behvs',calldata) -> do
     solbehvs <- removeFails <$> getBranches solvers bytecode calldata
     putStrLn $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m"
     -- equivalence check
     putStrLn "\x1b[1mChecking if behaviour is matched by EVM\x1b[m"
-    checkResult =<< checkEquiv solvers opts solbehvs behvs
+    checkResult =<< checkEquiv solvers opts solbehvs behvs'
     -- input space exhaustiveness check
     putStrLn "\x1b[1mChecking if the input spaces are the same\x1b[m"
-    checkResult =<< checkInputSpaces solvers opts solbehvs behvs
+    checkResult =<< checkInputSpaces solvers opts solbehvs behvs'
     where
       removeFails branches = filter isSuccess $ branches
 
@@ -457,11 +585,11 @@ checkInputSpaces solvers opts l1 l2 = do
 
 -- | Checks whether all successful EVM behaviors are withing the
 -- interfaces specified by Act
-checkAbi :: SolverGroup -> VeriOpts -> Act -> BS.ByteString -> IO ()
-checkAbi solver opts act bytecode = do
+checkAbi :: SolverGroup -> VeriOpts -> Contract -> BS.ByteString -> IO ()
+checkAbi solver opts contract bytecode = do
   putStrLn "\x1b[1mChecking if the ABI of the contract matches the specification\x1b[m"
   let txdata = EVM.AbstractBuf "txdata"
-  let selectorProps = assertSelector txdata <$> nubOrd (actSigs act)
+  let selectorProps = assertSelector txdata <$> nubOrd (actSigs contract)
   evmBehvs <- getBranches solver bytecode (txdata, [])
   let queries =  fmap (assertProps abstRefineDefault) $ filter (/= []) $ fmap (checkBehv selectorProps) evmBehvs
 
@@ -474,9 +602,7 @@ checkAbi solver opts act bytecode = do
 
   where
     actSig (Behaviour _ _ iface _ _ _ _ _) = T.pack $ makeIface iface
-    actSigs (Act _ [(Contract _ behvs)]) = actSig <$> behvs
-    -- TODO multiple contracts
-    actSigs (Act _ _) = error "TODO multiple contracts"
+    actSigs (Contract _ behvs) = actSig <$> behvs
 
     checkBehv :: [EVM.Prop] -> EVM.Expr EVM.End -> [EVM.Prop]
     checkBehv assertions (EVM.Success cnstr _ _ _) = assertions <> cnstr
@@ -487,6 +613,20 @@ checkAbi solver opts act bytecode = do
 
     msg = "\x1b[1mThe following function selector results in behaviors not covered by the Act spec:\x1b[m"
 
+checkContracts :: SolverGroup -> VeriOpts -> Store -> M.Map Id (Contract, BS.ByteString, BS.ByteString) -> IO ()
+checkContracts solvers opts store codemap =
+  mapM_ (\(_, (contract, initcode, bytecode)) -> do
+            putStrLn $ "\x1b[1mChecking contract \x1b[4m" <> nameOfContract contract <> "\x1b[m"
+            -- Constructor check
+            checkConstructors solvers opts initcode bytecode store contract codemap
+            -- Behavours check
+            checkBehaviours solvers opts bytecode store contract codemap
+            -- ABI exhaustiveness sheck
+            checkAbi solvers opts contract bytecode
+        ) (M.toList codemap)
+
+
+
 -- | decompiles the given EVM bytecode into a list of Expr branches
 getBranches :: SolverGroup -> BS.ByteString -> Calldata -> IO [EVM.Expr EVM.End]
 getBranches solvers bs calldata = do
diff --git a/src/Syntax.hs b/src/Syntax.hs
index 46349683..36dbe906 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -54,6 +54,9 @@ locsFromInvariant (Invariant _ pre bounds (predpre, predpost)) =
 -- * Extract from any typed AST * --
 ------------------------------------
 
+nameOfContract :: Contract t -> Id
+nameOfContract (Contract (Constructor cname _ _ _ _ _ _) _) = cname
+
 behvsFromAct :: Agnostic.Act t -> [Behaviour t]
 behvsFromAct (Act _ contracts) = behvsFromContracts contracts
 
diff --git a/tests/frontend/pass/multi/multi.act b/tests/frontend/pass/multi/multi.act
index 9cf24004..9dfbfc4a 100644
--- a/tests/frontend/pass/multi/multi.act
+++ b/tests/frontend/pass/multi/multi.act
@@ -12,7 +12,7 @@ creates
    A a := create A()
 
 behaviour remote of B
-interface set_remote(uint z)
+interface remote(uint z)
 
 iff
    CALLVALUE == 0
@@ -21,7 +21,7 @@ storage
    a.x => z
 
 behaviour multi of B
-interface set_remote2(uint z)
+interface multi(uint z)
 
 iff
    CALLVALUE == 0
diff --git a/tests/frontend/pass/multi/multi.act.parsed.hs b/tests/frontend/pass/multi/multi.act.parsed.hs
index 1b4b372b..adb56d01 100644
--- a/tests/frontend/pass/multi/multi.act.parsed.hs
+++ b/tests/frontend/pass/multi/multi.act.parsed.hs
@@ -1 +1 @@
-Main [Contract (Definition (AlexPn 15 1 16) "A" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 58 5 9) uint256 "x") (IntLit (AlexPn 63 5 14) 0)]) [] []) [],Contract (Definition (AlexPn 81 7 16) "B" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 124 11 9) uint256 "y") (IntLit (AlexPn 129 11 14) 0),AssignVal (StorageVar (AlexPn 136 12 6) A "a") (ECreate (AlexPn 148 12 18) "A" [])]) [] []) [Transition (AlexPn 153 14 1) "remote" "B" set_remote(uint256 z) [Iff (AlexPn 205 17 1) [EEq (AlexPn 222 18 14) (EnvExp (AlexPn 212 18 4) Callvalue) (IntLit (AlexPn 225 18 17) 0)]] (Direct (Post [Rewrite (EField (AlexPn 240 21 5) (EVar (AlexPn 239 21 4) "a") "x") (EUTEntry (EVar (AlexPn 246 21 11) "z"))] Nothing)) [],Transition (AlexPn 249 23 1) "multi" "B" set_remote2(uint256 z) [Iff (AlexPn 301 26 1) [EEq (AlexPn 318 27 14) (EnvExp (AlexPn 308 27 4) Callvalue) (IntLit (AlexPn 321 27 17) 0)]] (Direct (Post [Rewrite (EVar (AlexPn 335 30 4) "y") (IntLit (AlexPn 340 30 9) 1),Rewrite (EField (AlexPn 346 31 5) (EVar (AlexPn 345 31 4) "a") "x") (EUTEntry (EVar (AlexPn 352 31 11) "z"))] Nothing)) []]]
+Main [Contract (Definition (AlexPn 15 1 16) "A" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 58 5 9) uint256 "x") (IntLit (AlexPn 63 5 14) 0)]) [] []) [],Contract (Definition (AlexPn 81 7 16) "B" constructor() [] (Creates [AssignVal (StorageVar (AlexPn 124 11 9) uint256 "y") (IntLit (AlexPn 129 11 14) 0),AssignVal (StorageVar (AlexPn 136 12 6) A "a") (ECreate (AlexPn 148 12 18) "A" [])]) [] []) [Transition (AlexPn 153 14 1) "remote" "B" remote(uint256 z) [Iff (AlexPn 201 17 1) [EEq (AlexPn 218 18 14) (EnvExp (AlexPn 208 18 4) Callvalue) (IntLit (AlexPn 221 18 17) 0)]] (Direct (Post [Rewrite (EField (AlexPn 236 21 5) (EVar (AlexPn 235 21 4) "a") "x") (EUTEntry (EVar (AlexPn 242 21 11) "z"))] Nothing)) [],Transition (AlexPn 245 23 1) "multi" "B" multi(uint256 z) [Iff (AlexPn 291 26 1) [EEq (AlexPn 308 27 14) (EnvExp (AlexPn 298 27 4) Callvalue) (IntLit (AlexPn 311 27 17) 0)]] (Direct (Post [Rewrite (EVar (AlexPn 325 30 4) "y") (IntLit (AlexPn 330 30 9) 1),Rewrite (EField (AlexPn 336 31 5) (EVar (AlexPn 335 31 4) "a") "x") (EUTEntry (EVar (AlexPn 342 31 11) "z"))] Nothing)) []]]
diff --git a/tests/frontend/pass/multi/multi.act.typed.json b/tests/frontend/pass/multi/multi.act.typed.json
index c8ceeaed..d7fd41d0 100644
--- a/tests/frontend/pass/multi/multi.act.typed.json
+++ b/tests/frontend/pass/multi/multi.act.typed.json
@@ -30,7 +30,7 @@
             "True"
           ],
           "contract": "B",
-          "interface": "set_remote(uint256 z)",
+          "interface": "remote(uint256 z)",
           "kind": "Behaviour",
           "name": "remote",
           "postConditions": [],
@@ -165,7 +165,7 @@
             "True"
           ],
           "contract": "B",
-          "interface": "set_remote2(uint256 z)",
+          "interface": "multi(uint256 z)",
           "kind": "Behaviour",
           "name": "multi",
           "postConditions": [],
diff --git a/tests/hevm/fail/redundant/redundant.act b/tests/hevm/fail/redundant/redundant.act
index 42bddf49..57158094 100644
--- a/tests/hevm/fail/redundant/redundant.act
+++ b/tests/hevm/fail/redundant/redundant.act
@@ -1,12 +1,12 @@
 constructor of A
 interface constructor()
 
-creates
-
 iff
 
   CALLVALUE == 0
 
+creates
+
   uint x := 0
 
 behaviour f of A
diff --git a/tests/hevm/pass/multi/multi.act b/tests/hevm/pass/multi/multi.act
new file mode 100644
index 00000000..d724eee0
--- /dev/null
+++ b/tests/hevm/pass/multi/multi.act
@@ -0,0 +1,47 @@
+constructor of A
+interface constructor()
+
+iff
+   CALLVALUE == 0
+
+creates
+   uint x := 0
+
+behaviour set_x of A
+interface set_x(uint z)
+
+iff
+   CALLVALUE == 0
+
+storage
+   x => z
+
+
+constructor of B
+interface constructor()
+
+iff
+   CALLVALUE == 0
+
+creates
+   uint y := 0
+   A a := create A()
+
+// behaviour remote of B
+// interface remote(uint z)
+
+// iff
+//    CALLVALUE == 0
+
+// storage
+//    a.x => z
+
+// behaviour multi of B
+// interface multi(uint z)
+
+// iff
+//    CALLVALUE == 0
+
+// storage
+//    y => 1
+//    a.x => z
diff --git a/tests/hevm/pass/multi/multi.sol b/tests/hevm/pass/multi/multi.sol
new file mode 100644
index 00000000..60c30309
--- /dev/null
+++ b/tests/hevm/pass/multi/multi.sol
@@ -0,0 +1,31 @@
+contract A {
+    uint x;
+
+    constructor ()  {
+	x = 0;
+    }
+
+    function set_x(uint z) public {
+	x = z;
+    }
+}
+
+contract B {
+
+    uint y;
+    A a;
+
+    constructor() {
+	y = 0;
+	a = new A();
+    }
+
+    /* function remote(uint z) public { */
+    /* 	a.set_x(z); */
+    /* } */
+
+    /* function multi(uint z) public { */
+    /* 	y = 1; */
+    /* 	a.set_x(z); */
+    /* } */
+}
diff --git a/tests/hevm/pass/multi2/multi2.act b/tests/hevm/pass/multi2/multi2.act
new file mode 100644
index 00000000..f58065ab
--- /dev/null
+++ b/tests/hevm/pass/multi2/multi2.act
@@ -0,0 +1,39 @@
+constructor of A
+interface constructor(uint z)
+
+iff
+   CALLVALUE == 0
+   inRange(uint256, z + 1)
+
+creates
+   uint x := z + 1
+
+
+behaviour x of A
+interface x()
+
+iff
+   CALLVALUE == 0
+
+returns
+   pre(x)
+
+behaviour set_x of A
+interface set_x(uint z)
+
+iff
+   CALLVALUE == 0
+
+storage
+  x => z
+
+constructor of B
+interface constructor(uint u)
+
+iff
+   CALLVALUE == 0
+   inRange(uint256, u + 1)
+
+creates
+   uint y := 0
+   A a := create A(u)
\ No newline at end of file
diff --git a/tests/hevm/pass/multi2/multi2.sol b/tests/hevm/pass/multi2/multi2.sol
new file mode 100644
index 00000000..a9679dfb
--- /dev/null
+++ b/tests/hevm/pass/multi2/multi2.sol
@@ -0,0 +1,32 @@
+contract A {
+    uint public x;
+
+    constructor (uint z)  {
+	x = z + 1;
+    }
+
+    function set_x(uint z) public {
+	x = z;
+    }
+}
+
+contract B {
+
+    uint y;
+    A a;
+
+    constructor(uint u) {
+	y = 0;
+	a = new A(u);
+    }
+
+    /* TODO */
+    /* function remote(uint z) public { */
+    /* 	a.set_x(z); */
+    /* } */
+
+    /* function multi(uint z) public { */
+    /* 	y = 1; */
+    /* 	a.set_x(z); */
+    /* } */
+}
diff --git a/tests/hevm/pass/multi3/multi3.act b/tests/hevm/pass/multi3/multi3.act
new file mode 100644
index 00000000..8963253f
--- /dev/null
+++ b/tests/hevm/pass/multi3/multi3.act
@@ -0,0 +1,47 @@
+// contract A
+
+constructor of A
+interface constructor(uint z)
+
+iff
+   CALLVALUE == 0
+   inRange(uint256, z + 1)
+
+creates
+   uint x := z + 1
+
+
+behaviour x of A
+interface x()
+
+iff
+   CALLVALUE == 0
+
+returns
+   pre(x)
+
+
+// contract B
+constructor of B
+interface constructor(uint i)
+iff
+   CALLVALUE == 0
+   inRange(uint256, i + 42)
+
+creates
+   uint z := i + 42
+
+
+// contract C
+constructor of C
+interface constructor(uint u)
+
+iff
+   CALLVALUE == 0
+   inRange(uint256, u + 1)
+   inRange(uint256, u + 42)
+
+creates
+   uint y := 0
+   A a := create A(u)
+   B b := create B(u)
\ No newline at end of file
diff --git a/tests/hevm/pass/multi3/multi3.sol b/tests/hevm/pass/multi3/multi3.sol
new file mode 100644
index 00000000..eebf41e9
--- /dev/null
+++ b/tests/hevm/pass/multi3/multi3.sol
@@ -0,0 +1,29 @@
+contract A {
+    uint public x;
+
+    constructor (uint z)  {
+	x = z + 1;
+    }
+}
+
+contract B {
+    uint z;
+
+    constructor (uint i)  {
+	z = i + 42;
+    }
+
+}
+
+contract C {
+
+    uint y;
+    A a;
+    B b;
+
+    constructor(uint u) {
+	y = 0;
+	a = new A(u);
+	b = new B(u);
+    }
+}