diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index 210d37a37..287856a27 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -220,6 +220,7 @@ assertPropsNoSimp psPreConc = do
   <> smt2Line ""
   <> (declareAddrs addresses)
   <> smt2Line ""
+  <> declareGasVars psPreConc
   <> (declareBufs toDeclarePsElim bufs stores)
   <> smt2Line ""
   <> (declareVars . nubOrd $ foldl (<>) [] allVars)
@@ -438,6 +439,16 @@ declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cex
     declare n = "(declare-fun " <> n <> " () Addr)"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
+declareGasVars :: [Prop] -> SMT2
+declareGasVars ps = SMT2 (["; gas variables"] <> fmap declare names) mempty mempty
+  where
+    declare n = "(declare-fun gas_" <> n <> " () (_ BitVec 256))"
+    names :: [Builder] = nubOrd $ concatMap (foldProp go mempty) ps
+    go :: Expr a -> [Builder]
+    go e = case e of
+      Gas g -> [fromLazyText $ T.pack $ show g]
+      _ -> []
+
 declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
 declareFrameContext names = do
   decls <- concatMapM declare names
@@ -845,6 +856,7 @@ exprToSMT = \case
     encPrev <- exprToSMT prev
     pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"
   SLoad idx store -> op2 "select" store idx
+  Gas freshVar -> pure $ fromLazyText $ "gas_"  <> (T.pack $ show freshVar)
 
   a -> internalError $ "TODO: implement: " <> show a
   where
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index e8e435221..7f1bc5942 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -286,7 +286,7 @@ data Expr (a :: EType) where
 
   Balance        :: Expr EAddr -> Expr EWord
 
-  Gas            :: Int                -- frame idx
+  Gas            :: Int                -- fresh gas variable
                  -> Expr EWord
 
   -- code