diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
index 114f834bd..fbdad7d7b 100644
--- a/src/nfa/operations.cc
+++ b/src/nfa/operations.cc
@@ -516,6 +516,16 @@ bool mata::nfa::Nfa::is_prfx_in_lang(const Run& run) const {
 }
 
 bool mata::nfa::Nfa::is_lang_empty(Run* cex) const {
+    //TOOD: hot fix for performance reasons for TACAS.
+    // Perhaps make the get_useful_states return a witness on demand somehow.
+    if (!cex) {
+        BoolVector useful_states = get_useful_states();
+        for (auto useful: useful_states)
+            if (useful)
+                return false;
+        return true;
+    }
+
     std::list<State> worklist(initial.begin(), initial.end());
     std::unordered_set<State> processed(initial.begin(), initial.end());
 
diff --git a/tests-integration/src/bench-bool-comb-cox-inter.cc b/tests-integration/src/bench-bool-comb-cox-inter.cc
index ee135743e..c916d0407 100644
--- a/tests-integration/src/bench-bool-comb-cox-inter.cc
+++ b/tests-integration/src/bench-bool-comb-cox-inter.cc
@@ -35,9 +35,15 @@ int main(int argc, char *argv[]) {
     TIME_BEGIN(intersection);
     Nfa intersect_aut = intersection(lhs, rhs);
     TIME_END(intersection);
+    std::cout<<"states: "<<intersect_aut.num_of_states()<<std::endl;
     TIME_BEGIN(is_lang_empty);
     intersect_aut.is_lang_empty();
     TIME_END(is_lang_empty);
+    //intersect_aut.final.clear();
+    TIME_BEGIN(trim);
+    intersect_aut.trim();
+    TIME_END(trim);
+    std::cout<<"states: "<<intersect_aut.num_of_states()<<std::endl;
 
     return EXIT_SUCCESS;
 }