diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,14 @@
 
 ## Unreleased
 
+## 0.6.0.0 -- 2024-07-13
+
+* Fix a soundness bug that would cause equality saturation to be broken when
+  `VariablePattern` was used explicitly with low numbers such as 1,2,3...
+  This bug could also be triggered in the unlikely case when the hash of the
+  given IsString variable instance collided with the Var Ids internally
+  associated to NonVariablePatterns. Fixes #20 and #32.
+
 ## 0.5.0.0 -- 2023-10-31
 
 * Change `'modifyA'` to instead operate over e-graphs, instead of being
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -303,3 +303,10 @@
 open hegg-test.svg
 open hegg-test.eventlog.html
 ```
+
+## Coverage
+
+```
+cabal test hegg-test --enable-coverage --enable-library-coverage
+```
+
diff --git a/hegg.cabal b/hegg.cabal
--- a/hegg.cabal
+++ b/hegg.cabal
@@ -1,7 +1,7 @@
 cabal-version:      2.4
 name:               hegg
-version:            0.5.0.0
-Tested-With:        GHC ==9.6.2 || ==9.4.5 || ==9.2.7 || ==8.10.7
+version:            0.6.0.0
+Tested-With:        GHC ==9.10.1 || ==9.8.4 || ==9.6.7
 synopsis:           Fast equality saturation in Haskell
 
 description:        Fast equality saturation and equality graphs based on "egg:
@@ -101,8 +101,8 @@
     -- LANGUAGE extensions used by modules in this package.
     -- base-4.13, because foldMap' is used.
     build-depends:    base         >= 4.13 && < 5,
-                      transformers >= 0.4 && < 0.7,
-                      containers   >= 0.4 && < 0.7
+                      transformers >= 0.4 && < 0.8,
+                      containers   >= 0.4 && < 0.8
     if flag(vizdot)
         build-depends: graphviz >= 2999.20 && < 2999.21,
                        text
@@ -118,7 +118,7 @@
     hs-source-dirs:   test
     main-is:          Test.hs
     other-modules:    Invariants, Sym, Lambda, SimpleSym,
-                      T1, T2, T3
+                      T1, T2, T3, T32
 
     other-extensions: OverloadedStrings
     build-depends:    base,
diff --git a/src/Data/Equality/Matching.hs b/src/Data/Equality/Matching.hs
--- a/src/Data/Equality/Matching.hs
+++ b/src/Data/Equality/Matching.hs
@@ -10,7 +10,11 @@
     ( ematch
     , eGraphToDatabase
     , Match(..)
+
+    -- * Compiling a Pattern to a Query
     , compileToQuery
+    , VarsState(varNames), findVarName
+    , userPatVars
 
     , module Data.Equality.Matching.Pattern
     )
@@ -31,6 +35,7 @@
 import Data.Equality.Graph.Lens
 import Data.Equality.Matching.Database
 import Data.Equality.Matching.Pattern
+import Data.Coerce (coerce)
 
 -- | Matching a pattern on an e-graph returns the e-class in which the pattern
 -- was matched and an e-class substitution for every 'VariablePattern' in the pattern.
@@ -41,7 +46,8 @@
 
 -- TODO: Perhaps e-graph could carry database and rebuild it on rebuild
 
--- | Match a pattern against a 'Database', which can be gotten from an 'EGraph' with 'eGraphToDatabase'
+-- | Match a pattern 'Query', gotten from 'compileToQuery' on a 'Pattern',
+-- against a 'Database', which is built from an 'EGraph' with 'eGraphToDatabase'.
 --
 -- Returns a list of matches, one 'Match' for each set of valid substitutions
 -- for all variables and the equivalence class in which the pattern was matched.
@@ -50,21 +56,20 @@
 -- could be constructed only once and shared accross matching.
 ematch :: Language l
        => Database l
-       -> Pattern l
+       -> (Query l, Var {- query root var -})
        -> [Match]
-ematch db patr =
+ematch db (q, root) =
     let
-        (q, root) = compileToQuery patr
-
         -- | Convert each substitution into a match by getting the class-id
         -- where we matched from the subst
         --
         -- If the substitution is empty there is no match
         f :: Subst -> Maybe Match
-        f s = if IM.null s then Nothing
-                           else case IM.lookup root s of
-                                  Nothing -> error "how is root not in map?"
-                                  Just found -> pure (Match s found)
+        f s = if nullSubst s
+                then Nothing
+                else case lookupSubst root s of
+                  Nothing -> error "how is root not in map?"
+                  Just found -> pure (Match s found)
 
      in mapMaybe f (genericJoin db q)
 
@@ -97,24 +102,28 @@
 -- | Auxiliary result in 'compileToQuery' algorithm
 data AuxResult lang = {-# UNPACK #-} !Var :~ [Atom lang]
 
+
 -- | Compiles a 'Pattern' to a 'Query' and returns the query root variable with
 -- it.
 -- The root variable's substitutions are the e-classes where the pattern
 -- matched
-compileToQuery :: (Traversable lang) => Pattern lang -> (Query lang, Var)
-compileToQuery (VariablePattern x) = (SelectAllQuery x, x)
-compileToQuery pa@(NonVariablePattern _) =
+compileToQuery :: (Traversable lang) => Pattern lang -> ((Query lang, Var), VarsState)
+compileToQuery (VariablePattern n) = flip runState emptyVarsState $ do
+  v <- getVarName n
+  return (SelectAllQuery v, v)
+compileToQuery pa =
 
-  let root :~ atoms = evalState (aux pa) 0
-   in (Query (nubInt $ root:vars pa) atoms, root)
+  let (root :~ atoms, varsState) = runState (aux pa) emptyVarsState
+   in ((Query (nubVars $ root:userPatVars varsState) atoms, root), varsState)
 
     where
 
-        aux :: (Traversable lang) => Pattern lang -> State Int (AuxResult lang)
-        aux (VariablePattern x) = return (x :~ []) -- from definition in relational e-matching paper (needed for as base case for recursion)
+        aux :: (Traversable lang) => Pattern lang -> State VarsState (AuxResult lang)
+        aux (VariablePattern x) = do
+          v <- getVarName x
+          return (v :~ []) -- from definition in relational e-matching paper (needed for as base case for recursion)
         aux (NonVariablePattern p) = do
-            v <- get
-            modify' (+1)
+            v <- nextVar
             (toList -> auxs) <- traverse aux p
             let boundVars = map (\(b :~ _) -> b) auxs
                 atoms     = join $ map (\(_ :~ a) -> a) auxs
@@ -128,9 +137,48 @@
                     -- taking from the bound vars array
                     subPatsToVars :: Traversable lang => lang (Pattern lang) -> [Var] -> State Int (lang Var)
                     subPatsToVars p' boundVars = traverse (const $ (boundVars !!) <$> (get >>= \i -> modify' (+1) >> return i)) p'
-
-        -- | Return distinct variables in a pattern
-        vars :: Foldable lang => Pattern lang -> [Var]
-        vars (VariablePattern x) = [x]
-        vars (NonVariablePattern p) = nubInt $ join $ map vars $ toList p
 {-# INLINABLE compileToQuery #-}
+
+--------------------------------------------------------------------------------
+-- ** Vars utils for compileToQuery
+--------------------------------------------------------------------------------
+
+-- | Map user-given Variable names to internal 'Var's plus a counter
+data VarsState = VarsState
+  { varNames  :: !(M.Map String Var)
+  , nextVarId :: !Int
+  }
+
+-- | An empty 'VarsState'
+emptyVarsState :: VarsState
+emptyVarsState = VarsState mempty 0
+
+-- | Compute the next internal 'Var' from the current 'VarNameMap'
+nextVar :: State VarsState Var
+nextVar = do
+  n <- gets nextVarId
+  modify' (\vs -> vs{nextVarId = nextVarId vs +1})
+  return (MatchVar n)
+
+-- | Add a name to the 'VarNameMap' and get the resulting 'Var'.
+getVarName :: String -> State VarsState Var
+getVarName s = do
+  vm <- gets varNames
+  case M.lookup s vm of
+    Nothing -> do
+      n <- nextVar
+      modify' (\vs -> vs{varNames = M.insert s n (varNames vs)})
+      return n
+    Just v ->
+      return v
+
+findVarName :: VarsState -> String -> Var
+findVarName vs s = (varNames vs) M.! s
+
+-- | Return the variables given in a pattern by a user, from the 'VarsState'
+userPatVars :: VarsState -> [Var]
+userPatVars = M.elems . varNames
+
+-- | Deduplicate list of pattern Vars
+nubVars :: [Var] -> [Var]
+nubVars = coerce . nubInt . coerce
diff --git a/src/Data/Equality/Matching/Database.hs b/src/Data/Equality/Matching/Database.hs
--- a/src/Data/Equality/Matching/Database.hs
+++ b/src/Data/Equality/Matching/Database.hs
@@ -21,10 +21,15 @@
   , Database(..)
   , Query(..)
   , IntTrie(..)
-  , Subst
-  , Var
+  , Var(..)
   , Atom(..)
   , ClassIdOrVar(..)
+
+    -- * Subst
+  , Subst
+  , lookupSubst
+  , nullSubst
+  , sizeSubst
   ) where
 
 import Data.List (sortBy)
@@ -32,10 +37,10 @@
 import Data.Maybe (mapMaybe)
 import Control.Monad
 
-#if MIN_VERSION_base(4,20,0)
-import Data.Foldable as F (toList, length)
+#if !MIN_VERSION_base(4,20,0)
+import Data.Foldable (foldl')
 #endif
-import Data.Foldable as F (toList, foldl', length)
+import qualified Data.Foldable as F (toList, length)
 import qualified Data.Map.Strict    as M
 import qualified Data.IntMap.Strict as IM
 import qualified Data.IntSet as IS
@@ -43,6 +48,7 @@
 import Data.Equality.Graph.Classes.Id
 import Data.Equality.Graph.Nodes
 import Data.Equality.Language
+import Data.Coerce
 
 -- | A variable in a query is identified by an 'Int'.
 -- This is much more efficient than using e.g. a 'String'.
@@ -50,11 +56,8 @@
 -- As a consequence, patterns also use 'Int' to represent a variable, but we
 -- can still have an 'Data.String.IsString' instance for variable patterns by hashing the
 -- string into a unique number.
-type Var = Int
-
--- | Mapping from 'Var' to 'ClassId'. In a 'Subst' there is only one
--- substitution for each variable
-type Subst = IM.IntMap ClassId
+newtype Var = MatchVar { unsafeMatchVar :: Int }
+  deriving (Show, Eq, Ord)
 
 -- | A value which is either a 'ClassId' or a 'Var'
 data ClassIdOrVar = CClassId {-# UNPACK #-} !ClassId
@@ -70,7 +73,9 @@
 
 -- | A conjunctive query to be run on the database
 data Query lang
-    = Query ![Var] ![Atom lang]
+    = Query -- Q(x1,...,xk) <- R1(x11,...x1n), ..., Rn(xn1,...,xnn)
+        ![Var] {- query head -}
+        ![Atom lang] {- query body -}
     | SelectAllQuery {-# UNPACK #-} !Var
 
 -- | The relational representation of an e-graph, as described in section 3.1
@@ -117,19 +122,18 @@
 
 -- We want to match against ANYTHING, so we return a valid substitution for
 -- all existing e-class: get all relations and make a substition for each class in that relation, then join all substitutions across all classes
-genericJoin (DB m) (SelectAllQuery x) = concatMap (map (IM.singleton x) . IS.toList . tkeys) (M.elems m)
+genericJoin (DB m) (SelectAllQuery x) = concatMap (map (singleSubstVar x) . IS.toList . tkeys) (M.elems m)
 
 -- This is the last variable, so we return a valid substitution for every
 -- possible value for the variable (hence, we prepend @x@ to each and make it
 -- its own substitution)
--- ROMES:TODO: Start here. Map vars to indexs in an array and substitute in the resulting subst
 genericJoin d q@(Query _ atoms) = genericJoin' atoms (orderedVarsInQuery q)
 
  where
    genericJoin' :: [Atom l] -> [Var] -> [Subst]
    genericJoin' atoms' = \case
 
-     [] -> mempty <$> atoms'
+     [] -> const emptySubst <$> atoms'
 
      (!x):xs -> do
 
@@ -138,7 +142,7 @@
        -- Each valid sub-query assumes x -> x_in_D substitution
        y <- genericJoin' (substitute x x_in_D atoms') xs
 
-       return $! IM.insert x x_in_D y -- TODO: A bit contrieved, perhaps better to avoid map ?
+       return $! insertSubstVar x x_in_D y
 
    domainX :: Var -> [Atom l] -> [Int]
    domainX x = IS.toList . intersectAtoms x d . filter (x `elemOfAtom`)
@@ -170,11 +174,14 @@
 -- described in the paper (such as batching)
 orderedVarsInQuery :: (Functor lang, Foldable lang) => Query lang -> [Var]
 orderedVarsInQuery (SelectAllQuery x) = [x]
-orderedVarsInQuery (Query _ atoms) = IS.toList . IS.fromAscList $ sortBy (compare `on` varCost) $ mapMaybe toVar $ foldl' f mempty atoms
+orderedVarsInQuery (Query _ atoms) = coerce . IS.toList . IS.fromAscList . coerce $
+                                     sortBy (compare `on` varCost)                $
+                                     mapMaybe toVar                               $
+                                     foldl' f mempty atoms
     where
 
         f :: Foldable lang => [ClassIdOrVar] -> Atom lang -> [ClassIdOrVar]
-        f s (Atom v (toList -> l)) = v:(l <> s)
+        f s (Atom v (F.toList -> l)) = v:(l <> s)
         {-# INLINE f #-}
 
         -- First, prioritize variables that occur in many relations; second,
@@ -214,7 +221,7 @@
 
         -- If needed relation does exist, find intersection in it
         -- Add list of found intersections to existing
-        Just r  -> case intersectInTrie var mempty r (v:toList l) of
+        Just r  -> case intersectInTrie var emptySubst r (v:F.toList l) of
                      Nothing ->  error "intersectInTrie should return valid substitution for variable query"
                      Just xs -> xs
 
@@ -239,7 +246,7 @@
 --
 -- TODO: Really, a valid substitution is one which isn't empty...
 intersectInTrie :: Var -- ^ The variable whose domain we are looking for
-                -> IM.IntMap ClassId -- ^ A mapping from variables that have been substituted
+                -> Subst -- ^ A mapping from variables that have been substituted
                 -> IntTrie  -- ^ The trie
                 -> [ClassIdOrVar]  -- ^ The "query"
                 -> Maybe IS.IntSet -- ^ The resulting domain for a valid substitution
@@ -273,7 +280,7 @@
     --      continue the recursion again to validate the assumption and
     --      possibly find the domain of the variable we're looking for ahead
     --
-    CVar x:xs -> case IM.lookup x substs of
+    CVar x:xs -> case lookupSubst x substs of
         -- (2) or (4), we simply continue
         Just varVal -> IM.lookup varVal m >>= \next -> intersectInTrie var substs next xs
         -- (1) or (3)
@@ -287,14 +294,14 @@
             if all (isVarDifferentFrom x) xs
               then trieKeys
               else IM.foldrWithKey (\k ls (!acc) ->
-               case intersectInTrie var (IM.insert x k substs) ls xs of
+               case intersectInTrie var (insertSubstVar x k substs) ls xs of
                    Nothing -> acc
                    Just _  -> k `IS.insert` acc
                          ) mempty m
           -- (3)
           -- else IS.unions $ IM.elems $ IM.mapMaybeWithKey (\k ls -> intersectInTrie var (IM.insert x k substs) ls xs) m
           else IM.foldrWithKey (\k ls (!acc) ->
-            case intersectInTrie var (IM.insert x k substs) ls xs of
+            case intersectInTrie var (insertSubstVar x k substs) ls xs of
                 Nothing -> acc
                 Just rs -> rs <> acc) mempty m
     where
@@ -304,3 +311,36 @@
       isVarDifferentFrom _ (CClassId _) = False
       isVarDifferentFrom x (CVar     y) = x /= y
       {-# INLINE isVarDifferentFrom #-}
+
+--------------------------------------------------------------------------------
+-- * Subst
+--------------------------------------------------------------------------------
+
+-- | Mapping from 'Var' to 'ClassId'. In a 'Subst' there is only one
+-- substitution for each variable
+newtype Subst = Subst (IM.IntMap ClassId)
+
+-- | Insert a 'Var' in a 'Subst'
+insertSubstVar :: Var -> ClassId -> Subst -> Subst
+insertSubstVar (MatchVar k) v (Subst s) = Subst (IM.insert k v s)
+
+-- | Make a singleton 'Var' in a 'Subst'
+singleSubstVar :: Var -> ClassId -> Subst
+singleSubstVar (MatchVar k) v = Subst (IM.singleton k v)
+
+-- | Lookup a 'Var' in a 'Subst'
+lookupSubst :: Var -> Subst -> Maybe ClassId
+lookupSubst (MatchVar k) (Subst s) = IM.lookup k s
+
+-- | An empty substitution
+emptySubst :: Subst
+emptySubst = Subst IM.empty
+
+-- | Is the 'Subst' empty?
+nullSubst :: Subst -> Bool
+nullSubst (Subst s) = IM.null s
+
+sizeSubst :: Subst -> Int
+sizeSubst (Subst s) = IM.size s
+
+
diff --git a/src/Data/Equality/Matching/Pattern.hs b/src/Data/Equality/Matching/Pattern.hs
--- a/src/Data/Equality/Matching/Pattern.hs
+++ b/src/Data/Equality/Matching/Pattern.hs
@@ -7,9 +7,6 @@
 
 import Data.String
 
-import Data.Equality.Utils
-import Data.Equality.Matching.Database
-
 -- | A pattern can be either a variable or an non-variable expression of
 -- patterns.
 --
@@ -64,7 +61,7 @@
 -- @
 data Pattern lang
     = NonVariablePattern (lang (Pattern lang))
-    | VariablePattern Var -- ^ Should be a >0 positive number
+    | VariablePattern String
 
 -- | Synonym for 'NonVariablePattern'.
 --
@@ -93,5 +90,5 @@
     showsPrec d (NonVariablePattern x) = showsPrec d x
 
 instance IsString (Pattern lang) where
-    fromString = VariablePattern . hashString
+    fromString = VariablePattern
 
diff --git a/src/Data/Equality/Saturation.hs b/src/Data/Equality/Saturation.hs
--- a/src/Data/Equality/Saturation.hs
+++ b/src/Data/Equality/Saturation.hs
@@ -46,7 +46,6 @@
 
 import qualified Data.IntMap.Strict as IM
 
-import Data.Bifunctor
 import Control.Monad
 
 import Data.Equality.Utils
@@ -123,7 +122,9 @@
       -- Read-only phase, invariants are preserved
       -- With backoff scheduler
       -- ROMES:TODO parMap with chunks
-      let (!matches, newStats) = mconcat (fmap (\(rw_id,rw) -> first (map (rw,)) $ matchWithScheduler db i stats rw_id rw) (zip [1..] rewrites))
+      let (!matches, newStats) = mconcat (fmap (\(rw_id,rw) ->
+            let (ms, ss, vss) = matchWithScheduler db i stats rw_id rw
+             in (map (\m -> (rw,m,vss)) ms, ss)) (zip [1..] rewrites))
 
       -- Write-only phase, temporarily break invariants
       forM_ matches applyMatchesRhs
@@ -141,61 +142,64 @@
                 && IM.size afterClasses == IM.size beforeClasses)
           (runEqualitySaturation' (i+1) newStats)
 
-  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> Int -> Rewrite a l -> ([Match], IM.IntMap (Stat schd))
+  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> Int -> Rewrite a l
+                     -> ([Match], IM.IntMap (Stat schd), VarsState {- the vars mapping resulting from compiling the query -})
   matchWithScheduler db i stats rw_id = \case
       rw  :| _ -> matchWithScheduler db i stats rw_id rw
       lhs := _ -> do
+          let (lhs_query, varsState) = compileToQuery lhs
+
           case IM.lookup rw_id stats of
             -- If it's banned until some iteration, don't match this rule
             -- against anything.
-            Just s | isBanned @schd i s -> ([], stats)
+            Just s | isBanned @schd i s -> ([], stats, varsState)
 
             -- Otherwise, match and update stats
             x -> do
 
                 -- Match pattern
-                let matches' = ematch db lhs -- Add rewrite to the e-match substitutions
+                let matches' = ematch db lhs_query -- Add rewrite to the e-match substitutions
 
                 -- Backoff scheduler: update stats
                 let newStats = updateStats schd i rw_id x stats matches'
 
-                (matches', newStats)
+                (matches', newStats, varsState)
 
-  applyMatchesRhs :: (Rewrite a l, Match) -> EGraphM a l ()
+  applyMatchesRhs :: (Rewrite a l, Match, VarsState) -> EGraphM a l ()
   applyMatchesRhs =
       \case
-          (rw :| cond, m@(Match subst _)) -> do
+          (rw :| cond, m@(Match subst _), vss) -> do
               -- If the rewrite condition is satisfied, applyMatchesRhs on the rewrite rule.
               egr <- get
-              when (cond subst egr) $
-                 applyMatchesRhs (rw, m)
+              when (cond vss subst egr) $
+                 applyMatchesRhs (rw, m, vss)
 
-          (_ := VariablePattern v, Match subst eclass) -> do
+          (_ := VariablePattern v, Match subst eclass, vss) -> do
               -- rhs is equal to a variable, simply merge class where lhs
               -- pattern was found (@eclass@) and the eclass the pattern
               -- variable matched (@lookup v subst@)
-              case IM.lookup v subst of
+              case lookupSubst (findVarName vss v) subst of
                 Nothing -> error "impossible: couldn't find v in subst"
                 Just n  -> do
                     _ <- merge n eclass
                     return ()
 
-          (_ := NonVariablePattern rhs, Match subst eclass) -> do
+          (_ := NonVariablePattern rhs, Match subst eclass, vss) -> do
               -- rhs is (at the top level) a non-variable pattern, so substitute
               -- all pattern variables in the pattern and create a new e-node (and
               -- e-class that represents it), then merge the e-class of the
               -- substituted rhs with the class that matched the left hand side
-              eclass' <- reprPat subst rhs
+              eclass' <- reprPat vss subst rhs
               _ <- merge eclass eclass'
               return ()
 
   -- | Represent a pattern in the e-graph a pattern given substitions
-  reprPat :: Subst -> l (Pattern l) -> EGraphM a l ClassId
-  reprPat subst = add . Node <=< traverse \case
+  reprPat :: VarsState -> Subst -> l (Pattern l) -> EGraphM a l ClassId
+  reprPat vss subst = add . Node <=< traverse \case
       VariablePattern v ->
-          case IM.lookup v subst of
+          case lookupSubst (findVarName vss v) subst of
               Nothing -> error "impossible: couldn't find v in subst?"
               Just i  -> return i
-      NonVariablePattern p -> reprPat subst p
+      NonVariablePattern p -> reprPat vss subst p
 {-# INLINEABLE runEqualitySaturation #-}
 
diff --git a/src/Data/Equality/Saturation/Rewrites.hs b/src/Data/Equality/Saturation/Rewrites.hs
--- a/src/Data/Equality/Saturation/Rewrites.hs
+++ b/src/Data/Equality/Saturation/Rewrites.hs
@@ -49,7 +49,7 @@
 --      Just class_id ->
 --          egr^._class class_id._data /= Just 0
 -- @
-type RewriteCondition anl lang = Subst -> EGraph anl lang -> Bool
+type RewriteCondition anl lang = VarsState -> Subst -> EGraph anl lang -> Bool
 
 
 instance (∀ a. Show a => Show (lang a)) => Show (Rewrite anl lang) where
diff --git a/src/Data/Equality/Saturation/Scheduler.hs b/src/Data/Equality/Saturation/Scheduler.hs
--- a/src/Data/Equality/Saturation/Scheduler.hs
+++ b/src/Data/Equality/Saturation/Scheduler.hs
@@ -16,6 +16,7 @@
 
 import qualified Data.IntMap.Strict as IM
 import Data.Equality.Matching
+import Data.Equality.Matching.Database (sizeSubst)
 
 -- | A 'Scheduler' determines whether a certain rewrite rule is banned from
 -- being used based on statistics it defines and collects on applied rewrite
@@ -76,7 +77,7 @@
         where
 
           -- TODO: Overall difficult, and buggy at the moment.
-          total_len = sum (map (length . matchSubst) matches)
+          total_len = sum (map (sizeSubst . matchSubst) matches)
 
           bannedN = case currentStat of
                       Nothing -> 0;
diff --git a/src/Data/Equality/Utils.hs b/src/Data/Equality/Utils.hs
--- a/src/Data/Equality/Utils.hs
+++ b/src/Data/Equality/Utils.hs
@@ -9,7 +9,6 @@
 #else
 import Data.Foldable
 #endif
-import Data.Bits
 
 -- import qualified Data.Set    as S
 -- import qualified Data.IntSet as IS
@@ -35,15 +34,6 @@
 cata :: Functor f => (f a -> a) -> (Fix f -> a)
 cata f = f . fmap (cata f) . unFix
 {-# INLINE cata #-}
-
--- | Get the hash of a string.
---
--- This util is currently used to generate an 'Int' used for the internal
--- pattern variable representation from the external pattern variable
--- representation ('String')
-hashString :: String -> Int
-hashString = foldl' (\h c -> 33*h `xor` fromEnum c) 5381
-{-# INLINE hashString #-}
 
 -- -- | We don't have the parallel package, so roll our own simple parMap
 -- parMap :: (a -> b) -> [a] -> [b]
diff --git a/test/Invariants.hs b/test/Invariants.hs
--- a/test/Invariants.hs
+++ b/test/Invariants.hs
@@ -16,7 +16,6 @@
 
 import Control.Monad
 
-import qualified Data.Containers.ListUtils as LU
 import qualified Data.Foldable as F
 import qualified Data.List   as L
 import qualified Data.IntSet as IS
@@ -50,7 +49,7 @@
         _   -> False
     where
         eg :: EGraph () l
-        eg = snd $ equalitySaturation expr [VariablePattern 1:=fromInteger i] (error "Cost function shouldn't be used" :: CostFunction l Int)
+        eg = snd $ equalitySaturation expr [VariablePattern "1":=fromInteger i] (error "Cost function shouldn't be used" :: CostFunction l Int)
 
 -- | Test 'compileToQuery'.
 --
@@ -60,14 +59,14 @@
 -- The number of atoms should also match the number of non variable patterns
 -- since we should create an additional atom (with a new bound variable) for each. 
 testCompileToQuery :: Traversable lang => Pattern lang -> Bool
-testCompileToQuery p = case fst $ compileToQuery p of
-                         -- Handle special case for selectAll queries...
-                         SelectAllQuery x -> [x] == vars p && numNonVarPatterns p == 0
-                         q@(Query _ atoms)
-                           | [] <- queryHeadVars q   -> False
-                           | _:xs <- queryHeadVars q ->
-                               L.sort xs == L.sort (vars p)
-                                 && length atoms == numNonVarPatterns p
+testCompileToQuery p = case compileToQuery p of
+     -- Handle special case for selectAll queries...
+     ((SelectAllQuery x, _), vss) -> [x] == userPatVars vss && numNonVarPatterns p == 0
+     ((q@(Query _ atoms), _), vss)
+       | _:xs <- queryHeadVars q ->
+           L.sort xs == L.sort (userPatVars vss)
+             && length atoms == numNonVarPatterns p
+       | otherwise -> False
     where
         numNonVarPatterns :: Foldable lang => Pattern lang -> Int
         numNonVarPatterns (VariablePattern _) = 0
@@ -77,18 +76,14 @@
         queryHeadVars (SelectAllQuery x) = [x]
         queryHeadVars (Query qv _) = qv
 
-        -- | Return distinct variables in a pattern
-        vars :: Foldable lang => Pattern lang -> [Var]
-        vars (VariablePattern x) = [x]
-        vars (NonVariablePattern p') = LU.nubInt $ join $ map vars $ F.toList p'
-
 -- | If we match a singleton variable pattern against an e-graph, we should get
 -- a match on all e-classes in the e-graph
-ematchSingletonVar :: Language lang => Var -> EGraph () lang -> Bool
+ematchSingletonVar :: Language lang => String -> EGraph () lang -> Bool
 ematchSingletonVar v eg =
     let
         db = eGraphToDatabase eg
-        matches = IS.fromList $ map matchClassId $ ematch db (VariablePattern v)
+        (q, _) = compileToQuery (VariablePattern v)
+        matches = IS.fromList $ map matchClassId $ ematch db q
         eclasses = IM.keysSet (classes eg)
     in
         matches == eclasses 
@@ -181,7 +176,7 @@
 instance Arbitrary (Pattern SimpleExpr) where
     arbitrary = sized p'
       where
-        p' 0 = VariablePattern <$> oneof (return <$> [1..16])
+        p' 0 = VariablePattern <$> arbitrary
         p' n = NonVariablePattern <$> resize (n `div` 2) arbitrary
 
 newtype Name = Name { un :: String }
diff --git a/test/Lambda.hs b/test/Lambda.hs
--- a/test/Lambda.hs
+++ b/test/Lambda.hs
@@ -14,7 +14,6 @@
 
 import Data.Maybe
 
-import qualified Data.IntMap as IM
 import qualified Data.Set as S
 
 import Control.Applicative ((<|>))
@@ -111,17 +110,17 @@
     abs = error "todo..."
     signum = error "todo..."
 
-unsafeGetSubst :: Pattern Lambda -> D.Subst -> ClassId
-unsafeGetSubst (NonVariablePattern _) _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"
-unsafeGetSubst (VariablePattern v) subst = case IM.lookup v subst of
+unsafeGetSubst :: Pattern Lambda -> VarsState -> D.Subst -> ClassId
+unsafeGetSubst (NonVariablePattern _) _ _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"
+unsafeGetSubst (VariablePattern v) vss subst = case lookupSubst (findVarName vss v) subst of
       Nothing -> error "Searching for non existent bound var in conditional"
       Just class_id -> class_id
 
 isConst :: Pattern Lambda -> RewriteCondition LA Lambda
-isConst v subst egr = isJust $ snd $ egr^._class (unsafeGetSubst v subst)._data
+isConst v vss subst egr = isJust $ snd $ egr^._class (unsafeGetSubst v vss subst)._data
 
 isNotSameVar :: Pattern Lambda -> Pattern Lambda -> RewriteCondition LA Lambda
-isNotSameVar v1 v2 subst egr = find (unsafeGetSubst v1 subst) egr /= find (unsafeGetSubst v2 subst) egr
+isNotSameVar v1 v2 vss subst egr = find (unsafeGetSubst v1 vss subst) egr /= find (unsafeGetSubst v2 vss subst) egr
 
 rules :: [Rewrite LA Lambda]
 rules =
diff --git a/test/Sym.hs b/test/Sym.hs
--- a/test/Sym.hs
+++ b/test/Sym.hs
@@ -14,7 +14,6 @@
 import Test.Tasty
 import Test.Tasty.HUnit
 
-import qualified Data.IntMap.Strict as IM
 import qualified Data.Set    as S
 import Data.String
 import Data.Maybe (isJust)
@@ -148,28 +147,29 @@
     Sym _ -> Nothing
     Const x -> Just x
     
-unsafeGetSubst :: Pattern Expr -> Subst -> ClassId
-unsafeGetSubst (NonVariablePattern _) _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"
-unsafeGetSubst (VariablePattern v) subst = case IM.lookup v subst of
+unsafeGetSubst :: Pattern Expr -> VarsState -> Subst -> ClassId
+unsafeGetSubst (NonVariablePattern _) _ _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"
+unsafeGetSubst (VariablePattern v) vss subst = case lookupSubst (findVarName vss v) subst of
       Nothing -> error "Searching for non existent bound var in conditional"
       Just class_id -> class_id
 
+-- | TODO: This condition is incorrect. See #35
 is_not_zero :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
-is_not_zero v subst egr =
-    egr^._class (unsafeGetSubst v subst)._data /= Just 0
+is_not_zero v vss subst egr =
+    egr^._class (unsafeGetSubst v vss subst)._data /= Just 0
 
 is_sym :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
-is_sym v subst egr =
-    any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class (unsafeGetSubst v subst)._nodes)
+is_sym v vss subst egr =
+    any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class (unsafeGetSubst v vss subst)._nodes)
 
 is_const :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
-is_const v subst egr =
-    isJust (egr^._class (unsafeGetSubst v subst)._data)
+is_const v vss subst egr =
+    isJust (egr^._class (unsafeGetSubst v vss subst)._data)
 
 is_const_or_distinct_var :: Pattern Expr -> Pattern Expr -> RewriteCondition (Maybe Double) Expr
-is_const_or_distinct_var v w subst egr =
-    let v' = unsafeGetSubst v subst
-        w' = unsafeGetSubst w subst
+is_const_or_distinct_var v w vss subst egr =
+    let v' = unsafeGetSubst v vss subst
+        w' = unsafeGetSubst w vss subst
      in (eClassId (egr^._class v') /= eClassId (egr^._class w'))
         && (isJust (egr^._class v'._data)
             || any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class v'._nodes))
diff --git a/test/T32.hs b/test/T32.hs
new file mode 100644
--- /dev/null
+++ b/test/T32.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TypeApplications #-}
+module T32 where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Data.Equality.Utils
+import Data.Equality.Matching
+import Data.Equality.Saturation
+import Data.Equality.Graph
+import qualified Data.Equality.Graph as EG
+import Data.Equality.Saturation.Scheduler (defaultBackoffScheduler)
+import Data.Equality.Graph.Monad
+
+data SymExpr a = Symbol String
+               | a :+: a
+               deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
+infix 6 :+:
+
+-- This test tests that using "VariablePattern 1, VariablePattern 2,
+-- VariablePattern 3" in a rewrite rule succeeds, as opposed to using the
+-- IsString instance for Pattern.
+-- (Well, it tests that we can no longer screw up by writing the numbers
+-- directly as well. Now the implementation transforms the strings into Ids
+-- when compiling the pattern)
+rewrites :: [Rewrite () SymExpr]
+rewrites =
+  [ pat (VariablePattern "1" :+: pat (VariablePattern "2" :+: VariablePattern "3")) := pat (pat (VariablePattern "1" :+: VariablePattern "2") :+: VariablePattern "3")
+  ]
+
+e1, e1' :: Fix SymExpr
+e1 = Fix (Fix (Fix (Symbol "a") :+: Fix (Symbol "b")) :+: Fix (Symbol "c"))
+e1' = Fix (Fix (Symbol "a") :+: Fix (Fix (Symbol "b") :+: Fix (Symbol "c")))
+
+somePattern :: Pattern []
+somePattern = NonVariablePattern [VariablePattern "0",VariablePattern "1"] 
+
+-- Test basic associativity using pattern vars
+testT32 :: TestTree
+testT32 = testGroup "T32"
+    [ testCase "basic associativity with VarPattern 1,2,3" $
+        let
+          (e1_id, eg0)  = EG.represent @() e1 emptyEGraph
+          (e1'_id, eg1) = EG.represent @() e1' eg0
+          ((), eg2)     = runEGraphM eg1 (runEqualitySaturation defaultBackoffScheduler rewrites)
+          e1_canon      = EG.find e1_id eg2
+          e1'_canon     = EG.find e1'_id eg2
+         in e1_canon @?= e1'_canon
+    -- , testCase "compiling pattern" $
+    --     compileToQuery somePattern @?= Query ...
+    ]
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -10,6 +10,7 @@
 import Sym
 import Lambda
 import SimpleSym
+import T32
 
 import qualified T1
 import qualified T2
@@ -24,6 +25,7 @@
   , testCase "T1" (T1.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
   , testCase "T2" (T2.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
   , testCase "T3" (T3.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
+  , testT32
   ]
 
 main :: IO ()