diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 4c23e44bd..a3693158a 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -28,6 +28,7 @@ LDADD = ../libspot.la
 check_SCRIPTS = defs
 # Keep this sorted alphabetically.
 check_PROGRAMS = \
+  consterm \
   equals \
   length \
   ltl2dot \
@@ -47,6 +48,7 @@ noinst_PROGRAMS = \
   genltl \
   randltl
 
+consterm_SOURCES = consterm.cc
 equals_SOURCES = equals.cc
 genltl_SOURCES = genltl.cc
 length_SOURCES = length.cc
@@ -86,6 +88,7 @@ TESTS = \
   tunabbrev.test \
   nenoform.test \
   tunenoform.test \
+  consterm.test \
   syntimpl.test \
   reduc.test \
   reduccmp.test
diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc
new file mode 100644
index 000000000..ddf0b2e8d
--- /dev/null
+++ b/src/ltltest/consterm.cc
@@ -0,0 +1,57 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developement de
+// l'Epita (LRDE).
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <iostream>
+#include <cassert>
+#include <cstdlib>
+#include "ltlparse/public.hh"
+#include "ltlvisit/consterm.hh"
+#include "ltlast/allnodes.hh"
+
+void
+syntax(char *prog)
+{
+  std::cerr << prog << " formula" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char **argv)
+{
+  if (argc != 2)
+    syntax(argv[0]);
+
+  spot::ltl::parse_error_list p1;
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
+    return 2;
+
+  bool b = spot::ltl::constant_term_as_bool(f1);
+
+  std::cout << b << std::endl;
+
+  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::multop::instance_count() == 0);
+  return b;
+}
diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test
new file mode 100755
index 000000000..864b489b4
--- /dev/null
+++ b/src/ltltest/consterm.test
@@ -0,0 +1,40 @@
+#! /bin/sh
+# Copyright (C) 2010 Laboratoire de Recherche et Developement to
+# l'Epita (LRDE).
+#
+# 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+# Check for the constant_term visitor
+
+. ./defs || exit 1
+
+set -e
+
+run 0 ../consterm 'a'
+run 0 ../consterm '1'
+run 0 ../consterm '0'
+run 1 ../consterm '#e'
+run 1 ../consterm 'a*'
+run 1 ../consterm '0*'
+run 0 ../consterm '!#e'
+run 0 ../consterm '((a U b) + c)'
+run 1 ../consterm '((a U b) + #e)'
+run 0 ../consterm '((a U b) + #e) & e'
+run 1 ../consterm '((a U b) + #e) & #e'
+run 1 ../consterm '((a U b) + #e) & (a* + b)'
diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am
index 6456f4250..298447792 100644
--- a/src/ltlvisit/Makefile.am
+++ b/src/ltlvisit/Makefile.am
@@ -1,4 +1,4 @@
-## Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+## Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement de
 ## l'Epita (LRDE).
 ## Copyright (C) 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -29,6 +29,7 @@ ltlvisitdir = $(pkgincludedir)/ltlvisit
 ltlvisit_HEADERS = \
   apcollect.hh \
   basicreduce.hh \
+  consterm.hh \
   contain.hh \
   clone.hh \
   destroy.hh \
@@ -49,6 +50,7 @@ noinst_LTLIBRARIES = libltlvisit.la
 libltlvisit_la_SOURCES = \
   apcollect.cc \
   basicreduce.cc \
+  consterm.cc \
   contain.cc \
   clone.cc \
   destroy.cc \
diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc
new file mode 100644
index 000000000..f2816b6c5
--- /dev/null
+++ b/src/ltlvisit/consterm.cc
@@ -0,0 +1,150 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'EPITA (LRDE).
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "ltlvisit/consterm.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlast/visitor.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    namespace
+    {
+      class consterm_visitor: public const_visitor
+      {
+      public:
+	consterm_visitor() {}
+	virtual ~consterm_visitor() {}
+
+	bool result() const { return result_; }
+
+	void
+	visit(const atomic_prop*)
+	{
+	  result_ = false;
+	}
+
+	void
+	visit(const constant* c)
+	{
+	  result_ = (c == constant::empty_word_instance());
+	}
+
+	void
+	visit(const binop* bo)
+	{
+	  switch (bo->op())
+	    {
+	    case binop::Xor:
+	    case binop::Implies:
+	    case binop::Equiv:
+	      assert(!"const_term not yet defined on Xor, Implies and Equiv");
+	      break;
+	    case binop::U:
+	    case binop::W:
+	    case binop::M:
+	    case binop::R:
+	      result_ = false;
+	      break;
+	    }
+	}
+
+	void
+	visit(const unop* uo)
+	{
+	  switch (uo->op())
+	    {
+	    case unop::Not:
+	    case unop::X:
+	    case unop::F:
+	    case unop::G:
+	    case unop::Finish:
+	      result_ = false;
+	      break;
+	    case unop::Star:
+	      result_ = true;
+	      break;
+	    }
+	}
+
+	void
+	visit(const automatop*)
+	{
+	  assert(!"automatop not supported for constant term");
+	  result_ = false;
+	}
+
+	void
+	visit(const multop* mo)
+	{
+	  if (mo->op() == multop::Concat)
+	    {
+	      result_ = false;
+	      return;
+	    }
+
+	  unsigned max = mo->size();
+	  // This sets the initial value of result_.
+	  mo->nth(0)->accept(*this);
+
+	  for (unsigned n = 1; n < max; ++n)
+	    {
+	      bool r = constant_term_as_bool(mo->nth(n));
+
+	      switch (mo->op())
+		{
+		case multop::Or:
+		  result_ |= r;
+		  if (result_)
+		    return;
+		  break;
+		case multop::And:
+		  result_ &= r;
+		  if (!result_)
+		    return;
+		  break;
+		case multop::Concat:
+		  assert(!"unreachable code");
+		  break;
+		}
+	    }
+	}
+
+      private:
+	bool result_;
+      };
+
+    }
+
+    bool constant_term_as_bool(const formula* f)
+    {
+      consterm_visitor v;
+      f->accept(v);
+      return v.result();
+    }
+
+    formula* constant_term(const formula* f)
+    {
+      return constant_term_as_bool(f) ?
+	constant::empty_word_instance() : constant::false_instance();
+    }
+  }
+}
diff --git a/src/ltlvisit/consterm.hh b/src/ltlvisit/consterm.hh
new file mode 100644
index 000000000..e40f42df5
--- /dev/null
+++ b/src/ltlvisit/consterm.hh
@@ -0,0 +1,54 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'EPITA (LRDE).
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_LTLVISIT_CONSTERM_HH
+# define SPOT_LTLVISIT_CONSTERM_HH
+
+#include "ltlast/formula.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    /// \brief Compute the constant term of a formula.
+    /// \ingroup ltl_misc
+    ///
+    /// The constant term of a formula is the empty word if the empty
+    /// word is a model of the formula, it is false otherwise.
+    ///
+    /// \see constant_term_as_bool
+    formula* constant_term(const formula* f);
+
+    /// \brief Compute the constant term of a formula.
+    /// \ingroup ltl_misc
+    ///
+    /// The constant term of a formula is the empty word if the empty
+    /// word is a model of the formula, it is false otherwise.
+    ///
+    /// This variant of the function return true instead of
+    /// constant::empty_word_instance() and false instead of
+    /// constant::false_instance().
+    ///
+    /// \see constant_term
+    bool constant_term_as_bool(const formula* f);
+  }
+}
+
+#endif // SPOT_LTLVISIT_LENGTH_HH