diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc
index 243bc7a1f..b3730f31d 100644
--- a/src/bin/randltl.cc
+++ b/src/bin/randltl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -283,7 +283,8 @@ main(int argc, char** argv)
       break;
     case OutputSERE:
       rf = rs = new spot::ltl::random_sere(&aprops);
-      tok_pS = rf->parse_options(opt_pS);
+      tok_pS = rs->parse_options(opt_pS);
+      tok_pB = rs->rb.parse_options(opt_pB);
       if (opt_pL)
 	error(2, 0, "option --ltl-priorities unsupported for SERE output");
       break;
@@ -335,6 +336,7 @@ main(int argc, char** argv)
 	default:
 	  error(2, 0, "internal error: unknown type of output");
 	}
+      destroy_atomic_prop_set(aprops);
       exit(0);
     }
 
@@ -409,10 +411,6 @@ main(int argc, char** argv)
       (*i)->destroy();
   }
   // Cleanup the atomic_prop set.
-  {
-    spot::ltl::atomic_prop_set::const_iterator i = aprops.begin();
-    while (i != aprops.end())
-      (*(i++))->destroy();
-  }
+  destroy_atomic_prop_set(aprops);
   return 0;
 }
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 887530240..f241a6443 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -1,8 +1,9 @@
-## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
+## Recherche et Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-## Université Pierre et Marie Curie.
+## 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.
 ##
@@ -101,6 +102,7 @@ TESTS = \
   latex.test \
   lbt.test \
   lenient.test \
+  rand.test \
   isop.test \
   syntimpl.test \
   reduc.test \
diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test
new file mode 100755
index 000000000..b7750582c
--- /dev/null
+++ b/src/ltltest/rand.test
@@ -0,0 +1,99 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2014 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+set -e
+
+randltl=../../bin/randltl
+
+run 0 $randltl -S -n 20 a b c --tree-size=10 \
+    --sere-priorities=and=0,andNLM=0 \
+    --boolean-priorities=equiv=0,implies=0,xor=0,and=0,not=0 \
+    --dump-priorities > stdout
+
+cat >expected <<EOF
+Use --sere-priorities to set the following SERE priorities:
+eword	1
+boolform	1
+star	1
+star_b	1
+and	0
+andNLM	0
+or	1
+concat	1
+fusion	1
+Use --boolean-priorities to set the following Boolean formula priorities:
+ap	3
+false	1
+true	1
+not	0
+equiv	0
+implies	0
+xor	0
+and	0
+or	1
+EOF
+diff stdout expected
+
+
+run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \
+   --sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \
+   --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \
+   --dump-pr > stdout
+
+cat >expected <<EOF
+Use --sere-priorities to set the following SERE priorities:
+eword	0
+boolform	1
+star	0
+star_b	0
+and	0
+andNLM	0
+or	0
+concat	0
+fusion	0
+Use --boolean-priorities to set the following Boolean formula priorities:
+ap	3
+false	0
+true	0
+not	0
+equiv	0
+implies	0
+xor	0
+and	0
+or	0
+EOF
+diff stdout expected
+
+
+
+# Disabling all operators will prevent more formulas to be generated.
+$randltl -S -n 10000 a b c --tree-size=10..20 \
+ --sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \
+ --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out &&
+  exit 1
+sort out > out2
+cat >expected <<EOF
+a
+b
+c
+EOF
+
+diff expected out2
diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc
index be32748f4..50d99a615 100644
--- a/src/ltlvisit/apcollect.cc
+++ b/src/ltlvisit/apcollect.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -53,6 +53,14 @@ namespace spot
       };
     }
 
+    void destroy_atomic_prop_set(atomic_prop_set& aprops)
+    {
+      atomic_prop_set::const_iterator i = aprops.begin();
+      while (i != aprops.end())
+	(*(i++))->destroy();
+    }
+
+
     atomic_prop_set*
     atomic_prop_collect(const formula* f, atomic_prop_set* s)
     {
diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh
index 480480b0e..382f203ea 100644
--- a/src/ltlvisit/apcollect.hh
+++ b/src/ltlvisit/apcollect.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -40,6 +40,11 @@ namespace spot
     typedef std::set<const atomic_prop*,
 		     formula_ptr_less_than> atomic_prop_set;
 
+    /// \brief Destroy all the atomic propositions in an
+    /// atomic_prop_set.
+    SPOT_API void
+    destroy_atomic_prop_set(atomic_prop_set& as);
+
     /// \brief Return the set of atomic propositions occurring in a formula.
     ///
     /// \param f the formula to inspect
diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc
index 99c268cf6..029e77692 100644
--- a/src/ltlvisit/randomltl.cc
+++ b/src/ltlvisit/randomltl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -191,9 +191,7 @@ namespace spot
 	  else
 	    assert(!"unexpected max_n");
 	}
-      assert(total_1_ != 0.0);
-      assert(total_2_ != 0.0);
-      assert(total_2_and_more_ != 0.0);
+      assert(total_2_and_more_ >= total_2_);
     }
 
     const formula*
@@ -204,6 +202,30 @@ namespace spot
       double r = drand();
       op_proba* p;
 
+      // Approximate impossible cases.
+      if (n == 1 && total_1_ == 0.0)
+	{
+	  if (total_2_ != 0.0)
+	    n = 2;
+	  else
+	    n = 3;
+	}
+      else if (n == 2 && total_2_ == 0.0)
+	{
+	  if (total_1_ != 0.0)
+	    n = 1;
+	  else
+	    n = 3;
+	}
+      else if (n > 2 && total_2_and_more_ == 0.0)
+	{
+	  if (total_1_ != 0.0)
+	    n = 1;
+	  else
+	    assert(total_2_ == 0.0);
+	}
+
+
       if (n == 1)
 	{
 	  r *= total_1_;