diff --git a/src/Search/EpsilonElimination.hs b/src/Search/EpsilonElimination.hs
index a7a7c08151f4b9f21fa9caffcbcb48dc2794e8c8..09f39c31e07e680b6fb1d3284a3918a84950efd0 100644
--- a/src/Search/EpsilonElimination.hs
+++ b/src/Search/EpsilonElimination.hs
@@ -1,12 +1,15 @@
 module Search.EpsilonElimination
   ( eliminateEpsilons
   -- * Internal functions exported for easier testing
+  , mergeEquivalent
   , epsilonClosure
   , addTransitiveEdges
   , removeEpsilonEdges
   , removeUnreachableNodes
   ) where
 
+import           Data.Foldable
+
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
@@ -18,13 +21,54 @@ import           Search.Types
 eliminateEpsilons :: Vertex -> Graph -> Graph
 eliminateEpsilons start graph =
   let
-    closureMap = epsilonClosure graph
-    transitiveClosure = addTransitiveEdges graph closureMap
+    merged = mergeEquivalent graph
+    closureMap = epsilonClosure merged
+    transitiveClosure = addTransitiveEdges merged closureMap
     withoutEpsilons = removeEpsilonEdges transitiveClosure
     finalGraph = removeUnreachableNodes start withoutEpsilons
   in
     finalGraph
 
+-- | Merge equivalent nodes.
+--
+-- This is not part of the standard epsilon elimination algorithm, but it's what
+-- dOSEK does. Adjacent nodes are equivalent, if they are connected only through
+-- an epsilon transition and this is the _only_ outgoing edge of the first
+-- vertex. The process of merging those has to be iterated until nothing else is
+-- possible.
+mergeEquivalent :: Graph -> Graph
+mergeEquivalent graph = case msum $ S.map onlyEpsilonOutgoing (M.keysSet graph) of
+  Nothing -> graph  -- no more nodes to merge
+  Just (from, to) ->
+      let
+        -- Set outgoing edges of 'from' to outgoing edges of 'to'. It's ok to
+        -- overwrite the previous edges of 'from', since the only edge is always
+        -- the one to 'to'
+        edgesMerged = M.insert from (outgoing to graph) graph
+        -- Remove 'to' from the set of vertices
+        toRemoved = M.delete to edgesMerged
+        -- Update all edges pointing to 'to' to point to 'from'
+        referencesToToAltered = M.map (replace to from) toRemoved
+      in
+        mergeEquivalent referencesToToAltered
+
+  where
+    -- Decide if the outgoing edges of vertex are exactly one ɛ-transition
+    onlyEpsilonOutgoing vertex = case S.maxView (graph M.! vertex) of
+      Nothing -> Nothing -- No successors
+      Just (e, es)
+         -- One successor and it's an epsilon
+        | null es && isEpsilon e  -> Just (vertex, edgeTo e)
+        | otherwise -> Nothing
+
+    outgoing = M.findWithDefault S.empty
+
+    -- Replace all edges pointing to v1 with v2
+    replace v1 v2 = S.map (replaceEdge v1 v2)
+    replaceEdge v1 v2 edge
+      | edgeTo edge == v1  = edge { edgeTo = v2 }
+      | otherwise          = edge
+
 type Closure = Set Vertex
 
 -- | Compute the epsilon closure for all vertices.
@@ -83,8 +127,10 @@ removeUnreachableNodes start graph =
     getReachable visited node
       | node `S.member` visited = visited
       | otherwise =
-        S.foldr (\succ visited' -> getReachable visited' succ) (S.insert node visited) (successors node)
-    successors node = S.map edgeTo $ M.findWithDefault S.empty node graph
+        S.foldr (\succ visited' -> getReachable visited' succ) (S.insert node visited) (successors graph node)
+
+successors :: Graph -> Vertex -> Set Vertex
+successors graph node = S.map edgeTo $ M.findWithDefault S.empty node graph
 
 -- | Return true iff the edge is an ɛ-transition
 isEpsilon :: Edge -> Bool
diff --git a/src/Search/Search2.hs b/src/Search/Search2.hs
index 259d232909e33f80128955c096cdf039159e2e5b..6658eeca5643e10d743b9983f20de71e7a5cadd8 100644
--- a/src/Search/Search2.hs
+++ b/src/Search/Search2.hs
@@ -79,11 +79,14 @@ driver ee prog = driver' ee prog (Vertex "start" "" "")
 
 driver' :: EliminateEpsilons -> FilePath -> Vertex -> IO ()
 driver' elimEpsis prog startVertex = do
-  state <- newIORef (State M.empty (Just startVertex) M.empty Nothing [])
+  let startOS = Just "startOS"  -- first edge
+  state <- newIORef (State M.empty (Just startVertex) M.empty startOS [])
   oneProgRun prog state Nothing
 
   forever $ do
-    modifyIORef state $ \s -> s { curTrace = [], currentVertex = Just startVertex }
+    modifyIORef state $ \s -> s { curTrace = [], currentVertex = Just startVertex
+                                , currentSyscall = startOS
+                                }
     findOpenDecision <$> readIORef state >>= \case
       Nothing    -> do
         s <- readIORef state
diff --git a/test/Search/EpsilonEliminationSpec.hs b/test/Search/EpsilonEliminationSpec.hs
index 6006f1476f2e64b2a2267c5cf0b9da96c105128f..b3a46ff661905c395e63ec807bc999a0c0aa2e29 100644
--- a/test/Search/EpsilonEliminationSpec.hs
+++ b/test/Search/EpsilonEliminationSpec.hs
@@ -22,6 +22,7 @@ spec = do
   describe "addTransitiveEdges" addTransitiveEdgesSpec
   describe "removeEpsilonEdges" removeEpsilonEdgesSpec
   describe "removeUnreachableNodes" removeUnreachableNodesSpec
+  describe "mergeEquivalent" mergeEquivalentSpec
 
 eliminateEpsilonsSpec :: Spec
 eliminateEpsilonsSpec = do
@@ -63,6 +64,43 @@ eliminateEpsilonsSpec = do
                        ]
     in eliminateEpsilons (mkVertex "A") graph1 `shouldBe` graph2
 
+  it "merges equivalent states" $
+    let graph1 = mkGraph [ ("A", edges [(Nothing, "B")])
+                         , ("B", edges [(Just "a", "C")])
+                         , ("C", edges [(Just "b", "D")])
+                         , ("D", edges [(Just "c", "B")])
+                         ]
+        graph2 = mkGraph [ ("A", edges [(Just "a", "C")])
+                         , ("C", edges [(Just "b", "D")])
+                         , ("D", edges [(Just "c", "A")])
+                         ]
+    in eliminateEpsilons (mkVertex "A") graph1 `shouldBe`graph2
+
+mergeEquivalentSpec :: Spec
+mergeEquivalentSpec = do
+  it "does nothing without epsilon transitions" $
+    let graph = mkGraph [ ("A", edges [(Just "a", "B"), (Just "c", "C")])
+                        , ("B", edges [(Just "b", "C")])
+                        , ("C", [])
+                        ]
+    in mergeEquivalent graph `shouldBe` graph
+
+  it "Works for a very simple example" $
+    let graph1 = mkGraph [ ("A", edges [(Nothing, "B")])
+                         , ("B", [])
+                         ]
+        graph2 = mkGraph [ ("A", []) ]
+    in mergeEquivalent graph1 `shouldBe` graph2
+
+  it "collapses a graph with only epsilon transitions to a single node" $
+    let graph1 = mkGraph [ ("A", edges [(Nothing, "B")])
+                         , ("B", edges [(Nothing, "C"), (Nothing, "D")])
+                         , ("C", edges [(Nothing, "E")])
+                         , ("D", edges [(Nothing, "E")])
+                         ]
+        graph2 = mkGraph [ ("A", []) ]
+    in mergeEquivalent graph1 `shouldBe` graph2
+
 epsilonClosureSpec :: Spec
 epsilonClosureSpec = do
   it "Returns the identity map for a graph without epsilons" $