diff --git a/Makefile b/Makefile
index cfb038e7..1a82888a 100644
--- a/Makefile
+++ b/Makefile
@@ -54,7 +54,8 @@ test-parse: parser compiler $(parser_pass:=.parse.pass) $(parser_fail:=.parse.fa
 test-type: parser compiler $(typing_pass:=.type.pass) $(typing_fail:=.type.fail)
 test-invariant: parser compiler $(invariant_pass:=.invariant.pass) $(invariant_fail:=.invariant.fail)
 test-hevm: parser compiler $(hevm_pass:=.hevm.pass) $(hevm_fail:=.hevm.fail)
-
+test-cabal: src/*.hs
+	cd src && cabal v2-run test
 
 # Just checks parsing
 tests/%.parse.pass:
@@ -91,4 +92,4 @@ tests/hevm/fail/%.act.hevm.fail:
 	./bin/act hevm --spec tests/hevm/fail/$*.act --soljson tests/hevm/fail/$*.sol.json && exit 1 || echo 0
 	rm tests/hevm/fail/$*.sol.json
 
-test: test-parse test-type test-invariant test-coq test-hevm
+test: test-parse test-type test-invariant test-coq test-hevm test-cabal
diff --git a/default.nix b/default.nix
index 05ca14e3..62af66d9 100644
--- a/default.nix
+++ b/default.nix
@@ -12,11 +12,11 @@ let
       hevm = dapptools.haskellPackages.hevm;
       sbv = dapptools.haskellPackages.sbv;
       act =
-        hself.callCabal2nixWithOptions
+        pkgs.haskell.lib.dontCheck (hself.callCabal2nixWithOptions
           "act"
           (gitignore ./src)
           "-fci"
-          {};
+          {});
     };
   };
 
@@ -27,6 +27,8 @@ let
     buildInputs = with pkgs.haskellPackages; [
       cabal-install
       pkgs.jq
+      pkgs.z3
+      pkgs.cvc4
       pkgs.coq_8_10
       dapptools.solc
     ];
diff --git a/src/Enrich.hs b/src/Enrich.hs
index 2b693957..b454219c 100644
--- a/src/Enrich.hs
+++ b/src/Enrich.hs
@@ -10,7 +10,7 @@ import EVM.ABI (AbiType(..))
 import EVM.Solidity (SlotType(..))
 
 import RefinedAst
-import Type (bound, defaultStore, metaType)
+import Type (bound, defaultStore)
 import Syntax (EthEnv(..), Id, Decl(..), Interface(..))
 import Extract
 
@@ -21,11 +21,11 @@ enrich claims = [S store]
                 <> (C <$> (enrichConstructor store <$> constructors))
                 <> (B <$> (enrichBehaviour store <$> behaviours))
   where
-    store = head $ [s | S s <- claims]
+    store = head [s | S s <- claims]
     behaviours = [b | B b <- claims]
     invariants = [i | I i <- claims]
     constructors = [c | C c <- claims]
-    definition (Invariant c _ _) = head $ filter (\b -> Pass == _cmode b && _cname b == c) [c' | C c' <- claims]
+    definition (Invariant c _ _ _) = head [c' | c' <- constructors, _cmode c' == Pass, _cname c' == c]
 
 -- |Adds type bounds for calldata , environment vars, and external storage vars as preconditions
 enrichConstructor :: Store -> Constructor -> Constructor
@@ -33,9 +33,9 @@ enrichConstructor store ctor@(Constructor _ _ (Interface _ decls) pre _ _ storag
   ctor { _cpreconditions = pre' }
     where
       pre' = pre
-             <> (mkCallDataBounds decls)
-             <> (mkStorageBounds store storageUpdates)
-             <> (mkEthEnvBounds $ ethEnvFromConstructor ctor)
+             <> mkCallDataBounds decls
+             <> mkStorageBounds store storageUpdates
+             <> mkEthEnvBounds (ethEnvFromConstructor ctor)
 
 -- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
 enrichBehaviour :: Store -> Behaviour -> Behaviour
@@ -43,19 +43,20 @@ enrichBehaviour store behv@(Behaviour _ _ _ (Interface _ decls) pre _ stateUpdat
   behv { _preconditions = pre' }
     where
       pre' = pre
-             <> (mkCallDataBounds decls)
-             <> (mkStorageBounds store stateUpdates)
-             <> (mkEthEnvBounds $ ethEnvFromBehaviour behv)
+             <> mkCallDataBounds decls
+             <> mkStorageBounds store stateUpdates
+             <> mkEthEnvBounds (ethEnvFromBehaviour behv)
 
--- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
+-- | Adds type bounds for calldata, environment vars, and storage vars
 enrichInvariant :: Store -> Constructor -> Invariant -> Invariant
-enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invariant _ conds predicate) =
-  inv { _ipreconditions = conds' }
+enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds predicate) =
+  inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
-      conds' = conds
-               <> (mkCallDataBounds decls)
-               <> (mkStorageBounds store (Left <$> locsFromExp predicate))
-               <> (mkEthEnvBounds $ ethEnvFromExp predicate)
+      preconds' = preconds
+                  <> mkCallDataBounds decls
+                  <> mkEthEnvBounds (ethEnvFromExp predicate)
+      storagebounds' = storagebounds
+                       <> mkStorageBounds store (Left <$> locsFromExp predicate)
 
 mkEthEnvBounds :: [EthEnv] -> [Exp Bool]
 mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
diff --git a/src/Extract.hs b/src/Extract.hs
index 3689eaf0..fcc41bb0 100644
--- a/src/Extract.hs
+++ b/src/Extract.hs
@@ -6,6 +6,7 @@ import qualified Data.List.NonEmpty as NonEmpty
 
 import RefinedAst
 import Syntax
+import EVM.ABI (AbiType(..))
 
 locsFromReturnExp :: ReturnExp -> [StorageLocation]
 locsFromReturnExp (ExpInt e) = locsFromExp e
@@ -43,10 +44,10 @@ locsFromExp e = case e of
   IntVar _  -> []
   LitBool _ -> []
   BoolVar _ -> []
-  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
+  NewAddr a b -> locsFromExp a <> locsFromExp b
   IntEnv _ -> []
   ByEnv _ -> []
-  ITE x y z -> (locsFromExp x) <> (locsFromExp y) <> (locsFromExp z)
+  ITE x y z -> locsFromExp x <> locsFromExp y <> locsFromExp z
   TEntry a -> case a of
     DirectInt contract name -> [IntLoc $ DirectInt contract name]
     DirectBool contract slot -> [BoolLoc $ DirectBool contract slot]
@@ -138,6 +139,19 @@ mkLoc (IntUpdate item _) = IntLoc item
 mkLoc (BoolUpdate item _) = BoolLoc item
 mkLoc (BytesUpdate item _) = BytesLoc item
 
+metaType :: AbiType -> MType
+metaType (AbiUIntType _)     = Integer
+metaType (AbiIntType  _)     = Integer
+metaType AbiAddressType      = Integer
+metaType AbiBoolType         = Boolean
+metaType (AbiBytesType _)    = ByteStr
+metaType AbiBytesDynamicType = ByteStr
+metaType AbiStringType       = ByteStr
+--metaType (AbiArrayDynamicType a) =
+--metaType (AbiArrayType        Int AbiType
+--metaType (AbiTupleType        (Vector AbiType)
+metaType _ = error "Extract.metaType: TODO"
+
 nameFromStorage :: Syntax.Storage -> Id
 nameFromStorage (Rewrite (Entry _ name _) _) = name
 nameFromStorage (Constant (Entry _ name _)) = name
diff --git a/src/HEVM.hs b/src/HEVM.hs
index c1f77a9f..ebbc2803 100644
--- a/src/HEVM.hs
+++ b/src/HEVM.hs
@@ -1,31 +1,37 @@
 {-# Language RecordWildCards #-}
 {-# Language TypeApplications #-}
 {-# Language OverloadedStrings #-}
+{-# Language ScopedTypeVariables #-}
 {-# Language DataKinds #-}
 {-# Language GADTs #-}
 
 module HEVM where
 
 import Prelude hiding (lookup)
-import Syntax
+import Syntax hiding (Post)
 import RefinedAst hiding (S)
 import Extract
 
+import Data.ByteString (ByteString)
+import Data.ByteString.UTF8 (toString)
 import Data.Text (Text, pack, splitOn)
 import Data.Maybe
 import Data.Either
 import Data.List hiding (lookup)
-import Data.Map hiding (drop, null, findIndex, splitAt, foldl, filter)
+import qualified Data.List.NonEmpty as NonEmpty (toList)
+import Data.Map hiding (drop, null, findIndex, splitAt, foldl, foldr, filter)
 import qualified Data.Map as Map
 import Control.Monad.State.Strict (execState)
 import Data.SBV.Control
 import Data.SBV
-import Control.Lens hiding (pre)
+import Data.SBV.String ((.++), subStr)
+import Control.Lens hiding (pre, (.>))
 import Control.Monad
 import qualified Data.Vector as Vec
+import Data.Type.Equality
+import Data.Typeable
 
-import Prove
-import Type
+import Print
 
 import EVM hiding (Query)
 import EVM.VMTest
@@ -283,3 +289,201 @@ keccak' (SymbolicBuffer bytes) = case maybeLitBytes bytes of
   Nothing -> symkeccak' bytes
   Just bs -> keccak' (ConcreteBuffer bs)
 keccak' (ConcreteBuffer bytes) = literal $ toSizzle $ wordValue $ keccakBlob bytes
+
+--- Symbolic Expression Generation ---
+
+data Ctx = Ctx ContractName Method Args HEVM.Storage HEVM.Env
+  deriving (Show)
+
+data SMType
+  = SymInteger (SBV Integer)
+  | SymBool (SBV Bool)
+  | SymBytes (SBV String)
+  deriving (Show)
+
+type ContractName = Id
+type Method = Id
+type Args = Map Id SMType
+type Storage = Map Id (SMType, SMType)
+type Env = Map Id SMType
+data When = Pre | Post
+
+symExp :: Ctx -> When -> ReturnExp -> SMType
+symExp ctx whn ret = case ret of
+  ExpInt e -> SymInteger $ symExpInt ctx whn e
+  ExpBool e -> SymBool $ symExpBool ctx whn e
+  ExpBytes e -> SymBytes $ symExpBytes ctx whn e
+
+symExpBool :: Ctx -> When -> Exp Bool -> SBV Bool
+symExpBool ctx@(Ctx c m args store _) w e = case e of
+  And a b   -> symExpBool ctx w a .&& symExpBool ctx w b
+  Or a b    -> symExpBool ctx w a .|| symExpBool ctx w b
+  Impl a b  -> symExpBool ctx w a .=> symExpBool ctx w b
+  LE a b    -> symExpInt ctx w a .< symExpInt ctx w b
+  LEQ a b   -> symExpInt ctx w a .<= symExpInt ctx w b
+  GE a b    -> symExpInt ctx w a .> symExpInt ctx w b
+  GEQ a b   -> symExpInt ctx w a .>= symExpInt ctx w b
+  NEq a b   -> sNot (symExpBool ctx w (Eq a b))
+  Neg a     -> sNot (symExpBool ctx w a)
+  LitBool a -> literal a
+  BoolVar a -> get (nameFromArg c m a) (catBools args)
+  TEntry a  -> get (nameFromItem m a) (catBools store')
+  ITE x y z -> ite (symExpBool ctx w x) (symExpBool ctx w y) (symExpBool ctx w z)
+  Eq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
+    Just Refl -> symExpInt ctx w a .== symExpInt ctx w b
+    Nothing -> case eqT @t @Bool of
+      Just Refl -> symExpBool ctx w a .== symExpBool ctx w b
+      Nothing -> case eqT @t @ByteString of
+        Just Refl -> symExpBytes ctx w a .== symExpBytes ctx w b
+        Nothing -> error "Internal Error: invalid expression type"
+ where store' = case w of
+         Pre -> fst <$> store
+         Post -> snd <$> store
+
+symExpInt :: Ctx -> When -> Exp Integer -> SBV Integer
+symExpInt ctx@(Ctx c m args store environment) w e = case e of
+  Add a b   -> symExpInt ctx w a + symExpInt ctx w b
+  Sub a b   -> symExpInt ctx w a - symExpInt ctx w b
+  Mul a b   -> symExpInt ctx w a * symExpInt ctx w b
+  Div a b   -> symExpInt ctx w a `sDiv` symExpInt ctx w b
+  Mod a b   -> symExpInt ctx w a `sMod` symExpInt ctx w b
+  Exp a b   -> symExpInt ctx w a .^ symExpInt ctx w b
+  LitInt a  -> literal a
+  IntMin a  -> literal $ intmin a
+  IntMax a  -> literal $ intmax a
+  UIntMin a -> literal $ uintmin a
+  UIntMax a -> literal $ uintmax a
+  IntVar a  -> get (nameFromArg c m a) (catInts args)
+  TEntry a  -> get (nameFromItem m a) (catInts store')
+  IntEnv a -> get (nameFromEnv c m a) (catInts environment)
+  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
+  ITE x y z -> ite (symExpBool ctx w x) (symExpInt ctx w y) (symExpInt ctx w z)
+ where store' = case w of
+         Pre -> fst <$> store
+         Post -> snd <$> store
+
+symExpBytes :: Ctx -> When -> Exp ByteString -> SBV String
+symExpBytes ctx@(Ctx c m args store environment) w e = case e of
+  Cat a b -> symExpBytes ctx w a .++ symExpBytes ctx w b
+  ByVar a  -> get (nameFromArg c m a) (catBytes args)
+  ByStr a -> literal a
+  ByLit a -> literal $ toString a
+  TEntry a  -> get (nameFromItem m a) (catBytes store')
+  Slice a x y -> subStr (symExpBytes ctx w a) (symExpInt ctx w x) (symExpInt ctx w y)
+  ByEnv a -> get (nameFromEnv c m a) (catBytes environment)
+  ITE x y z -> ite (symExpBool ctx w x) (symExpBytes ctx w y) (symExpBytes ctx w z)
+ where store' = case w of
+         Pre -> fst <$> store
+         Post -> snd <$> store
+
+
+-- *** SMT Variable Names *** --
+
+
+nameFromItem :: Method -> TStorageItem a -> Id
+nameFromItem method item = case item of
+  DirectInt c name -> c @@ method @@ name
+  DirectBool c name -> c @@ method @@ name
+  DirectBytes c name -> c @@ method @@ name
+  MappedInt c name ixs -> c @@ method @@ name >< showIxs c ixs
+  MappedBool c name ixs -> c @@ method @@ name >< showIxs c ixs
+  MappedBytes c name ixs -> c @@ method @@ name >< showIxs c ixs
+  where
+    x >< y = x <> "-" <> y
+    showIxs c ixs = intercalate "-" (NonEmpty.toList $ nameFromExp c method <$> ixs)
+
+nameFromExp :: ContractName -> Method -> ReturnExp -> Id
+nameFromExp c method e = case e of
+  ExpInt e' -> nameFromExpInt c method e'
+  ExpBool e' -> nameFromExpBool c method e'
+  ExpBytes e' -> nameFromExpBytes c method e'
+
+nameFromExpInt :: ContractName -> Method -> Exp Integer -> Id
+nameFromExpInt c m e = case e of
+  Add a b   -> nameFromExpInt c m a <> "+" <> nameFromExpInt c m b
+  Sub a b   -> nameFromExpInt c m a <> "-" <> nameFromExpInt c m b
+  Mul a b   -> nameFromExpInt c m a <> "*" <> nameFromExpInt c m b
+  Div a b   -> nameFromExpInt c m a <> "/" <> nameFromExpInt c m b
+  Mod a b   -> nameFromExpInt c m a <> "%" <> nameFromExpInt c m b
+  Exp a b   -> nameFromExpInt c m a <> "^" <> nameFromExpInt c m b
+  LitInt a  -> show a
+  IntMin a  -> show $ intmin a
+  IntMax a  -> show $ intmax a
+  UIntMin a -> show $ uintmin a
+  UIntMax a -> show $ uintmax a
+  IntVar a  -> a
+  TEntry a  -> nameFromItem m a
+  IntEnv a -> nameFromEnv c m a
+  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
+  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpInt c m y <> "-else-" <> nameFromExpInt c m z
+
+nameFromExpBool :: ContractName -> Method -> Exp Bool -> Id
+nameFromExpBool c m e = case e of
+  And a b   -> nameFromExpBool c m a <> "&&" <> nameFromExpBool c m b
+  Or a b    -> nameFromExpBool c m a <> "|" <> nameFromExpBool c m b
+  Impl a b  -> nameFromExpBool c m a <> "=>" <> nameFromExpBool c m b
+  LE a b    -> nameFromExpInt c m a <> "<" <> nameFromExpInt c m b
+  LEQ a b   -> nameFromExpInt c m a <> "<=" <> nameFromExpInt c m b
+  GE a b    -> nameFromExpInt c m a <> ">" <> nameFromExpInt c m b
+  GEQ a b   -> nameFromExpInt c m a <> ">=" <> nameFromExpInt c m b
+  Neg a     -> "~" <> nameFromExpBool c m a
+  LitBool a -> show a
+  BoolVar a -> nameFromArg c m a
+  TEntry a  -> nameFromItem m a
+  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpBool c m y <> "-else-" <> nameFromExpBool c m z
+  Eq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
+    Just Refl -> nameFromExpInt c m a <> "==" <> nameFromExpInt c m b
+    Nothing -> case eqT @t @Bool of
+      Just Refl -> nameFromExpBool c m a <> "==" <> nameFromExpBool c m b
+      Nothing -> case eqT @t @ByteString of
+        Just Refl -> nameFromExpBytes c m a <> "==" <> nameFromExpBytes c m b
+        Nothing -> error "Internal Error: invalid expression type"
+  NEq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
+    Just Refl -> nameFromExpInt c m a <> "=/=" <> nameFromExpInt c m b
+    Nothing -> case eqT @t @Bool of
+      Just Refl -> nameFromExpBool c m a <> "=/=" <> nameFromExpBool c m b
+      Nothing -> case eqT @t @ByteString of
+        Just Refl -> nameFromExpBytes c m a <> "=/=" <> nameFromExpBytes c m b
+        Nothing -> error "Internal Error: invalid expression type"
+
+nameFromExpBytes :: ContractName -> Method -> Exp ByteString -> Id
+nameFromExpBytes c m e = case e of
+  Cat a b -> nameFromExpBytes c m a <> "++" <> nameFromExpBytes c m b
+  ByVar a  -> nameFromArg c m a
+  ByStr a -> show a
+  ByLit a -> show a
+  TEntry a  -> nameFromItem m a
+  Slice a x y -> nameFromExpBytes c m a <> "[" <> show x <> ":" <> show y <> "]"
+  ByEnv a -> nameFromEnv c m a
+  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpBytes c m y <> "-else-" <> nameFromExpBytes c m z
+
+nameFromDecl :: ContractName -> Method -> Decl -> Id
+nameFromDecl c m (Decl _ name) = nameFromArg c m name
+
+nameFromArg :: ContractName -> Method -> Id -> Id
+nameFromArg c method name = c @@ method @@ name
+
+nameFromEnv :: ContractName -> Method -> EthEnv -> Id
+nameFromEnv c method e = c @@ method @@ (prettyEnv e)
+
+(@@) :: Id -> Id -> Id
+x @@ y = x <> "_" <> y
+
+
+-- *** Utils *** --
+
+
+get :: (Show a, Ord a, Show b) => a -> Map a b -> b
+get name vars = fromMaybe (error (show name <> " not found in " <> show vars)) $ Map.lookup name vars
+
+catInts :: Map Id SMType -> Map Id (SBV Integer)
+catInts m = Map.fromList [(name, i) | (name, SymInteger i) <- Map.toList m]
+
+catBools :: Map Id SMType -> Map Id (SBV Bool)
+catBools m = Map.fromList [(name, i) | (name, SymBool i) <- Map.toList m]
+
+catBytes :: Map Id SMType -> Map Id (SBV String)
+catBytes m = Map.fromList [(name, i) | (name, SymBytes i) <- Map.toList m]
+
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM f xs = liftM concat (mapM f xs)
diff --git a/src/Main.hs b/src/Main.hs
index 243ced19..f4d8aa96 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -17,7 +17,6 @@ import System.IO (hPutStrLn, stderr)
 import Data.SBV hiding (preprocess)
 import Data.Text (pack, unpack)
 import Data.Maybe
-import Data.List
 import qualified EVM.Solidity as Solidity
 import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
@@ -35,9 +34,9 @@ import Parse
 import RefinedAst
 import Enrich
 import K hiding (normalize)
+import SMT
 import Syntax
 import Type
-import Prove
 import Coq
 import HEVM
 import Print
@@ -96,34 +95,35 @@ main = do
                        Bad e -> prettyErr contents e
 
       (Prove file' solver' smttimeout' debug') -> do
+        let
+          parseSolver s = case s of
+            Just "z3" -> SMT.Z3
+            Just "cvc4" -> SMT.CVC4
+            Nothing -> SMT.Z3
+            Just _ -> error "unrecognized solver"
+          config = SMT.SMTConfig (parseSolver solver') (fromMaybe 20000 smttimeout') debug'
         contents <- readFile file'
         proceed contents (compile contents) $ \claims -> do
-            let
-                handleResults ((Invariant c _ e), rs) = do
-                  let msg = "\n============\n\nInvariant " <> show (prettyExp e) <> " of " <> show c <> ": "
-                      sep = "\n\n---\n\n"
-                      results' = handleRes <$> rs
-                      ok = not $ or $ fst <$> results'
-                  if ok
-                  then putStrLn $ msg <> "Q.E.D."
-                  else do
-                      putStrLn $ msg <> "\n\n" <> intercalate sep (snd <$> results')
-                      exitFailure
-
-                handleRes (SatResult res) = case res of
-                  Unsatisfiable _ _ -> (False, "")
-                  Satisfiable _ model -> (True, "Counter example found!\n\n" <> show model)
-                  Unknown _ reason -> (True, "Unknown! " <> show reason)
-                  ProofError _ reasons _  -> (True, "Proof error! " <> show reasons)
-                  SatExtField _ _ -> error "Extension field containing Infinite/epsilon"
-                  DeltaSat {} -> error "Unexpected DeltaSat"
-
-            results <- forM (queries claims)
-                          (\(i, qs) -> do
-                            rs <- mapM (satWithTimeOut solver' smttimeout' debug') qs
-                            pure (i, rs)
-                          )
-            mapM_ handleResults results
+          let
+            handleRes (query, res) = case res of
+                  Unsat -> (True, typ <> " " <> prettyExp target <> " holds :)", show $ getSMT query)
+                  Sat -> (False, typ <> " " <> prettyExp target <> " does not hold :(", show $ getSMT query)
+                  SMT.Unknown -> (False, typ <> " " <> prettyExp target <> " could not be proved due to a solver timeout :(", show $ getSMT query)
+                  SMT.Error _ str -> (False, typ <> " " <> prettyExp target <> " could not be proved to due a solver error: " <> str, show $ getSMT query)
+              where
+                target = getTarget query
+                typ = case query of
+                  Postcondition {} -> "postcondition"
+                  Inv {} -> "invariant"
+
+          pcResults <- mapM (runQuery config) (concatMap mkPostconditionQueries claims)
+          invResults <- mapM (runQuery config) (mkInvariantQueries claims)
+          let results = map handleRes (pcResults <> invResults)
+          allGood <- foldM (\acc (r, msg, smt) -> do
+            if (_debug config) then putStrLn (msg <> "\n\n" <> smt) else putStrLn msg
+            pure $ if acc == False then False else r
+            ) True results
+          unless allGood exitFailure
 
       (Coq f) -> do
         contents <- readFile f
@@ -168,20 +168,6 @@ main = do
                  return False
           unless (and passes) exitFailure
 
--- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)`
-satWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic () -> IO SatResult
-satWithTimeOut solver' maybeTimeout debug' sym = case solver' of
-  Just "cvc4" -> do
-    setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --interactive --incremental --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)
-    res <- satWith cvc4{verbose=debug'} sym
-    setEnv "SBV_CVC4_OPTIONS" ""
-    return res
-  Just "z3" -> runwithz3
-  Nothing -> runwithz3
-  _ -> error "Unknown solver. Currently supported solvers; z3, cvc4"
-  where timeout = fromMaybe 20000 maybeTimeout
-        runwithz3 = satWith z3{verbose=debug'} $ (setTimeOut timeout) >> sym
-
 -- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)`
 runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic a -> IO a
 runSMTWithTimeOut solver' maybeTimeout debug' sym
@@ -191,7 +177,7 @@ runSMTWithTimeOut solver' maybeTimeout debug' sym
       setEnv "SBV_CVC4_OPTIONS" ""
       return res
   | solver' == Just "z3" = runwithz3
-  | solver' == Nothing = runwithz3
+  | isNothing solver' = runwithz3
   | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"
  where timeout = fromMaybe 20000 maybeTimeout
        runwithz3 = runSMTWith z3{verbose=debug'} $ (setTimeOut timeout) >> sym
diff --git a/src/Print.hs b/src/Print.hs
index 159132fa..1410ec29 100644
--- a/src/Print.hs
+++ b/src/Print.hs
@@ -1,6 +1,6 @@
 {-# Language GADTs #-}
 
-module Print (prettyEnv, prettyExp, prettyType, prettyBehaviour) where
+module Print (prettyEnv, prettyExp, prettyType, prettyBehaviour, prettyItem) where
 
 import Data.ByteString.UTF8 (toString)
 
diff --git a/src/Prove.hs b/src/Prove.hs
deleted file mode 100644
index ddd5c22c..00000000
--- a/src/Prove.hs
+++ /dev/null
@@ -1,447 +0,0 @@
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# Language ScopedTypeVariables #-}
-{-# Language TypeFamilies #-}
-{-# Language TypeApplications #-}
-
-module Prove
-  ( queries
-  , Ctx(..)
-  , When(..)
-  , SMType(..)
-  , Method
-  , getLoc
-  , get
-  , mkContext
-  , mkConstraint
-  , symExpBool
-  , symExpInt
-  , symExpBytes
-  , symExp
-  , nameFromItem
-  , nameFromEnv
-  , nameFromDecl
-  , concatMapM
-  ) where
-
-import Control.Monad (when)
-import Data.ByteString (ByteString)
-import Data.ByteString.UTF8 (toString)
-import Data.List (intercalate, (\\), nub)
-import Data.List.NonEmpty as NonEmpty (toList)
-import Data.Map.Strict as Map (Map, lookup, fromList, toList)
-import Data.Maybe
-import Data.Type.Equality
-import Data.Typeable
-
-import Data.SBV hiding (name)
-import Data.SBV.String ((.++), subStr)
-
-import RefinedAst
-import Syntax (Id, Interface(..), Decl(..), EthEnv(..))
-import Type (metaType)
-import Print (prettyEnv)
-import Extract (locsFromExp, getLoc)
-
--- *** Interface *** --
-
-
-{-|
-   For each invariant claim, we build an SMT query for each pass behaviour in the transtion system.
-
-   If the behaviour is a constructor, the query asks the solver to find instances where:
-
-   - the preconditions hold
-   - the storage values in the poststate match those specified by the `creates` block of the constructor holds
-   - the invariant does not hold over the post state or the postconditions do not hold over the poststate
-
-   If the behaviour is a method, the query asks the solver to find instances where:
-
-   - the invariant holds over the pre state
-   - the preconditions hold
-   - all storage variables are within the range specified by their type
-   - a predicate relating the pre and post state according to the specification in the `storage` block holds
-   - the invariant does not hold over the post state or the postconditions do not hold over the poststate
-
-   If all of the queries for an invariant claim return `unsat`, then we have proved two things:
-
-   1. The invariant holds over the post state
-   2. The postconditions hold for every method level behaviour
--}
-queries :: [Claim] -> [(Invariant, [Symbolic ()])]
-queries claims = fmap mkQueries gathered
-  where
-    gathered = fmap (\inv -> (inv, definition inv, getBehaviours inv)) invariants
-    invariants = [i | I i <- claims]
-    getBehaviours (Invariant c _ _) = filter (\b -> isPass b && contractMatches c b) [b | B b <- claims]
-    definition (Invariant c _ _) = head $ filter (\b -> Pass == _cmode b && _cname b == c) [c' | C c' <- claims]
-    contractMatches c b = c == (_contract b)
-    isPass b = (_mode b) == Pass
-
-
--- *** Data *** --
-
-
-type Contract = Id
-type Method = Id
-type Args = Map Id SMType
-type Storage = Map Id (SMType, SMType)
-type Env = Map Id SMType
-data When = Pre | Post
-
-  deriving (Eq, Show)
-
-data Ctx = Ctx Contract Method Args Storage Env
-  deriving (Show)
-
-data SMType
-  = SymInteger (SBV Integer)
-  | SymBool (SBV Bool)
-  | SymBytes (SBV String)
-  deriving (Show)
-
-instance EqSymbolic SMType where
-  SymInteger a .== SymInteger b = a .== b
-  SymBool a .== SymBool b = a .== b
-  SymBytes a .== SymBytes b = a .== b
-  _ .== _ = literal False
-
-
--- *** Query Construction *** --
-
-
-mkQueries :: (Invariant, Constructor, [Behaviour]) -> (Invariant, [Symbolic ()])
-mkQueries (inv, constr, behvs) = (inv, inits:methods)
-  where
-    inits = mkInit inv constr
-    methods = mkMethod inv constr <$> behvs
-
-mkInit :: Invariant -> Constructor -> Symbolic ()
-mkInit inv@(Invariant _ invConds invExp) constr@(Constructor _ _ _ preConds postConds statedef otherstorages) = do
-  ctx <- mkContext inv (Right constr)
-
-  let
-    mkBool = symExpBool ctx
-    storages = (Right <$> statedef) <> otherstorages
-    postInv' = mkBool Post invExp
-    preCond' = mkBool Pre (mconcat (nub $ preConds <> invConds))
-    postCond' = mkBool Pre (mconcat postConds)
-    stateUpdates' = mkStorageConstraints ctx storages (references inv (Right constr))
-
-  constrain $ preCond' .&& sAnd stateUpdates' .&& (sNot postCond' .|| sNot postInv')
-
-mkMethod :: Invariant -> Constructor -> Behaviour -> Symbolic ()
-mkMethod inv@(Invariant _ invConds invExp) initBehv behv = do
-  ctx@(Ctx c m _ store' env) <- mkContext inv (Left behv)
-
-  let (Interface _ initdecls) = _cinterface initBehv
-  initArgs <- mkArgs c m initdecls
-  let invCtx = Ctx c m initArgs store' env
-
-  let
-    preInv = symExpBool invCtx Pre invExp
-    postInv = symExpBool invCtx Post invExp
-    invConds' = symExpBool invCtx Pre (mconcat (invConds \\ (_preconditions behv)))
-    preCond = symExpBool ctx Pre (mconcat $ _preconditions behv)
-    postCond = symExpBool ctx Pre (mconcat $ _postconditions behv)
-    stateUpdates = mkStorageConstraints ctx (_stateUpdates behv) (references inv (Left behv))
-
-  constrain $ preInv .&& preCond .&& invConds'
-           .&& sAnd stateUpdates
-           .&& (sNot postCond .|| sNot postInv)
-
-mkContext :: Invariant -> Either Behaviour Constructor -> Symbolic Ctx
-mkContext inv@(Invariant contract _ _) spec = do
-  let (c1, decls, method) = either
-        (\(Behaviour m _ c (Interface _ ds) _ _ _ _) -> (c,ds, m))
-        (\(Constructor c _ (Interface _ ds) _ _ _ _) -> (c, ds, "init"))
-        spec
-  -- TODO: refine AST so we don't need this anymore
-  when (contract /= c1) $ error "Internal error: contract mismatch"
-
-  store <- Map.fromList <$> mapM (mkSymStorage method) (references inv spec)
-  env <- mkEnv contract method
-  args <- mkArgs contract method decls
-
-  return $ Ctx contract method args store env
-
-mkArgs :: Contract -> Method -> [Decl] -> Symbolic (Map Id SMType)
-mkArgs c m ds = Map.fromList <$> mapM (mkSymArg c m) ds
-
-references :: Invariant -> Either Behaviour Constructor -> [StorageLocation]
-references (Invariant _ _ invExp) spec
-  = nub $ (getLoc <$> updates) <> locsFromExp invExp
-      where
-        updates = either
-          (\(Behaviour _ _ _ _ _ _ u _) -> u)
-          (\(Constructor _ _ _ _ _ i cs) -> (Right <$> i) <> cs)
-          spec
-
-mkSymArg :: Contract -> Method -> Decl -> Symbolic (Id, SMType)
-mkSymArg contract method decl@(Decl typ _) = case metaType typ of
-  Integer -> do
-    v <- sInteger name
-    return (name, SymInteger v)
-  Boolean -> do
-    v <- sBool name
-    return (name, SymBool v)
-  ByteStr -> do
-    v <- sString name
-    return (name, SymBytes v)
-  where
-    name = nameFromDecl contract method decl
-
-mkSymStorage :: Method -> StorageLocation -> Symbolic (Id, (SMType, SMType))
-mkSymStorage method loc = case loc of
-  IntLoc item -> do
-    v <- SymInteger <$> sInteger (pre item)
-    w <- SymInteger <$> sInteger (post item)
-    return (name item, (v, w))
-  BoolLoc item -> do
-    v <- SymBool <$> sBool (pre item)
-    w <- SymBool <$> sBool (post item)
-    return (name item, (v, w))
-  BytesLoc item -> do
-    v <- SymBytes <$> sString (pre item)
-    w <- SymBytes <$> sString (post item)
-    return (name item, (v, w))
-  where
-    name :: TStorageItem a -> Id
-    name i = nameFromItem method i
-
-    pre :: TStorageItem a -> Id
-    pre i = (name i) ++ "_pre"
-
-    post :: TStorageItem a -> Id
-    post i = (name i) ++ "_post"
-
-mkEnv :: Contract -> Method -> Symbolic Env
-mkEnv contract method = Map.fromList <$> mapM makeSymbolic
-  [ Caller, Callvalue, Calldepth, Origin, Blockhash, Blocknumber
-  , Difficulty, Chainid, Gaslimit, Coinbase, Timestamp, This, Nonce ]
-  where
-    makeSymbolic :: EthEnv -> Symbolic (Id, SMType)
-    makeSymbolic Blockhash = mkBytes Blockhash
-    makeSymbolic env = mkInt env
-
-    mkInt :: EthEnv -> Symbolic (Id, SMType)
-    mkInt env = do
-      let k = nameFromEnv contract method env
-      v <- SymInteger <$> sInteger k
-      return (k, v)
-
-    mkBytes :: EthEnv -> Symbolic (Id, SMType)
-    mkBytes env = do
-      let k = nameFromEnv contract method env
-      v <- SymBytes <$> sString k
-      return (k, v)
-
-mkStorageConstraints :: Ctx -> [Either StorageLocation StorageUpdate] -> [StorageLocation] -> [SBV Bool]
-mkStorageConstraints ctx updates locs
-  = mkConstraint ctx <$> (unchanged <> updates)
-  where
-    unchanged = Left <$> (locs \\ (fmap getLoc updates))
-
-mkConstraint :: Ctx -> (Either StorageLocation StorageUpdate) -> SBV Bool
-mkConstraint ctx (Left loc) = fromLocation ctx loc
-mkConstraint ctx (Right update) = fromUpdate ctx update
-
-getVar :: (Show b) => Ctx -> TStorageItem a -> (Map Id (SMType, SMType) -> Map Id b) -> b
-getVar (Ctx _ m _ store _) i f = get (nameFromItem m i) (f store)
-
-fromLocation :: Ctx -> StorageLocation -> SBV Bool
-fromLocation ctx loc = case loc of
-  IntLoc item -> getVar ctx item (catInts . (fst <$>)) .== getVar ctx item (catInts . (snd <$>))
-  BoolLoc item -> getVar ctx item (catBools . (fst <$>)) .== getVar ctx item (catBools . (snd <$>))
-  BytesLoc item -> getVar ctx item (catBytes . (fst <$>)) .== getVar ctx item (catBytes . (snd <$>))
-
-fromUpdate :: Ctx -> StorageUpdate -> SBV Bool
-fromUpdate ctx update = case update of
-  IntUpdate item e -> getVar ctx item (catInts . (snd <$>)) .== symExpInt ctx Pre e
-  BoolUpdate item e -> getVar ctx item (catBools . (snd <$>)) .== symExpBool ctx Pre e
-  BytesUpdate item e -> getVar ctx item (catBytes . (snd <$>)) .== symExpBytes ctx Pre e
-
-
--- *** Symbolic Expression Construction *** ---
-
-symExp :: Ctx -> When -> ReturnExp -> SMType
-symExp ctx whn ret = case ret of
-  ExpInt e -> SymInteger $ symExpInt ctx whn e
-  ExpBool e -> SymBool $ symExpBool ctx whn e
-  ExpBytes e -> SymBytes $ symExpBytes ctx whn e
-
-symExpBool :: Ctx -> When -> Exp Bool -> SBV Bool
-symExpBool ctx@(Ctx c m args store _) w e = case e of
-  And a b   -> (symExpBool ctx w a) .&& (symExpBool ctx w b)
-  Or a b    -> (symExpBool ctx w a) .|| (symExpBool ctx w b)
-  Impl a b  -> (symExpBool ctx w a) .=> (symExpBool ctx w b)
-  LE a b    -> (symExpInt ctx w a) .< (symExpInt ctx w b)
-  LEQ a b   -> (symExpInt ctx w a) .<= (symExpInt ctx w b)
-  GE a b    -> (symExpInt ctx w a) .> (symExpInt ctx w b)
-  GEQ a b   -> (symExpInt ctx w a) .>= (symExpInt ctx w b)
-  NEq a b   -> sNot (symExpBool ctx w (Eq a b))
-  Neg a     -> sNot (symExpBool ctx w a)
-  LitBool a -> literal a
-  BoolVar a -> get (nameFromArg c m a) (catBools args)
-  TEntry a  -> get (nameFromItem m a) (catBools store')
-  ITE x y z -> ite (symExpBool ctx w x) (symExpBool ctx w y) (symExpBool ctx w z)
-  Eq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
-    Just Refl -> symExpInt ctx w a .== symExpInt ctx w b
-    Nothing -> case eqT @t @Bool of
-      Just Refl -> symExpBool ctx w a .== symExpBool ctx w b
-      Nothing -> case eqT @t @ByteString of
-        Just Refl -> symExpBytes ctx w a .== symExpBytes ctx w b
-        Nothing -> error "Internal Error: invalid expression type"
- where store' = case w of
-         Pre -> fst <$> store
-         Post -> snd <$> store
-
-symExpInt :: Ctx -> When -> Exp Integer -> SBV Integer
-symExpInt ctx@(Ctx c m args store env) w e = case e of
-  Add a b   -> (symExpInt ctx w a) + (symExpInt ctx w b)
-  Sub a b   -> (symExpInt ctx w a) - (symExpInt ctx w b)
-  Mul a b   -> (symExpInt ctx w a) * (symExpInt ctx w b)
-  Div a b   -> (symExpInt ctx w a) `sDiv` (symExpInt ctx w b)
-  Mod a b   -> (symExpInt ctx w a) `sMod` (symExpInt ctx w b)
-  Exp a b   -> (symExpInt ctx w a) .^ (symExpInt ctx w b)
-  LitInt a  -> literal a
-  IntMin a  -> literal $ intmin a
-  IntMax a  -> literal $ intmax a
-  UIntMin a -> literal $ uintmin a
-  UIntMax a -> literal $ uintmax a
-  IntVar a  -> get (nameFromArg c m a) (catInts args)
-  TEntry a  -> get (nameFromItem m a) (catInts store')
-  IntEnv a -> get (nameFromEnv c m a) (catInts env)
-  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
-  ITE x y z -> ite (symExpBool ctx w x) (symExpInt ctx w y) (symExpInt ctx w z)
- where store' = case w of
-         Pre -> fst <$> store
-         Post -> snd <$> store
-
-symExpBytes :: Ctx -> When -> Exp ByteString -> SBV String
-symExpBytes ctx@(Ctx c m args store env) w e = case e of
-  Cat a b -> (symExpBytes ctx w a) .++ (symExpBytes ctx w b)
-  ByVar a  -> get (nameFromArg c m a) (catBytes args)
-  ByStr a -> literal a
-  ByLit a -> literal $ toString a
-  TEntry a  -> get (nameFromItem m a) (catBytes store')
-  Slice a x y -> subStr (symExpBytes ctx w a) (symExpInt ctx w x) (symExpInt ctx w y)
-  ByEnv a -> get (nameFromEnv c m a) (catBytes env)
-  ITE x y z -> ite (symExpBool ctx w x) (symExpBytes ctx w y) (symExpBytes ctx w z)
- where store' = case w of
-         Pre -> fst <$> store
-         Post -> snd <$> store
-
-
--- *** SMT Variable Names *** --
-
-
-nameFromItem :: Method -> TStorageItem a -> Id
-nameFromItem method item = case item of
-  DirectInt c name -> c @@ method @@ name
-  DirectBool c name -> c @@ method @@ name
-  DirectBytes c name -> c @@ method @@ name
-  MappedInt c name ixs -> c @@ method @@ name >< showIxs c ixs
-  MappedBool c name ixs -> c @@ method @@ name >< showIxs c ixs
-  MappedBytes c name ixs -> c @@ method @@ name >< showIxs c ixs
-  where
-    x >< y = x <> "-" <> y
-    showIxs contract ixs = intercalate "-" (NonEmpty.toList $ nameFromExp contract method <$> ixs)
-
-nameFromExp :: Contract -> Method -> ReturnExp -> Id
-nameFromExp contract method e = case e of
-  ExpInt e' -> nameFromExpInt contract method e'
-  ExpBool e' -> nameFromExpBool contract method e'
-  ExpBytes e' -> nameFromExpBytes contract method e'
-
-nameFromExpInt :: Contract -> Method -> Exp Integer -> Id
-nameFromExpInt c m e = case e of
-  Add a b   -> (nameFromExpInt c m a) <> "+" <> (nameFromExpInt c m b)
-  Sub a b   -> (nameFromExpInt c m a) <> "-" <> (nameFromExpInt c m b)
-  Mul a b   -> (nameFromExpInt c m a) <> "*" <> (nameFromExpInt c m b)
-  Div a b   -> (nameFromExpInt c m a) <> "/" <> (nameFromExpInt c m b)
-  Mod a b   -> (nameFromExpInt c m a) <> "%" <> (nameFromExpInt c m b)
-  Exp a b   -> (nameFromExpInt c m a) <> "^" <> (nameFromExpInt c m b)
-  LitInt a  -> show a
-  IntMin a  -> show $ intmin a
-  IntMax a  -> show $ intmax a
-  UIntMin a -> show $ uintmin a
-  UIntMax a -> show $ uintmax a
-  IntVar a  -> a
-  TEntry a  -> nameFromItem m a
-  IntEnv a -> nameFromEnv c m a
-  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
-  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpInt c m y <> "-else-" <> nameFromExpInt c m z
-
-nameFromExpBool :: Contract -> Method -> Exp Bool -> Id
-nameFromExpBool c m e = case e of
-  And a b   -> nameFromExpBool c m a <> "&&" <> nameFromExpBool c m b
-  Or a b    -> nameFromExpBool c m a <> "|" <> nameFromExpBool c m b
-  Impl a b  -> nameFromExpBool c m a <> "=>" <> nameFromExpBool c m b
-  LE a b    -> nameFromExpInt c m a <> "<" <> nameFromExpInt c m b
-  LEQ a b   -> nameFromExpInt c m a <> "<=" <> nameFromExpInt c m b
-  GE a b    -> nameFromExpInt c m a <> ">" <> nameFromExpInt c m b
-  GEQ a b   -> nameFromExpInt c m a <> ">=" <> nameFromExpInt c m b
-  Neg a     -> "~" <> nameFromExpBool c m a
-  LitBool a -> show a
-  BoolVar a -> nameFromArg c m a
-  TEntry a  -> nameFromItem m a
-  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpBool c m y <> "-else-" <> nameFromExpBool c m z
-  Eq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
-    Just Refl -> nameFromExpInt c m a <> "==" <> nameFromExpInt c m b
-    Nothing -> case eqT @t @Bool of
-      Just Refl -> nameFromExpBool c m a <> "==" <> nameFromExpBool c m b
-      Nothing -> case eqT @t @ByteString of
-        Just Refl -> nameFromExpBytes c m a <> "==" <> nameFromExpBytes c m b
-        Nothing -> error "Internal Error: invalid expressio type"
-  NEq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
-    Just Refl -> nameFromExpInt c m a <> "=/=" <> nameFromExpInt c m b
-    Nothing -> case eqT @t @Bool of
-      Just Refl -> nameFromExpBool c m a <> "=/=" <> nameFromExpBool c m b
-      Nothing -> case eqT @t @ByteString of
-        Just Refl -> nameFromExpBytes c m a <> "=/=" <> nameFromExpBytes c m b
-        Nothing -> error "Internal Error: invalid expressio type"
-
-nameFromExpBytes :: Contract -> Method -> Exp ByteString -> Id
-nameFromExpBytes c m e = case e of
-  Cat a b -> nameFromExpBytes c m a <> "++" <> nameFromExpBytes c m b
-  ByVar a  -> nameFromArg c m a
-  ByStr a -> show a
-  ByLit a -> show a
-  TEntry a  -> nameFromItem m a
-  Slice a x y -> nameFromExpBytes c m a <> "[" <> show x <> ":" <> show y <> "]"
-  ByEnv a -> nameFromEnv c m a
-  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpBytes c m y <> "-else-" <> nameFromExpBytes c m z
-
-nameFromDecl :: Contract -> Method -> Decl -> Id
-nameFromDecl c m (Decl _ name) = nameFromArg c m name
-
-nameFromArg :: Contract -> Method -> Id -> Id
-nameFromArg contract method name = contract @@ method @@ name
-
-nameFromEnv :: Contract -> Method -> EthEnv -> Id
-nameFromEnv contract method e = contract @@ method @@ (prettyEnv e)
-
-(@@) :: Id -> Id -> Id
-x @@ y = x <> "_" <> y
-
-
--- *** Utils *** --
-
-
-get :: (Show a, Ord a, Show b) => a -> Map a b -> b
-get name vars = fromMaybe (error (show name <> " not found in " <> show vars)) $ Map.lookup name vars
-
-catInts :: Map Id SMType -> Map Id (SBV Integer)
-catInts m = Map.fromList [(name, i) | (name, SymInteger i) <- Map.toList m]
-
-catBools :: Map Id SMType -> Map Id (SBV Bool)
-catBools m = Map.fromList [(name, i) | (name, SymBool i) <- Map.toList m]
-
-catBytes :: Map Id SMType -> Map Id (SBV String)
-catBytes m = Map.fromList [(name, i) | (name, SymBytes i) <- Map.toList m]
-
-concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
-concatMapM op' = foldr f (pure [])
-    where f x xs = do x' <- op' x; if null x' then xs else do xs' <- xs; pure $ x'++xs'
diff --git a/src/RefinedAst.hs b/src/RefinedAst.hs
index 71f996a9..043bf2a9 100644
--- a/src/RefinedAst.hs
+++ b/src/RefinedAst.hs
@@ -33,9 +33,23 @@ data Claim = C Constructor | B Behaviour | I Invariant | S Store deriving (Show,
 
 type Store = Map Id (Map Id SlotType)
 
+-- | Represents a contract level invariant along with some associated metadata.
+-- The invariant is defined in the context of the constructor, but must also be
+-- checked against each behaviour in the contract, and thus may reference variables
+-- that are not present in a given behaviour (constructor args, or storage
+-- variables that are not referenced in the behaviour), so we additionally
+-- attach some constraints over the variables referenced by the predicate in
+-- the `_ipreconditions` and `_istoragebounds` fields. These fields are
+-- seperated as the constraints derived from the types of the storage
+-- references must be treated differently in the constructor specific queries
+-- (as the storage variables have no prestate in the constructor...), wheras
+-- the constraints derived from the types of the environment variables and
+-- calldata args (stored in _ipreconditions) have a uniform semantics over both
+-- the constructor and behaviour claims.
 data Invariant = Invariant
   { _icontract :: Id
   , _ipreconditions :: [Exp Bool]
+  , _istoragebounds :: [Exp Bool]
   , _predicate :: Exp Bool
   } deriving (Show, Eq)
 
@@ -71,7 +85,6 @@ data MType
   = Integer
   | Boolean
   | ByteStr
---  | Mapping (Map MType MType)
   deriving (Eq, Ord, Show, Read)
 
 data StorageUpdate
@@ -209,6 +222,7 @@ instance ToJSON Claim where
   toJSON (I (Invariant {..})) = object [ "kind" .= (String "Invariant")
                                        , "predicate" .= toJSON _predicate
                                        , "preconditions" .= toJSON _ipreconditions
+                                       , "storagebounds" .= toJSON _istoragebounds
                                        , "contract" .= _icontract]
   toJSON (C (Constructor {..})) = object  [ "kind" .= (String "Constructor")
                                           , "contract" .= _cname
diff --git a/src/SMT.hs b/src/SMT.hs
new file mode 100644
index 00000000..342fd57c
--- /dev/null
+++ b/src/SMT.hs
@@ -0,0 +1,477 @@
+{-# LANGUAGE GADTs #-}
+
+module SMT (Solver(..), SMTConfig(..), Query(..), SMTResult(..), runSMT, runQuery, mkPostconditionQueries, mkInvariantQueries, getTarget, getSMT) where
+
+import Data.Map (Map)
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Maybe
+import Data.List
+import Data.Containers.ListUtils (nubOrd)
+
+import RefinedAst
+import Extract
+import Syntax (Id, EthEnv(..), Interface(..), Decl(..))
+import Print (prettyEnv)
+import Type (defaultStore, metaType)
+
+import System.Process (readProcessWithExitCode)
+import System.Exit (ExitCode(..))
+
+
+--- ** Data ** ---
+
+
+data Solver = Z3 | CVC4
+  deriving Eq
+
+instance Show Solver where
+  show Z3 = "z3"
+  show CVC4 = "cvc4"
+
+data SMTConfig = SMTConfig
+  { _solver :: Solver
+  , _timeout :: Integer
+  , _debug :: Bool
+  }
+
+type SMT2 = String
+
+-- | Context needed to produce SMT from an act expression
+--   - Id : The name of the interface from which calldata vars were extracted
+--   - When : Whether or not storage references should refer to the pre or post state
+data Ctx = Ctx Id When
+
+data When = Pre | Post
+
+instance Show When where
+  show Pre = "pre"
+  show Post = "post"
+
+-- | An SMTExp is a structured representation of an SMT Expression
+--   The _storage, _calldata, and _environment fields hold variable declarations
+--   The _assertions field holds the various constraints that should be satisfied
+data SMTExp = SMTExp
+  { _storage :: [SMT2]
+  , _calldata :: [SMT2]
+  , _environment :: [SMT2]
+  , _assertions :: [SMT2]
+  }
+
+instance Show SMTExp where
+  show e = unlines [storage, calldata, environment, assertions]
+    where
+      storage = unlines $ ";STORAGE:" : (nubOrd $ _storage e)
+      calldata = unlines $ ";CALLDATA:" : (nubOrd $ _calldata e)
+      environment = unlines $ ";ENVIRONMENT:" : (nubOrd $ _environment e)
+      assertions = unlines $ ";ASSERTIONS:" : (nubOrd $ _assertions e)
+
+-- A Query is a structured representation of an SMT query for an individual
+-- expression, along with the metadata needed to pretty print the result
+data Query
+  = Postcondition Claim (Exp Bool) SMTExp
+  | Inv Claim Invariant SMTExp
+  deriving (Show)
+
+data SMTResult
+  = Sat
+  | Unsat
+  | Unknown
+  | Error Int String
+  deriving (Show)
+
+data Model = Model
+  { _mstorage :: Map Id (MType, MType)
+  , _mcalldata :: Map Id MType
+  , _menvironment :: Map Id MType
+  }
+  deriving (Show)
+
+
+--- ** Analysis Passes ** ---
+
+
+-- | For each postcondition in the claim we construct a query that:
+--    - Asserts that the preconditions hold
+--    - Asserts that storage has been updated according to the rewrites in the behaviour
+--    - Asserts that the postcondition cannot be reached
+--   If this query is unsatisfiable, then there exists no case where the postcondition can be violated.
+mkPostconditionQueries :: Claim -> [Query]
+mkPostconditionQueries (B behv@(Behaviour _ _ _ (Interface ifaceName decls) preconds postconds stateUpdates _)) = mkQuery <$> postconds
+  where
+    -- declare vars
+    storage = concatMap (declareStorageLocation . getLoc) stateUpdates
+    args = declareArg ifaceName <$> decls
+    envs = declareEthEnv <$> ethEnvFromBehaviour behv
+
+    -- constraints
+    pres = mkAssert (Ctx ifaceName Pre) <$> preconds
+    updates = encodeUpdate ifaceName <$> stateUpdates
+
+    mksmt e = SMTExp
+      { _storage = storage
+      , _calldata = args
+      , _environment = envs
+      , _assertions = [mkAssert (Ctx ifaceName Pre) . Neg $ e] <> pres <> updates
+      }
+    mkQuery e = Postcondition (B behv) e (mksmt e)
+mkPostconditionQueries (C constructor@(Constructor _ _ (Interface ifaceName decls) preconds postconds initialStorage stateUpdates)) = mkQuery <$> postconds
+  where
+    -- declare vars
+    localStorage = declareInitialStorage <$> initialStorage
+    externalStorage = concatMap (declareStorageLocation . getLoc) stateUpdates
+    args = declareArg ifaceName <$> decls
+    envs = declareEthEnv <$> ethEnvFromConstructor constructor
+
+    -- constraints
+    pres = mkAssert (Ctx ifaceName Pre) <$> preconds
+    updates = encodeUpdate ifaceName <$> stateUpdates
+    initialStorage' = encodeInitialStorage ifaceName <$> initialStorage
+
+    mksmt e = SMTExp
+      { _storage = localStorage <> externalStorage
+      , _calldata = args
+      , _environment = envs
+      , _assertions = [mkAssert (Ctx ifaceName Pre) . Neg $ e] <> pres <> updates <> initialStorage'
+      }
+    mkQuery e = Postcondition (C constructor) e (mksmt e)
+mkPostconditionQueries _ = []
+
+-- | For each invariant in the list of input claims, we first gather all the
+--   specs relevant to that invariant (i.e. the constructor for that contract,
+--   and all passing behaviours for that contract).
+--
+--   For the constructor we build a query that:
+--     - Asserts that all preconditions hold
+--     - Asserts that external storage has been updated according to the spec
+--     - Asserts that internal storage values have the value given in the creates block
+--     - Asserts that the invariant does not hold over the poststate
+--
+--   For the behaviours, we build a query that:
+--     - Asserts that the invariant holds over the prestate
+--     - Asserts that all preconditions hold
+--     - Asserts that storage has been updated according to the spec
+--     - Asserts that the invariant does not hold over the poststate
+--
+--   If all of the queries return `unsat` then we have an inductive proof that
+--   the invariant holds for all possible contract states.
+mkInvariantQueries :: [Claim] -> [Query]
+mkInvariantQueries claims = concatMap mkQueries gathered
+  where
+    mkQueries (inv, constructor, behvs) = mkInit inv constructor : fmap (mkBehv inv constructor) behvs
+    gathered = fmap (\inv -> (inv, getConstructor inv, getBehaviours inv)) [i | I i <- claims]
+
+    getBehaviours (Invariant c _ _ _) = [b | B b <- claims, matchBehaviour c b]
+    getConstructor (Invariant c _ _ _) = head [c' | C c' <- claims, matchConstructor c c']
+    matchBehaviour contract behv = (_mode behv) == Pass && (_contract behv) == contract
+    matchConstructor contract defn = _cmode defn == Pass && _cname defn == contract
+
+    mkInit :: Invariant -> Constructor -> Query
+    mkInit inv@(Invariant _ invConds _ invExp) ctor@(Constructor _ _ (Interface ifaceName decls) preconds _ initialStorage stateUpdates) = Inv (C ctor) inv smt
+      where
+        -- declare vars
+        localStorage = declareInitialStorage <$> initialStorage
+        externalStorage = concatMap (declareStorageLocation . getLoc) stateUpdates
+        args = declareArg ifaceName <$> decls
+        envs = declareEthEnv <$> ethEnvFromConstructor ctor
+
+        -- constraints
+        pres = (mkAssert (Ctx ifaceName Pre)) <$> (preconds <> invConds)
+        updates = encodeUpdate ifaceName <$> stateUpdates
+        initialStorage' = encodeInitialStorage ifaceName <$> initialStorage
+        postInv = mkAssert (Ctx ifaceName Post) . Neg $ invExp
+
+        smt = SMTExp
+          { _storage = localStorage <> externalStorage
+          , _calldata = args
+          , _environment = envs
+          , _assertions = postInv : pres <> updates <> initialStorage'
+          }
+
+    mkBehv :: Invariant -> Constructor -> Behaviour -> Query
+    mkBehv inv@(Invariant _ invConds invStorageBounds invExp) ctor behv = Inv (B behv) inv smt
+      where
+        (Interface ctorIface ctorDecls) = _cinterface ctor
+        (Interface behvIface behvDecls) = _interface behv
+        -- storage locs mentioned in the invariant but not in the behaviour
+        implicitLocs = Left <$> (locsFromExp invExp \\ (getLoc <$> _stateUpdates behv))
+
+        -- declare vars
+        invEnv = declareEthEnv <$> ethEnvFromExp invExp
+        behvEnv = declareEthEnv <$> ethEnvFromBehaviour behv
+        initArgs = declareArg ctorIface <$> ctorDecls
+        behvArgs = declareArg behvIface <$> behvDecls
+        storage = concatMap (declareStorageLocation . getLoc) (_stateUpdates behv <> implicitLocs)
+
+        -- constraints
+        preInv = mkAssert (Ctx ctorIface Pre) invExp
+        postInv = mkAssert (Ctx ctorIface Post) . Neg $ invExp
+        behvConds = mkAssert (Ctx behvIface Pre) <$> (_preconditions behv)
+        invConds' = mkAssert (Ctx ctorIface Pre) <$> (invConds <> invStorageBounds)
+        implicitLocs' = encodeUpdate ctorIface <$> implicitLocs
+        updates = encodeUpdate behvIface <$> (_stateUpdates behv)
+
+        smt = SMTExp
+          { _storage = storage
+          , _calldata = initArgs <> behvArgs
+          , _environment = invEnv <> behvEnv
+          , _assertions = [preInv, postInv] <> behvConds <> invConds' <> implicitLocs' <> updates
+          }
+
+
+--- ** Solver Interaction ** ---
+
+
+runQuery :: SMTConfig -> Query -> IO (Query, SMTResult)
+runQuery conf q = do
+  (exitCode, stdout, _) <- runSMT conf ((show . getSMT $ q) <> "\n(check-sat)")
+  let output = filter (/= "") . lines $ stdout
+      containsErrors = any (isPrefixOf "(error") output
+      res = case exitCode of
+        ExitFailure code -> Error code stdout
+        ExitSuccess ->
+          if containsErrors
+          then Error 0 stdout -- cvc4 returns exit code zero even if there are errors
+          else case output of
+                 [] -> Unknown
+                 l -> case last l of
+                   "sat" -> Sat
+                   "unsat" -> Unsat
+                   "timeout" -> Unknown -- TODO: disambiguate
+                   "unknown" -> Unknown
+                   _ -> Error 0 $ "Unable to parse SMT output: " <> stdout
+  pure (q, res)
+
+runSMT :: SMTConfig -> SMT2 -> IO (ExitCode, String, String)
+runSMT (SMTConfig solver timeout _) e = do
+  let input = intercalate "\n" ["(set-logic ALL)", e]
+      args = case solver of
+               Z3 ->
+                 [ "-in"
+                 , "-t:" <> show timeout]
+               CVC4 ->
+                 [ "--lang=smt"
+                 , "--interactive"
+                 , "--no-interactive-prompt"
+                 , "--tlimit=" <> show timeout]
+  readProcessWithExitCode (show solver) args input
+
+
+--- ** SMT2 generation ** ---
+
+
+-- | encodes a storage update from a constructor creates block as an smt assertion
+encodeInitialStorage :: Id -> StorageUpdate -> SMT2
+encodeInitialStorage behvName update = case update of
+  IntUpdate item e -> encode item e
+  BoolUpdate item e -> encode item e
+  BytesUpdate item e -> encode item e
+  where
+    ctx = Ctx behvName Post
+
+    encode :: TStorageItem a -> Exp a -> SMT2
+    encode item e = "(assert (= " <> expToSMT2 ctx (TEntry item) <> " " <> expToSMT2 ctx e <> "))"
+
+-- | declares a storage location that is created by the constructor, these
+--   locations have no prestate, so we declare a post var only
+declareInitialStorage :: StorageUpdate -> SMT2
+declareInitialStorage update = case getLoc . Right $ update of
+  IntLoc item -> case item of
+    DirectInt {} -> mkdirect item Integer
+    MappedInt _ _ ixs -> mkarray item ixs Integer
+  BoolLoc item -> case item of
+    DirectBool {} -> mkdirect item Boolean
+    MappedBool _ _ ixs -> mkarray item ixs Boolean
+  BytesLoc item -> case item of
+    DirectBytes {} -> mkdirect item ByteStr
+    MappedBytes _ _ ixs -> mkarray item ixs ByteStr
+  where
+    mkdirect item tp = constant (nameFromItem Post item) tp
+    mkarray item ixs tp = array (nameFromItem Post item) ixs tp
+
+-- | encodes a storge update rewrite as an smt assertion
+encodeUpdate :: Id -> Either StorageLocation StorageUpdate -> SMT2
+encodeUpdate _ (Left loc) = "(assert (= " <> nameFromLoc Pre loc <> " " <> nameFromLoc Post loc <> "))"
+encodeUpdate behvName (Right update) = case update of
+  IntUpdate item e -> encode item e
+  BoolUpdate item e -> encode item e
+  BytesUpdate item e -> encode item e
+  where
+    encode :: TStorageItem a -> Exp a -> SMT2
+    encode item e = "(assert (= " <> expToSMT2 (Ctx behvName Post) (TEntry item) <> " " <> expToSMT2 (Ctx behvName Pre) e <> "))"
+
+-- | declares a storage location that exists both in the pre state and the post
+--   state (i.e. anything except a loc created by a constructor claim)
+declareStorageLocation :: StorageLocation -> [SMT2]
+declareStorageLocation loc = case loc of
+  IntLoc item -> case item of
+    DirectInt {} -> mkdirect item Integer
+    MappedInt _ _ ixs -> mkarray item ixs Integer
+  BoolLoc item -> case item of
+    DirectBool {} -> mkdirect item Boolean
+    MappedBool _ _ ixs -> mkarray item ixs Boolean
+  BytesLoc item -> case item of
+    DirectBytes {} -> mkdirect item ByteStr
+    MappedBytes _ _ ixs -> mkarray item ixs ByteStr
+  where
+    mkdirect item tp = [constant (nameFromItem Pre item) tp, constant (nameFromItem Post item) tp]
+    mkarray item ixs tp = [array (nameFromItem Pre item) ixs tp, array (nameFromItem Post item) ixs tp]
+
+declareArg :: Id -> Decl -> SMT2
+declareArg behvName d@(Decl typ _) = constant (nameFromDecl behvName d) (metaType typ)
+
+declareEthEnv :: EthEnv -> SMT2
+declareEthEnv env = constant (prettyEnv env) tp
+  where tp = fromJust . lookup env $ defaultStore
+
+returnExpToSMT2 :: Ctx -> ReturnExp -> SMT2
+returnExpToSMT2 c e = case e of
+  ExpInt ei -> expToSMT2 c ei
+  ExpBool eb -> expToSMT2 c eb
+  ExpBytes ebs -> expToSMT2 c ebs
+
+expToSMT2 :: Ctx -> Exp a -> SMT2
+expToSMT2 ctx@(Ctx behvName whn) e = case e of
+
+  -- booleans
+  And a b -> binop "and" a b
+  Or a b -> binop "or" a b
+  Impl a b -> binop "=>" a b
+  Neg a -> unop "not" a
+  LE a b -> binop "<" a b
+  LEQ a b -> binop "<=" a b
+  GEQ a b -> binop ">=" a b
+  GE a b -> binop ">" a b
+  LitBool a -> if a then "true" else "false"
+  BoolVar _ -> nameFromVar behvName e
+
+  -- integers
+  Add a b -> binop "+" a b
+  Sub a b -> binop "-" a b
+  Mul a b -> binop "*" a b
+  Div a b -> binop "div" a b
+  Mod a b -> binop "mod" a b
+  Exp a b -> expToSMT2 ctx (simplifyExponentiation a b)
+  LitInt a -> if a >= 0
+              then show a
+              else "(- " <> (show . negate $ a) <> ")" -- cvc4 does not accept negative integer literals
+  IntVar _ -> nameFromVar behvName e
+  IntEnv a -> prettyEnv a
+
+  -- bounds
+  IntMin a -> expToSMT2 ctx (LitInt $ intmin a)
+  IntMax a -> show $ intmax a
+  UIntMin a -> show $ uintmin a
+  UIntMax a -> show $ uintmax a
+
+  -- bytestrings
+  Cat a b -> binop "str.++" a b
+  Slice a start end -> triop "str.substr" a start (Sub end start)
+  ByVar _ -> nameFromVar behvName e
+  ByStr a -> a
+  ByLit a -> show a
+  ByEnv a -> prettyEnv a
+
+  -- builtins
+  NewAddr {} -> error "TODO: NewAddr"
+
+  -- polymorphic
+  Eq a b -> binop "=" a b
+  NEq a b -> unop "not" (Eq a b)
+  ITE a b c -> triop "ite" a b c
+  TEntry item -> case item of
+    DirectInt {} -> nameFromItem whn item
+    DirectBool {} -> nameFromItem whn item
+    DirectBytes {} -> nameFromItem whn item
+    MappedInt _ _ ixs -> select (nameFromItem whn item) ixs
+    MappedBool _ _ ixs -> select (nameFromItem whn item) ixs
+    MappedBytes _ _ ixs -> select (nameFromItem whn item) ixs
+
+  where
+    asSMT2 :: Exp a -> SMT2
+    asSMT2 = expToSMT2 ctx
+
+    unop :: String -> Exp a -> SMT2
+    unop op a = "(" <> op <> " " <> asSMT2 a <> ")"
+
+    binop :: String -> Exp a -> Exp b -> SMT2
+    binop op a b = "(" <> op <> " " <> asSMT2 a <> " " <> asSMT2 b <> ")"
+
+    triop :: String -> Exp a -> Exp b -> Exp c -> SMT2
+    triop op a b c = "(" <> op <> " " <> asSMT2 a <> " " <> asSMT2 b <> " " <> asSMT2 c <> ")"
+
+    select :: String -> NonEmpty ReturnExp -> SMT2
+    select name (hd :| tl) = foldl' (\smt ix -> "(select " <> smt <> " " <> returnExpToSMT2 ctx ix <> ")") inner tl
+      where
+        inner = "(" <> "select" <> " " <> name <> " " <> returnExpToSMT2 ctx hd <> ")"
+
+-- | SMT2 has no support for exponentiation, but we can do some preprocessing
+--   if the RHS is concrete to provide some limited support for exponentiation
+--   TODO: support any exponentiation expression where the RHS evaluates to a concrete value
+simplifyExponentiation :: Exp Integer -> Exp Integer -> Exp Integer
+simplifyExponentiation (LitInt a) (LitInt b) = LitInt (a ^ b)
+simplifyExponentiation _ _ = error "Internal Error: exponentiation is unsupported in SMT lib"
+
+constant :: Id -> MType -> SMT2
+constant name tp = "(declare-const " <> name <> " " <> (sType tp) <> ")"
+
+mkAssert :: Ctx -> Exp Bool -> SMT2
+mkAssert c e = "(assert " <> expToSMT2 c e <> ")"
+
+array :: Id -> NonEmpty ReturnExp -> MType -> SMT2
+array name (hd :| tl) ret = "(declare-const " <> name <> " (Array " <> sType' hd <> " " <> valueDecl tl <> "))"
+  where
+    valueDecl [] = sType ret
+    valueDecl (h : t) = "(Array " <> sType' h <> " " <> valueDecl t <> ")"
+
+sType :: MType -> SMT2
+sType Integer = "Int"
+sType Boolean = "Bool"
+sType ByteStr = "String"
+
+sType' :: ReturnExp -> SMT2
+sType' (ExpInt {}) = "Int"
+sType' (ExpBool {}) = "Bool"
+sType' (ExpBytes {}) = "String"
+
+
+--- ** Variable Names ** ---
+
+
+nameFromItem :: When -> TStorageItem a -> Id
+nameFromItem when item = case item of
+  DirectInt c name -> c @@ name @@ show when
+  DirectBool c name -> c @@ name @@ show when
+  DirectBytes c name -> c @@ name @@ show when
+  MappedInt c name _ -> c @@ name @@ show when
+  MappedBool c name _ -> c @@ name @@ show when
+  MappedBytes c name _ -> c @@ name @@ show when
+
+nameFromLoc :: When -> StorageLocation -> Id
+nameFromLoc when loc = case loc of
+  IntLoc item -> nameFromItem when item
+  BoolLoc item -> nameFromItem when item
+  BytesLoc item -> nameFromItem when item
+
+nameFromDecl :: Id -> Decl -> Id
+nameFromDecl behvName (Decl _ name) = behvName @@ name
+
+nameFromVar :: Id -> Exp a -> Id
+nameFromVar behvName (IntVar name) = behvName @@ name
+nameFromVar behvName (ByVar name) = behvName @@ name
+nameFromVar behvName (BoolVar name) = behvName @@ name
+nameFromVar _ _ = error "Internal Error: cannot produce a variable name for non variable expressions"
+
+(@@) :: String -> String -> String
+x @@ y = x <> "_" <> y
+
+
+--- ** Util ** ---
+
+
+getTarget :: Query -> Exp Bool
+getTarget (Postcondition _ t _) = t
+getTarget (Inv _ (Invariant _ _ _ t) _) = t
+
+getSMT :: Query -> SMTExp
+getSMT (Postcondition _ _ e) = e
+getSMT (Inv _ _ e) = e
diff --git a/src/Type.hs b/src/Type.hs
index f40895de..021a8d43 100644
--- a/src/Type.hs
+++ b/src/Type.hs
@@ -5,7 +5,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE LambdaCase #-}
 
-module Type (typecheck, metaType, bound, lookupVars, defaultStore) where
+module Type (typecheck, bound, lookupVars, defaultStore, metaType) where
 
 import Data.List
 import EVM.ABI
@@ -149,7 +149,7 @@ splitBehaviour store (Definition contract iface@(Interface _ decls) iffs (Create
                else [ C $ Constructor contract Pass iface iffs' ensures stateUpdates []
                        , C $ Constructor contract Fail iface [Neg (mconcat iffs')] ensures [] []]
 
-  return $ ((I . (Invariant contract [])) <$> invariants')
+  return $ ((I . (Invariant contract [] [])) <$> invariants')
            <> cases'
 
 mkEnv :: Id -> Store -> [Decl]-> Env
@@ -321,19 +321,6 @@ upperBound (AbiIntType n) = IntMax n
 upperBound AbiAddressType = UIntMax 160
 upperBound typ  = error $ "upperBound not implemented for " ++ show typ
 
-metaType :: AbiType -> MType
-metaType (AbiUIntType _)     = Integer
-metaType (AbiIntType  _)     = Integer
-metaType AbiAddressType      = Integer
-metaType AbiBoolType         = Boolean
-metaType (AbiBytesType _)    = ByteStr
-metaType AbiBytesDynamicType = ByteStr
-metaType AbiStringType       = ByteStr
---metaType (AbiArrayDynamicType a) =
---metaType (AbiArrayType        Int AbiType
---metaType (AbiTupleType        (Vector AbiType)
-metaType _ = error "TODO"
-
 
 checkExpr :: Pn -> Env -> Expr -> AbiType -> Err ReturnExp
 checkExpr p env e typ = case metaType typ of
diff --git a/src/act.cabal b/src/act.cabal
index eff20ce1..a87c462c 100644
--- a/src/act.cabal
+++ b/src/act.cabal
@@ -23,8 +23,9 @@ common deps
                  bytestring       >= 0.10.8,
                  sbv              >= 8.4,
                  mtl              >= 2.2.2,
-                 utf8-string      >= 1.0.1.1
-  other-modules: Lex ErrM Extract Parse RefinedAst K HEVM Coq Syntax Type Prove Print Enrich
+                 utf8-string      >= 1.0.1.1,
+                 process          >= 1.6.5.0,
+  other-modules: Lex ErrM Extract Parse RefinedAst K HEVM Coq Syntax Type Print Enrich SMT
   if flag(ci)
       ghc-options: -O2 -Wall -Werror -Wno-orphans
   else
@@ -43,8 +44,10 @@ Test-Suite test
   default-language: Haskell2010
   main-is:          Test.hs
   hs-source-dirs:   test, .
-  build-depends:    pretty-simple        >= 2.2,
-                    quickcheck-instances >= 0.3,
-                    tasty-hunit          >= 0.10,
-                    tasty-quickcheck     >= 0.10,
-                    tasty                >= 1.2
+  build-depends:    pretty-simple          >= 2.2,
+                    quickcheck-instances   >= 0.3,
+                    quickcheck-transformer >= 0.3,
+                    tasty-hunit            >= 0.10,
+                    tasty-quickcheck       >= 0.10,
+                    QuickCheck             >= 2.13.2,
+                    tasty                  >= 1.2
diff --git a/src/test/Test.hs b/src/test/Test.hs
index f2433ba2..b8e57803 100644
--- a/src/test/Test.hs
+++ b/src/test/Test.hs
@@ -6,11 +6,17 @@ module Main where
 
 import EVM.ABI (AbiType(..))
 import Test.Tasty
-import Test.Tasty.QuickCheck
+import Test.Tasty.QuickCheck (Gen, arbitrary, testProperty, Property)
 import Test.QuickCheck.Instances.ByteString()
+import Test.QuickCheck.GenT
+import Test.QuickCheck.Monadic
 
 import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.Reader
+import Data.List
 import Data.ByteString (ByteString)
+import System.Exit (ExitCode(..))
 import qualified Data.Set as Set
 import qualified Data.Map as Map (empty)
 
@@ -20,43 +26,67 @@ import Parse (parse)
 import Type (typecheck)
 import Print (prettyBehaviour)
 import Syntax (Interface(..), EthEnv(..), Decl(..))
+import SMT
 import RefinedAst hiding (Mode)
 
 import Debug.Trace
 import Text.Pretty.Simple
 import Data.Text.Lazy as T (unpack)
 
+-- Transformer stack to keep track of whether we are to generate expressions
+-- with exponentiation or not (for compatibility with SMT).
+type ExpoGen a = GenT (Reader Bool) a
 
--- *** Test Cases *** --
+noExponents, withExponents :: ExpoGen a -> Gen a
+noExponents   = fmap (`runReader` False) . runGenT
+withExponents = fmap (`runReader` True)  . runGenT
 
+--
+-- *** Test Cases *** --
 
 main :: IO ()
 main = defaultMain $ testGroup "act"
   [ testGroup "frontend"
-    {-
-       Generates a random concrete behaviour, prints it, runs it through the frontend
-       (lex -> parse -> type), and then checks that the typechecked output matches the
-       generated behaviour.
-
-       If the generated behaviour contains some preconditions, then the structure of the
-       fail spec is also checked.
-    -}
-    [ testProperty "single roundtrip" $ do
-        behv@(Behaviour name _ contract iface preconds _ _ _) <- sized genBehv
-        let actual = parse (lexer $ prettyBehaviour behv) >>= typecheck
-            expected = if null preconds then
-                [ S Map.empty, B behv ]
-              else
-                [ S Map.empty, B behv
-                , B $ Behaviour name Fail contract iface [Neg $ mconcat preconds] [] [] Nothing ]
-        return $ case actual of
-          Ok a -> a == expected
-          Bad _ -> False
-    ]
+      {-
+         Generates a random behaviour, prints it, runs it through the frontend
+         (lex -> parse -> type), and then checks that the typechecked output matches the
+         generated behaviour.
+
+         If the generated behaviour contains some preconditions, then the structure of the
+         fail spec is also checked.
+      -}
+      [ testProperty "roundtrip" . withExponents $ do
+          behv@(Behaviour name _ contract iface preconds _ _ _) <- sized genBehv
+          let actual = parse (lexer $ prettyBehaviour behv) >>= typecheck
+              expected = if null preconds then
+                  [ S Map.empty, B behv ]
+                else
+                  [ S Map.empty, B behv
+                  , B $ Behaviour name Fail contract iface [Neg $ mconcat preconds] [] [] Nothing ]
+          return $ case actual of
+            Ok a -> a == expected
+            Bad _ -> False
+      ]
+
+  , testGroup "smt"
+      [ testProperty "generated smt is well typed (z3)" . noExponents $ typeCheckSMT Z3
+      , testProperty "generated smt is well typed (cvc4)" . noExponents $ typeCheckSMT CVC4
+      ]
   ]
 
+typeCheckSMT :: Solver -> GenT (Reader Bool) Property
+typeCheckSMT solver = do
+  behv <- genBehv 3
+  let smtconf = SMTConfig solver 1 False
+      smt = show . getSMT <$> mkPostconditionQueries (B behv)
+  pure . monadicIO . run $ and . fmap parseOutput <$> mapM (runSMT smtconf) smt
+    where
+      parseOutput (exitCode, stdout, _) = case exitCode of
+        ExitFailure _ -> False
+        ExitSuccess -> not . any (isPrefixOf "(error") . filter (/= "") . lines $ stdout
+
 
--- ** QuickCheck Generators ** --
+-- *** QuickCheck Generators *** --
 
 
 data Mode = Concrete | Symbolic deriving (Eq, Show)
@@ -73,7 +103,7 @@ data Names = Names { _ints :: [String]
 
    Storage conditions are currently not generated.
 -}
-genBehv :: Int -> Gen Behaviour
+genBehv :: Int -> ExpoGen Behaviour
 genBehv n = do
   name <- ident
   contract <- ident
@@ -94,7 +124,7 @@ genBehv n = do
                    }
 
 
-mkDecls :: Names -> Gen [Decl]
+mkDecls :: Names -> ExpoGen [Decl]
 mkDecls (Names ints bools bytes) = mapM mkDecl names
   where
     mkDecl (n, typ) = ((flip Decl) n) <$> (genType typ)
@@ -102,7 +132,7 @@ mkDecls (Names ints bools bytes) = mapM mkDecl names
     prepare typ ns = (,typ) <$> ns
 
 
-genType :: MType -> Gen AbiType
+genType :: MType -> ExpoGen AbiType
 genType typ = case typ of
   Integer -> oneof [ AbiUIntType <$> validIntSize
                    , AbiIntType <$> validIntSize
@@ -116,7 +146,7 @@ genType typ = case typ of
     validBytesSize = elements [1..32]
 
 
-genReturnExp :: Names -> Int -> Gen ReturnExp
+genReturnExp :: Names -> Int -> ExpoGen ReturnExp
 genReturnExp names n = oneof
   [ ExpInt <$> genExpInt names n
   , ExpBool <$> genExpBool names n
@@ -125,18 +155,17 @@ genReturnExp names n = oneof
 
 
 -- TODO: literals, cat slice, ITE, storage, ByStr
-genExpBytes :: Names -> Int -> Gen (Exp ByteString)
+genExpBytes :: Names -> Int -> ExpoGen (Exp ByteString)
 genExpBytes names _ = oneof
   [ ByVar <$> (selectName ByteStr names)
   , return $ ByEnv Blockhash
   ]
 
-
 -- TODO: ITE, storage
-genExpBool :: Names -> Int -> Gen (Exp Bool)
+genExpBool :: Names -> Int -> ExpoGen (Exp Bool)
 genExpBool names 0 = oneof
   [ BoolVar <$> (selectName Boolean names)
-  , LitBool <$> arbitrary
+  , LitBool <$> liftGen arbitrary
   ]
 genExpBool names n = oneof
   [ liftM2 And subExpBool subExpBool
@@ -158,9 +187,9 @@ genExpBool names n = oneof
 
 
 -- TODO: storage
-genExpInt :: Names -> Int -> Gen (Exp Integer)
+genExpInt :: Names -> Int -> ExpoGen (Exp Integer)
 genExpInt names 0 = oneof
-  [ LitInt <$> arbitrary
+  [ LitInt <$> liftGen arbitrary
   , IntVar <$> (selectName Integer names)
   , return $ IntEnv Caller
   , return $ IntEnv Callvalue
@@ -175,20 +204,24 @@ genExpInt names 0 = oneof
   , return $ IntEnv This
   , return $ IntEnv Nonce
   ]
-genExpInt names n = oneof
-  [ liftM2 Add subExpInt subExpInt
-  , liftM2 Sub subExpInt subExpInt
-  , liftM2 Mul subExpInt subExpInt
-  , liftM2 Div subExpInt subExpInt
-  , liftM2 Mod subExpInt subExpInt
-  , liftM2 Exp subExpInt subExpInt
-  , liftM3 ITE subExpBool subExpInt subExpInt
-  ]
+genExpInt names n = do
+  expo <- lift ask
+  oneof $
+    (if expo
+      then ((liftM2 Exp subExpInt subExpInt):)
+      else id)
+        [ liftM2 Add subExpInt subExpInt
+        , liftM2 Sub subExpInt subExpInt
+        , liftM2 Mul subExpInt subExpInt
+        , liftM2 Div subExpInt subExpInt
+        , liftM2 Mod subExpInt subExpInt
+        , liftM3 ITE subExpBool subExpInt subExpInt
+        ]
   where subExpInt = genExpInt names (n `div` 2)
         subExpBool = genExpBool names (n `div` 2)
 
 
-selectName :: MType -> Names -> Gen String
+selectName :: MType -> Names -> ExpoGen String
 selectName typ (Names ints bools bytes) = do
   let names = case typ of
                 Integer -> ints
@@ -201,7 +234,7 @@ selectName typ (Names ints bools bytes) = do
 -- |Generates a record type containing identifier names.
 -- Ensures each generated name appears once only.
 -- Names are seperated by type to ensure that e.g. an int expression does not reference a bool
-genNames :: Gen Names
+genNames :: ExpoGen Names
 genNames = mkNames <$> (split <$> unique)
   where
     mkNames :: [[String]] -> Names
@@ -210,7 +243,7 @@ genNames = mkNames <$> (split <$> unique)
                        , _bytes = cs!!2
                        }
 
-    unique :: Gen [String]
+    unique :: ExpoGen [String]
     unique = (Set.toList . Set.fromList <$> (listOf1 ident))
                 `suchThat` (\l -> (length l) > 3)
 
@@ -222,7 +255,7 @@ genNames = mkNames <$> (split <$> unique)
           where (as,bs) = splitAt n xs
 
 
-ident :: Gen String
+ident :: ExpoGen String
 ident = liftM2 (<>) (listOf1 (elements chars)) (listOf (elements $ chars <> digits))
           `suchThat` (`notElem` reserved)
   where
diff --git a/tests/frontend/pass/creation/create.act.typed.json b/tests/frontend/pass/creation/create.act.typed.json
index 3c18b51c..d5d031ea 100644
--- a/tests/frontend/pass/creation/create.act.typed.json
+++ b/tests/frontend/pass/creation/create.act.typed.json
@@ -16,7 +16,8 @@
     "kind": "Invariant",
     "predicate": "True",
     "preconditions": [],
-    "contract": "Modest"
+    "contract": "Modest",
+    "storagebounds": []
   },
   {
     "kind": "Constructor",
diff --git a/tests/frontend/pass/multi/multi.act.typed.json b/tests/frontend/pass/multi/multi.act.typed.json
index 8550c5eb..7e1ea78d 100644
--- a/tests/frontend/pass/multi/multi.act.typed.json
+++ b/tests/frontend/pass/multi/multi.act.typed.json
@@ -18,13 +18,15 @@
     "kind": "Invariant",
     "predicate": "True",
     "preconditions": [],
-    "contract": "a"
+    "contract": "a",
+    "storagebounds": []
   },
   {
     "kind": "Invariant",
     "predicate": "True",
     "preconditions": [],
-    "contract": "B"
+    "contract": "B",
+    "storagebounds": []
   },
   {
     "kind": "Constructor",
diff --git a/tests/frontend/pass/token/transfer.act.typed.json b/tests/frontend/pass/token/transfer.act.typed.json
index 6f2b9a1e..c22c5047 100644
--- a/tests/frontend/pass/token/transfer.act.typed.json
+++ b/tests/frontend/pass/token/transfer.act.typed.json
@@ -60,7 +60,10 @@
           }
         ],
         "symbol": "and"
-      },
+      }
+    ],
+    "contract": "Token",
+    "storagebounds": [
       {
         "arity": 2,
         "args": [
@@ -89,8 +92,7 @@
         ],
         "symbol": "and"
       }
-    ],
-    "contract": "Token"
+    ]
   },
   {
     "kind": "Invariant",
@@ -126,7 +128,8 @@
         "symbol": "and"
       }
     ],
-    "contract": "Token"
+    "contract": "Token",
+    "storagebounds": []
   },
   {
     "kind": "Invariant",
@@ -162,7 +165,8 @@
         "symbol": "and"
       }
     ],
-    "contract": "Token"
+    "contract": "Token",
+    "storagebounds": []
   },
   {
     "kind": "Constructor",
diff --git a/tests/invariants/fail/duplicated_argument_name.act b/tests/invariants/fail/duplicated_argument_name.act
new file mode 100644
index 00000000..7fcd902e
--- /dev/null
+++ b/tests/invariants/fail/duplicated_argument_name.act
@@ -0,0 +1,17 @@
+constructor of C
+interface constructor(uint _x)
+
+creates
+
+    uint x := _x
+
+invariants
+
+    x == _x
+
+behaviour f of C
+interface f(uint _x)
+
+storage
+
+    x => _x
diff --git a/tests/invariants/fail/constructor_indirect_assignment.act b/tests/invariants/pass/constructor_indirect_assignment.act
similarity index 100%
rename from tests/invariants/fail/constructor_indirect_assignment.act
rename to tests/invariants/pass/constructor_indirect_assignment.act
diff --git a/tests/invariants/pass/mapping-assignments.act b/tests/invariants/pass/mapping-assignments.act
new file mode 100644
index 00000000..cdda9008
--- /dev/null
+++ b/tests/invariants/pass/mapping-assignments.act
@@ -0,0 +1,11 @@
+constructor of C
+interface constructor()
+
+creates
+
+   uint a := 0
+   mapping(uint=>uint) b := [0 := 1]
+
+invariants
+
+  b[a] == 1