diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc
index dd8e2155e..73df7189b 100644
--- a/src/bin/ltl2tgba.cc
+++ b/src/bin/ltl2tgba.cc
@@ -224,6 +224,7 @@ namespace
 	  break;
 	}
       delete aut;
+      f->destroy();
       flush_cout();
       return 0;
     }
diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc
index b908cc034..4e0ecd87e 100644
--- a/src/bin/ltl2tgta.cc
+++ b/src/bin/ltl2tgta.cc
@@ -229,6 +229,7 @@ namespace
 	}
 
       delete aut;
+      f->destroy();
       flush_cout();
       return 0;
     }
diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcheck.cc
index 65cc94a52..3c94faea5 100644
--- a/src/bin/ltlcheck.cc
+++ b/src/bin/ltlcheck.cc
@@ -143,11 +143,6 @@ bool want_stats = false;
 bool allow_dups = false;
 bool no_checks = false;
 
-typedef Sgi::hash_set<const spot::ltl::formula*,
-		      const spot::ptr_hash<const spot::ltl::formula> > fset_t;
-
-fset_t unique_set;
-
 std::vector<char*> translators;
 bool global_error_flag = false;
 
@@ -727,11 +722,23 @@ namespace
     return res;
   }
 
+  typedef
+  Sgi::hash_set<const spot::ltl::formula*,
+		const spot::ptr_hash<const spot::ltl::formula> > fset_t;
+
+
   class processor: public job_processor
   {
     translator_runner runner;
-
+    fset_t unique_set;
   public:
+    ~processor()
+    {
+      fset_t::iterator i = unique_set.begin();
+      while (i != unique_set.end())
+	(*i++)->destroy();
+    }
+
     int
     process_formula(const spot::ltl::formula* f,
 		    const char* filename = 0, int linenum = 0)
diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc
index 0f2cfc04f..e691b15da 100644
--- a/src/bin/ltlfilt.cc
+++ b/src/bin/ltlfilt.cc
@@ -340,6 +340,13 @@ namespace
     spot::ltl::ltl_simplifier& simpl;
     fset_t unique_set;
 
+    ~ltl_processor()
+    {
+      fset_t::iterator i = unique_set.begin();
+      while (i != unique_set.end())
+	(*i++)->destroy();
+    }
+
     ltl_processor(spot::ltl::ltl_simplifier& simpl)
     : simpl(simpl)
     {