diff --git a/boost_tests/explicit_engine_test.cpp b/boost_tests/explicit_engine_test.cpp
index 0a55c93e8..f0369293c 100644
--- a/boost_tests/explicit_engine_test.cpp
+++ b/boost_tests/explicit_engine_test.cpp
@@ -16,18 +16,23 @@ BOOST_AUTO_TEST_CASE(DirectoryTest) {
     BOOST_REQUIRE(getenv("TEST_FILES"));
 }
 
-void test_explicit_engine(const char* fn, ExplicitColoredModelChecker::Result expected, size_t quid = 0) { 
+void test_explicit_engine(const char* fn, ExplicitColoredModelChecker::Result expected, size_t quid = 0,
+                          uint32_t kbound = 4, const char* expectedOutput = nullptr) {
     std::string model = std::string("/models/explicit-engine/") + fn + ".pnml";
     std::string query = std::string("/models/explicit-engine/") + fn + ".xml";
     std::set<size_t> qnums{quid};
     auto [queries, querynames, sset, options] = load_explicit(model, query, qnums);
-    options.kbound = 4;
+    options.kbound = kbound;
 
     ExplicitColoredModelChecker checker(sset, std::cout);
-    
-    auto result = checker.checkQuery(queries[0], options);
+    std::ostringstream output;
+    ColoredResultPrinter printer(quid, output, querynames[0], options.seed(), output);
+    auto result = checker.checkQuery(queries[0], options, expectedOutput ? &printer : nullptr);
     
     BOOST_REQUIRE_EQUAL(expected, result);
+    if (expectedOutput) {
+        BOOST_REQUIRE(output.str().find(expectedOutput) != std::string::npos);
+    }
 }
 
 BOOST_AUTO_TEST_CASE(SubtractionWithVars, * utf::timeout(5)) {
@@ -37,3 +42,9 @@ BOOST_AUTO_TEST_CASE(SubtractionWithVars, * utf::timeout(5)) {
 BOOST_AUTO_TEST_CASE(ReferendumColoredSubtraction, * utf::timeout(5)) {
     test_explicit_engine("referendum_colored_subtraction", ExplicitColoredModelChecker::Result::SATISFIED);
 }
+
+BOOST_AUTO_TEST_CASE(KBound, * utf::timeout(5)) {
+    test_explicit_engine("referendum_colored_subtraction", ExplicitColoredModelChecker::Result::UNSATISFIED, 1, 9,
+                         "FORMULA Ten voting tokens are reachable FALSE");
+    test_explicit_engine("referendum_colored_subtraction", ExplicitColoredModelChecker::Result::SATISFIED, 1, 10);
+}
diff --git a/boost_tests/models/explicit-engine/referendum_colored_subtraction.xml b/boost_tests/models/explicit-engine/referendum_colored_subtraction.xml
index 11b6091ff..51be9b88a 100644
--- a/boost_tests/models/explicit-engine/referendum_colored_subtraction.xml
+++ b/boost_tests/models/explicit-engine/referendum_colored_subtraction.xml
@@ -22,4 +22,21 @@
       </exists-path>
     </formula>
   </property>
+
+  <property>
+    <id>Ten voting tokens are reachable</id>
+    <description>Ten voting tokens are reachable</description>
+    <formula>
+      <exists-path>
+        <finally>
+          <integer-eq>
+            <tokens-count>
+              <place>Referendum_colored_voting</place>
+            </tokens-count>
+            <integer-constant>10</integer-constant>
+          </integer-eq>
+        </finally>
+      </exists-path>
+    </formula>
+  </property>
 </property-set>
diff --git a/include/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.h b/include/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.h
index 6509f7a74..360ecdcf6 100644
--- a/include/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.h
+++ b/include/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.h
@@ -36,10 +36,11 @@ namespace PetriEngine::ExplicitColored {
             const std::unordered_map<std::string, uint32_t>& placeNameIndices,
             const std::unordered_map<std::string, Transition_t>& transitionNameIndices,
             size_t seed,
-            bool createTrace
+            bool createTrace,
+            uint32_t kbound
         );
 
-        bool check(Strategy searchStrategy, ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption);
+        Reachability::AbstractHandler::Result check(Strategy searchStrategy, ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption);
         [[nodiscard]] const SearchStatistics& GetSearchStatistics() const;
         std::optional<uint64_t> getCounterExampleId() const;
         std::optional<std::vector<InternalTraceStep>> getTraceTo(uint64_t counterExampleId) const;
@@ -50,26 +51,28 @@ namespace PetriEngine::ExplicitColored {
         const ColoredPetriNet& _net;
         const ColoredSuccessorGenerator _successorGenerator;
         const size_t _seed;
+        uint32_t _kbound;
         bool _fullStatespace = true;
         bool _createTrace;
         StateMap _stateMap;
         SearchStatistics _searchStatistics;
         template <typename SuccessorGeneratorState>
-        [[nodiscard]] bool _search(Strategy searchStrategy);
+        [[nodiscard]] Reachability::AbstractHandler::Result _search(Strategy searchStrategy);
         [[nodiscard]] bool _check(const ColoredPetriNetMarking& state, size_t id) const;
+        [[nodiscard]] uint64_t _tokenCount(const ColoredPetriNetMarking& marking) const;
 
         template <typename T>
-        [[nodiscard]] bool _dfs();
+        [[nodiscard]] Reachability::AbstractHandler::Result _dfs();
         template <typename T>
-        [[nodiscard]] bool _bfs();
+        [[nodiscard]] Reachability::AbstractHandler::Result _bfs();
         template <typename T>
-        [[nodiscard]] bool _rdfs();
+        [[nodiscard]] Reachability::AbstractHandler::Result _rdfs();
         template <typename T>
-        [[nodiscard]] bool _bestfs();
+        [[nodiscard]] Reachability::AbstractHandler::Result _bestfs();
 
         template <template <typename> typename WaitingList, typename T>
-        [[nodiscard]] bool _genericSearch(WaitingList<T> waiting);
-        [[nodiscard]] bool _getResult(bool found, bool fullStatespace) const;
+        [[nodiscard]] Reachability::AbstractHandler::Result _genericSearch(WaitingList<T> waiting);
+        [[nodiscard]] Reachability::AbstractHandler::Result _getResult(bool found, bool fullStatespace) const;
     };
 }
 
diff --git a/include/PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h b/include/PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h
index ae0d4702e..4e40447ac 100644
--- a/include/PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h
+++ b/include/PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h
@@ -10,8 +10,9 @@ namespace PetriEngine::ExplicitColored {
         uint32_t endWaitingStates = 0;
         uint32_t peakWaitingStates = 0;
         uint32_t discoveredStates = 0;
+        uint64_t maxTokens = 0;
         size_t biggestEncoding = 0;
     };
 }
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.cpp b/src/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.cpp
index 5779f7c3b..2a9c8c8b1 100644
--- a/src/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.cpp
+++ b/src/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.cpp
@@ -18,10 +18,12 @@ namespace PetriEngine::ExplicitColored {
         const std::unordered_map<std::string, uint32_t>& placeNameIndices,
         const std::unordered_map<std::string, Transition_t>& transitionNameIndices,
         const size_t seed,
-        bool createTrace
+        bool createTrace,
+        const uint32_t kbound
     ) : _net(std::move(net)),
         _successorGenerator(ColoredSuccessorGenerator{_net}),
         _seed(seed),
+        _kbound(kbound),
         _createTrace(createTrace)
     {
         const ExplicitQueryPropositionCompiler queryCompiler(placeNameIndices, transitionNameIndices, _successorGenerator);
@@ -36,7 +38,7 @@ namespace PetriEngine::ExplicitColored {
         }
     }
 
-    bool ExplicitWorklist::check(const Strategy searchStrategy, const ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption) {
+    Reachability::AbstractHandler::Result ExplicitWorklist::check(const Strategy searchStrategy, const ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption) {
         if (coloredSuccessorGeneratorOption == ColoredSuccessorGeneratorOption::FIXED) {
             return _search<ColoredPetriNetStateFixed>(searchStrategy);
         }
@@ -75,13 +77,28 @@ namespace PetriEngine::ExplicitColored {
         return _gammaQuery->eval(_successorGenerator, state, id);
     }
 
+    uint64_t ExplicitWorklist::_tokenCount(const ColoredPetriNetMarking& marking) const {
+        uint64_t totalTokens = 0;
+        for (const auto& placeMarking : marking.markings) {
+            totalTokens += placeMarking.totalCount();
+        }
+        return totalTokens;
+    }
+
     template <template <typename> typename WaitingList, typename T>
-    bool ExplicitWorklist::_genericSearch(WaitingList<T> waiting) {
+    Reachability::AbstractHandler::Result ExplicitWorklist::_genericSearch(WaitingList<T> waiting) {
         ptrie::set<uint8_t> passed;
         ColoredEncoder encoder = ColoredEncoder{_net.getPlaces()};
         const auto& initialState = _net.initial();
         const auto earlyTerminationCondition = _quantifier == Quantifier::EF;
 
+        _searchStatistics.exploredStates = 1;
+        _searchStatistics.discoveredStates = 1;
+        _searchStatistics.maxTokens = _tokenCount(initialState);
+        if (_kbound != 0 && _searchStatistics.maxTokens > _kbound) {
+            return _getResult(false, encoder.isFullStatespace());
+        }
+
         auto size = encoder.encode(initialState);
         passed.insert(encoder.data(), size);
         if constexpr (std::is_same_v<T, ColoredPetriNetStateEven>) {
@@ -94,9 +111,6 @@ namespace PetriEngine::ExplicitColored {
             waiting.add(std::move(initial));
         }
 
-        _searchStatistics.exploredStates = 1;
-        _searchStatistics.discoveredStates = 1;
-
         if (_check(initialState, 0) == earlyTerminationCondition) {
             _counterExampleId = 0;
             return _getResult(true, encoder.isFullStatespace());
@@ -124,8 +138,14 @@ namespace PetriEngine::ExplicitColored {
 
             successor.shrink();
             const auto& marking = successor.marking;
-            size = encoder.encode(marking);
             _searchStatistics.discoveredStates++;
+            const auto tokens = _tokenCount(marking);
+            _searchStatistics.maxTokens = std::max(tokens, _searchStatistics.maxTokens);
+            if (_kbound != 0 && tokens > _kbound) {
+                continue;
+            }
+            
+            size = encoder.encode(marking);
             if (!passed.exists(encoder.data(), size).first) {
                 if (_createTrace) {
                     _stateMap.transitions.emplace(successor.id, traceStep);
@@ -149,7 +169,7 @@ namespace PetriEngine::ExplicitColored {
     }
 
     template<typename SuccessorGeneratorState>
-    bool ExplicitWorklist::_search(const Strategy searchStrategy) {
+    Reachability::AbstractHandler::Result ExplicitWorklist::_search(const Strategy searchStrategy) {
         switch (searchStrategy) {
             case Strategy::DEFAULT:
             case Strategy::DFS:
@@ -166,22 +186,22 @@ namespace PetriEngine::ExplicitColored {
     }
 
     template <typename T>
-    bool ExplicitWorklist::_dfs() {
+    Reachability::AbstractHandler::Result ExplicitWorklist::_dfs() {
         return _genericSearch<DFSStructure>(DFSStructure<T> {});
     }
 
     template <typename T>
-    bool ExplicitWorklist::_bfs() {
+    Reachability::AbstractHandler::Result ExplicitWorklist::_bfs() {
         return _genericSearch<BFSStructure>(BFSStructure<T> {});
     }
 
     template <typename T>
-    bool ExplicitWorklist::_rdfs() {
+    Reachability::AbstractHandler::Result ExplicitWorklist::_rdfs() {
         return _genericSearch<RDFSStructure>(RDFSStructure<T>(_seed));
     }
 
     template <typename T>
-    bool ExplicitWorklist::_bestfs() {
+    Reachability::AbstractHandler::Result ExplicitWorklist::_bestfs() {
         return _genericSearch<BestFSStructure>(
             BestFSStructure<T>(
                 _seed,
@@ -191,19 +211,16 @@ namespace PetriEngine::ExplicitColored {
             );
     }
 
-    bool ExplicitWorklist::_getResult(const bool found, const bool fullStatespace) const {
-        Reachability::ResultPrinter::Result res;
+    Reachability::AbstractHandler::Result ExplicitWorklist::_getResult(const bool found, const bool fullStatespace) const {
         if (!found && !fullStatespace) {
-            res = Reachability::ResultPrinter::Result::Unknown;
-        }else {
-            res = (
-           (!found && _quantifier == Quantifier::AG) ||
-           (found && _quantifier == Quantifier::EF))
-               ? Reachability::ResultPrinter::Result::Satisfied
-               : Reachability::ResultPrinter::Result::NotSatisfied;
+            return Reachability::AbstractHandler::Unknown;
         }
-        return res == Reachability::ResultPrinter::Result::Satisfied;
+
+        return ((!found && _quantifier == Quantifier::AG) ||
+                (found && _quantifier == Quantifier::EF))
+            ? Reachability::AbstractHandler::Satisfied
+            : Reachability::AbstractHandler::NotSatisfied;
     }
 }
 
-#endif //NAIVEWORKLIST_CPP
\ No newline at end of file
+#endif //NAIVEWORKLIST_CPP
diff --git a/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp b/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
index 72746a037..04da604c2 100644
--- a/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
+++ b/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
@@ -10,12 +10,13 @@ namespace PetriEngine::ExplicitColored {
         const ExplicitColoredTraceContext* trace
     ) const {
         _printCommon(result, {});
-        _stream << "STATS:" << std::endl
-                << "	discovered states:     " << searchStatistics.discoveredStates << std::endl
-                << "	explored states:       " << searchStatistics.exploredStates << std::endl
-                << "	peak waiting states:   " << searchStatistics.peakWaitingStates << std::endl
-                << "	end waiting states:    " << searchStatistics.endWaitingStates << std::endl
-                << "	biggest encoded state: " << searchStatistics.biggestEncoding << " bytes" << std::endl;
+        _stream << "STATS:\n"
+                << "	discovered states:     " << searchStatistics.discoveredStates << '\n'
+                << "	explored states:       " << searchStatistics.exploredStates << '\n'
+                << "	peak waiting states:   " << searchStatistics.peakWaitingStates << '\n'
+                << "	end waiting states:    " << searchStatistics.endWaitingStates << '\n'
+                << "	max tokens:            " << searchStatistics.maxTokens << '\n'
+                << "	biggest encoded state: " << searchStatistics.biggestEncoding << " bytes\n";
         if (trace != nullptr) {
             _printTrace(*trace);
         }
@@ -30,56 +31,56 @@ namespace PetriEngine::ExplicitColored {
         if (result == Reachability::AbstractHandler::Unknown) {
             return;
         }
-        std::cout << "FORMULA " << _queryName  << " ";
+        _stream << "FORMULA " << _queryName << " ";
         if (result == Reachability::AbstractHandler::Satisfied) {
-            std::cout << "TRUE ";
+            _stream << "TRUE ";
         } else if (result == Reachability::AbstractHandler::NotSatisfied) {
-            std::cout << "FALSE ";
+            _stream << "FALSE ";
         }
 
-        std::cout << "TECHNIQUES ";
+        _stream << "TECHNIQUES ";
         for (const auto& techniqueFlag : _techniqueFlags) {
-            std::cout << techniqueFlag << " ";
+            _stream << techniqueFlag << " ";
         }
 
         for (const auto& techniqueFlag : extraTechniques) {
-            std::cout << techniqueFlag << " ";
+            _stream << techniqueFlag << " ";
         }
 
-        std::cout << std::endl;
+        _stream << '\n';
         if (result == Reachability::AbstractHandler::Satisfied || result == Reachability::AbstractHandler::NotSatisfied) {
-            std::cout << "Query index " << _queryOffset << " was solved" << std::endl;
+            _stream << "Query index " << _queryOffset << " was solved\n";
         }
-        std::cout << std::endl;
+        _stream << '\n';
 
-        std::cout << "Query is ";
+        _stream << "Query is ";
         if (result == Reachability::AbstractHandler::NotSatisfied) {
-            std::cout << "NOT ";
+            _stream << "NOT ";
         }
 
-        std::cout << "satisfied" << std::endl;
+        _stream << "satisfied.\n";
     }
 
     void ColoredResultPrinter::_printTrace(const ExplicitColoredTraceContext& trace) const {
-        _traceStream << "Trace: " << std::endl;
-        _traceStream << "<trace>" << std::endl;
+        _traceStream << "Trace:\n";
+        _traceStream << "<trace>\n";
         for (const auto& step : trace.traceSteps) {
             if (!step.isInitial) {
-                _traceStream << "\t<transition id=" << std::quoted(step.transitionId) << ">" << std::endl;
-                _traceStream << "\t\t<bindings>" << std::endl;
+                _traceStream << "\t<transition id=" << std::quoted(step.transitionId) << ">\n";
+                _traceStream << "\t\t<bindings>" << '\n';
                 for (const auto& [variableId, value] : step.binding) {
-                    _traceStream << "\t\t\t<variable id=" << std::quoted(variableId) << ">" << std::endl;
-                    _traceStream << "\t\t\t\t<color>" << value << "</color>" << std::endl;
-                    _traceStream << "\t\t\t</variable>" << std::endl;
+                    _traceStream << "\t\t\t<variable id=" << std::quoted(variableId) << ">\n";
+                    _traceStream << "\t\t\t\t<color>" << value << "</color>\n";
+                    _traceStream << "\t\t\t</variable>\n";
                 }
-                _traceStream << "\t\t</bindings>" << std::endl;
-                _traceStream << "\t</transition>" << std::endl;
+                _traceStream << "\t\t</bindings>\n";
+                _traceStream << "\t</transition>\n";
             }
-            _traceStream << "\t<marking>" << std::endl;
+            _traceStream << "\t<marking>\n";
             _printMarkings(trace.cpnBuilder, step);
-            _traceStream << "\t</marking>" << std::endl;
+            _traceStream << "\t</marking>\n";
         }
-        _traceStream << "</trace>" << std::endl;
+        _traceStream << "</trace>\n";
     }
 
     void ColoredResultPrinter::_printMarkings(
@@ -135,11 +136,10 @@ namespace PetriEngine::ExplicitColored {
         {
             if (!traceTokens.empty())
             {
-                _traceStream << "\t\t<place id=" << std::quoted(place_id) << ">" << std::endl;
+                _traceStream << "\t\t<place id=" << std::quoted(place_id) << ">\n";
                 writer.writeInitialTokens(place_id);
-                _traceStream << "\t\t</place>" << std::endl;
+                _traceStream << "\t\t</place>\n";
             }
         }
     }
 }
-
diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp
index 3cc4d9b96..8face42e2 100644
--- a/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp
+++ b/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp
@@ -261,8 +261,8 @@ namespace PetriEngine::ExplicitColored {
 
         auto net = cpnBuilder.takeNet();
 
-        ExplicitWorklist worklist(net, query, cpnBuilder.getPlaceIndices(), cpnBuilder.getTransitionIndices(), options.seed(), options.trace != TraceLevel::None);
-        bool result = worklist.check(options.strategy, options.colored_sucessor_generator);
+        ExplicitWorklist worklist(net, query, cpnBuilder.getPlaceIndices(), cpnBuilder.getTransitionIndices(), options.seed(), options.trace != TraceLevel::None, options.kbound);
+        const auto worklistResult = worklist.check(options.strategy, options.colored_sucessor_generator);
 
         if (searchStatistics) {
             *searchStatistics = worklist.GetSearchStatistics();
@@ -279,7 +279,12 @@ namespace PetriEngine::ExplicitColored {
                 }
             }
         }
-        return std::make_pair(result ? Result::SATISFIED : Result::UNSATISFIED, std::move(traceContext));
+        const auto result = worklistResult == AbstractHandler::Satisfied
+            ? Result::SATISFIED
+            : worklistResult == AbstractHandler::NotSatisfied
+                ? Result::UNSATISFIED
+                : Result::UNKNOWN;
+        return std::make_pair(result, std::move(traceContext));
     }
 
     void ExplicitColoredModelChecker::_reduce(