diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index 287856a27..05532eb83 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -322,7 +322,7 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr
     go = \case
       TxValue -> [(fromString "txvalue", [])]
       v@(Balance a) -> [(fromString "balance_" <> formatEAddr a, [PLT v (Lit $ 2 ^ (96 :: Int))])]
-      Gas {} -> internalError "TODO: GAS"
+      Gas freshVar -> [(fromString ("gas_" <> show freshVar), [])]
       _ -> []
 
 referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
@@ -446,7 +446,7 @@ declareGasVars ps = SMT2 (["; gas variables"] <> fmap declare names) mempty memp
     names :: [Builder] = nubOrd $ concatMap (foldProp go mempty) ps
     go :: Expr a -> [Builder]
     go e = case e of
-      Gas g -> [fromLazyText $ T.pack $ show g]
+      Gas freshVar -> [fromLazyText $ T.pack $ show freshVar]
       _ -> []
 
 declareFrameContext :: [(Builder, [Prop])] -> Err SMT2