diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc
index 53ab45286..de49de882 100644
--- a/src/ltltest/consterm.cc
+++ b/src/ltltest/consterm.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
 // Dévelopement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <iostream>
+#include <fstream>
+#include <sstream>
 #include <cassert>
 #include <cstdlib>
 #include "ltlparse/public.hh"
@@ -36,21 +38,47 @@ main(int argc, char **argv)
   if (argc != 2)
     syntax(argv[0]);
 
-  spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* f1 = spot::ltl::parse_sere(argv[1], p1);
+  std::ifstream input(argv[1]);
+  if (!input)
+    {
+      std::cerr << "failed to open " << argv[1] << '\n';
+      return 2;
+    }
 
-  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
-    return 2;
+  std::string s;
+  while (std::getline(input, s))
+    {
+      if (s[0] == '#')		// Skip comments
+	{
+	  std::cerr << s << '\n';
+	  continue;
+	}
+      std::istringstream ss(s);
+      std::string form;
+      bool expected;
+      std::getline(ss, form, ',');
+      ss >> expected;
 
-  bool b = f1->accepts_eword();
+      spot::ltl::parse_error_list p1;
+      const spot::ltl::formula* f1 = spot::ltl::parse_sere(form, p1);
+      if (spot::ltl::format_parse_errors(std::cerr, form, p1))
+	return 2;
 
-  std::cout << b << std::endl;
+      bool b = f1->accepts_eword();
+      std::cout << form << ',' << b << '\n';
+      if (b != expected)
+	{
+	  std::cerr << "computed '" << b
+		    << "' but expected '" << expected << "'\n";
+	  return 2;
+	}
+      f1->destroy();
+    }
 
-  f1->destroy();
   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::bunop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
-  return b;
+  return 0;
 }
diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test
index d1b840a8f..f95a1710f 100755
--- a/src/ltltest/consterm.test
+++ b/src/ltltest/consterm.test
@@ -25,26 +25,30 @@
 
 set -e
 
-run 0 ../consterm 'a'
-run 0 ../consterm '1'
-run 0 ../consterm '0'
-run 1 ../consterm '[*0]'
-run 1 ../consterm 'a*'
-run 1 ../consterm '0*'
-run 1 ../consterm 'a[*0]'
-run 1 ../consterm 'a[*0..]'
-run 1 ../consterm 'a[*0..3]'
-run 0 ../consterm 'a[*1..3]'
-run 0 ../consterm 'a[*3]'
-run 1 ../consterm 'a[*..4][*3]'
-run 0 ../consterm 'a[*1..4][*3]'
-run 1 ../consterm 'a[*1..4][*0..3]'
-run 0 ../consterm '((a ; b) + c)'
-run 1 ../consterm '((a ; b) + [*0])'
-run 0 ../consterm '((a ; b) + [*0]) & e'
-run 1 ../consterm '((a ; b) + [*0]) & [*0]'
-run 1 ../consterm '((a ; b) + [*0]) & (a* + b)'
-run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}'  # test braces
-run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])'
-run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])'
-run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])'
+cat >input2 <<EOF
+1,0
+0,0
+[*0],1
+a*,1
+0*,1
+a[*0],1
+a[*0..],1
+a[*0..3],1
+a[*1..3],0
+a[*3],0
+a[*..4][*3],1
+a[*1..4][*3],0
+a[*1..4][*0..3],1
+((a ; b) + c),0
+((a ; b) + [*0]),1
+((a ; b) + [*0]) & e,0
+((a ; b) + [*0]) & [*0],1
+((a ; b) + [*0]) & (a* + b),1
+# test braces
+{{a ; b} + {[*0]}} & {a* + b},1
+(a + [*0]);(b + [*0]);(c + [*0]),1
+(a + [*0]);(b + e);(c + [*0]),0
+(a + [*0]);(b + e)*;(c + [*0]),1
+EOF
+
+run 0 ../consterm input2
diff --git a/src/ltltest/kind.cc b/src/ltltest/kind.cc
index be448b00d..da45b7157 100644
--- a/src/ltltest/kind.cc
+++ b/src/ltltest/kind.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developement de
-// l'Epita (LRDE).
+// Copyright (C) 2010, 2012, 2015 Laboratoire de Recherche et
+// Developement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -18,6 +18,8 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <iostream>
+#include <fstream>
+#include <sstream>
 #include <cassert>
 #include <cstdlib>
 #include "ltlparse/public.hh"
@@ -36,16 +38,44 @@ main(int argc, char **argv)
   if (argc != 2)
     syntax(argv[0]);
 
-  spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  std::ifstream input(argv[1]);
+  if (!input)
+    {
+      std::cerr << "failed to open " << argv[1] << '\n';
+      return 2;
+    }
 
-  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
-    return 2;
+  std::string s;
+  while (std::getline(input, s))
+    {
+      if (s[0] == '#')		// Skip comments
+	{
+	  std::cerr << s << '\n';
+	  continue;
+	}
+      std::istringstream ss(s);
+      std::string form;
+      std::string expected;
+      std::getline(ss, form, ',');
+      std::getline(ss, expected);
 
-  spot::ltl::print_formula_props(std::cout, f1, true) << " = ";
-  spot::ltl::print_formula_props(std::cout, f1, false) << std::endl;
+      spot::ltl::parse_error_list p1;
+      const spot::ltl::formula* f1 = spot::ltl::parse(form, p1);
+      if (spot::ltl::format_parse_errors(std::cerr, form, p1))
+	return 2;
 
-  f1->destroy();
+      std::ostringstream so;
+      spot::ltl::print_formula_props(so, f1, true);
+      auto sost = so.str();
+      std::cout << form << ',' << sost << '\n';
+      if (sost != expected)
+	{
+	  std::cerr << "computed '" << sost
+		    << "' but expected '" << expected << "'\n";
+	  return 2;
+	}
+      f1->destroy();
+    }
   assert(spot::ltl::atomic_prop::instance_count() == 0);
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test
index 8d1d78812..e7dc64ff5 100755
--- a/src/ltltest/kind.test
+++ b/src/ltltest/kind.test
@@ -25,135 +25,111 @@
 
 set -e
 
-check()
-{
-    run 0 ../kind "$1" >out
-    read word rest <out
-    test "$word" = "$2"
-}
+cat >input<<EOF
+a,B&!xfLEPSFsgopr
+a<->b,BxfLEPSFsgopr
+!a,B&!xfLEPSFsgopr
+!(a|b),B&xfLEPSFsgopr
+F(a),&!xLPegopr
+G(a),&!xLPusopr
+a U b,&!xfLPgopr
+a U Fb,&!xLPegopr
+Ga U b,&!xLPopr
+1 U a,&!xfLPegopr
+a W b,&!xfLPsopr
+a W 0,&!xfLPusopr
+a M b,&!xfLPgopr
+a M 1,&!xfLPegopr
+a R b,&!xfLPsopr
+0 R b,&!xfLPusopr
+a R (b R (c R d)),&!xfLPsopr
+a U (b U (c U d)),&!xfLPgopr
+a W (b W (c W d)),&!xfLPsopr
+a M (b M (c M d)),&!xfLPgopr
+Fa -> Fb,xLPopr
+Ga -> Fb,xLPgopr
+Fa -> Gb,xLPsopr
+(Ga|Fc) -> Fb,xLPopr
+(Ga|Fa) -> Gb,xLPopr
+{a;c*;b}|->!Xb,&fPsopr
+{a;c*;b}|->X!b,&!fPsopr
+{a;c*;b}|->!Fb,&Psopr
+{a;c*;b}|->G!b,&!Psopr
+{a;c*;b}|->!Gb,&Pr
+{a;c*;b}|->F!b,&!Pr
+{a;c*;b}|->GFa,&!Pr
+{a;c*;b}|->FGa,&!P
+{a[+];c[+];b*}|->!Fb,&xPsopr
+{a[+];c*;b[+]}|->G!b,&!xPsopr
+{a*;c[+];b[+]}|->!Gb,&xPr
+{a[+];c*;b[+]}|->F!b,&!xPr
+{a[+];c[+];b*}|->GFa,&!xPr
+{a*;c[+];b[+]}|->FGa,&!xP
+{a;c;b|(d;e)}|->!Xb,&fPFsgopr
+{a;c;b|(d;e)}|->X!b,&!fPFsgopr
+{a;c;b|(d;e)}|->!Fb,&Psopr
+{a;c;b|(d;e)}|->G!b,&!Psopr
+{a;c;b|(d;e)}|->!Gb,&Pgopr
+{a;c;b|(d;e)}|->F!b,&!Pgopr
+{a;c;b|(d;e)}|->GFa,&!Pr
+{a;c;b|(d;e)}|->FGa,&!Pp
+{a[+] && c[+]}|->!Xb,&fPsopr
+{a[+] && c[+]}|->X!b,&!fPsopr
+{a[+] && c[+]}|->!Fb,&xPsopr
+{a[+] && c[+]}|->G!b,&!xPsopr
+{a[+] && c[+]}|->!Gb,&xPr
+{a[+] && c[+]}|->F!b,&!xPr
+{a[+] && c[+]}|->GFa,&!xPr
+{a[+] && c[+]}|->FGa,&!xP
+{a;c*;b}<>->!Gb,&Pgopr
+{a;c*;b}<>->F!b,&!Pgopr
+{a;c*;b}<>->FGb,&!Pp
+{a;c*;b}<>->!GFb,&Pp
+{a;c*;b}<>->GFb,&!P
+{a;c*;b}<>->!FGb,&P
+{a*;c[+];b[+]}<>->!FGb,&xP
+{a;c|d;b}<>->!Gb,&Pgopr
+{a;c|d;b}<>->G!b,&!Psopr
+{a;c|d;b}<>->FGb,&!Pp
+{a;c|d;b}<>->!GFb,&Pp
+{a;c|d;b}<>->GFb,&!Pr
+{a;c|d;b}<>->!FGb,&Pr
+# Equivalent to a&b&c&d
+{a:b:c:d}!,B&!xfLEPSFsgopr
+a&b&c&d,B&!xfLEPSFsgopr
+(Xa <-> XXXc) U (b & Fe),LPgopr
+(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopr
+(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopr
+(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopr
+(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopr
+(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPp
+(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPr
+(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPp
+(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPup
+(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPr
+(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPer
+(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPep
+(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LP
+(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPur
+(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LP
+GFa M GFb,&!xLPeu
+FGa M FGb,&!xLPeup
+Fa  M GFb,&!xLPer
+GFa W GFb,&!xLPeur
+FGa W FGb,&!xLPeu
+Ga  W FGb,&!xLPup
+Ga  W b,&!xLPsopr
+Fa  M b,&!xLPgopr
+{a;b*;c},&!fPsopr
+{a;b*;c}!,&!fPgopr
+# The negative normal form is {a;b*;c}[]->1
+!{a;b*;c}!,&fPsopr
+{a;b*;c}[]->0,&!fPsopr
+!{a;b*;c},&!fPgopr
+!{a[+];b*;c[+]},&!xfPgopr
+{a[+];b*;c[+]},&!xfPsopr
+{a[+] && b || c[+]},&!fPsopr
+{a[+] && b[+] || c[+]},&!xfPsopr
+EOF
 
-check 'a'         'B&!xfLEPSFsgopr'
-check 'a<->b'     'BxfLEPSFsgopr'
-check '!a'        'B&!xfLEPSFsgopr'
-check '!(a|b)'    'B&xfLEPSFsgopr'
-check 'F(a)'      '&!xLPegopr'
-check 'G(a)'      '&!xLPusopr'
-check 'a U b'     '&!xfLPgopr'
-check 'a U Fb'    '&!xLPegopr'
-check 'Ga U b'    '&!xLPopr'
-check '1 U a'     '&!xfLPegopr'
-check 'a W b'     '&!xfLPsopr'
-check 'a W 0'     '&!xfLPusopr'
-check 'a M b'     '&!xfLPgopr'
-check 'a M 1'     '&!xfLPegopr'
-check 'a R b'     '&!xfLPsopr'
-check '0 R b'     '&!xfLPusopr'
-check 'a R (b R (c R d))' '&!xfLPsopr'
-check 'a U (b U (c U d))' '&!xfLPgopr'
-check 'a W (b W (c W d))' '&!xfLPsopr'
-check 'a M (b M (c M d))' '&!xfLPgopr'
-check 'Fa -> Fb'  'xLPopr'
-check 'Ga -> Fb'  'xLPgopr'
-check 'Fa -> Gb'  'xLPsopr'
-check '(Ga|Fc) -> Fb'  'xLPopr'
-check '(Ga|Fa) -> Gb'  'xLPopr'
-check '{a;c*;b}|->!Xb' '&fPsopr'
-check '{a;c*;b}|->X!b' '&!fPsopr'
-check '{a;c*;b}|->!Fb' '&Psopr'
-check '{a;c*;b}|->G!b' '&!Psopr'
-check '{a;c*;b}|->!Gb' '&Pr'
-check '{a;c*;b}|->F!b' '&!Pr'
-check '{a;c*;b}|->GFa' '&!Pr'
-check '{a;c*;b}|->FGa' '&!P'
-check '{a[+];c[+];b*}|->!Fb' '&xPsopr'
-check '{a[+];c*;b[+]}|->G!b' '&!xPsopr'
-check '{a*;c[+];b[+]}|->!Gb' '&xPr'
-check '{a[+];c*;b[+]}|->F!b' '&!xPr'
-check '{a[+];c[+];b*}|->GFa' '&!xPr'
-check '{a*;c[+];b[+]}|->FGa' '&!xP'
-check '{a;c;b|(d;e)}|->!Xb' '&fPFsgopr'
-check '{a;c;b|(d;e)}|->X!b' '&!fPFsgopr'
-check '{a;c;b|(d;e)}|->!Fb' '&Psopr'
-check '{a;c;b|(d;e)}|->G!b' '&!Psopr'
-check '{a;c;b|(d;e)}|->!Gb' '&Pgopr'
-check '{a;c;b|(d;e)}|->F!b' '&!Pgopr'
-check '{a;c;b|(d;e)}|->GFa' '&!Pr'
-check '{a;c;b|(d;e)}|->FGa' '&!Pp'
-check '{a[+] && c[+]}|->!Xb' '&fPsopr'
-check '{a[+] && c[+]}|->X!b' '&!fPsopr'
-check '{a[+] && c[+]}|->!Fb' '&xPsopr'
-check '{a[+] && c[+]}|->G!b' '&!xPsopr'
-check '{a[+] && c[+]}|->!Gb' '&xPr'
-check '{a[+] && c[+]}|->F!b' '&!xPr'
-check '{a[+] && c[+]}|->GFa' '&!xPr'
-check '{a[+] && c[+]}|->FGa' '&!xP'
-check '{a;c*;b}<>->!Gb' '&Pgopr'
-check '{a;c*;b}<>->F!b' '&!Pgopr'
-check '{a;c*;b}<>->FGb' '&!Pp'
-check '{a;c*;b}<>->!GFb' '&Pp'
-check '{a;c*;b}<>->GFb' '&!P'
-check '{a;c*;b}<>->!FGb' '&P'
-check '{a*;c[+];b[+]}<>->!FGb' '&xP'
-check '{a;c|d;b}<>->!Gb' '&Pgopr'
-check '{a;c|d;b}<>->G!b' '&!Psopr'
-check '{a;c|d;b}<>->FGb' '&!Pp'
-check '{a;c|d;b}<>->!GFb' '&Pp'
-check '{a;c|d;b}<>->GFb' '&!Pr'
-check '{a;c|d;b}<>->!FGb' '&Pr'
-check '{a:b:c:d}!' 'B&!xfLEPSFsgopr'  # Equivalent to a&b&c&d
-check 'a&b&c&d'    'B&!xfLEPSFsgopr'
-check '(Xa <-> XXXc) U (b & Fe)' 'LPgopr'
-check '(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b))' 'LPegopr'
-check '(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b))' 'LPusopr'
-check '(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b))' 'LPeopr'
-check '(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b))' 'LPuopr'
-check '(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b))' 'LPp'
-check '(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b))' 'LPr'
-check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b))' 'LPp'
-check '(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b))' 'LPup'
-check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b))' 'LPr'
-check '(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b))' 'LPer'
-check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb))' 'LPep'
-check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb))' 'LP'
-check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb))' 'LPur'
-check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb))' 'LP'
-check 'GFa M GFb' '&!xLPeu'
-check 'FGa M FGb' '&!xLPeup'
-check 'Fa  M GFb' '&!xLPer'
-check 'GFa W GFb' '&!xLPeur'
-check 'FGa W FGb' '&!xLPeu'
-check 'Ga  W FGb' '&!xLPup'
-check 'Ga  W b'   '&!xLPsopr'
-check 'Fa  M b'   '&!xLPgopr'
-check '{a;b*;c}' '&!fPsopr'
-check '{a;b*;c}!' '&!fPgopr'
-check '!{a;b*;c}!' '&fPsopr'  # The negative normal form is {a;b*;c}[]->0
-check '{a;b*;c}[]->0' '&!fPsopr'
-check '!{a;b*;c}' '&!fPgopr'
-check '!{a[+];b*;c[+]}' '&!xfPgopr'
-check '{a[+];b*;c[+]}' '&!xfPsopr'
-check '{a[+] && b || c[+]}' '&!fPsopr'
-check '{a[+] && b[+] || c[+]}' '&!xfPsopr'
-
-run 0 ../consterm '1'
-run 0 ../consterm '0'
-run 1 ../consterm '[*0]'
-run 1 ../consterm 'a*'
-run 1 ../consterm '0*'
-run 1 ../consterm 'a[*0]'
-run 1 ../consterm 'a[*0..]'
-run 1 ../consterm 'a[*0..3]'
-run 0 ../consterm 'a[*1..3]'
-run 0 ../consterm 'a[*3]'
-run 1 ../consterm 'a[*..4][*3]'
-run 0 ../consterm 'a[*1..4][*3]'
-run 1 ../consterm 'a[*1..4][*0..3]'
-run 0 ../consterm '((a ; b) + c)'
-run 1 ../consterm '((a ; b) + [*0])'
-run 0 ../consterm '((a ; b) + [*0]) & e'
-run 1 ../consterm '((a ; b) + [*0]) & [*0]'
-run 1 ../consterm '((a ; b) + [*0]) & (a* + b)'
-run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}'  # test braces
-run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])'
-run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])'
-run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])'
+run 0 ../kind input