diff --git a/ChangeLog b/ChangeLog
index ff4c675ee..87b8669e5 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,12 @@
 2003-10-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* iface/gspn/Makefile.am (check_PROGRAMS): Add eltlgspn-srg.
+	(eltlgspn_srg_SOURCES, eltlgspn_srg_LDADD, eltlgspn_srg_CPPFLAGS):
+	New variables.
+	(TESTS): Add dcswaveeltl.test.
+	* iface/gspn/dcswaveeltl.test: New file.
+	* iface/gspn/ltlgspn.cc [CEC]: Use emptiness_check.
+
 	* m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New files.
 	* Makefile.am (EXTRA_DIST): Add them.
 	* configure.ac: Call adl_ENABLE_DEVEL, adl_ENABLE_DEBUG, ad_GCC_OPTIM,
diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am
index 94061c6c2..ae4848a28 100644
--- a/iface/gspn/Makefile.am
+++ b/iface/gspn/Makefile.am
@@ -16,6 +16,7 @@ check_PROGRAMS = \
   dottygspn-srg \
   ltlgspn-rg \
   ltlgspn-srg \
+  eltlgspn-srg \
   fmgspn-rg \
   fmgspn-srg
 
@@ -31,6 +32,10 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
 ltlgspn_srg_SOURCES = ltlgspn.cc
 ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
 
+eltlgspn_srg_SOURCES = ltlgspn.cc
+eltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
+eltlgspn_srg_CPPFLAGS = -DCEC $(AM_CPPFLAGS)
+
 fmgspn_rg_SOURCES = ltlgspn.cc
 fmgspn_rg_CPPFLAGS = -DFM $(AM_CPPFLAGS)
 fmgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
@@ -52,7 +57,8 @@ TESTS = \
   simple.test \
   dcswave.test \
   dcswaveltl.test \
-  dcswavefm.test
+  dcswavefm.test \
+  dcswaveeltl.test
 
 # Each test case depends on defs.
 check_SCRIPTS = defs
diff --git a/iface/gspn/dcswaveeltl.test b/iface/gspn/dcswaveeltl.test
new file mode 100755
index 000000000..223c0db5d
--- /dev/null
+++ b/iface/gspn/dcswaveeltl.test
@@ -0,0 +1,15 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+set -e
+
+cp -R $srcdir/examples/DCSwave .
+chmod +w DCSwave
+
+# G(ATTiIDLj => F(!SCj U SCi)) is true
+../eltlgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output
+
+# G(F(!SCj U SCi)) is false
+../eltlgspn-srg DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj > output \
+  || test $? = 1
diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc
index 32394987e..1eb483b68 100644
--- a/iface/gspn/ltlgspn.cc
+++ b/iface/gspn/ltlgspn.cc
@@ -6,6 +6,7 @@
 #include "tgbaalgos/ltl2tgba_lacim.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/magic.hh"
+#include "tgbaalgos/emptinesscheck.hh"
 
 int
 main(int argc, char **argv)
@@ -44,8 +45,22 @@ main(int argc, char **argv)
 
       spot::tgba* model        = new spot::tgba_gspn(dict, env);
       spot::tgba_product* prod = new spot::tgba_product(model, a_f);
+#if CEC
+      {
+	spot::emptiness_check empty_check;
+	bool res = empty_check.tgba_emptiness_check(prod);
+	if (!res)
+	  {
+	    empty_check.counter_example(prod);
+	    exit(1);
+	  }
+	else
+	  {
+	    std::cout << "not found";
+	  }
+      }
+#else
       spot::tgba_tba_proxy* d  = new spot::tgba_tba_proxy(prod);
-
       {
 	spot::magic_search ms(d);
 
@@ -59,8 +74,8 @@ main(int argc, char **argv)
 	    std::cout << "not found";
 	  }
       }
-
       delete d;
+#endif
       delete prod;
       delete model;
       delete a_f;