diff --git a/NEWS b/NEWS
index eb2ec2e4d..3666d89ae 100644
--- a/NEWS
+++ b/NEWS
@@ -7,6 +7,13 @@ New in spot 1.1.3a (not released)
     - When used from ltlcross, the same parser would fail to
       parse further neverclaims after the first failure.
     - Add a missing newline in some error message of ltlcross.
+    - Expressions like {SERE} were wrongly translated and simplified
+      for SEREs that accept the empty word: they were wrongly reduced
+      to true.  Simplification and translation rules have been fixed,
+      and the doc/tl/tl.pdf specifications have been updated to better
+      explain that {SERE} has the semantics of a closure operator that
+      is not exactly what one could expect after reading the PSL
+      standard.
 
 New in spot 1.1.3 (2013-07-09)
 
diff --git a/THANKS b/THANKS
index f318e8a9e..2960fe0ac 100644
--- a/THANKS
+++ b/THANKS
@@ -3,6 +3,7 @@ suggestions.
 
 Akim Demaille
 Christian Dax
+Ernesto Posse
 Étienne Renault
 Felix Klaedtke
 František Blahoudek
diff --git a/doc/tl/tl.bib b/doc/tl/tl.bib
index bf0bee99b..7ccab7f74 100644
--- a/doc/tl/tl.bib
+++ b/doc/tl/tl.bib
@@ -12,7 +12,7 @@
   publisher	= {Springer},
   series	= {Lecture Notes in Computer Science},
   volume	= {7214},
-  pages         = {95--109}
+  pages		= {95--109}
 }
 
 @InProceedings{	  beer.01.cav,
@@ -80,6 +80,20 @@
   note		= {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}}
 }
 
+@InProceedings{	  dax.09.atva,
+  author	= {Christian Dax and Felix Klaedtke and Stefan Leue},
+  title		= {Specification Languages for Stutter-Invariant Regular
+		  Properties},
+  booktitle	= {Proceedings of the 7th International Symposium on
+		  Automated Technology for Verification and Analysis
+		  (ATVA'09)},
+  pages		= {244--254},
+  year		= {2009},
+  volume	= {5799},
+  series	= {Lecture Notes in Computer Science},
+  publisher	= {Springer-Verlag}
+}
+
 @InProceedings{	  duret.11.vecos,
   author	= {Alexandre Duret-Lutz},
   title		= {{LTL} Translation Improvements in {Spot}},
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 8947c9cfa..57c9f8ede 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -833,6 +833,13 @@ is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT
     a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT
     a\STAR{}))}$} because this SERE does accept any word.
 
+Note that the semantics of $\sere{r}$ comes from the
+$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}.  This
+differs from the interpretation of a SERE in the context of a temporal
+formula given by the PSL standard~\citep[Appendix~B.3.1.1.2,
+item~7]{psl.04.lrm}: the $\mathit{cl}(\cdot)$ semantics accepts more
+words.
+
 \subsection{Syntactic Sugar}\label{sec:pslsugar}
 
 The syntax on the left is equivalent to the syntax on the right.
@@ -869,8 +876,8 @@ formula $b$, the following rewritings are systematically performed
 & \nsere{\1} & \equiv \0 \\
   \sere{\eword}\Asuffix f&\equiv \1
 & \sere{\eword}\Esuffix f&\equiv \0
-& \sere{\eword} & \equiv \1
-& \nsere{\eword} & \equiv \0 \\
+& \sere{\eword} & \equiv \0
+& \nsere{\eword} & \equiv \1 \\
   \sere{b}\Asuffix f&\equiv (\NOT{b})\OR f
 & \sere{b}\Esuffix f&\equiv b\AND f
 & \sere{b} &\equiv b
@@ -1531,10 +1538,12 @@ denoted with $\equiV$ can be disabled by setting the
 
 Here are basic the rewritings for the weak closure and its negation:
 \begin{align*}
-  \sere{r}&\equiv \1\text{~if~}\varepsilon\VDash r&
-  \nsere{r}&\equiv \0\text{~if~}\varepsilon\VDash r\\
-  \sere{r_1;r_2}&\equiv \sere{r_1}\text{~if~}\varepsilon\VDash r_2&
-  \nsere{r_1;r_2}&\equiv \nsere{r_1}\text{~if~}\varepsilon\VDash r_2\\
+  \sere{r\STAR{}}&\equiv \sere{r}&
+  \nsere{r\STAR{}}&\equiv \nsere{r}\\
+  \sere{r_1;r_2}&\equiv \sere{r_1}\phantom{{}\OR\sere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2&
+  \nsere{r_1;r_2}&\equiv \nsere{r_1}\phantom{{}\AND\nsere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2\\
+  \sere{r_1;r_2}&\equiv \sere{r_1}\OR\sere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2&
+  \nsere{r_1;r_2}&\equiv \nsere{r_1}\AND\nsere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2\\
   \sere{b;r}&\equiV b\AND\X\sere{r}&
   \nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\
   \sere{b\STAR{};r}&\equiv b\W\sere{r}&
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index 8717493f1..2ac6cbec8 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -292,19 +292,19 @@ namespace spot
 	  // {0} = 0, {1} = 1,  {b} = b
 	  if (child->is_boolean())
 	    return child;
-	  // {[*0]} = 1
+	  // {[*0]} = 0
 	  if (child == constant::empty_word_instance())
-	    return constant::true_instance();
+	    return constant::false_instance();
 	  break;
 
 	case NegClosure:
 	case NegClosureMarked:
-	  // {1} = 0,  {[*0]} = 0
-	  if (child == constant::true_instance()
-	      || child == constant::empty_word_instance())
+	  // {1} = 0
+	  if (child == constant::true_instance())
 	    return constant::false_instance();
-	  // {0} = 1
-	  if (child == constant::false_instance())
+	  // {0} = 1,  {[*0]} = 1
+	  if (child == constant::false_instance()
+	      || child == constant::empty_word_instance())
 	    return constant::true_instance();
 	  // {b} = !b
 	  if (child->is_boolean())
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 633346faf..e71e7ffd6 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -1550,16 +1550,17 @@ namespace spot
 	    case unop::Closure:
 	    case unop::NegClosure:
 	    case unop::NegClosureMarked:
-	      // {e} = 1 if e accepts [*0]
-	      // !{e} = 0 if e accepts [*0]
+	      // {e[*]} = {e}
+	      // !{e[*]} = !{e}
 	      if (result_->accepts_eword())
-		{
-		  result_->destroy();
-		  result_ = ((op == unop::Closure)
-			     ? constant::true_instance()
-			     : constant::false_instance());
-		  return;
-		}
+		if (const bunop* bo = is_Star(result_))
+		  {
+		    result_ =
+		      recurse_destroy(unop::instance(op,
+						     bo->child()->clone()));
+		    bo->destroy();
+		    return;
+		  }
 	      if (!opt_.reduce_size_strictly)
 		if (const multop* mo = is_OrRat(result_))
 		  {
@@ -1578,6 +1579,26 @@ namespace spot
 		  }
 	      if (const multop* mo = is_Concat(result_))
 		{
+		  if (mo->accepts_eword())
+		    {
+		      if (opt_.reduce_size_strictly)
+			break;
+		      // If all terms accept the empty word, we have
+		      // {e₁;e₂;e₃} =  {e₁}|{e₂}|{e₃}
+		      // !{e₁;e₂;e₃} = !{e₁}&!{e₂}&!{e₃}
+		      multop::vec* v = new multop::vec;
+		      unsigned end = mo->size();
+		      v->reserve(end);
+		      for (unsigned i = 0; i < end; ++i)
+			v->push_back(unop::instance(op, mo->nth(i)->clone()));
+		      mo->destroy();
+		      result_ = multop::instance(op == unop::Closure ?
+						 multop::Or : multop::And, v);
+		      result_ = recurse_destroy(result_);
+		      return;
+		    }
+
+		  // Some term does not accept the empty word.
 		  unsigned end = mo->size() - 1;
 		  // {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
 		  //    = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂}))
@@ -1601,15 +1622,25 @@ namespace spot
 		  unsigned s = end + 1 - start;
 		  if (s != mo->size())
 		    {
-		      multop::vec* v = new multop::vec;
-		      v->reserve(s);
-		      for (unsigned n = start; n <= end; ++n)
-			v->push_back(mo->nth(n)->clone());
-		      const formula* tail =
-			multop::instance(multop::Concat, v);
-		      tail = unop::instance(op, tail);
-
 		      bool doneg = op != unop::Closure;
+		      const formula* tail;
+		      if (s > 0)
+			{
+			  multop::vec* v = new multop::vec;
+			  v->reserve(s);
+			  for (unsigned n = start; n <= end; ++n)
+			    v->push_back(mo->nth(n)->clone());
+			  tail = multop::instance(multop::Concat, v);
+			  tail = unop::instance(op, tail);
+			}
+		      else
+			{
+			  if (doneg)
+			    tail = constant::false_instance();
+			  else
+			    tail = constant::true_instance();
+			}
+
 		      for (unsigned n = start; n > 0;)
 			{
 			  --n;
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 0988e461f..290f3b6b5 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1367,12 +1367,6 @@ namespace spot
 	    {
 	      // rat_seen_ = true;
 	      const formula* f = node->child();
-	      if (f->accepts_eword())
-		{
-		  res_ = bddtrue;
-		  return;
-		}
-
 	      tgba_succ_iterator* i = dict_.transdfa.succ(f);
 	      res_ = bddfalse;
 
@@ -1410,11 +1404,6 @@ namespace spot
 	    rat_seen_ = true;
 	    {
 	      const formula* c = node->child();
-	      if (c->accepts_eword())
-		{
-		  res_ = bddfalse;
-		  return;
-		}
 	      if (mark_all_)
 		{
 		  op = unop::NegClosureMarked;
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index a3098dd5a..afbf703d6 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -209,3 +209,11 @@ grep 'states: 4$' stdout
 # the following formula to be considered equivalent to anything...
 ../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'false' && exit 1
 ../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'true'
+
+# Test some equivalences fixed in Spot 1.1.4
+../../bin/ltlfilt    -f '{{a;b}[*]}'  --equivalent-to 'a & Xb'
+../../bin/ltlfilt -r -f '{{a;b}[*]}'  --equivalent-to 'a & Xb'
+../../bin/ltlfilt    -f '!{{a;b}[*]}' --equivalent-to '!a | X!b'
+../../bin/ltlfilt -r -f '!{{a;b}[*]}' --equivalent-to '!a | X!b'
+../../bin/ltlfilt    -f '{a[*];b[*]}' --equivalent-to 'a | b'
+../../bin/ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b'