diff --git a/regex-genex.cabal b/regex-genex.cabal
--- a/regex-genex.cabal
+++ b/regex-genex.cabal
@@ -1,9 +1,9 @@
 Name            : regex-genex
-Version         : 0.5.1
+Version         : 0.6.0
 license         : OtherLicense
 license-file    : LICENSE
 cabal-version   : >= 1.6
-copyright       : 2011-2012 Audrey Tang
+copyright       : 2011-2013 Audrey Tang
 maintainer      : Audrey Tang <audreyt@audreyt.org>
 category        : Text, Regex
 stability       : experimental
@@ -20,14 +20,14 @@
     other-modules:    Regex.Genex.Pure
     extensions      : ImplicitParams, NamedFieldPuns, ParallelListComp, PatternGuards, RecordWildCards
     build-depends:
-        base >= 3 && < 5, mtl, containers, sbv == 2.3, regex-tdfa, stream-monad, text, logict
+        base >= 3 && < 5, mtl, containers, sbv, regex-tdfa, stream-monad, text, logict
 
 executable genex
     main-is:            Main.hs
     hs-source-dirs:     . src
     extensions      : ImplicitParams, NamedFieldPuns, ParallelListComp, PatternGuards, RecordWildCards
     build-depends:
-        base >= 3 && < 5, mtl, containers, sbv == 2.3, regex-tdfa
+        base >= 3 && < 5, mtl, containers, sbv, regex-tdfa
 
 source-repository head
   type:     git
diff --git a/src/Regex/Genex.hs b/src/Regex/Genex.hs
--- a/src/Regex/Genex.hs
+++ b/src/Regex/Genex.hs
@@ -10,7 +10,7 @@
 <http://yices.csl.sri.com/download-yices2.shtml>
 
 -}
-module Regex.Genex (Model(..), genex, genexPure, genexPrint, genexModels) where
+module Regex.Genex (Model(..), genex, genexPure, genexPrint, genexModels, genexWith, regexMatch) where
 import Data.SBV
 import Data.SBV.Internals (SBV)
 import Data.Set (toList)
@@ -30,7 +30,8 @@
 -- | Given a list of regular repressions, returns all possible strings that matches every one of them.
 -- Guarantees to return shorter strings before longer ones.
 genex :: [String] -> IO [String]
-genex = genexWith getString
+genex = let ?maxRepeat = maxRepeatDefault
+        in genexWith getString
 
 -- | A match consists of a string (list of codepoints), and a rank representing alternation order.
 data Model = Model
@@ -41,11 +42,13 @@
 
 -- | Same as 'genex', but with the entire model returned instead.
 genexModels :: [String] -> IO [Model]
-genexModels = genexWith (getStringWith id)
+genexModels = let ?maxRepeat = maxRepeatDefault
+              in genexWith (getStringWith id)
 
 -- | Same as 'genexModels', but print the models to standard output instead.
 genexPrint :: [String] -> IO ()
-genexPrint = genexWith displayString
+genexPrint = let ?maxRepeat = maxRepeatDefault
+             in genexWith displayString
 
 -- | A pure and much faster variant of 'genex', but without support for
 --   back-references, anchors or word boundaries.
@@ -65,15 +68,18 @@
 maxHits :: Hits
 maxHits = maxBound -- 65535
 
-maxRepeat :: Int
-maxRepeat = 3 -- 7 and 15 are also good
+-- controlled by an implicit parameter, but this is the default
+-- when instantiated from functions that do not expose the implicit
+-- parameter to the user
+maxRepeatDefault :: Int
+maxRepeatDefault = 3 -- 7 and 15 are also good
 
 maxLength :: Len
 maxLength = maxBound -- 65535
 
 -- lengths p = let ?grp = mempty in IntSet.toList . fst $ runState (possibleLengths $ parse p) mempty
 
-minLen :: (?grp :: GroupLens) => Pattern -> Int
+minLen :: (?maxRepeat :: Int, ?grp :: GroupLens) => Pattern -> Int
 minLen p = case p of
     PEscape {getPatternChar = ch}
         | Data.Char.isDigit ch -> let num = charToDigit ch in
@@ -88,7 +94,7 @@
 type GroupLens = IntMap IntSet
 type BackReferences = IntSet
 
-possibleLengths :: (?grp :: GroupLens) => Pattern -> State (GroupLens, BackReferences) IntSet
+possibleLengths :: (?maxRepeat :: Int, ?grp :: GroupLens) => Pattern -> State (GroupLens, BackReferences) IntSet
 possibleLengths pat = case pat of
     _ | isOne pat -> one
     PGroup (Just idx) p -> do
@@ -112,9 +118,9 @@
         | Data.Char.isAlpha ch -> error $ "Unsupported escape: " ++ [ch]
         | otherwise -> one
     PBound low (Just high) p -> manyTimes p low high
-    PBound low _ p -> manyTimes p low (low+maxRepeat)
-    PPlus p -> manyTimes p 1 (maxRepeat+1)
-    PStar _ p -> manyTimes p 0 maxRepeat
+    PBound low _ p -> manyTimes p low (low + ?maxRepeat)
+    PPlus p -> manyTimes p 1 (?maxRepeat+1)
+    PStar _ p -> manyTimes p 0 ?maxRepeat
     PEmpty -> zero
     _ -> error $ show pat
     where
@@ -136,7 +142,7 @@
 charToDigit :: Char -> Int
 charToDigit ch = Data.Char.ord ch - Data.Char.ord '0'
 
-exactMatch :: (?pats :: [(Pattern, GroupLens)]) => Len -> Symbolic SBool
+exactMatch :: (?maxRepeat :: Int, ?pats :: [(Pattern, GroupLens)]) => Len -> Symbolic SBool
 exactMatch len = do
     str <- mkExistVars $ fromEnum len
     initialFlips <- mkExistVars 1
@@ -251,7 +257,7 @@
     isWhiteSpace = cur .== 32 ||| (9 .<= cur &&& 13 .>= cur &&& 11 ./= cur)
 
 
-match :: (?str :: Str, ?pat :: Pattern, ?grp :: GroupLens) => Status -> Status
+match :: (?maxRepeat :: Int, ?str :: Str, ?pat :: Pattern, ?grp :: GroupLens) => Status -> Status
 match s@Status{ pos, flips, captureAt, captureLen }
   | isOne ?pat = ite (pos .>= strLen) __FAIL__ one
   | otherwise = ite (pos + (toEnum $ minLen ?pat) .> strLen) __FAIL__ $ case ?pat of
@@ -300,7 +306,7 @@
           | otherwise  -> cond (ord ch .== cur)
     PBound low (Just high) p -> let s'@Status{ ok = ok' } = (let ?pat = PConcat (replicate low p) in match s) in
         if low == high then s' else ite ok' (let ?pat = p in (manyTimes s' $ high - low)) s'
-    PBound low _ p -> let ?pat = (PBound low (Just $ low+maxRepeat) p) in match s
+    PBound low _ p -> let ?pat = (PBound low (Just $ low + ?maxRepeat) p) in match s
     PPlus p ->
         let s'@Status{ok} = next p
             res = let ?pat = PStar True p in match s'
@@ -361,7 +367,7 @@
     where
     chr = Data.Char.chr . fromEnum
 
-genexWith :: Monoid a => ([SatResult] -> Hits -> (Hits -> IO a) -> IO a) -> [[Char]] -> IO a
+genexWith :: (?maxRepeat :: Int, Monoid a) => ([SatResult] -> Hits -> (Hits -> IO a) -> IO a) -> [[Char]] -> IO a
 genexWith f regexes = do
     let ?grp = mempty
     let p'lens = [ ((p', groupLens), lens)
@@ -373,7 +379,7 @@
     let lens = IntSet.toAscList $ foldl1 IntSet.intersection (map snd p'lens)
     tryWith f (filter (<= maxLength) $ map toEnum lens) 0
 
-tryWith :: (?pats :: [(Pattern, GroupLens)]) => 
+tryWith :: (?maxRepeat :: Int, ?pats :: [(Pattern, GroupLens)]) => 
     Monoid a => ResultHandler a -> [Len] -> Hits -> IO a
 tryWith _ [] _ = return mempty
 tryWith f (len:lens) acc = if len > maxLength then return mempty else do
@@ -394,3 +400,33 @@
 getString = getStringWith $ \Model{ modelChars } -> map chr modelChars
     where
     chr = Data.Char.chr . fromEnum
+
+-- Given a regex and a symbolic string, returns true if regex matches the string
+regexMatch :: (?maxRepeat :: Int) => [[Char]] -> Str -> Symbolic SBool
+regexMatch regexes str = do
+    let ?grp = mempty
+    let p'lens = [ ((p', groupLens), lens)
+                 | p <- [ if r == "" then PEmpty else parse r | r <- regexes ]
+                 , let (lens, (groupLens, backRefs)) = runState (possibleLengths p) mempty
+                 , let p' = normalize backRefs p
+                 ]
+    let ?pats = map fst p'lens
+    let lens = IntSet.toAscList $ foldl1 IntSet.intersection (map snd p'lens)
+    initialFlips <- mkExistVars 1
+    captureAt <- newArray_ (Just minBound)
+    captureLen <- newArray_ (Just minBound)
+    let ?str = str
+    let strLen = literal (fromIntegral (length str))
+    let initialStatus = Status
+            { ok = true
+            , pos = strLen
+            , flips = initialFlips
+            , captureAt = captureAt
+            , captureLen = captureLen
+            }
+        runPat s (pat, groupLens) = let ?pat = pat in let ?grp = groupLens in
+            ite (ok s &&& pos s .== strLen)
+                (match s{ pos = 0, captureAt, captureLen })
+                s{ ok = false, pos = maxBound, flips = [maxBound] }
+    let Status{ ok, pos, flips } = foldl runPat initialStatus ?pats
+    return (bAll (.== 0) flips &&& pos .== strLen &&& ok)
diff --git a/src/Regex/Genex/Pure.hs b/src/Regex/Genex/Pure.hs
--- a/src/Regex/Genex/Pure.hs
+++ b/src/Regex/Genex/Pure.hs
@@ -20,7 +20,7 @@
     Left x -> error $ show x
 
 genexPure :: [String] -> [String]
-genexPure = map T.unpack . foldl1 intersect . map (Stream.toList . run . normalize IntSet.empty . parse)
+genexPure = map T.unpack . foldl1 intersect . map (Stream.runStream . run . normalize IntSet.empty . parse)
 
 maxRepeat :: Int
 maxRepeat = 10