diff --git a/include/LTL/Structures/CompoundStateSet.h b/include/LTL/Structures/CompoundStateSet.h
index 81da2659e..843f04e18 100644
--- a/include/LTL/Structures/CompoundStateSet.h
+++ b/include/LTL/Structures/CompoundStateSet.h
@@ -146,7 +146,7 @@ namespace LTL { namespace Structures {
             assert(this->_states.exists(stateid).first);
             return this->_states[stateid];
         }
-
+        
     private:
         stateid_t _parent = 0;
     };
diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp
index dd0b1b5d3..6110d8dbf 100644
--- a/src/LTL/Algorithm/TarjanModelChecker.cpp
+++ b/src/LTL/Algorithm/TarjanModelChecker.cpp
@@ -148,7 +148,7 @@ namespace LTL {
                 if (stateid == std::numeric_limits<idx_t>::max()) {
                     continue;
                 }
-
+                
                 if constexpr (SaveTrace) {
                     if (isnew) {
                         seen.set_history(stateid, successorGenerator.fired());
@@ -270,9 +270,11 @@ namespace LTL {
             // either way update the component ID of the state we came from.
             cstack[from]._lowlink = cstack[to]._lowlink;
             if constexpr (T::save_trace()) {
-                _loop_state = cstack[to]._stateid;
-                _loop_trans = successorGenerator.fired();
-                cstack[to]._lowsource = from;
+                if (_violation) {
+                    _loop_state = cstack[to]._stateid;
+                    _loop_trans = successorGenerator.fired();
+                    cstack[to]._lowsource = from;
+                }
             }
         }
     }
@@ -334,8 +336,8 @@ namespace LTL {
                 p = cstack[p]._lowsource;
             }
         }
-        if(!had_deadlock && _loop_trans < _net.numberOfTransitions())
-        {
+
+        if(!had_deadlock && _loop_trans < _net.numberOfTransitions()) {
             assert(_loop_trans < _net.numberOfTransitions());
             _trace.push_back({_loop_trans});
         }