diff --git a/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp b/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp
index 51095e4f1c923dc1189f2aee4761ec774643d8a2..741bddc720443f9eb98a523df1ef1653c74bd949 100644
--- a/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp
+++ b/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp
@@ -147,9 +147,7 @@ automaton::ExtendedNFA StateEliminationFormal::eliminateState(const automaton::E
             );
 
             // regexp::FormalRegExp transitionRegExp(opt.optimize(regexp::FormalRegExp(alt)));
-            regexp::FormalRegExp transitionRegExp(alt);
-            transitionRegExp.setAlphabet(extendedAutomaton.getInputAlphabet());
-            newAutomaton.addTransition(p, regexp::RegExp{transitionRegExp}, r);
+            newAutomaton.addTransition(p, regexp::RegExp{regexp::FormalRegExp(alt)}, r);
         }
     }
 
@@ -192,13 +190,8 @@ automaton::ExtendedNFA StateEliminationFormal::constructExtendedNFA(const automa
     extendedAutomaton.setFinalStates(automaton.getFinalStates());
 
     for(const auto& transition : automaton.getTransitions()) // pair<State, symb/eps> -> set<State>
-    {
-        regexp::FormalRegExp regexp(regexp::FormalRegExpSymbol(transition.first.second));
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
-
         for(const auto& to : transition.second)
-            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp}, to);
-    }
+            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp::FormalRegExp(regexp::FormalRegExpSymbol(transition.first.second))}, to);
 
     return extendedAutomaton;
 }
@@ -213,11 +206,7 @@ automaton::ExtendedNFA StateEliminationFormal::constructExtendedNFA(const automa
     extendedAutomaton.setFinalStates(automaton.getFinalStates());
 
     for(const auto& transition : automaton.getTransitions()) // pair<State, symb/eps> -> set<State>
-    {
-        regexp::FormalRegExp regexp(regexp::FormalRegExpSymbol(transition.first.second));
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
-        extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp}, transition.second);
-    }
+        extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp::FormalRegExp(regexp::FormalRegExpSymbol(transition.first.second))}, transition.second);
 
     return extendedAutomaton;
 }
@@ -232,22 +221,12 @@ automaton::ExtendedNFA StateEliminationFormal::constructExtendedNFA(const automa
     extendedAutomaton.setFinalStates(automaton.getFinalStates());
 
     for(const auto& transition : automaton.getSymbolTransitions()) // pair<State, symb/eps> -> set<State>
-    {
-        regexp::FormalRegExp regexp(regexp::FormalRegExpSymbol(transition.first.second));
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
-
         for(const auto& to : transition.second)
-            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp}, to);
-    }
-    for(const auto& transition : automaton.getEpsilonTransitions())
-    {
-        regexp::FormalRegExp regexp;
-        regexp.setRegExp(regexp::FormalRegExpEpsilon());
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
+            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp::FormalRegExp(regexp::FormalRegExpSymbol(transition.first.second))}, to);
 
+    for(const auto& transition : automaton.getEpsilonTransitions())
         for(const auto& to : transition.second)
-            extendedAutomaton.addTransition(transition.first, regexp::RegExp{regexp}, to);
-    }
+            extendedAutomaton.addTransition(transition.first, regexp::RegExp{regexp::FormalRegExp(regexp::FormalRegExpEpsilon())}, to);
 
     return extendedAutomaton;
 }
@@ -268,7 +247,6 @@ void StateEliminationFormal::extendExtendedNFA(automaton::ExtendedNFA& automaton
 
         regexp::FormalRegExp regexp;
         regexp.setRegExp(regexp::FormalRegExpEpsilon());
-        regexp.setAlphabet(automaton.getInputAlphabet());
         automaton.addTransition(q0, regexp::RegExp{regexp}, initState);
 
         const std::set<automaton::State> automatonInitialStates = automaton.getInitialStates();
@@ -287,7 +265,6 @@ void StateEliminationFormal::extendExtendedNFA(automaton::ExtendedNFA& automaton
         {
             regexp::FormalRegExp regexp;
             regexp.setRegExp(regexp::FormalRegExpEpsilon());
-            regexp.setAlphabet(automaton.getInputAlphabet());
             automaton.addTransition(state, regexp::RegExp{regexp}, f);
 
             automaton.removeFinalState(state);
diff --git a/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp b/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp
index 890e1454b1b26da31f6d1c04e1de93063b864d46..9ba6c2388f5cd93a67810c4c7edfda57af4d33e9 100644
--- a/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp
+++ b/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp
@@ -140,9 +140,7 @@ automaton::ExtendedNFA StateEliminationUnbounded::eliminateState(const automaton
             alt.appendElement(std::move(*transition(extendedAutomaton, p, r)));
             alt.appendElement(concat);
 
-            regexp::UnboundedRegExp transitionRegExp(opt.optimize(regexp::UnboundedRegExp(alt)));
-            transitionRegExp.setAlphabet(extendedAutomaton.getInputAlphabet());
-            newAutomaton.addTransition(p, regexp::RegExp{transitionRegExp}, r);
+            newAutomaton.addTransition(p, regexp::RegExp{regexp::UnboundedRegExp(opt.optimize(regexp::UnboundedRegExp(alt)))}, r);
         }
     }
 
@@ -171,13 +169,8 @@ automaton::ExtendedNFA StateEliminationUnbounded::constructExtendedNFA(const aut
     extendedAutomaton.setFinalStates(automaton.getFinalStates());
 
     for(const auto& transition : automaton.getTransitions()) // pair<State, symb/eps> -> set<State>
-    {
-        regexp::UnboundedRegExp regexp(regexp::UnboundedRegExpSymbol(transition.first.second));
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
-
         for(const auto& to : transition.second)
-            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp}, to);
-    }
+            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp::UnboundedRegExp(regexp::UnboundedRegExpSymbol(transition.first.second))}, to);
 
     return extendedAutomaton;
 }
@@ -192,11 +185,7 @@ automaton::ExtendedNFA StateEliminationUnbounded::constructExtendedNFA(const aut
     extendedAutomaton.setFinalStates(automaton.getFinalStates());
 
     for(const auto& transition : automaton.getTransitions()) // pair<State, symb/eps> -> set<State>
-    {
-        regexp::UnboundedRegExp regexp(regexp::UnboundedRegExpSymbol(transition.first.second));
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
-        extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp}, transition.second);
-    }
+        extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp::UnboundedRegExp(regexp::UnboundedRegExpSymbol(transition.first.second))}, transition.second);
 
     return extendedAutomaton;
 }
@@ -211,22 +200,12 @@ automaton::ExtendedNFA StateEliminationUnbounded::constructExtendedNFA(const aut
     extendedAutomaton.setFinalStates(automaton.getFinalStates());
 
     for(const auto& transition : automaton.getSymbolTransitions()) // pair<State, symb/eps> -> set<State>
-    {
-        regexp::UnboundedRegExp regexp(regexp::UnboundedRegExpSymbol(transition.first.second));
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
-
         for(const auto& to : transition.second)
-            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp}, to);
-    }
-    for(const auto& transition : automaton.getEpsilonTransitions())
-    {
-        regexp::UnboundedRegExp regexp;
-        regexp.setRegExp(regexp::UnboundedRegExpEpsilon());
-        regexp.setAlphabet(extendedAutomaton.getInputAlphabet());
+            extendedAutomaton.addTransition(transition.first.first, regexp::RegExp{regexp::UnboundedRegExp(regexp::UnboundedRegExpSymbol(transition.first.second))}, to);
 
+    for(const auto& transition : automaton.getEpsilonTransitions())
         for(const auto& to : transition.second)
-            extendedAutomaton.addTransition(transition.first, regexp::RegExp{regexp}, to);
-    }
+            extendedAutomaton.addTransition(transition.first, regexp::RegExp{regexp::UnboundedRegExp(regexp::UnboundedRegExpEpsilon())}, to);
 
     return extendedAutomaton;
 }
@@ -247,7 +226,6 @@ void StateEliminationUnbounded::extendExtendedNFA(automaton::ExtendedNFA& automa
 
         regexp::UnboundedRegExp regexp;
         regexp.setRegExp(regexp::UnboundedRegExpEpsilon());
-        regexp.setAlphabet(automaton.getInputAlphabet());
         automaton.addTransition(q0, regexp::RegExp{regexp}, initState);
 
         const std::set<automaton::State> automatonInitialStates = automaton.getInitialStates();
@@ -266,7 +244,6 @@ void StateEliminationUnbounded::extendExtendedNFA(automaton::ExtendedNFA& automa
         {
             regexp::UnboundedRegExp regexp;
             regexp.setRegExp(regexp::UnboundedRegExpEpsilon());
-            regexp.setAlphabet(automaton.getInputAlphabet());
             automaton.addTransition(state, regexp::RegExp{regexp}, f);
 
             automaton.removeFinalState(state);
diff --git a/alib2data/src/automaton/FSM/ExtendedNFA.cpp b/alib2data/src/automaton/FSM/ExtendedNFA.cpp
index f4912a9f42e3ab741740b814559aff6621d67b0d..8daf106b2cf9c02f6310ff5fe9f8ae21ce5e8340 100644
--- a/alib2data/src/automaton/FSM/ExtendedNFA.cpp
+++ b/alib2data/src/automaton/FSM/ExtendedNFA.cpp
@@ -54,11 +54,10 @@ bool ExtendedNFA::addTransition(const State& from, const regexp::RegExp& input,
 	if (states.find(from) == states.end())
 		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
 
-	std::set<alphabet::Symbol> inputRegExpAlphabetDiff;
 	std::set<alphabet::Symbol> inputRegExpAlphabet = regexp::RegExpAlphabetGetter::REG_EXP_ALPHABET_GETTER.getAlphabet(input);
 
-	std::set_difference(inputAlphabet.begin(), inputAlphabet.end(), inputRegExpAlphabet.begin(), inputRegExpAlphabet.end(), std::inserter(inputRegExpAlphabetDiff, inputRegExpAlphabetDiff.end()));
-	if (inputRegExpAlphabetDiff.size() != 0)
+	// Transition regexp's alphabet must be subset of automaton's alphabet
+	if (inputRegExpAlphabet.size() > 0 && ! std::includes(inputAlphabet.begin(), inputAlphabet.end(), inputRegExpAlphabet.begin(), inputRegExpAlphabet.end()))
 		throw AutomatonException("Input string is over different alphabet than automaton");
 
 	if (states.find(to) == states.end())
diff --git a/alib2data/test-src/automaton/AutomatonTest.cpp b/alib2data/test-src/automaton/AutomatonTest.cpp
index 8e9024a7f196d10fba7cb000a0499346eeb84c76..96a9ab9bed2c27475b30a995f6bc43929f911fa3 100644
--- a/alib2data/test-src/automaton/AutomatonTest.cpp
+++ b/alib2data/test-src/automaton/AutomatonTest.cpp
@@ -7,18 +7,26 @@
 #include "automaton/UnknownAutomaton.h"
 
 #include "automaton/FSM/DFA.h"
+#include "automaton/FSM/ExtendedNFA.h"
 #include "automaton/PDA/SinglePopDPDA.h"
 #include "automaton/PDA/DPDA.h"
 #include "automaton/AutomatonFromXMLParser.h"
 #include "automaton/AutomatonToXMLComposer.h"
 
+#include "automaton/AutomatonException.h"
+
 #include "factory/DataFactory.hpp"
 
 #include "label/StringLabel.h"
 #include "label/IntegerLabel.h"
+#include "label/CharacterLabel.h"
 #include "label/Label.h"
 #include "alphabet/LabeledSymbol.h"
 
+#include "regexp/RegExp.h"
+#include "regexp/unbounded/UnboundedRegExp.h"
+#include "regexp/unbounded/UnboundedRegExpElements.h"
+
 #include "automaton/FSM/FiniteAutomatonFromStringParser.h"
 #include "automaton/FSM/FiniteAutomatonToStringComposer.h"
 
@@ -253,3 +261,33 @@ void AutomatonTest::DPDATransitions() {
   automaton.addFinalState(automaton::State(label::Label(label::IntegerLabel(3))));
 
 }
+
+void AutomatonTest::testExtendedNFAAlphabet() {
+    automaton::ExtendedNFA automaton;
+    automaton::State s0(label::Label(label::IntegerLabel(0)));
+    automaton::State s1(label::Label(label::IntegerLabel(1)));
+    automaton.addState(s0);
+    automaton.addState(s1);
+
+    automaton.setInputSymbols({
+            alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('a')))),
+            alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('b'))))
+            });
+
+    regexp::UnboundedRegExpConcatenation goodConcat1, goodConcat2;
+    regexp::UnboundedRegExpConcatenation badConcat;
+
+    goodConcat1.appendElement(regexp::UnboundedRegExpSymbol(alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('a'))))));
+    goodConcat1.appendElement(regexp::UnboundedRegExpSymbol(alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('b'))))));
+
+    goodConcat2.appendElement(regexp::UnboundedRegExpSymbol(alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('b'))))));
+    goodConcat2.appendElement(regexp::UnboundedRegExpSymbol(alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('b'))))));
+
+    badConcat.appendElement(regexp::UnboundedRegExpSymbol(alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('b'))))));
+    badConcat.appendElement(regexp::UnboundedRegExpSymbol(alphabet::Symbol(alphabet::LabeledSymbol(label::Label(label::CharacterLabel('d'))))));
+
+    CPPUNIT_ASSERT_THROW(automaton.addTransition(s0, regexp::RegExp{regexp::UnboundedRegExp(badConcat)}, s1), automaton::AutomatonException);
+    CPPUNIT_ASSERT_NO_THROW(automaton.addTransition(s0, regexp::RegExp{regexp::UnboundedRegExp(goodConcat1)}, s1));
+    CPPUNIT_ASSERT_NO_THROW(automaton.addTransition(s0, regexp::RegExp{regexp::UnboundedRegExp(goodConcat2)}, s1));
+    CPPUNIT_ASSERT_NO_THROW(automaton.addTransition(s0, regexp::RegExp{regexp::UnboundedRegExp(regexp::UnboundedRegExpEpsilon())}, s1));
+}
diff --git a/alib2data/test-src/automaton/AutomatonTest.h b/alib2data/test-src/automaton/AutomatonTest.h
index 65db52d914286e6eb89427877c9a877ed2bcc985..1891cdc6a6725661e646459dc44589729c3d259c 100644
--- a/alib2data/test-src/automaton/AutomatonTest.h
+++ b/alib2data/test-src/automaton/AutomatonTest.h
@@ -11,6 +11,7 @@ class AutomatonTest : public CppUnit::TestFixture
   CPPUNIT_TEST( FSMStringParserTest );
   CPPUNIT_TEST( SinglePopDPDATransitions );
   CPPUNIT_TEST( DPDATransitions );
+  CPPUNIT_TEST( testExtendedNFAAlphabet );
   CPPUNIT_TEST_SUITE_END();
 
 public:
@@ -22,6 +23,7 @@ public:
   void FSMStringParserTest();
   void SinglePopDPDATransitions();
   void DPDATransitions();
+  void testExtendedNFAAlphabet();
 };
 
 #endif  // AUTOMATON_TEST_H_