diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index b9758f9c9..06e4ea9f3 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
-## Recherche et Développement de l'Epita (LRDE).
+## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
+## de Recherche et Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ## Université Pierre et Marie Curie.
@@ -44,8 +44,7 @@ check_PROGRAMS = \
   syntimpl \
   tostring \
   tunabbrev \
-  tunenoform \
-  unabbrevwm
+  tunenoform
 
 consterm_SOURCES = consterm.cc
 equals_SOURCES = equalsf.cc
@@ -74,8 +73,6 @@ tunabbrev_SOURCES = equalsf.cc
 tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
 tunenoform_SOURCES = equalsf.cc
 tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV
-unabbrevwm_SOURCES = equals.cc
-unabbrevwm_CPPFLAGS = $(AM_CPPFLAGS) -DWM
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
deleted file mode 100644
index b88589330..000000000
--- a/src/ltltest/equals.cc
+++ /dev/null
@@ -1,203 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
-// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
-// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#include <iostream>
-#include <cassert>
-#include <cstdlib>
-#include <cstring>
-#include "ltlparse/public.hh"
-#include "ltlvisit/lunabbrev.hh"
-#include "ltlvisit/tunabbrev.hh"
-#include "ltlvisit/dump.hh"
-#include "ltlvisit/wmunabbrev.hh"
-#include "ltlvisit/nenoform.hh"
-#include "ltlast/allnodes.hh"
-#include "ltlvisit/simplify.hh"
-#include "ltlvisit/tostring.hh"
-
-void
-syntax(char* prog)
-{
-  std::cerr << prog << " [-E] formula1 formula2" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  bool check_first = true;
-
-  if (argc > 1 && !strcmp(argv[1], "-E"))
-    {
-      check_first = false;
-      argv[1] = argv[0];
-      ++argv;
-      --argc;
-    }
-  if (argc != 3)
-    syntax(argv[0]);
-
-  spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
-
-  if (check_first && spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
-    return 2;
-
-  spot::ltl::parse_error_list p2;
-  const spot::ltl::formula* f2 = spot::ltl::parse(argv[2], p2);
-
-  if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
-    return 2;
-
-  int exit_code = 0;
-
-  {
-#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
-    const spot::ltl::formula* tmp;
-#endif
-#ifdef LUNABBREV
-    tmp = f1;
-    f1 = spot::ltl::unabbreviate_logic(f1);
-    tmp->destroy();
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-#ifdef TUNABBREV
-    tmp = f1;
-    f1 = spot::ltl::unabbreviate_ltl(f1);
-    tmp->destroy();
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-#ifdef WM
-    tmp = f1;
-    f1 = spot::ltl::unabbreviate_wm(f1);
-    tmp->destroy();
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-#ifdef NENOFORM
-    tmp = f1;
-    f1 = spot::ltl::negative_normal_form(f1);
-    tmp->destroy();
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-#ifdef REDUC
-    spot::ltl::ltl_simplifier_options opt(true, true, true, false, false);
-#  ifdef EVENT_UNIV
-    opt.favor_event_univ = true;
-#  endif
-    spot::ltl::ltl_simplifier simp(opt);
-    {
-      const spot::ltl::formula* tmp;
-      tmp = f1;
-      f1 = simp.simplify(f1);
-
-      if (!simp.are_equivalent(f1, tmp))
-	{
-	  std::cerr << "Source and simplified formulae are not equivalent!\n";
-	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << '\n';
-	  exit_code = 1;
-	}
-
-      tmp->destroy();
-    }
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-#ifdef REDUC_TAU
-    spot::ltl::ltl_simplifier_options opt(false, false, false, true, false);
-    spot::ltl::ltl_simplifier simp(opt);
-    {
-      const spot::ltl::formula* tmp;
-      tmp = f1;
-      f1 = simp.simplify(f1);
-
-      if (!simp.are_equivalent(f1, tmp))
-	{
-	  std::cerr << "Source and simplified formulae are not equivalent!\n";
-	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << '\n';
-	  exit_code = 1;
-	}
-
-      tmp->destroy();
-    }
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-#ifdef REDUC_TAUSTR
-    spot::ltl::ltl_simplifier_options opt(false, false, false, true, true);
-    spot::ltl::ltl_simplifier simp(opt);
-    {
-      const spot::ltl::formula* tmp;
-      tmp = f1;
-      f1 = simp.simplify(f1);
-
-      if (!simp.are_equivalent(f1, tmp))
-	{
-	  std::cerr << "Source and simplified formulae are not equivalent!\n";
-	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << '\n';
-	  exit_code = 1;
-	}
-
-      tmp->destroy();
-    }
-    spot::ltl::dump(std::cout, f1);
-    std::cout << std::endl;
-#endif
-
-    exit_code |= f1 != f2;
-
-#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
-    spot::ltl::ltl_simplifier simp;
-#endif
-
-    if (!simp.are_equivalent(f1, f2))
-      {
-#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
-	std::cerr << "Source and destination formulae are not equivalent!\n";
-#else
-	std::cerr << "Simpl. and destination formulae are not equivalent!\n";
-#endif
-	exit_code = 1;
-      }
-
-    if (exit_code)
-      {
-	spot::ltl::dump(std::cerr, f1) << std::endl;
-	spot::ltl::dump(std::cerr, f2) << std::endl;
-      }
-
-    f1->destroy();
-    f2->destroy();
-  }
-  spot::ltl::atomic_prop::dump_instances(std::cerr);
-  spot::ltl::unop::dump_instances(std::cerr);
-  spot::ltl::binop::dump_instances(std::cerr);
-  spot::ltl::multop::dump_instances(std::cerr);
-  assert(spot::ltl::atomic_prop::instance_count() == 0);
-  assert(spot::ltl::unop::instance_count() == 0);
-  assert(spot::ltl::binop::instance_count() == 0);
-  assert(spot::ltl::multop::instance_count() == 0);
-  return exit_code;
-}
diff --git a/src/ltltest/unabbrevwm.test b/src/ltltest/unabbrevwm.test
index 05e75078e..ab5cbf3fa 100755
--- a/src/ltltest/unabbrevwm.test
+++ b/src/ltltest/unabbrevwm.test
@@ -25,7 +25,12 @@
 
 set -e
 
-# This caused a segfault at some point
-run 0 ../unabbrevwm \
-  '(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))' \
-  '(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))'
+# Removing W,M in this formula caused a segfault at some point.
+run 0 ../../bin/ltlfilt --remove-wm >out <<EOF
+(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
+(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
+EOF
+
+# The first formula will be simplified to the second, so after uniq
+# the output should have one line.
+test `uniq out | wc -l` = 1