diff --git a/SSTG.cabal b/SSTG.cabal
--- a/SSTG.cabal
+++ b/SSTG.cabal
@@ -1,5 +1,5 @@
 name:                SSTG
-version:             0.1.1.5
+version:             0.1.1.6
 synopsis:            STG Symbolic Execution
 description:         Prototype of STG-based Symbolic Execution for Haskell.
 homepage:            https://github.com/AntonXue/SSTG#readme
diff --git a/src/SSTG/Core/Execution/Rules.hs b/src/SSTG/Core/Execution/Rules.hs
--- a/src/SSTG/Core/Execution/Rules.hs
+++ b/src/SSTG/Core/Execution/Rules.hs
@@ -138,9 +138,9 @@
   where
     pass_in = LiftAct rhs locals globals heap confs
     pass_rest = LiftAct rs locals' globals' heap' confs'
-    pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf
+    pass_out = LiftAct (hobj : hs) localsf globalsf heapf confsf
     LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in
-    LiftAct hos localsf globalsf heapf confsf = liftBindRhss pass_rest
+    LiftAct hs localsf globalsf heapf confsf = liftBindRhss pass_rest
 
 -- | Lift `Binds`.
 liftBinds :: LiftAct Binds -> LiftAct ()
@@ -167,19 +167,19 @@
 
 -- | `Default` `Alt` branches in a `Case`.
 defaultAlts :: [Alt] -> [Alt]
-defaultAlts alts = [a | a @ (Alt Default _ _) <- alts]
+defaultAlts alts = [a | a @ (Alt Default _) <- alts]
 
 -- | `AltCon` `Alt` branches in a `Case`.
-altConAlts :: [Alt] -> [Alt]
-altConAlts alts = [a | a @ (Alt acon _ _) <- alts, acon /= Default]
+nonDefaultAlts :: [Alt] -> [Alt]
+nonDefaultAlts alts = [a | a @ (Alt acon _) <- alts, acon /= Default]
 
 -- | Match `LitAlt` `Alt` branches.
 matchLitAlts :: Lit -> [Alt] -> [Alt]
-matchLitAlts lit alts = [a | a @ (Alt (LitAlt alit) _ _) <- alts, lit == alit]
+matchLitAlts lit alts = [a | a @ (Alt (LitAlt alit) _) <- alts, lit == alit]
 
 -- | Match `DataCon` `Alt` branches.
 matchDataAlts :: DataCon -> [Alt] -> [Alt]
-matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc) _ _) <- alts, dc == adc]
+matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc _) _) <- alts, dc == adc]
 
 -- | Negate `Constraint`.
 negateConstraint :: Constraint -> Constraint
@@ -189,7 +189,8 @@
 liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, [Constraint])
 liftSymAlt (LiftAct args locals globals heap confs) = pass_out
   where
-    (mvar, addr, cvar, Alt ac params expr) = args
+    (mvar, addr, cvar, Alt acon expr) = args
+    params = case acon of { DataAlt _ ps -> ps ; _ -> [] }
     snames = freshSeededNames (map varName params) confs
     svars = map (\(p, n) -> Var n (varType p)) (zip params snames)
     hobjs = map (\s -> SymObj (Symbol s Nothing)) svars
@@ -198,7 +199,7 @@
     kvs = (cvar, MemVal addr) : zip params mem_vals
     locals' = insertLocalsVals kvs locals
     mexpr = Atom (VarAtom mvar)
-    conss = [Constraint (ac, params) mexpr locals' True]
+    conss = [Constraint acon mexpr locals' True]
     confs' = snames ++ confs
     pass_out = LiftAct (expr, conss) locals' globals heap' confs'
 
@@ -351,7 +352,7 @@
 
   -- Rule Case Lit
   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code
-  , (Alt _ _ expr):_ <- matchLitAlts lit alts =
+  , (Alt _ expr):_ <- matchLitAlts lit alts =
     let locals' = insertLocalsVal (cvar, LitVal lit) locals
     in Just (RuleCaseLit
             ,[state { state_code = Evaluate expr locals' }])
@@ -360,7 +361,7 @@
   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code
   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap
   , ConObj dcon vals <- hobj
-  , (Alt _ params expr):_ <- matchDataAlts dcon alts
+  , (Alt (DataAlt _ params) expr):_ <- matchDataAlts dcon alts
   , length params == length vals =
     let kvs = (cvar, MemVal addr) : zip params vals
         locals' = insertLocalsVals kvs locals
@@ -370,7 +371,7 @@
   -- Rule Case Any Lit
   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code
   , [] <- matchLitAlts lit alts
-  , (Alt _ _ expr):_ <- defaultAlts alts =
+  , (Alt _ expr):_ <- defaultAlts alts =
     let locals' = insertLocalsVal (cvar, LitVal lit) locals
     in Just (RuleCaseAnyLit
             ,[state { state_code = Evaluate expr locals' }])
@@ -380,7 +381,7 @@
   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap
   , ConObj dcon _ <- hobj
   , [] <- matchDataAlts dcon alts
-  , (Alt _ _ expr):_ <- defaultAlts alts =
+  , (Alt _ expr):_ <- defaultAlts alts =
     let locals' = insertLocalsVal (cvar, MemVal addr) locals
     in Just (RuleCaseAnyConPtr
             ,[state { state_code = Evaluate expr locals' }])
@@ -389,23 +390,23 @@
   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code
   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap
   , SymObj _ <- hobj
-  , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)
-  , length (acon_alts ++ def_alts) > 0 =
-    let acon_ins = map (\a -> LiftAct (mvar, addr, cvar, a)
-                                      locals globals heap confs) acon_alts
-        acon_lifts = map liftSymAlt acon_ins
+  , (ndef_alts, def_alts) <- (nonDefaultAlts alts, defaultAlts alts)
+  , length (ndef_alts ++ def_alts) > 0 =
+    let ndef_ins = map (\a -> LiftAct (mvar, addr, cvar, a)
+                                      locals globals heap confs) ndef_alts
+        ndef_lifts = map liftSymAlt ndef_ins
         def_ins = map (\a -> LiftAct (mvar, addr, cvar, a)
                                      locals globals heap confs) def_alts
         def_lifts = map liftSymAlt def_ins
         -- Make AltCon states first.
-        acon_sts = map (liftedAltToState state) acon_lifts
+        ndef_sts = map (liftedAltToState state) ndef_lifts
         -- Make DEFAULT states next.
-        all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts
+        all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) ndef_lifts
         negatives = map negateConstraint all_conss
         def_lifts' = map (\(LiftAct (e, _) l g h c) ->
                            (LiftAct (e, negatives) l g h c)) def_lifts
         def_sts = map (liftedAltToState state) def_lifts'
-    in Just (RuleCaseSym, acon_sts ++ def_sts)
+    in Just (RuleCaseSym, ndef_sts ++ def_sts)
 
 -- Stack Dependent Rules
 
diff --git a/src/SSTG/Core/Execution/Support.hs b/src/SSTG/Core/Execution/Support.hs
--- a/src/SSTG/Core/Execution/Support.hs
+++ b/src/SSTG/Core/Execution/Support.hs
@@ -165,8 +165,7 @@
 newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)
 
 -- | Constraints denote logical paths taken in program execution thus far.
-data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool
-                deriving (Show, Eq, Read)
+data Constraint = Constraint AltCon Expr Locals Bool deriving (Show, Eq, Read)
 
 -- Simple functions that require only the immediate data structure.
 
diff --git a/src/SSTG/Core/Language/Naming.hs b/src/SSTG/Core/Language/Naming.hs
--- a/src/SSTG/Core/Language/Naming.hs
+++ b/src/SSTG/Core/Language/Naming.hs
@@ -65,7 +65,12 @@
 
 -- | `Name`s in an `Alt`.
 altNames :: Alt -> [Name]
-altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr
+altNames (Alt acon expr) = altConNames acon ++ exprNames expr
+
+-- | `Name`s in an `AltCon`.
+altConNames :: AltCon -> [Name]
+altConNames (DataAlt dcon ps) = dataConNames dcon ++ concatMap varNames ps
+altConNames _ = []
 
 -- | `Name`s in a `Type`.
 typeNames :: Type -> [Name]
diff --git a/src/SSTG/Core/Language/Syntax.hs b/src/SSTG/Core/Language/Syntax.hs
--- a/src/SSTG/Core/Language/Syntax.hs
+++ b/src/SSTG/Core/Language/Syntax.hs
@@ -60,10 +60,10 @@
 
 -- | Alternatives utilize an `AltCon`, a list of parameters of that match to
 -- the appropriate `DataAlt` as applicable, and an expression for the result.
-data Alt = Alt AltCon [Var] Expr deriving (Show, Eq, Read)
+data Alt = Alt AltCon Expr deriving (Show, Eq, Read)
 
 -- | Alt Constructor
-data AltCon = DataAlt DataCon
+data AltCon = DataAlt DataCon [Var]
             | LitAlt Lit
             | Default
             deriving (Show, Eq, Read)
diff --git a/src/SSTG/Core/Language/Typing.hs b/src/SSTG/Core/Language/Typing.hs
--- a/src/SSTG/Core/Language/Typing.hs
+++ b/src/SSTG/Core/Language/Typing.hs
@@ -38,7 +38,7 @@
 
 -- | Alt type
 altType :: Alt -> Type
-altType (Alt _ _ expr) = exprType expr
+altType (Alt _ expr) = exprType expr
 
 -- | I wonder what this could possibly be?
 exprType :: Expr -> Type
diff --git a/src/SSTG/Core/Translation/Haskell.hs b/src/SSTG/Core/Translation/Haskell.hs
--- a/src/SSTG/Core/Translation/Haskell.hs
+++ b/src/SSTG/Core/Translation/Haskell.hs
@@ -172,13 +172,13 @@
 
 -- | Make SSTG `Alt`.
 mkAlt :: StgAlt -> SL.Alt
-mkAlt (a, b, _, e) = SL.Alt (mkAltCon a) (map mkVar b) (mkExpr e)
+mkAlt (a, ps, _, e) = SL.Alt (mkAltCon a ps) (mkExpr e)
 
 -- | Make SSTG `AltCon`.
-mkAltCon :: AltCon -> SL.AltCon
-mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc)
-mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit)
-mkAltCon (DEFAULT) = SL.Default
+mkAltCon :: AltCon -> [Var] -> SL.AltCon
+mkAltCon (DataAlt dcon) params = SL.DataAlt (mkData dcon) (map mkVar params)
+mkAltCon (LitAlt lit) _ = SL.LitAlt (mkLit lit)
+mkAltCon (DEFAULT) _ = SL.Default
 
 -- | Make SSTG `Type`.
 mkType :: Type -> SL.Type
diff --git a/src/SSTG/Utils/Printing.hs b/src/SSTG/Utils/Printing.hs
--- a/src/SSTG/Utils/Printing.hs
+++ b/src/SSTG/Utils/Printing.hs
@@ -283,11 +283,12 @@
 
 -- | Print `AltCon`.
 pprAltConStr :: AltCon -> String
-pprAltConStr (DataAlt dcon) = injSpace acc_strs
+pprAltConStr (DataAlt dcon params) = injSpace acc_strs
   where
     header = "DataAlt"
     dcon_str = (sub . pprDataConStr) dcon
-    acc_strs = [header, dcon_str]
+    ps_str = injIntoList (map pprVarStr params)
+    acc_strs = [header, dcon_str, ps_str]
 pprAltConStr (LitAlt lit) = injSpace acc_strs
   where
     header = "LitAlt"
@@ -297,13 +298,12 @@
 
 -- | Print `Alt`.
 pprAltStr :: Alt -> String
-pprAltStr (Alt acon var expr) = injSpace acc_strs
+pprAltStr (Alt acon expr) = injSpace acc_strs
   where
     header = "Alt"
     acon_str = (sub . pprAltConStr) acon
-    vars_str = injIntoList (map pprVarStr var)
     expr_str = (sub . pprExprStr) expr
-    acc_strs = [header, acon_str, vars_str, expr_str]
+    acc_strs = [header, acon_str, expr_str]
 
 -- | Print a list of `Alt`s.
 pprAltsStr :: [Alt] -> String
@@ -410,12 +410,11 @@
 
 -- | Print `PathCond`.
 pprConstraintStr :: Constraint -> String
-pprConstraintStr (Constraint (ac, ps) expr locals hold) = injIntoList acc_strs
+pprConstraintStr (Constraint acon expr locals hold) = injIntoList acc_strs
   where
-    acon_str = pprAltConStr ac
-    prms_str = injIntoList (map pprVarStr ps)
+    acon_str = pprAltConStr acon
     expr_str = pprExprStr expr
     locs_str = pprLocalsStr locals
     hold_str = if hold then "Positive" else "Negative"
-    acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]
+    acc_strs = [acon_str, expr_str, locs_str, hold_str]