diff --git a/flake.lock b/flake.lock
index 20a0b889..a8799f14 100644
--- a/flake.lock
+++ b/flake.lock
@@ -22,11 +22,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1726560853,
-        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
         "type": "github"
       },
       "original": {
@@ -135,16 +135,15 @@
         "solidity": "solidity"
       },
       "locked": {
-        "lastModified": 1729608902,
-        "narHash": "sha256-6uTYwVYGGyVUdIcejP5shHdIzF/jp4XPz3kpDKN8FJ4=",
+        "lastModified": 1743503242,
+        "narHash": "sha256-z+WWoVaQSmTuNICUIADuS0Skv8yO1QoerA3CO9C7Vz8=",
         "owner": "ethereum",
         "repo": "hevm",
-        "rev": "56d106e529162eda66253d4203dd4a39429317de",
+        "rev": "1637d3b0c492c4cf61969133cb6e8d8a88d2ca97",
         "type": "github"
       },
       "original": {
         "owner": "ethereum",
-        "ref": "dynamic-flake-output",
         "repo": "hevm",
         "type": "github"
       }
@@ -165,11 +164,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1726481836,
-        "narHash": "sha256-MWTBH4dd5zIz2iatDb8IkqSjIeFum9jAqkFxgHLdzO4=",
+        "lastModified": 1742272065,
+        "narHash": "sha256-ud8vcSzJsZ/CK+r8/v0lyf4yUntVmDq6Z0A41ODfWbE=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "20f9370d5f588fb8c72e844c54511cab054b5f40",
+        "rev": "3549532663732bfd89993204d40543e9edaec4f2",
         "type": "github"
       },
       "original": {
@@ -286,4 +285,4 @@
   },
   "root": "root",
   "version": 7
-}
\ No newline at end of file
+}
diff --git a/flake.nix b/flake.nix
index 6adc8f7d..73f0db70 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
     hevm = {
-      url = "github:ethereum/hevm/dynamic-flake-output";
+      url = "github:ethereum/hevm";
       inputs.nixpkgs.follows = "nixpkgs";
     };
   };
@@ -42,6 +42,7 @@
             pkgs.z3
             pkgs.cvc5
             pkgs.coq
+            pkgs.coqPackages.stdlib
             pkgs.solc
             pkgs.mdbook
             pkgs.mdbook-mermaid
diff --git a/lib/ActLib.v b/lib/ActLib.v
index 64918b78..9c0d0bec 100644
--- a/lib/ActLib.v
+++ b/lib/ActLib.v
@@ -1,8 +1,7 @@
 (** library to be included with user coq developments *)
+From Stdlib Require Import ZArith.
 
-Require Import Coq.ZArith.ZArith.
-Open Scope Z_scope.
-
+Print LoadPath.
 (** * type definitions *)
 Definition address := Z.
 
@@ -24,13 +23,13 @@ Record Env : Set :=
 
 (** * integer bounds *)
 Definition UINT_MIN (n : Z) := 0.
-Definition UINT_MAX (n : Z) := 2^n - 1.
-Definition INT_MIN  (n : Z) := 0 - 2^(n - 1).
-Definition INT_MAX  (n : Z) := 2^(n - 1) - 1.
+Definition UINT_MAX (n : Z) := (2^n - 1)%Z.
+Definition INT_MIN  (n : Z) := (0 - 2^(n - 1))%Z.
+Definition INT_MAX  (n : Z) := (2^(n - 1) - 1)%Z.
 
 (** * notations *)
 Notation "a =?? b" := (bool_eq a b) (at level 70, no associativity).
-Definition range256 (n : Z) := 0 <= n <= UINT_MAX 256.
+Definition range256 (n : Z) := (0 <= n <= UINT_MAX 256)%Z.
 
 (** * lemmas *)
 
diff --git a/src/Act/Coq.hs b/src/Act/Coq.hs
index 608f0f51..50e5700c 100644
--- a/src/Act/Coq.hs
+++ b/src/Act/Coq.hs
@@ -167,7 +167,7 @@ baseRef :: Ref Storage -> StorageUpdate -> Bool
 baseRef baseref (Update _ (Item _ _ r) _) = hasBase r
   where
     hasBase (SVar _ _ _) = False
-    hasBase (SMapping _ r' _) = r' == baseref || hasBase r'
+    hasBase (SMapping _ r' _ _) = r' == baseref || hasBase r'
     hasBase (SField _ r' _ _) = r' == baseref || hasBase r'
 
 
@@ -357,7 +357,7 @@ entry (Item _ _ r) _ = ref r
 ref :: Ref k -> T.Text
 ref (SVar _ _ name) = parens $ T.pack name <> " " <> stateVar
 ref (CVar _ _ name) = T.pack name
-ref (SMapping _ r ixs) = parens $ ref r <> " " <> coqargs ixs
+ref (SMapping _ r _ ixs) = parens $ ref r <> " " <> coqargs ixs
 ref (SField _ r cid name) = parens $ T.pack cid <> "." <> T.pack name <> " " <> ref r
 
 -- | coq syntax for a list of arguments
diff --git a/src/Act/Decompile.hs b/src/Act/Decompile.hs
index 90839ab4..d07f7973 100644
--- a/src/Act/Decompile.hs
+++ b/src/Act/Decompile.hs
@@ -404,6 +404,13 @@ fromWord layout w = simplify <$> go w
         a' <- go a
         b' <- go b
         pure . evmbool $ InRange nowhere (AbiUIntType 256) (Mul nowhere a' b')
+    go (EVM.Or (EVM.Eq b (EVM.Div (EVM.Mod (EVM.Mul c d) (EVM.Lit MAX_UINT)) e)) (EVM.IsZero a))
+      | a == c
+      , a == e
+      , b == d = do
+        a' <- go a
+        b' <- go b
+        pure . evmbool $ InRange nowhere (AbiUIntType 256) (Mul nowhere a' b')
 
 
     -- SLT (max(a, length txdata) - 4) b == 0  if a - 4 = b
@@ -443,7 +450,6 @@ fromWord layout w = simplify <$> go w
 
     go e = err e
 
-
 -- Verification ------------------------------------------------------------------------------------
 
 
diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs
index 19c5229b..2b96d304 100644
--- a/src/Act/HEVM.hs
+++ b/src/Act/HEVM.hs
@@ -35,6 +35,7 @@ import Control.Monad.State
 import Data.List.NonEmpty qualified as NE
 import Data.Validation
 import Data.Typeable hiding (typeRep)
+import qualified Data.Vector as V
 
 import Act.HEVM_utils
 import Act.Syntax.Annotated as Act
@@ -47,7 +48,7 @@ import Act.Syntax.Timing
 import EVM.ABI (Sig(..))
 import qualified EVM hiding (bytecode)
 import qualified EVM.Types as EVM hiding (FrameState(..))
-import EVM.Expr hiding (op2, inRange)
+import EVM.Expr hiding (op2, inRange, div, xor, readStorage)
 import EVM.SymExec hiding (EquivResult, isPartial, reachable)
 import qualified EVM.SymExec as SymExec (EquivResult, ProofResult(..))
 import EVM.SMT (SMTCex(..), assertProps)
@@ -61,7 +62,9 @@ type family ExprType a where
   ExprType 'ABoolean  = EVM.EWord
   ExprType 'AByteStr  = EVM.Buf
 
-type Layout = M.Map Id (M.Map Id Integer)
+-- | The storage layout. Maps each contract type to a map that maps storage
+-- variables to their slot, offset, and size in bytes in memory
+type Layout = M.Map Id (M.Map Id (Int, Int,Int))
 
 type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract, Id)
 
@@ -77,7 +80,43 @@ initAddr = EVM.SymAddr "entrypoint"
 
 slotMap :: Store -> Layout
 slotMap store =
-  M.map (M.map snd) store
+  M.map (\cstore ->
+      let vars = sortOn (snd . snd) $ M.toList cstore in
+      M.fromList $ makeLayout vars 0 0
+  ) store
+
+makeLayout :: [(String,(SlotType, Integer))] -> Int -> Int -> [(Id, (Int,Int,Int))]
+makeLayout [] _ _ = []
+makeLayout ((name,(typ,_)):vars) offset slot =
+  if itFits then
+    (name, (slot, offset, size)):makeLayout vars (offset+size) slot
+  else
+    (name, (slot+1, 0, size)):makeLayout vars size (slot+1)
+  where
+    size = sizeOfSlotType typ
+    itFits = size <= 32 - offset
+
+-- size of a storage item in bytes
+sizeOfSlotType :: SlotType -> Int
+sizeOfSlotType (StorageMapping _ _) = 32
+sizeOfSlotType (StorageValue v) = sizeOfValue v
+
+sizeOfValue :: ValueType -> Int
+sizeOfValue (ContractType _) = 20
+sizeOfValue (PrimitiveType t) = sizeOfAbiType t
+
+sizeOfAbiType :: AbiType -> Int
+sizeOfAbiType (AbiUIntType s) = s `div` 8
+sizeOfAbiType (AbiIntType s) = s `div` 8
+sizeOfAbiType AbiAddressType = 20
+sizeOfAbiType AbiBoolType = 1
+sizeOfAbiType (AbiBytesType s) = s
+sizeOfAbiType AbiBytesDynamicType = 32
+sizeOfAbiType AbiStringType = 32
+sizeOfAbiType (AbiArrayDynamicType _) = 32
+sizeOfAbiType (AbiArrayType s t) = s * sizeOfAbiType t
+sizeOfAbiType (AbiTupleType v) = V.foldr ((+) . sizeOfAbiType) 0 v
+sizeOfAbiType AbiFunctionType = 0 --
 
 
 -- * Act state monad
@@ -145,9 +184,8 @@ translateConstructor bytecode (Constructor cid iface _ preconds _ _ upds) cmap =
   let initmap =  M.insert initAddr (initcontract, cid) cmap
   preconds' <- mapM (toProp initmap) preconds
   cmap' <- applyUpdates initmap initmap upds
-  fresh <- getFresh
   let acmap = abstractCmap initAddr cmap'
-  pure ([EVM.Success (snd calldata <> preconds' <> symAddrCnstr 1 fresh) mempty (EVM.ConcreteBuf bytecode) (M.map fst cmap')], calldata, ifaceToSig iface, acmap)
+  pure ([simplify $ EVM.Success (snd calldata <> preconds' <> symAddrCnstr acmap) mempty (EVM.ConcreteBuf bytecode) (M.map fst cmap')], calldata, ifaceToSig iface, acmap)
   where
     calldata = makeCtrCalldata iface
     initcontract = EVM.C { EVM.code    = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
@@ -157,15 +195,17 @@ translateConstructor bytecode (Constructor cid iface _ preconds _ _ upds) cmap =
                          , EVM.nonce   = Just 1
                          }
 
-symAddrCnstr :: Int -> Int -> [EVM.Prop]
-symAddrCnstr start end = fmap (\i -> EVM.PNeg (EVM.PEq (EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show i))) (EVM.Lit 0))) [start..end]
+symAddrCnstr :: ContractMap -> [EVM.Prop]
+symAddrCnstr cmap =
+    (\(a1, a2) -> EVM.PNeg (EVM.PEq (EVM.WAddr a1) (EVM.WAddr a2))) <$> comb (M.keys cmap)
 
 translateBehvs :: Monad m => ContractMap -> [Behaviour] -> ActT m [(Id, [(EVM.Expr EVM.End, ContractMap)], Calldata, Sig)]
 translateBehvs cmap behvs = do
   let groups = (groupBy sameIface behvs) :: [[Behaviour]]
   mapM (\behvs' -> do
-           exprs <- mapM (translateBehv cmap) behvs'
-           pure (behvName behvs', exprs, behvCalldata behvs', behvSig behvs)) groups
+           let calldata = behvCalldata behvs'
+           exprs <- mapM (translateBehv cmap (snd calldata)) behvs'
+           pure (behvName behvs', exprs, calldata, behvSig behvs)) groups
   where
     behvCalldata (Behaviour _ _ iface _ _ _ _ _ _:_) = makeCalldata iface
     behvCalldata [] = error "Internal error: behaviour groups cannot be empty"
@@ -185,17 +225,14 @@ ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args)
   where
     fromdecl (Decl t _) = t
 
-translateBehv :: Monad m => ContractMap -> Behaviour -> ActT m (EVM.Expr EVM.End, ContractMap)
-translateBehv cmap (Behaviour _ _ _ _ preconds caseconds _ upds ret) = do
-  fresh <- getFresh
+translateBehv :: Monad m => ContractMap -> [EVM.Prop] -> Behaviour -> ActT m (EVM.Expr EVM.End, ContractMap)
+translateBehv cmap cdataprops (Behaviour _ _ _ _ preconds caseconds _ upds ret)  = do
   preconds' <- mapM (toProp cmap) preconds
   caseconds' <- mapM (toProp cmap) caseconds
   ret' <- returnsToExpr cmap ret
   cmap' <- applyUpdates cmap cmap upds
-  fresh' <- getFresh
   let acmap = abstractCmap initAddr cmap'
-  pure (EVM.Success (preconds' <> caseconds' <> symAddrCnstr (fresh+1) fresh') mempty ret' (M.map fst cmap'), acmap)
-
+  pure (EVM.Success (preconds' <> caseconds' <> cdataprops <> symAddrCnstr cmap') mempty ret' (M.map fst cmap'), acmap)
 
 applyUpdates :: Monad m => ContractMap -> ContractMap -> [StorageUpdate] -> ActT m ContractMap
 applyUpdates readMap writeMap upds = foldM (applyUpdate readMap) writeMap upds
@@ -203,32 +240,52 @@ applyUpdates readMap writeMap upds = foldM (applyUpdate readMap) writeMap upds
 applyUpdate :: Monad m => ContractMap -> ContractMap -> StorageUpdate -> ActT m ContractMap
 applyUpdate readMap writeMap (Update typ (Item _ _ ref) e) = do
   caddr' <- baseAddr readMap ref
-  offset <- refOffset readMap ref
+  (addr, offset, size) <- refOffset readMap ref
   let (contract, cid) = fromMaybe (error $ "Internal error: contract not found\n" <> show e) $ M.lookup caddr' writeMap
   case typ of
-    SInteger -> case e of
-     Create _ _ _ -> do
-       fresh <- getFreshIncr
-       let freshAddr = EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show fresh)
-       writeMap' <- localCaddr freshAddr $ createContract readMap writeMap freshAddr e
-       pure $ M.insert caddr' (updateNonce (updateStorage (EVM.SStore offset (EVM.WAddr freshAddr)) contract), cid) writeMap'
-     _ -> do
-      e' <- toExpr readMap e
-      pure $ M.insert caddr' (updateStorage (EVM.SStore offset e') contract, cid) writeMap
-    SBoolean -> do
-      e' <- toExpr readMap e
-      pure $ M.insert caddr' (updateStorage (EVM.SStore offset e') contract, cid) writeMap
+    SInteger | isCreate e -> do
+        fresh <- getFreshIncr
+        let freshAddr = EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show fresh)
+        writeMap' <- localCaddr freshAddr $ createContract readMap writeMap freshAddr e
+        pure $ M.insert caddr' (updateNonce (updateStorage (EVM.SStore addr (EVM.WAddr freshAddr)) contract), cid) writeMap'
     SByteStr -> error "Bytestrings not supported"
+    SInteger -> do
+        e' <- toExpr readMap e
+        let prevValue = readStorage addr contract
+        let e'' = storedValue e' prevValue offset size
+        pure $ M.insert caddr' (updateStorage (EVM.SStore addr e'') contract, cid) writeMap
+    SBoolean -> do
+        e' <- toExpr readMap e
+
+        let prevValue = readStorage addr contract
+        let e'' = storedValue e' prevValue offset size
+        pure $ M.insert caddr' (updateStorage (EVM.SStore addr e'') contract, cid) writeMap
+-- TODO test with out of bounds assignments
   where
+    storedValue :: EVM.Expr EVM.EWord -> EVM.Expr EVM.EWord -> EVM.Expr EVM.EWord -> Int -> EVM.Expr EVM.EWord
+    storedValue new prev offset size =
+        let offsetBits = EVM.Mul (EVM.Lit 8) offset in
+        let maxVal = EVM.Lit $ (2 ^ (8 * size)) - 1 in
+        let mask = EVM.Xor (EVM.SHL offsetBits maxVal) (EVM.Lit MAX_UINT) in
+        let newShifted = EVM.SHL offsetBits new in
+        EVM.Or newShifted (EVM.And prev mask)
+
     updateStorage :: (EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage) -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract
     updateStorage updfun (EVM.C code storage tstorage bal nonce) = EVM.C code (updfun storage) tstorage bal nonce
     updateStorage _ (EVM.GVar _) = error "Internal error: contract cannot be a global variable"
 
+    readStorage :: EVM.Expr EVM.EWord -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EWord
+    readStorage addr (EVM.C _ storage _ _ _) = EVM.SLoad addr storage
+    readStorage _ (EVM.GVar _) = error "Internal error: contract cannot be a global variable"
+
     updateNonce :: EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract
     updateNonce (EVM.C code storage tstorage bal (Just n)) = EVM.C code storage tstorage bal (Just (n + 1))
     updateNonce c@(EVM.C _ _ _ _ Nothing) = c
     updateNonce (EVM.GVar _) = error "Internal error: contract cannot be a global variable"
 
+    isCreate (Create _ _ _) = True
+    isCreate _ = False
+
 createContract :: Monad m => ContractMap -> ContractMap -> EVM.Expr EVM.EAddr -> Exp AInteger -> ActT m ContractMap
 createContract readMap writeMap freshAddr (Create _ cid args) = do
   codemap <- getCodemap
@@ -246,6 +303,7 @@ createContract readMap writeMap freshAddr (Create _ cid args) = do
       applyUpdates (M.insert freshAddr (contract, cid) readMap) (M.insert freshAddr (contract, cid) writeMap) upds'
     Nothing -> error "Internal error: constructor not found"
 createContract _ _ _ _ = error "Internal error: constructor call expected"
+-- TODO needs to propagate up preconditions and check pointer constraints
 
 -- | Substitutions
 
@@ -262,7 +320,7 @@ substUpd subst (Update s item expr) = case substItem subst item of
   ETItem SCalldata _ -> error "Internal error: expecting storage item"
 
 -- | Existential packages to abstract away from reference kinds. Needed to
--- define subtitutions. 
+-- define subtitutions.
 -- Note: it would be nice to have these abstracted in one date type that
 -- abstracts the higher-kinded type, but Haskell does not allow partially
 -- applied type synonyms
@@ -279,8 +337,8 @@ substRef subst (CVar _ _ x) = case M.lookup x subst of
     Just (TExp _ (TEntry _ _ k (Item _ _ ref))) -> ERef k ref
     Just _ -> error "Internal error: cannot access fields of non-pointer var"
     Nothing -> error "Internal error: ill-formed substitution"
-substRef subst (SMapping pn sref args) = case substRef subst sref of
-  ERef k ref -> ERef k $ SMapping pn ref (substArgs subst args)
+substRef subst (SMapping pn sref ts args) = case substRef subst sref of
+  ERef k ref -> ERef k $ SMapping pn ref ts (substArgs subst args)
 substRef subst (SField pn sref x y) = case substRef subst sref of
   ERef k ref -> ERef k $ SField pn ref x y
 
@@ -352,6 +410,14 @@ typedExpToBuf cmap expr =
   case expr of
     TExp styp e -> expToBuf cmap styp e
 
+typedExpToWord :: Monad m => ContractMap -> TypedExp  -> ActT m (EVM.Expr EVM.EWord)
+typedExpToWord cmap te = do
+    case te of
+        TExp styp e -> case styp of
+            SInteger -> toExpr cmap e
+            SBoolean -> toExpr cmap e
+            SByteStr -> error "Bytestring in unexpected position"
+
 expToBuf :: Monad m => forall a. ContractMap -> SType a -> Exp a  -> ActT m (EVM.Expr EVM.Buf)
 expToBuf cmap styp e = do
   case styp of
@@ -360,42 +426,49 @@ expToBuf cmap styp e = do
       pure $ EVM.WriteWord (EVM.Lit 0) e' (EVM.ConcreteBuf "")
     SBoolean -> do
       e' <- toExpr cmap e
-      pure $ EVM.WriteWord (EVM.Lit 0) e' (EVM.ConcreteBuf "")
+      pure $ EVM.WriteWord (EVM.Lit 0) (EVM.IsZero $ EVM.IsZero e') (EVM.ConcreteBuf "")
     SByteStr -> toExpr cmap e
 
-getSlot :: Layout -> Id -> Id -> Integer
-getSlot layout cid name =
+-- | Get the slot and the offset of a storage variable in storage
+getPosition :: Layout -> Id -> Id -> (Int, Int, Int)
+getPosition layout cid name =
   case M.lookup cid layout of
     Just m -> case M.lookup name m of
-      Just v -> v
+      Just pos -> pos
       Nothing -> error $ "Internal error: invalid variable name: " <> show name
     Nothing -> error "Internal error: invalid contract name"
 
-refOffset :: Monad m => ContractMap -> Ref k -> ActT m (EVM.Expr EVM.EWord)
+-- | For the given storage reference, it returs the memory slot, the offset
+-- of the value within the slot, and the size of the value.
+refOffset :: Monad m => ContractMap -> Ref k -> ActT m (EVM.Expr EVM.EWord, EVM.Expr EVM.EWord, Int)
 refOffset _ (CVar _ _ _) = error "Internal error: ill-typed entry"
 refOffset _ (SVar _ cid name) = do
   layout <- getLayout
-  let slot = getSlot layout cid name
-  pure $ EVM.Lit (fromIntegral slot)
-refOffset cmap (SMapping _ ref ixs) = do
-  slot <- refOffset cmap ref
-  foldM (\slot' i -> do
+  let (slot, off, size) = getPosition layout cid name
+  pure (EVM.Lit (fromIntegral slot), EVM.Lit $ fromIntegral off, size)
+refOffset cmap (SMapping _ ref typ ixs) = do
+  (slot, _, _) <- refOffset cmap ref
+  addr <- foldM (\slot' i -> do
             buf <- typedExpToBuf cmap i
             pure (EVM.keccak (buf <> (wordToBuf slot')))) slot ixs
+  pure (addr, EVM.Lit 0, sizeOfValue typ)
 refOffset _ (SField _ _ cid name) = do
   layout <- getLayout
-  let slot = getSlot layout cid name
-  pure $ EVM.Lit (fromIntegral slot)
+  let (slot, off, size) = getPosition layout cid name
+  pure (EVM.Lit (fromIntegral slot), EVM.Lit $ fromIntegral off, size)
+
 
+-- | Get the address of the contract whoose storage contrains the given
+-- reference
 baseAddr :: Monad m => ContractMap -> Ref k -> ActT m (EVM.Expr EVM.EAddr)
 baseAddr _ (SVar _ _ _) = getCaddr
 baseAddr _ (CVar _ _ _) = error "Internal error: ill-typed entry"
 baseAddr cmap (SField _ ref _ _) = do
-  expr <- refToExp cmap ref 
+  expr <- refToExp cmap ref
   case simplify expr of
     EVM.WAddr symaddr -> pure symaddr
     e -> error $ "Internal error: did not find a symbolic address: " <> show e
-baseAddr cmap (SMapping _ ref _) = baseAddr cmap ref
+baseAddr cmap (SMapping _ ref _ _) = baseAddr cmap ref
 
 
 ethEnvToWord :: Monad m => EthEnv -> ActT m (EVM.Expr EVM.EWord)
@@ -445,7 +518,7 @@ toProp cmap = \case
     pure $ EVM.PNeg e
   (NEq _ _ _ _) -> error "unsupported"
   (ITE _ _ _ _) -> error "Internal error: expecting flat expression"
-  (TEntry _ _ _ _) -> error "TODO" -- EVM.SLoad addr idx
+  (TEntry _ _ _ (Item SBoolean _ ref)) -> EVM.PEq (EVM.Lit 0) <$> EVM.IsZero <$> refToExp cmap ref
   (InRange _ t e) -> toProp cmap (inRange t e)
   where
     op2 :: Monad m => forall a b. (EVM.Expr (ExprType b) -> EVM.Expr (ExprType b) -> a) -> Exp b -> Exp b -> ActT m a
@@ -482,7 +555,7 @@ toExpr cmap =  fmap stripMods . go
       (Impl _ e1 e2) -> op2 (EVM.Or . EVM.Not) e1 e2
       (Neg _ e1) -> do
         e1' <- toExpr cmap e1
-        pure $ EVM.Not e1'
+        pure $ EVM.IsZero e1' -- XXX why EVM.Not fails here?
       (Act.LT _ e1 e2) -> op2 EVM.LT e1 e2
       (LEQ _ e1 e2) -> op2 EVM.LEq e1 e2
       (GEQ _ e1 e2) -> op2 EVM.GEq e1 e2
@@ -528,6 +601,7 @@ toExpr cmap =  fmap stripMods . go
       (NEq _ _ _ _) -> error "unsupported"
 
       (TEntry _ _ _ (Item SInteger _ ref)) -> refToExp cmap ref
+      (TEntry _ _ _ (Item SBoolean _ ref)) -> refToExp cmap ref
 
       e@(ITE _ _ _ _) -> error $ "Internal error: expecting flat expression. got: " <> show e
 
@@ -540,6 +614,13 @@ toExpr cmap =  fmap stripMods . go
       pure $ op e1' e2'
 
 
+-- | Extract a value from a slot using its offset and size
+extractValue ::  EVM.Expr EVM.EWord -> EVM.Expr EVM.EWord -> Int -> EVM.Expr EVM.EWord
+extractValue slot offset size =
+    let mask = EVM.Lit $ 2 ^ (8 * size) - 1 in
+    let bits = EVM.Mul offset (EVM.Lit 8) in
+    EVM.And (EVM.SHR bits slot) mask
+
 
 refToExp :: forall m k. Monad m => ContractMap -> Ref k -> ActT m (EVM.Expr EVM.EWord)
 -- calldata variable
@@ -552,8 +633,9 @@ refToExp _ (CVar _ typ x) = pure $ fromCalldataFramgment $ symAbiArg (T.pack x)
 
 refToExp cmap r = do
   caddr <- baseAddr cmap r
-  slot <- refOffset cmap r
-  pure $ accessStorage cmap slot caddr
+  (slot, offset, size) <- refOffset cmap r
+  let word = accessStorage cmap slot caddr
+  pure $ extractValue word offset size
 
 accessStorage :: ContractMap -> EVM.Expr EVM.EWord -> EVM.Expr EVM.EAddr -> EVM.Expr EVM.EWord
 accessStorage cmap slot addr = case M.lookup addr cmap of
@@ -595,7 +677,7 @@ checkOp (Create _ _ _) = error "Internal error: invalid in range expression"
 -- | Wrapper for the equivalenceCheck function of hevm
 checkEquiv :: App m => SolverGroup -> [EVM.Expr EVM.End] -> [EVM.Expr EVM.End] -> m [EquivResult]
 checkEquiv solvers l1 l2 = do
-  res <- equivalenceCheck' solvers l1 l2
+  (res, _) <- equivalenceCheck' solvers l1 l2 False
   pure $ fmap toEquivRes res
   where
     toEquivRes :: SymExec.EquivResult -> EquivResult
@@ -640,9 +722,6 @@ getInitContractState solvers iface pointers preconds cmap = do
     getContractState [] = error "Internal error: Cast cannot be empty"
     getContractState _ = error "Error: Cannot have different casts to the same address"
 
-    comb :: [a] -> [(a,a)]
-    comb xs = [(x,y) | (x:ys) <- tails xs, y <- ys]
-
     checkAliasing :: App m => ContractMap -> [ContractMap] -> ActT m (Error String ())
     checkAliasing cmap' cmaps = do
       let allkeys = M.foldrWithKey (\k (_, cid) l -> (k, cid):l) [] <$> cmaps
@@ -677,6 +756,9 @@ getInitContractState solvers iface pointers preconds cmap = do
       let pairs = comb cmaps in
       assert (nowhere, "Names of symbolic adresses must be unique") (foldl (\b (c1, c2) -> S.disjoint (M.keysSet c1) (M.keysSet c2) && b) True pairs)
 
+comb :: Show a => [a] -> [(a,a)]
+comb xs = [(x,y) | (x:ys) <- tails xs, y <- ys]
+
 checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Contract -> ActT m (Error String ContractMap)
 checkConstructors solvers initcode runtimecode (Contract ctor@(Constructor _ iface pointers preconds _ _ _)  _) = do
   -- Construct the initial contract state
@@ -687,7 +769,7 @@ checkConstructors solvers initcode runtimecode (Contract ctor@(Constructor _ ifa
   (actbehvs, calldata, sig, cmap) <- translateConstructor runtimecode ctor actinitmap
   -- Symbolically execute bytecode
   -- TODO check if contrainsts about preexistsing fresh symbolic addresses are necessary
-  solbehvs <- lift $ removeFails <$> getInitcodeBranches solvers initcode hevminitmap calldata (symAddrCnstr 1 fresh) fresh
+  solbehvs <- lift $ removeFails <$> getInitcodeBranches solvers initcode hevminitmap calldata [] fresh
 
   -- Check equivalence
   lift $ showMsg "\x1b[1mChecking if constructor results are equivalent.\x1b[m"
@@ -708,6 +790,7 @@ checkBehaviours solvers (Contract _ behvs) actstorage = do
     let (behvs', fcmaps) = unzip actbehv
 
     solbehvs <- lift $ removeFails <$> getRuntimeBranches solvers hevmstorage calldata fresh
+
     lift $ showMsg $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m"
     -- equivalence check
     lift $ showMsg "\x1b[1mChecking if behaviour is matched by EVM\x1b[m"
@@ -806,13 +889,13 @@ pruneContractState entryaddr cmap =
 -- Perform a breadth first traversal and try to find a bijection between the addresses of the two stores
 -- Note that is problem is not as difficult as graph isomorphism since edges are labeld.
 -- Assumes that the stores are abstracted, pruned, and simplified.
--- All writes are to a unique concrete slot and the value is a simbolic address. 
+-- All writes are to a unique concrete slot and the value is a simbolic address.
 checkStoreIsomorphism :: ContractMap -> ContractMap -> Error String ()
 checkStoreIsomorphism cmap1 cmap2 = bfs [(idOfAddr initAddr, idOfAddr initAddr)] [] M.empty M.empty
   where
-    -- tries to find a bijective renaming between the addresses of the two maps  
+    -- tries to find a bijective renaming between the addresses of the two maps
     bfs :: [(T.Text, T.Text)]                         -- Queue of the addresses we are exploring (dequeue)
-        -> [(T.Text, T.Text)]                         -- Queue of the addresses we are exploring (enueue) 
+        -> [(T.Text, T.Text)]                         -- Queue of the addresses we are exploring (enueue)
         -> M.Map T.Text T.Text -> M.Map T.Text T.Text -- Two renamings keeping track of the address bijection
         -> Error String ()
     bfs [] [] _ _  = pure ()
@@ -866,10 +949,6 @@ checkInputSpaces :: App m => SolverGroup -> [EVM.Expr EVM.End] -> [EVM.Expr EVM.
 checkInputSpaces solvers l1 l2 = do
   let p1 = inputSpace l1
   let p2 = inputSpace l2
-  -- traceM "Solc props: "
-  -- traceM $ showProps p1
-  -- traceM "Act props: "
-  -- traceM $ showProps p2
 
   conf <- readConfig
 
diff --git a/src/Act/HEVM_utils.hs b/src/Act/HEVM_utils.hs
index 18715a9b..f1c188e0 100644
--- a/src/Act/HEVM_utils.hs
+++ b/src/Act/HEVM_utils.hs
@@ -49,12 +49,14 @@ defaultActConfig = Config
   , dumpExprs = False
   , dumpEndStates = False
   , debug = False
-  , abstRefineArith = False
-  , abstRefineMem   = False
   , dumpTrace = False
   , numCexFuzz = 0
   , onlyCexFuzz = False
   , decomposeStorage = False
+  , maxBranch = 100
+  , promiseNoReent = False
+  , maxBufSize = 64
+  , verb = 0
   }
 
 debugActConfig :: Config
@@ -67,12 +69,12 @@ makeCalldata iface@(Interface _ decls) =
     mkArg (Decl typ x) = symAbiArg (T.pack x) typ
     makeSig = T.pack $ makeIface iface
     calldatas = fmap mkArg decls
-    (cdBuf, _) = combineFragments calldatas (EVM.ConcreteBuf "")
+    (cdBuf, props) = combineFragments calldatas (EVM.ConcreteBuf "")
     withSelector = writeSelector cdBuf makeSig
     sizeConstraints
       = (bufLength withSelector EVM..>= cdLen calldatas)
         EVM..&& (bufLength withSelector EVM..< (EVM.Lit (2 ^ (64 :: Integer))))
-  in (withSelector, [sizeConstraints])
+  in (withSelector, sizeConstraints:props)
 
 makeCtrCalldata :: Interface -> Calldata
 makeCtrCalldata (Interface _ decls) =
diff --git a/src/Act/Parse.y b/src/Act/Parse.y
index 0b8d0853..d3a3f372 100644
--- a/src/Act/Parse.y
+++ b/src/Act/Parse.y
@@ -229,15 +229,15 @@ Decl : AbiType id                                     { Decl $1 (name $2) }
 StorageVar : SlotType id                              { StorageVar (posn $2) $1 (name $2) }
 
 AbiType : 'uint'
-         { case validsize $1 of
-	     True  -> AbiUIntType $1
-	     False -> error $ "invalid uint size: uint" <> (show $1)
-	 }
-       | 'int'
-         { case validsize $1 of
-	     True  -> AbiIntType $1
-	     False -> error $ "invalid int size: int" <> (show $1)
-	 }
+        { case validsize $1 of
+         True  -> AbiUIntType $1
+         False -> error $ "invalid uint size: uint" <> (show $1)
+        }
+        | 'int'
+        { case validsize $1 of
+            True  -> AbiIntType $1
+            False -> error $ "invalid int size: int" <> (show $1)
+        }
        | 'bytes'                                      { AbiBytesType $1 }
        | AbiType '[' ilit ']'                         { AbiArrayType (fromIntegral $ value $3) $1 }
        | 'address'                                    { AbiAddressType }
diff --git a/src/Act/Print.hs b/src/Act/Print.hs
index 61b42ecc..076a2ea7 100644
--- a/src/Act/Print.hs
+++ b/src/Act/Print.hs
@@ -156,7 +156,7 @@ prettyRef :: Ref k t -> String
 prettyRef = \case
   CVar _ _ n -> n
   SVar _ _ n -> n
-  SMapping _ r args -> prettyRef r <> concatMap (brackets . prettyTypedExp) args
+  SMapping _ r _ args -> prettyRef r <> concatMap (brackets . prettyTypedExp) args
   SField _ r _ n -> prettyRef r <> "." <> n
   where
     brackets str = "[" <> str <> "]"
@@ -199,7 +199,7 @@ prettyInvPred = prettyExp . untime . fst
     untimeRef:: Ref k t -> Ref k Untimed
     untimeRef (SVar p c a) = SVar p c a
     untimeRef (CVar p c a) = CVar p c a
-    untimeRef (SMapping p e xs) = SMapping p (untimeRef e) (fmap untimeTyped xs)
+    untimeRef (SMapping p e ts xs) = SMapping p (untimeRef e) ts (fmap untimeTyped xs)
     untimeRef (SField p e c x) = SField p (untimeRef e) c x
 
     untime :: Exp a t -> Exp a Untimed
diff --git a/src/Act/SMT.hs b/src/Act/SMT.hs
index 80d3566e..ad7cb55f 100644
--- a/src/Act/SMT.hs
+++ b/src/Act/SMT.hs
@@ -552,7 +552,7 @@ declareStorage :: [When] -> StorageLocation -> [SMT2]
 declareStorage times (Loc _ item@(Item _ _ ref)) = declareRef ref
   where
     declareRef (SVar _ _ _) = (\t -> constant (nameFromSItem t item) (itemType item) ) <$> times
-    declareRef (SMapping _ _ ixs) = (\t -> array (nameFromSItem t item) ixs (itemType item)) <$> times
+    declareRef (SMapping _ _ _ ixs) = (\t -> array (nameFromSItem t item) ixs (itemType item)) <$> times
     declareRef (SField _ ref' _ _) = declareRef ref'
 
 
@@ -693,7 +693,7 @@ nameFromSItem whn (Item _ _ ref) = nameFromSRef ref @@ show whn
 
 nameFromSRef :: Ref Storage -> Id
 nameFromSRef (SVar _ c name) = c @@ name
-nameFromSRef (SMapping _ e _) = nameFromSRef e
+nameFromSRef (SMapping _ e _ _) = nameFromSRef e
 nameFromSRef (SField _ ref c x) = nameFromSRef ref @@ c @@ x
 
 nameFromItem :: When -> TItem k a -> Ctx Id
@@ -706,7 +706,7 @@ nameFromItem whn (Item _ _ ref) = do
 nameFromRef :: Ref k -> Ctx Id
 nameFromRef (CVar _ _ name) = nameFromVarId name
 nameFromRef (SVar _ c name) = pure $ c @@ name
-nameFromRef (SMapping _ e _) = nameFromRef e
+nameFromRef (SMapping _ e _ _) = nameFromRef e
 nameFromRef (SField _ ref c x) = do 
   name <- nameFromRef ref
   pure $ name @@ c @@ x
diff --git a/src/Act/Syntax.hs b/src/Act/Syntax.hs
index b16a9320..5ae2b2ad 100644
--- a/src/Act/Syntax.hs
+++ b/src/Act/Syntax.hs
@@ -272,7 +272,7 @@ idFromItem (Item _ _ ref) = idFromRef ref
 idFromRef :: Ref k t -> Id
 idFromRef (SVar _ _ x) = x
 idFromRef (CVar _ _ x) = x
-idFromRef (SMapping _ e _) = idFromRef e
+idFromRef (SMapping _ e _ _) = idFromRef e
 idFromRef (SField _ e _ _) = idFromRef e
 
 idFromUpdate :: StorageUpdate t -> Id
@@ -287,7 +287,7 @@ ixsFromItem (Item _ _ item) = ixsFromRef item
 ixsFromRef :: Ref k t -> [TypedExp t]
 ixsFromRef (SVar _ _ _) = []
 ixsFromRef (CVar _ _ _) = []
-ixsFromRef (SMapping _ ref ixs) = ixs ++ ixsFromRef ref
+ixsFromRef (SMapping _ ref _ ixs) = ixs ++ ixsFromRef ref
 ixsFromRef (SField _ ref _ _) = ixsFromRef ref
 
 ixsFromLocation :: StorageLocation t -> [TypedExp t]
diff --git a/src/Act/Syntax/TimeAgnostic.hs b/src/Act/Syntax/TimeAgnostic.hs
index f443dba9..c069d20d 100644
--- a/src/Act/Syntax/TimeAgnostic.hs
+++ b/src/Act/Syntax/TimeAgnostic.hs
@@ -181,16 +181,16 @@ eqKind fa fb = maybe False (\Refl -> fa == fb) $ testEquality (sing @a) (sing @b
 data Ref (k :: RefKind) (t :: Timing) where
   CVar :: Pn -> AbiType -> Id -> Ref Calldata t     -- Calldata variable
   SVar :: Pn -> Id -> Id -> Ref Storage t           -- Storage variable. First Id is the contract the var belogs to
-  SMapping :: Pn -> Ref k t -> [TypedExp t] -> Ref k t
+  SMapping :: Pn -> Ref k t -> ValueType -> [TypedExp t] -> Ref k t
   SField :: Pn -> Ref k t -> Id -> Id -> Ref k t    -- first Id is the contract the field belogs to
 deriving instance Show (Ref k t)
 
 instance Eq (Ref k t) where
-  CVar _ at x      == CVar _ at' x'      = at == at' && x == x'
-  SVar _ c x       == SVar _ c' x'       = c == c' && x == x'
-  SMapping _ r ixs == SMapping _ r' ixs' = r == r' && ixs == ixs'
-  SField _ r c x   == SField _ r' c' x'  = r == r' && c == c' && x == x'
-  _                == _                  = False
+  CVar _ at x         == CVar _ at' x'          = at == at' && x == x'
+  SVar _ c x          == SVar _ c' x'           = c == c' && x == x'
+  SMapping _ r ts ixs == SMapping _ r' ts' ixs' = r == r' && ts == ts' && ixs == ixs'
+  SField _ r c x      == SField _ r' c' x'      = r == r' && c == c' && x == x'
+  _                   == _                      = False
 
 -- | Item is a reference together with its Act type. The type is
 -- parametrized on a timing `t`, a type `a`, and the reference kind
@@ -373,7 +373,7 @@ instance Timable (TItem a k) where
    setTime time (Item t vt ref) = Item t vt $ setTime time ref
 
 instance Timable (Ref k) where
-  setTime time (SMapping p e ixs) = SMapping p (setTime time e) (setTime time <$> ixs)
+  setTime time (SMapping p e ts ixs) = SMapping p (setTime time e) ts (setTime time <$> ixs)
   setTime time (SField p e c x) = SField p (setTime time e) c x
   setTime _ (SVar p c x) = SVar p c x
   setTime _ (CVar p c x) = CVar p c x
@@ -483,9 +483,9 @@ instance ToJSON (Ref k t) where
                                , "svar" .=  pack x
                                , "contract" .= pack c ]
   toJSON (CVar _ at x) = object [ "kind" .= pack "Var"
-                                  , "var" .=  pack x
-                                  , "abitype" .=  toJSON at ]                                  
-  toJSON (SMapping _ e xs) = mapping e xs
+                                , "var" .=  pack x
+                                , "abitype" .=  toJSON at ]                                  
+  toJSON (SMapping _ e _ xs) = mapping e xs
   toJSON (SField _ e c x) = field e c x
 
 
diff --git a/src/Act/Traversals.hs b/src/Act/Traversals.hs
index 420b47bf..58566e1b 100644
--- a/src/Act/Traversals.hs
+++ b/src/Act/Traversals.hs
@@ -155,10 +155,10 @@ mapRefM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> Ref k t -> m (Ref k
 mapRefM f = \case
   SVar p a b -> pure (SVar p a b)
   CVar p a b -> pure (CVar p a b)
-  SMapping p a b -> do
+  SMapping p a ts b -> do
     a' <- mapRefM f a
     b' <- mapM (mapTypedExpM f) b
-    pure $ SMapping p a' b'
+    pure $ SMapping p a' ts b'
   SField p r a b -> do
     r' <- mapRefM f r
     pure $ SField p r' a b
diff --git a/src/Act/Type.hs b/src/Act/Type.hs
index 93208055..6133935c 100644
--- a/src/Act/Type.hs
+++ b/src/Act/Type.hs
@@ -339,7 +339,7 @@ checkAssign _ _ = error "todo: support struct assignment in constructors"
 checkDefn :: Pn -> Env -> ValueType -> ValueType -> Id -> U.Defn -> Err StorageUpdate
 checkDefn pn env@Env{contract} keyType vt@(FromVType valType) name (U.Defn k val) =
   _Update
-  <$> (_Item vt . SMapping nowhere (SVar pn contract name) <$> checkIxs env (getPosn k) [k] [keyType])
+  <$> (_Item vt . SMapping nowhere (SVar pn contract name) vt <$> checkIxs env (getPosn k) [k] [keyType])
   <*> checkExpr env valType val
 
 -- | Typechecks a postcondition, returning typed versions of its storage updates and return expression.
@@ -371,7 +371,8 @@ checkEntry Env{contract,store,calldata, pointers} kind (U.EVar p name) = case (k
 checkEntry env kind (U.EMapping p e args) =
   checkEntry env kind e `bindValidation` \(typ, _, ref) -> case typ of
     StorageValue _ -> throw (p, "Expression should have a mapping type" <> show e)
-    StorageMapping argtyps restyp -> (StorageValue restyp, Nothing,) . SMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
+    StorageMapping argtyps restyp -> 
+        (StorageValue restyp, Nothing,) . SMapping p ref restyp <$> checkIxs env p args (NonEmpty.toList argtyps)
 checkEntry env@Env{theirs} kind (U.EField p e x) =
   checkEntry env kind e `bindValidation` \(_, oc, ref) -> case oc of
     Just c -> case Map.lookup c theirs of
diff --git a/tests/hevm/pass/amm/amm.act b/tests/hevm/pass/amm/amm.act
index 1af234c7..e7a880eb 100644
--- a/tests/hevm/pass/amm/amm.act
+++ b/tests/hevm/pass/amm/amm.act
@@ -41,17 +41,21 @@ case from == to:
 
 
 constructor of Amm
-interface constructor(uint256 amt1, uint256 amt2)
+interface constructor(address t0, address t1)
+
+pointers
+   t0 |-> Token
+   t1 |-> Token
 
 iff
 
     CALLVALUE == 0
-
+    t0 =/= t1
 
 creates
 
-    Token token0 := create Token(amt1)
-    Token token1 := create Token(amt2)
+    Token token0 := t0 
+    Token token1 := t1
 
 behaviour swap0 of Amm
 interface swap0(uint256 amt)
@@ -88,7 +92,6 @@ ensures
     post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS]) <= pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) + pre(token0.balanceOf[THIS]) + amt
 
 
-
 behaviour swap1 of Amm
 interface swap1(uint256 amt)
 
diff --git a/tests/hevm/pass/amm/amm.sol b/tests/hevm/pass/amm/amm.sol
index 9077840a..9e87dc06 100644
--- a/tests/hevm/pass/amm/amm.sol
+++ b/tests/hevm/pass/amm/amm.sol
@@ -9,7 +9,7 @@ contract Token {
 
 
     function transferFrom(uint256 value, address from, address to) public returns (uint) {
-	balanceOf[from] = balanceOf[from] - value;
+        balanceOf[from] = balanceOf[from] - value;
         balanceOf[to] = balanceOf[to] + value;
         return 1;
     }
@@ -22,29 +22,30 @@ contract Amm {
     Token token0;
     Token token1;
 
-    constructor(uint256 amt1, uint256 amt2) {
-        token0 = new Token(amt1);
-	token1 = new Token(amt2);
+    constructor(address t0, address t1) {
+        require (t0 != t1);
+        token0 = Token(t0);
+        token1 = Token(t1);
     }
 
     function swap0(uint256 amt) public returns (uint) {
-	uint256 reserve0 = token0.balanceOf(address(this));
-	uint256 reserve1 = token1.balanceOf(address(this));
+        uint256 reserve0 = token0.balanceOf(address(this));
+        uint256 reserve1 = token1.balanceOf(address(this));
 
-	token0.transferFrom(amt, msg.sender, address(this));
-	token1.transferFrom((reserve1*amt)/(reserve0+amt), address(this), msg.sender);
+        token0.transferFrom(amt, msg.sender, address(this));
+        token1.transferFrom((reserve1*amt)/(reserve0+amt), address(this), msg.sender);
 
-	return 1;
+        return 1;
     }
 
     function swap1(uint256 amt) public returns (uint) {
-	uint256 reserve0 = token0.balanceOf(address(this));
-	uint256 reserve1 = token1.balanceOf(address(this));
+        uint256 reserve0 = token0.balanceOf(address(this));
+        uint256 reserve1 = token1.balanceOf(address(this));
 
-	token1.transferFrom(amt, msg.sender, address(this));
-	token0.transferFrom((reserve0*amt)/(reserve1+amt), address(this), msg.sender);
+        token1.transferFrom(amt, msg.sender, address(this));
+        token0.transferFrom((reserve0*amt)/(reserve1+amt), address(this), msg.sender);
 
-	return 1;
+        return 1;
     }
 
 }
diff --git a/tests/hevm/pass/cast-3/cast-3.sol b/tests/hevm/pass/cast-3/cast-3.sol
index 5926bd39..cc49da8c 100644
--- a/tests/hevm/pass/cast-3/cast-3.sol
+++ b/tests/hevm/pass/cast-3/cast-3.sol
@@ -10,7 +10,7 @@ contract Token {
 
 
     function transfer(address to, uint256 value) public returns (uint) {
-	balanceOf[msg.sender] = balanceOf[msg.sender] - value;
+        balanceOf[msg.sender] = balanceOf[msg.sender] - value;
         balanceOf[to] = balanceOf[to] + value;
         return 1;
     }
@@ -31,6 +31,6 @@ contract TransferOneToken {
         // Transfer 1 token from the contract to the sender
         uint256 transferAmt = 1;
         token.transfer(msg.sender, transferAmt);
-	return 1;
+        return 1;
     }
 }
diff --git a/tests/hevm/pass/cast-4/cast-4.sol b/tests/hevm/pass/cast-4/cast-4.sol
index 545d788c..324aa44f 100644
--- a/tests/hevm/pass/cast-4/cast-4.sol
+++ b/tests/hevm/pass/cast-4/cast-4.sol
@@ -4,7 +4,7 @@ contract C {
     uint z;
 
     constructor(uint z1) {
-	z = z1;
+        z = z1;
     }
 
 }
@@ -15,8 +15,8 @@ contract A {
     C c;
     
     constructor(uint x1) {
-	x = x1;
-	c = new C(42);
+        x = x1;
+        c = new C(42);
     }
 }
 
@@ -26,13 +26,13 @@ contract B {
     A a2;
 
     constructor(address x, address y) {
-	require (x != y);
-	a1 = A(x);
-	a2 = A(y);
+        require (x != y);
+        a1 = A(x);
+        a2 = A(y);
     }
 
     function upd() public {
-	a1 = new A(42);
-	a2 = new A(43);
+        a1 = new A(42);
+        a2 = new A(43);
     }
 }
diff --git a/tests/hevm/pass/cast-5/cast-5.sol b/tests/hevm/pass/cast-5/cast-5.sol
index dce372bc..9ad61d5a 100644
--- a/tests/hevm/pass/cast-5/cast-5.sol
+++ b/tests/hevm/pass/cast-5/cast-5.sol
@@ -4,7 +4,7 @@ contract A {
     uint z;
 
     constructor(uint z1) {
-	z = z1;
+        z = z1;
     }
 
 }
@@ -13,7 +13,7 @@ contract B {
     uint t;
 
     constructor(uint t1) {
-	t = t1;
+        t = t1;
     }
 }
 
@@ -22,15 +22,15 @@ contract C {
     B b;
 
     constructor(address x, address y) {
-	a = A(x);
-	b = B(y);	
+        a = A(x);
+        b = B(y);
     }
 }
 
 contract D {
     C c2;
-    
+
     constructor(address x, address y) {
-	c2 = new C(x,y);	
+        c2 = new C(x,y);
     }
 }
diff --git a/tests/hevm/pass/cast-6/cast-6.sol b/tests/hevm/pass/cast-6/cast-6.sol
index 7f8ccb49..599d1183 100644
--- a/tests/hevm/pass/cast-6/cast-6.sol
+++ b/tests/hevm/pass/cast-6/cast-6.sol
@@ -4,7 +4,7 @@ contract C {
     uint z;
 
     constructor(uint z1) {
-	z = z1;
+        z = z1;
     }
 
 }
@@ -15,8 +15,8 @@ contract A {
     C public c;
     
     constructor(uint x1) {
-	x = x1;
-	c = new C(42);
+        x = x1;
+        c = new C(42);
     }
 }
 
@@ -26,7 +26,7 @@ contract B {
     C c;
 
     constructor(address x) {
-	a = A(x);
-	c = a.c();
+        a = A(x);
+        c = a.c();
     }
 }
diff --git a/tests/hevm/pass/cast/cast.sol b/tests/hevm/pass/cast/cast.sol
index bdd4f6c1..56c7ec75 100644
--- a/tests/hevm/pass/cast/cast.sol
+++ b/tests/hevm/pass/cast/cast.sol
@@ -4,16 +4,16 @@ contract A {
     uint x;
 
     constructor(uint _x) {
-	x = _x;
+        x = _x;
     }
 
 
     function getx() public returns (uint) {
-	return x;
+        return x;
     }
 
     function setx(uint _x1) public {
-	x = _x1;
+        x = _x1;
     }
 
 }
@@ -24,15 +24,15 @@ contract B {
     A a2;
 
     constructor(address x, address y) {
-	require(x!=y);
-	a1 = A(x);
-	a2 = A(y);
+        require(x!=y);
+        a1 = A(x);
+        a2 = A(y);
     }
 
 
     function upd() public {
-	a1.setx(42);
-	a2.setx(11);
+        a1.setx(42);
+        a2.setx(11);
     }
 
 }
diff --git a/tests/hevm/pass/layout1/layout1.act b/tests/hevm/pass/layout1/layout1.act
new file mode 100644
index 00000000..aed166a1
--- /dev/null
+++ b/tests/hevm/pass/layout1/layout1.act
@@ -0,0 +1,25 @@
+constructor of A
+interface constructor()
+
+iff
+
+  CALLVALUE == 0
+
+creates
+
+  uint128 x := 11
+  uint128 y := 42
+
+behaviour swap of A
+interface swap()
+
+iff
+
+  CALLVALUE == 0
+
+  storage
+
+    x => y
+    y => x
+
+  returns 1
\ No newline at end of file
diff --git a/tests/hevm/pass/layout1/layout1.sol b/tests/hevm/pass/layout1/layout1.sol
new file mode 100644
index 00000000..69ea8807
--- /dev/null
+++ b/tests/hevm/pass/layout1/layout1.sol
@@ -0,0 +1,19 @@
+contract A {
+    uint128 x;
+    uint128 y;
+    
+    constructor() {
+        x = 11;
+        y = 42;
+    }
+
+    function swap() external returns (uint) {
+
+        uint128 tmp = x;
+        
+        x = y;
+        y = tmp;
+
+        return 1;
+    }
+}
\ No newline at end of file
diff --git a/tests/hevm/pass/layout2/layout2.act b/tests/hevm/pass/layout2/layout2.act
new file mode 100644
index 00000000..59a8fcfc
--- /dev/null
+++ b/tests/hevm/pass/layout2/layout2.act
@@ -0,0 +1,73 @@
+constructor of A
+interface constructor()
+
+iff
+
+  CALLVALUE == 0
+
+creates
+
+  uint128 x := 11
+  bool flag := true
+  uint32 u := 17
+  uint8 z := 3
+  uint128 y := 42
+  uint256 i := 128
+
+behaviour foo of A
+interface foo()
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  x => y
+  y => x
+  z => 11
+  flag => not flag
+
+returns 1
+
+behaviour set_flag of A
+interface set_flag(bool b)
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  flag => b
+
+
+behaviour get_flag of A
+interface get_flag()
+
+iff
+
+  CALLVALUE == 0
+
+returns
+
+  pre(flag)
+
+
+behaviour set_y_if_flag of A
+interface set_y_if_flag(uint128 v)
+
+iff
+
+  CALLVALUE == 0
+
+case flag:
+
+storage
+  y => v
+
+returns 1
+
+case (not flag):
+returns 1
+
diff --git a/tests/hevm/pass/layout2/layout2.sol b/tests/hevm/pass/layout2/layout2.sol
new file mode 100644
index 00000000..b31a7ae2
--- /dev/null
+++ b/tests/hevm/pass/layout2/layout2.sol
@@ -0,0 +1,45 @@
+contract A {
+    uint128 x;
+    bool flag;
+    uint32 u;
+    uint8 z;
+    uint128 y;
+    uint256 i;
+
+    constructor() {
+        x = 11;
+        flag = true;
+        u = 17;
+        z = 3;
+        y = 42;
+        i = 128;
+    }
+
+    function foo() external returns (uint) {
+
+        uint128 tmp = x;
+
+        x = y;
+        y = tmp;
+        z = 11;
+        flag = !flag;
+
+        return 1;
+    }
+
+    function set_flag(bool b) external {
+        flag = b;
+    }
+
+    function get_flag() external returns (bool) {
+        return flag;
+    }
+
+    function set_y_if_flag(uint128 v) external returns (uint) {
+        if (flag) {
+            y = v;
+        }
+
+        return 1;
+    }
+}
\ No newline at end of file
diff --git a/tests/hevm/pass/layout3/layout3.act b/tests/hevm/pass/layout3/layout3.act
new file mode 100644
index 00000000..af26f4a3
--- /dev/null
+++ b/tests/hevm/pass/layout3/layout3.act
@@ -0,0 +1,42 @@
+constructor of Map
+interface constructor()
+
+iff
+
+  CALLVALUE == 0
+
+creates
+  uint128 val := 11
+  mapping(uint => uint128) f := [11 := 42]
+
+behaviour val of Map
+interface val()
+
+iff
+
+  CALLVALUE == 0
+
+returns pre(val)
+
+behaviour f of Map
+interface f(uint x)
+
+iff
+
+  CALLVALUE == 0
+
+returns pre(f[x])
+
+
+behaviour set of Map
+interface set(uint128 value, uint key)
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  f[key] => value
+
+returns 1
\ No newline at end of file
diff --git a/tests/hevm/pass/layout3/layout3.sol b/tests/hevm/pass/layout3/layout3.sol
new file mode 100644
index 00000000..af5ad422
--- /dev/null
+++ b/tests/hevm/pass/layout3/layout3.sol
@@ -0,0 +1,14 @@
+contract Map {
+    uint128 public val;
+    mapping (uint => uint128) public f;
+    
+    constructor() {
+        val = 11;
+        f[11] = 42;
+    }
+
+    function set(uint128 value, uint key) external returns (uint) {
+        f[key] = value;
+        return 1;
+    }
+}
\ No newline at end of file
diff --git a/tests/hevm/pass/layout4/layout4.act b/tests/hevm/pass/layout4/layout4.act
new file mode 100644
index 00000000..e6ba27ca
--- /dev/null
+++ b/tests/hevm/pass/layout4/layout4.act
@@ -0,0 +1,69 @@
+constructor of Map
+interface constructor()
+
+iff
+
+  CALLVALUE == 0
+
+creates
+  uint128 val := 11
+  mapping(uint => uint128) f := [11 := 42, 42 := 1]
+  mapping(uint128 => bool) g := [22 := true, 1 := false]
+  
+
+behaviour val of Map
+interface val()
+
+iff
+
+  CALLVALUE == 0
+
+returns pre(val)
+
+behaviour f of Map
+interface f(uint x)
+
+iff
+
+  CALLVALUE == 0
+
+returns pre(f[x])
+
+
+behaviour g of Map
+interface g(uint128 x)
+
+iff
+
+  CALLVALUE == 0
+
+returns pre(g[x])
+
+
+
+behaviour setf of Map
+interface setf(uint128 value, uint key)
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  f[key] => value
+
+returns 1
+
+
+behaviour setg of Map
+interface setg(bool value,  uint128 key)
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  g[key] => value
+
+returns 1
\ No newline at end of file
diff --git a/tests/hevm/pass/layout4/layout4.sol b/tests/hevm/pass/layout4/layout4.sol
new file mode 100644
index 00000000..eca793ce
--- /dev/null
+++ b/tests/hevm/pass/layout4/layout4.sol
@@ -0,0 +1,23 @@
+contract Map {
+    uint128 public val;
+    mapping (uint => uint128) public f;
+    mapping (uint128 => bool) public g;
+
+    constructor() {
+        val = 11;
+        f[11] = 42;
+        g[22] = true;
+        g[1] = false;
+        f[42] = 1;
+    }
+
+    function setf(uint128 value, uint key) external returns (uint) {
+        f[key] = value;
+        return 1;
+    }
+
+    function setg(bool value, uint128 key) external returns (uint) {
+        g[key] = value;
+        return 1;
+    }
+}
\ No newline at end of file
diff --git a/tests/hevm/pass/maps/maps.sol b/tests/hevm/pass/maps/maps.sol
index b2a95412..bc2e5349 100644
--- a/tests/hevm/pass/maps/maps.sol
+++ b/tests/hevm/pass/maps/maps.sol
@@ -5,14 +5,13 @@ contract Map {
     mapping (uint => uint) public f;
 
     constructor () {
-	val = 0;
+        val = 0;
         f[0] = 42;
     }
 
 
     function set(uint value, uint key) public returns (uint) {
-	f[key] = value;
-
-	return 1;
+        f[key] = value;
+        return 1;
     }
 }
diff --git a/tests/hevm/pass/transfer-simple/transfer-simple.sol b/tests/hevm/pass/transfer-simple/transfer-simple.sol
index cb1c62bb..7308945c 100644
--- a/tests/hevm/pass/transfer-simple/transfer-simple.sol
+++ b/tests/hevm/pass/transfer-simple/transfer-simple.sol
@@ -9,7 +9,7 @@ contract Token {
 
 
     function transfer(uint256 value, address to) public returns (uint) {
-	balanceOf[msg.sender] = balanceOf[msg.sender] - value;
+        balanceOf[msg.sender] = balanceOf[msg.sender] - value;
         balanceOf[to] = balanceOf[to] + value;
         return 1;
     }
diff --git a/tests/invariants/pass/mutex.act b/tests/invariants/pass/mutex.act
index 1ecf0d2c..d66bb215 100644
--- a/tests/invariants/pass/mutex.act
+++ b/tests/invariants/pass/mutex.act
@@ -8,15 +8,13 @@ creates
 
 invariants
 
-	// Ideally this would be `not lock`
-	lock => false
+	not lock
 
 behaviour f of Mutex
 interface setX(uint256 _x)
 
 iff
-	// Ideally this would be `not lock`
-	lock => false
+	not lock
 
 storage
 	x => _x
diff --git a/tests/postconditions/pass/amm.act b/tests/postconditions/pass/amm.act
index c8c88e15..1af234c7 100644
--- a/tests/postconditions/pass/amm.act
+++ b/tests/postconditions/pass/amm.act
@@ -85,6 +85,8 @@ returns 1
 ensures
 
     pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
+    post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS]) <= pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) + pre(token0.balanceOf[THIS]) + amt
+
 
 
 behaviour swap1 of Amm
@@ -118,4 +120,5 @@ returns 1
 
 ensures
 
-    pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
\ No newline at end of file
+    pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
+    post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS]) <= pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) + pre(token1.balanceOf[THIS]) + amt