diff --git a/src/ltltest/.gitignore b/src/ltltest/.gitignore
index 436b60d5e..568d222e4 100644
--- a/src/ltltest/.gitignore
+++ b/src/ltltest/.gitignore
@@ -8,6 +8,7 @@ parser.dot
 expect
 defs
 equals
+nequals
 lunabbrev
 tunabbrev
 nenoform
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 51455e8dd..e4c17523b 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -35,11 +35,11 @@ check_PROGRAMS = \
   ltl2text \
   ltlrel \
   lunabbrev \
+  nequals \
   nenoform \
   reduc \
   reduccmp \
   reduceu \
-  reductau \
   reductaustr \
   syntimpl \
   tostring \
@@ -48,31 +48,31 @@ check_PROGRAMS = \
   unabbrevwm
 
 consterm_SOURCES = consterm.cc
-equals_SOURCES = equals.cc
+equals_SOURCES = equalsf.cc
 kind_SOURCES = kind.cc
 length_SOURCES = length.cc
 ltl2dot_SOURCES = readltl.cc
 ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
 ltl2text_SOURCES = readltl.cc
 ltlrel_SOURCES = ltlrel.cc
-lunabbrev_SOURCES = equals.cc
+lunabbrev_SOURCES = equalsf.cc
 lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
-nenoform_SOURCES = equals.cc
+nenoform_SOURCES = equalsf.cc
 nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
+nequals_SOURCES = equalsf.cc
+nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE
 reduc_SOURCES = reduc.cc
 reduccmp_SOURCES = equalsf.cc
 reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
-reduceu_SOURCES = equals.cc
+reduceu_SOURCES = equalsf.cc
 reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
-reductau_SOURCES = equals.cc
-reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU
 reductaustr_SOURCES = equalsf.cc
 reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR
 syntimpl_SOURCES = syntimpl.cc
 tostring_SOURCES = tostring.cc
-tunabbrev_SOURCES = equals.cc
+tunabbrev_SOURCES = equalsf.cc
 tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
-tunenoform_SOURCES = equals.cc
+tunenoform_SOURCES = equalsf.cc
 tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV
 unabbrevwm_SOURCES = equals.cc
 unabbrevwm_CPPFLAGS = $(AM_CPPFLAGS) -DWM
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 3760fe867..665e5ab98 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -25,181 +25,189 @@
 # Check for the equals visitor
 
 . ./defs || exit 1
+set -e
 
+cat >equal.txt <<\EOF
 # A few things which are equal
-run 0 ../equals 'a' 'a'
-run 0 ../equals '~a' '!a'
-run 0 ../equals '1' '1'
-run 0 ../equals '0' '0'
-run 0 ../equals 'a => b' 'a --> b'
-run 0 ../equals 'a <-> b' 'a <--> b'
-run 0 ../equals 'G a ' ' G a'
-run 0 ../equals 'a U b' 'a U b'
-run 0 ../equals 'a & b' 'a & b'
-run 0 ../equals 'a & b' 'b & a'
-run 0 ../equals 'a & b & c' 'c & a && b'
-run 0 ../equals 'a & b & c' 'b & c & a'
-run 0 ../equals 'a && b & a' 'b & a & b'
-run 0 ../equals 'a & b' 'b & a & b'
-run 0 ../equals 'a & b' 'b & a & a'
-run 0 ../equals 'a & b & (c |(f U g)|| e)' \
-                'b & a & a & (c | e |(f U g)| e | c) & b'
-run 0 ../equals 'a & a' 'a'
-run 0 ../equals 'a & a & true' 'a'
-run 0 ../equals 'a & false & a' 'false'
-run 0 ../equals 'a | false | a' 'a'
-run 0 ../equals 'true | a | a' 'true'
-run 0 ../equals 'Ga=1*Gb=0' '(G(a)) & (G(!b))'
-
-# other formulae which are not
-run 1 ../equals 'a' 'b'
-run 1 ../equals '1' '0'
-run 1 ../equals 'a => b' 'b => a'
-run 1 ../equals 'a => b' 'a <=> b'
-run 1 ../equals 'a => b' 'a U b'
-run 1 ../equals 'a R b' 'a U b'
-run 1 ../equals 'a & b & c' 'c & a'
-run 1 ../equals 'b & c' 'c & a & b'
-run 1 ../equals 'a & b & (c |(f U g)| e)' \
-                'b & a & a & (c | e |(g U g)| e | c) & b'
-run 1 ../equals '{a*}' '{a*}<>->1'
-run 1 ../equals '!{a*}' '{a*}<>->1'
-run 1 ../equals '{a*}' '{a*}!'
-run 1 ../equals '!{a*}' '{a*}!'
-
+a, a
+~a, !a
+1, 1
+0, 0
+a => b, a --> b
+a <-> b, a <--> b
+G a ,  G a
+a U b, a U b
+a & b, a & b
+a & b, b & a
+a & b & c, c & a && b
+a & b & c, b & c & a
+a && b & a, b & a & b
+a & b, b & a & b
+a & b, b & a & a
+a & b & (c |(f U g)|| e), b & a & a & (c | e |(f U g)| e | c) & b
+a & a, a
+a & a & true, a
+a & false & a, false
+a | false | a, a
+true | a | a, true
+Ga=1*Gb=0, (G(a)) & (G(!b))
+FFx, Fx
+FFFFFx, Fx
+GGx, Gx
+GGGGGx, Gx
+!!x, x
+!!!!!x, !x
+{[*0];x}<>->1, {x}<>->1
+{x;[*0]}<>->1, {x}<>-> 1
+{[*0];x;[*0];[*0]}<>->1, {x}<>->1
+{[*0];x;[*0];x;[*0]}<>->1, {x;x}<>->1
+{x;x;x;[*0];x;x}<>->1, {x;x;x;x;x}<>->1
+{x;0;x;x;x}<>->1, 0
+{x;0;x;x;x}[]->1, 1
+{0*;1}<>->x, x
+{[*0]*;1}<>->x, x
+{x;x}<>->FF(0), 0
+{x;x}<>->GX(1), {x;x}<>->1
+{x;x}[]->GX(1), 1
+{x;x}[]->FF(0), {x;x}[]->0
+{x;x}[]->y, {x;x}|->y
+{x;x}[]->y, {x;x}(y)
+{a*}!, {a*}<>->1
+{a -> b} (c), !(a->b)|c
+{a & !b}!, a & !b
+{a;[*0]}|->!Xb, !a | !Xb
+{{a;b}:b:c:d*:e:f}!, {{a;b}:{b && c }:d[*]:{e && f}}!
+{a:b:c}|->!Xb, !(a&&b&&c) | !Xb
+{a:b:c*}|->!Xb, {(a&&b):c*}|-> !Xb
+{a&b&c*}|->!Xb, {(a&&b)&c*}|-> !Xb
+{[*]&&a&&[*]}!, a
+{[*]||a||[*]}!, {[*]}!
+{0&{f;g*}}!, 0
+{1&{f;g*}}!, {f;g*}!
 # Precedence
-run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a'
+a & b ^ c | d, d | c ^ b & a
 
 # Corner cases parsing
-run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))'
+FFG__GFF, F(F(G("__GFF")))
 
 # Trivial simplifications
-run 0 ../equals '{0*}<>->a' '{[*0]}<>->a'
-run 0 ../equals '{[*0]*}<>->a' '{[*0]}<>->a'
-run 0 ../equals '{Exp**}<>->a' '{Exp*}<>->a'
-run 0 ../equals 'FF(Exp)' 'F(Exp)'
-run 0 ../equals 'GG(Exp)' 'G(Exp)'
-run 0 ../equals 'F(0)' '0'
-run 0 ../equals 'G(0)' '0'
-run 0 ../equals 'F(1)' '1'
-run 0 ../equals 'G(1)' '1'
-run 0 ../equals 'F({[*0]}<>->1)' 'F({[*0]}<>->1)'
-run 0 ../equals 'G({[*0]}<>->1)' 'G({[*0]}<>->1)'
-run 0 ../equals 'F({1}<>->1)' '1'
-run 0 ../equals 'G({1}<>->1)' '1'
-run 0 ../equals '!1' '0'
-run 0 ../equals '!0' '1'
-run 0 ../equals '!!Exp' 'Exp'
+{0*}<>->a, {[*0]}<>->a
+{[*0]*}<>->a, {[*0]}<>->a
+{Exp**}<>->a, {Exp*}<>->a
+FF(Exp), F(Exp)
+GG(Exp), G(Exp)
+F(0), 0
+G(0), 0
+F(1), 1
+G(1), 1
+F({[*0]}<>->1), F({[*0]}<>->1)
+G({[*0]}<>->1), G({[*0]}<>->1)
+F({1}<>->1), 1
+G({1}<>->1), 1
+!1, 0
+!0, 1
+!!Exp, Exp
 
-run 0 ../equals '(1 => Exp)' 'Exp'
-run 0 ../equals '(0 => Exp)' '1'
-run 0 ../equals '(Exp => 1)' '1'
-run 0 ../equals '(Exp => 0)' '!Exp'
-run 0 ../equals '(Exp => Exp)' '1'
-run 0 ../equals '(1 ^ Exp)' '!Exp'
-run 0 ../equals '(0 ^ Exp)' 'Exp'
-run 0 ../equals '(Exp ^ Exp)' '0'
-run 0 ../equals '(0 <=> Exp)' '!Exp'
-run 0 ../equals '(1 <=> Exp)' 'Exp'
-run 0 ../equals '(Exp <=> Exp)' '1'
-run 0 ../equals '(Exp U 1)' '1'
-run 0 ../equals '(Exp U 0)' '0'
-run 0 ../equals '(0 U Exp)' 'Exp'
-run 0 ../equals '(Exp U Exp)' 'Exp'
-run 0 ../equals '(Exp R 1)' '1'
-run 0 ../equals '(Exp R 0)' '0'
-run 0 ../equals '(Exp R Exp)' 'Exp'
-run 0 ../equals '(1 R Exp)' 'Exp'
-run 0 ../equals '(Exp W 1)' '1'
-run 0 ../equals '(0 W Exp)' 'Exp'
-run 0 ../equals '(1 W Exp)' '1'
-run 0 ../equals '(Exp W Exp)' 'Exp'
-run 0 ../equals '(Exp M 0)' '0'
-run 0 ../equals '(1 M Exp)' 'Exp'
-run 0 ../equals '(0 M Exp)' '0'
-run 0 ../equals '(Exp M Exp)' 'Exp'
+(1 => Exp), Exp
+(0 => Exp), 1
+(Exp => 1), 1
+(Exp => 0), !Exp
+(Exp => Exp), 1
+(1 ^ Exp), !Exp
+(0 ^ Exp), Exp
+(Exp ^ Exp), 0
+(0 <=> Exp), !Exp
+(1 <=> Exp), Exp
+(Exp <=> Exp), 1
+(Exp U 1), 1
+(Exp U 0), 0
+(0 U Exp), Exp
+(Exp U Exp), Exp
+(Exp R 1), 1
+(Exp R 0), 0
+(Exp R Exp), Exp
+(1 R Exp), Exp
+(Exp W 1), 1
+(0 W Exp), Exp
+(1 W Exp), 1
+(Exp W Exp), Exp
+(Exp M 0), 0
+(1 M Exp), Exp
+(0 M Exp), 0
+(Exp M Exp), Exp
+
+{1:{a;b}:1:c*}!, {{a;b}:c*}!
+{c*:1:{a;b}:1}!, {c*:{a;b}}!
+
+{z;a*;b*;*;c;d;*;b*;e;a*;*;b*}, {z;[*];c;d;[*];e;[*]}
+{((a;b)|[*0]);[*];c}!, {[*];c}!
+{a;a;a*;a;b;b[*];c[*2:3];c[*4:5]}, {a[*3..];b[+];c[*6..8]}
+
+{a[*0]}, {[*0]}
+{a[*..]}, {a[*]}
+{a[*2..3][*4..5]}, {a[*8..15]}
+{a[*4..5][*2..3]}, {a[*4..5][*2..3]}
+{a[*2:3][*]}, {a[*2 to 3][*]}
+{a[*1..3][*]}, {a[*]}
+{a[*][*2..3]}, {a[*]}
+{a[*..3][*2]}, {a[*..6]}
+{a[*..3][*to2]}, {a[*:6]}
+{a[*..3][*2..$]}, {a[*]}
+{a[*..3][*2:]}, {a[*:inf]}
+{a[*1..]}, {a[+]}
+{a[*1]}, {a}
+{a[+][*1..3]}, {a[+]}
+{a[*1..3][+]}, {a[+]}
+{[*2][+]}, {[*2][+]}
+{[+][*2]}, {[*2..inf]}
+
+{0[=2]}, 0
+{0[=2..]}, 0
+{0[=1..10]}, 0
+{0[=0]}, {[*]}
+{0[=0..10]}, {*}
+{0[=0..]}, {*}
+{1[=0]}, {[*0]}
+{1[=1..2]}, {[*1\,2]}
+{1[=..4]}, {1[*..4]}
+{b[=0]}, {(!b)[*]}
+{b[=0to$]}, {*}
+
+{0[->10..100];b}, 0
+{0[->1..];b}, 0
+{0[->0\,100];b}, b
+{0[->0..$];b}, b
+!{1[->0];b}, !b
+{1[->10\,20];b}, {[*10..20];b}
+{1[->..];b}, {[*1..];b}
+{{a&!c}[->0];b}, b
+EOF
+
+
+cat >nequal.txt <<\EOF
+# other formulae which are not
+a, b
+1, 0
+a => b, b => a
+a => b, a <=> b
+a => b, a U b
+a R b, a U b
+a & b & c, c & a
+b & c, c & a & b
+a & b & (c |(f U g)| e), b & a & a & (c | e |(g U g)| e | c) & b
+{a*}, {a*}<>->1
+!{a*}, {a*}<>->1
+{a*}, {a*}!
+!{a*}, {a*}!
 
-run 0 ../equals FFx Fx
-run 0 ../equals FFFFFx Fx
-run 0 ../equals GGx Gx
-run 0 ../equals GGGGGx Gx
-run 0 ../equals '!!x' x
-run 0 ../equals '!!!!!x' '!x'
-run 0 ../equals '{[*0];x}<>->1' '{x}<>->1'
-run 0 ../equals '{x;[*0]}<>->1' '{x}<>-> 1'
-run 0 ../equals '{[*0];x;[*0];[*0]}<>->1' '{x}<>->1'
-run 0 ../equals '{[*0];x;[*0];x;[*0]}<>->1' '{x;x}<>->1'
-run 0 ../equals '{x;x;x;[*0];x;x}<>->1' '{x;x;x;x;x}<>->1'
-run 0 ../equals '{x;0;x;x;x}<>->1' '0'
-run 0 ../equals '{x;0;x;x;x}[]->1' '1'
-run 0 ../equals '{0*;1}<>->x' 'x'
-run 0 ../equals '{[*0]*;1}<>->x' 'x'
-run 0 ../equals '{x;x}<>->FF(0)' '0'
-run 0 ../equals '{x;x}<>->GX(1)' '{x;x}<>->1'
-run 0 ../equals '{x;x}[]->GX(1)' '1'
-run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0'
-run 0 ../equals '{x;x}[]->y' '{x;x}|->y'
-run 0 ../equals '{x;x}[]->y' '{x;x}(y)'
-run 0 ../equals '{a*}!' '{a*}<>->1'
-run 0 ../equals '{a -> b} (c)' '!(a->b)|c'
-run 0 ../equals '{a & !b}!' 'a & !b'
-run 0 ../equals '{a;[*0]}|->!Xb' '!a | !Xb'
-run 0 ../equals '{{a;b}:b:c:d*:e:f}!' '{{a;b}:{b && c }:d[*]:{e && f}}!'
-run 0 ../equals '{a:b:c}|->!Xb' '!(a&&b&&c) | !Xb'
-run 0 ../equals '{a:b:c*}|->!Xb' '{(a&&b):c*}|-> !Xb'
-run 0 ../equals '{a&b&c*}|->!Xb' '{(a&&b)&c*}|-> !Xb'
-run 0 ../equals '{[*]&&a&&[*]}!' 'a'
-run 0 ../equals '{[*]||a||[*]}!' '{[*]}!'
-run 0 ../equals '{0&{f;g*}}!' '0'
-run 0 ../equals '{1&{f;g*}}!' '{f;g*}!'
 # 1 should not be removed in the following two formulae
-run 1 ../equals '{1&{g*}}!' '{g*}!'
-run 1 ../equals '{1|{b;c}}<>->a' '{b;c}<>->a'
-run 0 ../equals '{1:{a;b}:1:c*}!' '{{a;b}:c*}!'
-run 0 ../equals '{c*:1:{a;b}:1}!' '{c*:{a;b}}!'
+{1&{g*}}!, {g*}!
+{1|{b;c}}<>->a, {b;c}<>->a
 # make sure twin arguments are not reduced in Fusion.
-run 1 ../equals '{(a;!a)*:(a;!a)*:b}!' '{(a;!a)*:b}!'
+{(a;!a)*:(a;!a)*:b}!, {(a;!a)*:b}!
 # make sure 1:a* is not reduced to a*.
-run 1 ../equals '{(1:a*);b}!' '{a*;b}!'
-run 0 ../equals '{z;a*;b*;*;c;d;*;b*;e;a*;*;b*}' '{z;[*];c;d;[*];e;[*]}'
-run 0 ../equals '{((a;b)|[*0]);[*];c}!' '{[*];c}!'
-run 0 ../equals '{a;a;a*;a;b;b[*];c[*2:3];c[*4:5]}' '{a[*3..];b[+];c[*6..8]}'
+{(1:a*);b}!, {a*;b}!
+EOF
 
-run 0 ../equals '{a[*0]}' '{[*0]}'
-run 0 ../equals '{a[*..]}' '{a[*]}'
-run 0 ../equals '{a[*2..3][*4..5]}' '{a[*8..15]}'
-run 0 ../equals '{a[*4..5][*2..3]}' '{a[*4..5][*2..3]}'
-run 0 ../equals '{a[*2:3][*]}' '{a[*2 to 3][*]}'
-run 0 ../equals '{a[*1..3][*]}' '{a[*]}'
-run 0 ../equals '{a[*][*2..3]}' '{a[*]}'
-run 0 ../equals '{a[*..3][*2]}' '{a[*..6]}'
-run 0 ../equals '{a[*..3][*to2]}' '{a[*:6]}'
-run 0 ../equals '{a[*..3][*2..$]}' '{a[*]}'
-run 0 ../equals '{a[*..3][*2:]}' '{a[*:inf]}'
-run 0 ../equals '{a[*1..]}' '{a[+]}'
-run 0 ../equals '{a[*1]}' '{a}'
-run 0 ../equals '{a[+][*1..3]}' '{a[+]}'
-run 0 ../equals '{a[*1..3][+]}' '{a[+]}'
-run 0 ../equals '{[*2][+]}' '{[*2][+]}'
-run 0 ../equals '{[+][*2]}' '{[*2..inf]}'
-
-run 0 ../equals '{0[=2]}' '0'
-run 0 ../equals '{0[=2..]}' '0'
-run 0 ../equals '{0[=1..10]}' '0'
-run 0 ../equals '{0[=0]}' '{[*]}'
-run 0 ../equals '{0[=0..10]}' '{*}'
-run 0 ../equals '{0[=0..]}' '{*}'
-run 0 ../equals '{1[=0]}' '{[*0]}'
-run 0 ../equals '{1[=1..2]}' '{[*1,2]}'
-run 0 ../equals '{1[=..4]}' '{1[*..4]}'
-run 0 ../equals '{b[=0]}' '{(!b)[*]}'
-run 0 ../equals '{b[=0to$]}' '{*}'
-
-run 0 ../equals '{0[->10..100];b}' '0'
-run 0 ../equals '{0[->1..];b}' '0'
-run 0 ../equals '{0[->0,100];b}' 'b'
-run 0 ../equals '{0[->0..$];b}' 'b'
-run 0 ../equals '!{1[->0];b}' '!b'
-run 0 ../equals '{1[->10,20];b}' '{[*10..20];b}'
-run 0 ../equals '{1[->..];b}' '{[*1..];b}'
-run 0 ../equals '{{a&!c}[->0];b}' 'b'
+run 0 ../equals equal.txt
+run 0 ../nequals nequal.txt
diff --git a/src/ltltest/equalsf.cc b/src/ltltest/equalsf.cc
index f4a345814..b33a8c7dd 100644
--- a/src/ltltest/equalsf.cc
+++ b/src/ltltest/equalsf.cc
@@ -58,6 +58,11 @@ main(int argc, char** argv)
   if (argc != 2)
     syntax(argv[0]);
   std::ifstream input(argv[1]);
+  if (!input)
+    {
+      std::cerr << "failed to open " << argv[1] << '\n';
+      return 2;
+    }
 
   std::string s;
   unsigned line = 0;
@@ -72,7 +77,16 @@ main(int argc, char** argv)
 	std::istringstream ss(s);
 	std::string form;
 	while (std::getline(ss, form, ','))
-	  formulas.push_back(form);
+	  {
+	    std::string tmp;
+	    while (form.size() > 0 && form.back() == '\\'
+		   && std::getline(ss, tmp, ','))
+	      {
+		form.back() = ',';
+		form += tmp;
+	      }
+	    formulas.push_back(form);
+	  }
       }
 
       unsigned size = formulas.size();
@@ -226,6 +240,9 @@ main(int argc, char** argv)
 		exit_code = 1;
 	      }
 
+#if NEGATE
+	    exit_code ^= 1;
+#endif
 	    if (exit_code)
 	      {
 		spot::ltl::dump(std::cerr, f1) << std::endl;
diff --git a/src/ltltest/eventuniv.test b/src/ltltest/eventuniv.test
index 304e3c903..91d15489d 100755
--- a/src/ltltest/eventuniv.test
+++ b/src/ltltest/eventuniv.test
@@ -19,42 +19,46 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 . ./defs || exit 1
+set -e
 
-check()
-{
-  run 0 ../reduceu "$@"
-}
+cat >reduceu.txt <<EOF
+Xa | GFb, Xa | GFb
+X(a | GXFb), Xa | GFb
+Xa & GFb, Xa & GFb
+X(a & GXFb), Xa & GFb
 
-check 'Xa | GFb'    'Xa | GFb'
-check 'X(a | GXFb)' 'Xa | GFb'
-check 'Xa & GFb'    'Xa & GFb'
-check 'X(a & GXFb)' 'Xa & GFb'
+F(a & b & GFc & FGd), F(a & b) & G(Fc & FGd)
+Fa | Fb | GFc | GFd, F(a|b) | GF(c | d)
+Fa | Fb | GFc | GFd | FGe, F(a|b) | F(G(e) | GF(c | d))
+Ga | Gb | GFd | FGe | FGf, Ga | Gb | F(GFd | Ge | Gf)
 
-check 'F(a & b & GFc & FGd)' 'F(a & b) & G(Fc & FGd)'
-check 'Fa | Fb | GFc | GFd' 'F(a|b) | GF(c | d)'
-check 'Fa | Fb | GFc | GFd | FGe' 'F(a|b) | F(G(e) | GF(c | d))'
-cehck 'Ga | Gb | GFd | FGe | FGf' 'Ga | Gb | F(GFd | Ge | Gf)'
+G(Ga & Fb & c & GFd), G(a&c) & G(Fb & Fd)
+G(Ga & GFb & c & GFd), G(a&c) & G(Fb & Fd)
+G(a & GFb & c & GFd), G(a&c) & G(Fb & Fd)
+G(Ga & Fb & c & GFd & FGe), G(a & c) & G(Fb & Fd & FGe)
+G(Ga & XFGb & c & FGd & FGe), FG(b & d & e) & G(a & c)
+G(Ga & GXFb & c & FGd & FGe & Fc), G(Fb & FG(d & e)) & G(a & c)
+Ga & Gb & GFd & FGe & FGf, G(Fd & FG(e & f)) & G(a & b)
+G(Ga & Gb & GFd & FGe) & FGf, G(Fd & FG(e & f)) & G(a & b)
 
-check 'G(Ga & Fb & c & GFd)'  'G(a&c) & G(Fb & Fd)'
-check 'G(Ga & GFb & c & GFd)' 'G(a&c) & G(Fb & Fd)'
-check 'G(a & GFb & c & GFd)'  'G(a&c) & G(Fb & Fd)'
-check 'G(Ga & Fb & c & GFd & FGe)' 'G(a & c) & G(Fb & Fd & FGe)'
-check 'G(Ga & XFGb & c & FGd & FGe)' 'FG(b & d & e) & G(a & c)'
-check 'G(Ga & GXFb & c & FGd & FGe & Fc)' 'G(Fb & FG(d & e)) & G(a & c)'
-check 'Ga & Gb & GFd & FGe & FGf'    'G(Fd & FG(e & f)) & G(a & b)'
-check 'G(Ga & Gb & GFd & FGe) & FGf' 'G(Fd & FG(e & f)) & G(a & b)'
-
-check 'a U (b | Fc)'  '(a U b) | Fc'
-check 'a W (b | Fc)'  '(a W b) | Fc'
-check 'a U (b & GFc)' '(a U b) & GFc'
-check 'a W (b & GFc)' 'a W (b & GFc)'  # Unchanged
-check '(a | Gc) W g'  '(a | Gc) W g'   # Unchanged
-check '(a | Gc) U g'  '(a | Gc) U g'   # Unchanged
-
-check '(a & GFc) M b' '(a M b) & GFc'
-check '(a | GFc) M b' '(a | GFc) M b'  # Unchanged
-check '(a & GFc) R b' '(a & GFc) R b'  # Unchanged
-check '(a | GFc) R b' '(a | GFc) R b'  # Unchanged
-check 'a R (b & Gc)'  '(a R b) & Gc'
-check 'a M (b & Gc)'  '(a M b) & Gc'
+a U (b | Fc), (a U b) | Fc
+a W (b | Fc), (a W b) | Fc
+a U (b & GFc), (a U b) & GFc
+# Unchanged
+a W (b & GFc), a W (b & GFc)
+# Unchanged
+(a | Gc) W g, (a | Gc) W g
+# Unchanged
+(a | Gc) U g, (a | Gc) U g
+(a & GFc) M b, (a M b) & GFc
+# Unchanged
+(a | GFc) M b, (a | GFc) M b
+# Unchanged
+(a & GFc) R b, (a & GFc) R b
+# Unchanged
+(a | GFc) R b, (a | GFc) R b
+a R (b & Gc), (a R b) & Gc
+a M (b & Gc), (a M b) & Gc
+EOF
 
+run 0 ../reduceu reduceu.txt
diff --git a/src/ltltest/lunabbrev.test b/src/ltltest/lunabbrev.test
index 0f6f5a261..0b4911e24 100755
--- a/src/ltltest/lunabbrev.test
+++ b/src/ltltest/lunabbrev.test
@@ -1,8 +1,9 @@
 #! /bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -27,25 +28,27 @@
 
 set -e
 
+cat >lunabbrev.txt<<EOF
 # A few things that do not change
-run 0 ../lunabbrev 'a' 'a'
-run 0 ../lunabbrev '1' '1'
-run 0 ../lunabbrev '0' '0'
-run 0 ../lunabbrev 'G a ' ' G a'
-run 0 ../lunabbrev 'a U b' 'a U b'
-run 0 ../lunabbrev 'a & b' 'a & b'
-run 0 ../lunabbrev 'a & b' 'b & a'
-run 0 ../lunabbrev 'a & b & c' 'c & a & b'
-run 0 ../lunabbrev 'a & b & c' 'b & c & a'
-run 0 ../lunabbrev 'a & b & a' 'b & a & b'
-run 0 ../lunabbrev 'a & b' 'b & a & b'
-run 0 ../lunabbrev 'a & b' 'b & a & a'
-run 0 ../lunabbrev 'a & b & (c |(f U g)| e)' \
-                  'b & a & a & (c | e |(f U g)| e | c) & b'
+a, a
+1, 1
+0, 0
+G a ,  G a
+a U b, a U b
+a & b, a & b
+a & b, b & a
+a & b & c, c & a & b
+a & b & c, b & c & a
+a & b & a, b & a & b
+a & b, b & a & b
+a & b, b & a & a
+a & b & (c |(f U g)| e), b & a & a & (c | e |(f U g)| e | c) & b
 # other formulae that do change
-run 0 ../lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
-run 0 ../lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
-run 0 ../lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
-run 0 ../lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
-run 0 ../lunabbrev '(a ^ b) | (b ^ c)' \
-                   '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+a ^ b, (a & !b) | (!a & b)
+a ^ Xb, (!Xb & a) | (!a & Xb) | (Xb & !a)
+GF a => F G(b), !GFa | F Gb
+!a <-> Xb, (Xb & !a) | (!!a & !Xb)
+(a ^ b) | (b ^ c), (c & !b) | (!c & b) | (a & !b) | (!a & b)
+EOF
+
+run 0 ../lunabbrev lunabbrev.txt
diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test
index 70bae63fc..737ab16ac 100755
--- a/src/ltltest/nenoform.test
+++ b/src/ltltest/nenoform.test
@@ -1,6 +1,7 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2010, 2011, 2014 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -27,44 +28,46 @@
 
 set -e
 
+cat >nenoform.txt<<EOF
 # A few things that do not change
-run 0 ../nenoform 'a' 'a'
-run 0 ../nenoform '1' '1'
-run 0 ../nenoform '0' '0'
-run 0 ../nenoform '!a' '!a'
-run 0 ../nenoform 'a U b' 'a U b'
-run 0 ../nenoform 'a & b' 'a & b'
-run 0 ../nenoform 'a & b' 'b & a'
-run 0 ../nenoform 'a & !b & c' 'c & a & !b'
-run 0 ../nenoform 'a & b & c' 'b & c & a'
-run 0 ../nenoform 'Xa & b & Xa' 'b & Xa & b'
-run 0 ../nenoform 'a & b' 'b & a & b'
-run 0 ../nenoform 'a & !b' '!b & a & a'
-run 0 ../nenoform 'a & b & (Xc |(f U !g)| e)' \
-                  'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
-run 0 ../nenoform 'GFa => FGb' 'FG!a || FGb'
+a, a
+1, 1
+0, 0
+!a, !a
+a U b, a U b
+a & b, a & b
+a & b, b & a
+a & !b & c, c & a & !b
+a & b & c, b & c & a
+Xa & b & Xa, b & Xa & b
+a & b, b & a & b
+a & !b, !b & a & a
+a & b & (Xc |(f U !g)| e), b & a & a & (Xc | e |(f U !g)| e | Xc) & b
+GFa => FGb, FG!a || FGb
 
 # Basic rewritings
-run 0 ../nenoform '!!a' 'a'
-run 0 ../nenoform '!!!!!a' '!a'
-run 0 ../nenoform '!Xa' 'X!a'
-run 0 ../nenoform '!Fa' 'G!a'
-run 0 ../nenoform '!Ga' 'F!a'
-run 0 ../nenoform '!(a ^ b)' '!a&!b | a&b'
-run 0 ../nenoform '!(a <=> b)' '(!a&b) | a&!b'
-run 0 ../nenoform '!(a => b)' 'a&!b'
-run 0 ../nenoform '!(!a => !b)' '!a&b'
-run 0 ../nenoform '!(a U b)' '!a R !b'
-run 0 ../nenoform '!(a R b)' '!a U !b'
-run 0 ../nenoform '!(!a R !b)' 'a U b'
-run 0 ../nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
-run 0 ../nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
+!!a, a
+!!!!!a, !a
+!Xa, X!a
+!Fa, G!a
+!Ga, F!a
+!(a ^ b), !a&!b | a&b
+!(a <=> b), (!a&b) | a&!b
+!(a => b), a&!b
+!(!a => !b), !a&b
+!(a U b), !a R !b
+!(a R b), !a U !b
+!(!a R !b), a U b
+!(a & b & c & d & b), !a | !b | !c | !d
+!(a | b | c | d), !a & !b & !c & !d
 
 # Nested rewritings
-run 0 ../nenoform '!(a U (!b U ((a & b & c) R d)))' \
-                  '!a R (b R ((!a | !b | !c) U !d))'
-run 0 ../nenoform '!(GF a => FG b)' 'GFa & GF!b'
+!(a U (!b U ((a & b & c) R d))), !a R (b R ((!a | !b | !c) U !d))
+!(GF a => FG b), GFa & GF!b
 
 # Rational operators
-run 0 ../nenoform '!X{a;b}<>->Fx' 'X{a;b}[]->G!x'
-run 0 ../nenoform '!F({a*}<>->{b*}<>->c)' 'G({a*}[]->{b*}[]->!c)'
+!X{a;b}<>->Fx, X{a;b}[]->G!x
+!F({a*}<>->{b*}<>->c), G({a*}[]->{b*}[]->!c)
+EOF
+
+run 0 ../nenoform nenoform.txt
diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test
index 9c3fad466..141029e13 100755
--- a/src/ltltest/parseerr.test
+++ b/src/ltltest/parseerr.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -26,6 +26,7 @@
 # resulting tree looks like.
 
 . ./defs || exit 1
+set -e
 
 check()
 {
@@ -64,33 +65,36 @@ check '' ''
 check '+' ''
 check '/2/3/4/5 a + b /6/7/8/' ''
 
+
+cat >recover.txt <<EOF
 # leading and trailing garbage are skipped
-run 0 ../equals -E 'a U b c' 'a U b'
+a U b c, a U b
 # (check multop merging while we are at it)
-run 0 ../equals -E 'a & b & c & d e' 'a & b & c & d'
-run 0 ../equals -E 'a & (b | c) & d should work' 'a & (b | c) & d'
+a & b & c & d e, a & b & c & d
+a & (b | c) & d should work, a & (b | c) & d
 # Binop recovery
-run 0 ../equals -E 'a U' a
-run 0 ../equals -E 'a U b V c R' 'a U b V c'
-run 0 ../equals -E 'a &&& b' 'a & b'
-run 0 ../equals -E 'a &&| b' 'a | b'
+a U, a
+a U b V c R, a U b V c
+a &&& b, a & b
+a &&| b, a | b
 
 # Recovery inside parentheses
-run 0 ../equals -E 'a U (b c) U e R (f g <=> h)' 'a U b U e R f'
-run 0 ../equals -E 'a U ((c) U e) R (<=> f g)' 'a U ((c) U e) R (0)'
+a U (b c) U e R (f g <=> h), a U b U e R f
+a U ((c) U e) R (<=> f g), a U ((c) U e) R (0)
 
 # Missing parentheses
-run 0 ../equals -E 'a & (a + b' 'a & (a + b)'
-run 0 ../equals -E 'a & (a + b c' 'a & (a + b)'
-run 0 ../equals -E 'a & (+' 'a & 0'
-run 0 ../equals -E 'a & ('  'a & 0'
+a & (a + b, a & (a + b)
+a & (a + b c, a & (a + b)
+a & (+, a & 0
+a & (, a & 0
 
 # Invalid ranges
-run 0 ../equals -E '{a[*8..1];b}' '{a[*1..8];b}'
-run 0 ../equals -E '{a[=8..1];b}' '{a[=1..8];b}'
-run 0 ../equals -E '{a[->8..1];b}' '{a[->1..8];b}'
-run 0 ../equals -E '{a[->..0];b}' '{a[->0..1];b}'
-
+{a[*8..1];b}, {a[*1..8];b}
+{a[=8..1];b}, {a[=1..8];b}
+{a[->8..1];b}, {a[->1..8];b}
+{a[->..0];b}, {a[->0..1];b}
+EOF
+run 0 ../equals -E recover.txt
 
 check 'a - b' 'AP(a)' '>>> a - b
       ^
diff --git a/src/ltltest/tunabbrev.test b/src/ltltest/tunabbrev.test
index b80230846..dfb733a9f 100755
--- a/src/ltltest/tunabbrev.test
+++ b/src/ltltest/tunabbrev.test
@@ -1,9 +1,10 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# -*- coding: utf-8-
+# Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
-# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-# d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre
-# et Marie Curie.
+# Copyright (C) 2003, 2004 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.
 #
@@ -27,32 +28,33 @@
 
 set -e
 
+cat >tunabbrev.txt<<EOF
 # A few things that do not change
-run 0 ../tunabbrev 'a' 'a'
-run 0 ../tunabbrev '1' '1'
-run 0 ../tunabbrev '0' '0'
-run 0 ../tunabbrev 'a U b' 'a U b'
-run 0 ../tunabbrev 'a & b' 'a & b'
-run 0 ../tunabbrev 'a & b' 'b & a'
-run 0 ../tunabbrev 'a & b & c' 'c & a & b'
-run 0 ../tunabbrev 'a & b & c' 'b & c & a'
-run 0 ../tunabbrev 'a & b & a' 'b & a & b'
-run 0 ../tunabbrev 'a & b' 'b & a & b'
-run 0 ../tunabbrev 'a & b' 'b & a & a'
-run 0 ../tunabbrev 'a & b & (c |(f U g)| e)' \
-                   'b & a & a & (c | e |(f U g)| e | c) & b'
+a, a
+1, 1
+0, 0
+a U b, a U b
+a & b, a & b
+a & b, b & a
+a & b & c, c & a & b
+a & b & c, b & c & a
+a & b & a, b & a & b
+a & b, b & a & b
+a & b, b & a & a
+a & b & (c |(f U g)| e), b & a & a & (c | e |(f U g)| e | c) & b
 
 # same as in lunabbrev.test:
-run 0 ../tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
-run 0 ../tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
-run 0 ../tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
-run 0 ../tunabbrev '(a ^ b) | (b ^ c)' \
-                   '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+a ^ b, (a & !b) | (!a & b)
+a ^ Xb, (!Xb & a) | (!a & Xb) | (Xb & !a)
+!a <-> Xb, (Xb & !a) | (!!a & !Xb)
+(a ^ b) | (b ^ c), (c & !b) | (!c & b) | (a & !b) | (!a & b)
 
 # LTL unabbreviations:
-run 0 ../tunabbrev 'G a ' 'false R a'
-run 0 ../tunabbrev 'GF a => F G(b)' \
-                   '!(false R (true U a)) | (true U (false V b))'
-run 0 ../tunabbrev 'GGGGa' 'false V a'
-run 0 ../tunabbrev 'FFFfalse' '0'
-run 0 ../tunabbrev 'FFFf' 'true U f'
+G a , false R a
+GF a => F G(b), !(false R (true U a)) | (true U (false V b))
+GGGGa, false V a
+FFFfalse, 0
+FFFf, true U f
+EOF
+
+run 0 ../tunabbrev tunabbrev.txt
diff --git a/src/ltltest/tunenoform.test b/src/ltltest/tunenoform.test
index 9c23c0b3a..b900ed447 100755
--- a/src/ltltest/tunenoform.test
+++ b/src/ltltest/tunenoform.test
@@ -1,8 +1,9 @@
 #! /bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -27,10 +28,14 @@
 
 set -e
 
-run 0 ../tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
-run 0 ../tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
-run 0 ../tunenoform '!(a => b)' 'a&!b'
-run 0 ../tunenoform '!(!a => !b)' '!a&b'
-run 0 ../tunenoform '!Fa' 'false R !a'
-run 0 ../tunenoform '!G!a' 'true U a'
-run 0 ../tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
+cat >tunenoform.txt<<EOF
+!(a ^ b), (a|!b) & (!a|b)
+!(a <=> b), (a|b) & (!a|!b)
+!(a => b), a&!b
+!(!a => !b), !a&b
+!Fa, false R !a
+!G!a, true U a
+!(GF a => FG b), (0 R (1 U a)) & (0 R (1 U !b))
+EOF
+
+run 0 ../tunenoform tunenoform.txt