diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc
index 767eec734..e20781729 100644
--- a/src/ltlvisit/reduce.cc
+++ b/src/ltlvisit/reduce.cc
@@ -27,7 +27,6 @@
 
 #include "lunabbrev.hh"
 #include "simpfg.hh"
-#include "nenoform.hh"
 #include "simplify.hh"
 
 namespace spot
@@ -68,10 +67,6 @@ namespace spot
 	  f1 = unabbreviate_logic(f);
 	  f2 = simplify_f_g(f1);
 	  f1->destroy();
-	  f1 = negative_normal_form(f2);
-	  f2->destroy();
-	  f2 = f1;
-
 	  f = simplifier.simplify(f2);
 	  f2->destroy();
 	}
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 39480fbcb..9d58c7982 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -2222,7 +2222,13 @@ namespace spot
     formula*
     ltl_simplifier::simplify(const formula* f)
     {
-      return const_cast<formula*>(simplify_recursively(f, cache_));
+      formula* neno = 0;
+      if (!f->is_in_nenoform())
+	f = neno = negative_normal_form(f);
+      formula* res = const_cast<formula*>(simplify_recursively(f, cache_));
+      if (neno)
+	neno->destroy();
+      return res;
     }
 
     formula*