diff --git a/NEWS b/NEWS
index cd7c00763..178ba5327 100644
--- a/NEWS
+++ b/NEWS
@@ -2,6 +2,9 @@ New in spot 2.12.0.dev (not yet released)
 
   Command-line tools:
 
+  - ltlmix is a new tool that generate formulas by combining existing
+    ones. See https://spot.lre.epita.fr/ltlmix.html for examples.
+
   - autfilt learned --restrict-dead-end-edges, to restricts labels of
     edges leading to dead-ends.  See the description of
     restrict_dead_end_edges_here() below.
@@ -38,8 +41,8 @@ New in spot 2.12.0.dev (not yet released)
 
   Bug fixes:
 
-  - Generating random formula without any unary opertors would very
-    often create formulas much smaller than asked.
+  - Generating random formulas without any unary opertor would very
+    often create formulas much smaller than specified.
 
 New in spot 2.12  (2024-05-16)
 
diff --git a/bin/Makefile.am b/bin/Makefile.am
index 78d189dc9..b665d859c 100644
--- a/bin/Makefile.am
+++ b/bin/Makefile.am
@@ -69,6 +69,7 @@ bin_PROGRAMS = \
   ltldo \
   ltlfilt \
   ltlgrind \
+  ltlmix \
   ltlsynt \
   randaut \
   randltl
@@ -92,6 +93,7 @@ ltl2tgta_SOURCES = ltl2tgta.cc
 ltlcross_SOURCES = ltlcross.cc
 ltlgrind_SOURCES = ltlgrind.cc
 ltldo_SOURCES = ltldo.cc
+ltlmix_SOURCES = ltlmix.cc
 ltlsynt_SOURCES = ltlsynt.cc
 dstar2tgba_SOURCES = dstar2tgba.cc
 spot_x_SOURCES = spot-x.cc
diff --git a/bin/ltlmix.cc b/bin/ltlmix.cc
new file mode 100644
index 000000000..9e6ada1c1
--- /dev/null
+++ b/bin/ltlmix.cc
@@ -0,0 +1,302 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) by the Spot authors, see the AUTHORS file for details.
+//
+// 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/>.
+
+
+#include "common_sys.hh"
+#include <argp.h>
+#include "error.h"
+
+#include "common_setup.hh"
+#include "common_finput.hh"
+#include "common_output.hh"
+#include "common_conv.hh"
+#include "common_cout.hh"
+#include "common_range.hh"
+
+#include <spot/tl/defaultenv.hh>
+#include <spot/tl/randomltl.hh>
+#include <spot/misc/random.hh>
+
+enum {
+  OPT_BOOLEAN_PRIORITIES = 256,
+  OPT_DUMP_PRIORITIES,
+  OPT_DUPS,
+  OPT_LTL_PRIORITIES,
+  OPT_SEED,
+  OPT_TREE_SIZE,
+};
+
+static const char * argp_program_doc =
+  "Combine formulas taken randomly from an input set.\n\n\
+The input set is specified using FILENAME, -F FILENAME, or -f formula.\n\
+By default this generates a Boolean pattern of size 5, for instance\n\
+\"(φ₁ & φ₂) | φ₃\", where each φᵢ is randomly taken from the input set.\n\
+The size and nature of the pattern can be changed using generation\n\
+parameters.  Additionally, it is possible to rename the atomic propositions\n\
+in each φᵢ using -A or -P.\v\
+Example:\n\
+\n\
+Generates 10 random Boolean combinations of terms of the form GFa, with\n\
+'a' picked from a set of 5 atomic propositions:\n\
+  % ltlmix -f GFa -n10 -A5\n\
+\n\
+Build a single LTL formula over subformulas taken randomly from the list of\n\
+55 patterns by Dwyer et al., using a choice of 10 atomic propositions to\n\
+relabel subformulas:\n\
+  % genltl --dac | ltlmix -L -A10\n\
+\n\
+Build 5 random positive Boolean combination of GFa and GFb:\n"
+  // next line is in its own double-quote to please sanity.test
+  "  % ltlmix -f GFa -f GFb --boolean-prio=not=0,xor=0,implies=0,equiv=0 -n5";
+
+static const argp_option options[] = {
+    // Keep this alphabetically sorted (expect for aliases).
+    /**************************************************/
+    { nullptr, 0, nullptr, 0, "Generation parameters:", 2 },
+    { "ap-count", 'A', "N", 0,
+      "rename the atomic propositions in each selected formula by drawing "
+      "randomly from N atomic propositions (the rewriting is bijective "
+      "if N is larger than the original set)", 0 },
+    { "polarized-ap", 'P', "N", 0,
+      "similar to -A N, but randomize the polarity of the new atomic "
+      "proposition", 0 },
+    { "boolean", 'B', nullptr, 0,
+      "generate Boolean combination of formulas (default)", 0 },
+    { "allow-dups", OPT_DUPS, nullptr, 0,
+      "allow duplicate formulas to be output", 0 },
+    { "ltl", 'L', nullptr, 0, "generate LTL combinations of subformulas", 0 },
+    { "formulas", 'n', "INT", 0,
+      "number of formulas to generate (default: 1);\n"
+      "use a negative value for unbounded generation", 0 },
+    { "seed", OPT_SEED, "INT", 0,
+      "seed for the random number generator (default: 0)", 0 },
+    { "tree-size", OPT_TREE_SIZE, "RANGE", 0,
+      "tree size of main pattern generated (default: 5);\n"
+      "input formulas count as size 1.", 0 },
+    /**************************************************/
+    { nullptr, 0, nullptr, 0, "Adjusting probabilities:", 4 },
+    { "dump-priorities", OPT_DUMP_PRIORITIES, nullptr, 0,
+      "show current priorities, do not generate any formula", 0 },
+    { "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0,
+      "set priorities for LTL formulas", 0 },
+    { "boolean-priorities", OPT_BOOLEAN_PRIORITIES, "STRING", 0,
+      "set priorities for Boolean formulas", 0 },
+    { nullptr, 0, nullptr, 0, "STRING should be a comma-separated list of "
+      "assignments, assigning integer priorities to the tokens "
+      "listed by --dump-priorities.", 0 },
+    /**************************************************/
+    { nullptr, 0, nullptr, 0, "Output options:", -20 },
+    { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
+      "the following interpreted sequences:", -19 },
+    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the formula (in the selected syntax)", 0 },
+    { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the (serial) number of the formula (0-based)", 0 },
+    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the (serial) number of the formula (1-based)", 0 },
+    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "a single %", 0 },
+    COMMON_LTL_OUTPUT_SPECS,
+    /**************************************************/
+    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
+    { nullptr, 0, nullptr, 0, nullptr, 0 }
+};
+
+static const argp_child children[] = {
+  { &finput_argp, 0, nullptr, 0 },
+  { &output_argp, 0, nullptr, 0 },
+  { &misc_argp, 0, nullptr, 0 },
+  { nullptr, 0, nullptr, 0 }
+};
+
+static int opt_formulas = 1;
+static spot::randltlgenerator::output_type output =
+  spot::randltlgenerator::Bool;
+static char* opt_pL = nullptr;
+static char* opt_pB = nullptr;
+static bool opt_dump_priorities = false;
+static int opt_seed = 0;
+static range opt_tree_size = { 5, 5 };
+static bool opt_unique = true;
+static int opt_ap_count = 0;
+static bool opt_literal = false;
+
+namespace
+{
+  // We want all these variables to be destroyed when we exit main, to
+  // make sure it happens before all other global variables (like the
+  // atomic propositions maps) are destroyed.  Otherwise we risk
+  // accessing deleted stuff.
+  static struct opt_t
+  {
+    spot::atomic_prop_set sub;
+  }* opt = nullptr;
+
+  class sub_processor final: public job_processor
+  {
+  public:
+    int
+    process_formula(spot::formula f, const char* filename = nullptr,
+                    int linenum = 0) override
+    {
+      (void) filename;
+      (void) linenum;
+      opt->sub.insert(f);
+      return 0;
+    }
+  };
+}
+
+static sub_processor subreader;
+
+static int
+parse_opt(int key, char* arg, struct argp_state*)
+{
+  // Called from C code, so should not raise any exception.
+  BEGIN_EXCEPTION_PROTECT;
+  switch (key)
+    {
+    case 'A':
+      opt_ap_count = to_int(arg, "-A/--ap-count");
+      opt_literal = false;
+      break;
+    case 'B':
+      output = spot::randltlgenerator::Bool;
+      break;
+    case 'L':
+      output = spot::randltlgenerator::LTL;
+      break;
+    case 'n':
+      opt_formulas = to_int(arg, "-n/--formulas");
+      break;
+    case 'P':
+      opt_ap_count = to_int(arg, "-P/--polarized-ap");
+      opt_literal = true;
+      break;
+    case OPT_BOOLEAN_PRIORITIES:
+      opt_pB = arg;
+      break;
+    case OPT_LTL_PRIORITIES:
+      opt_pL = arg;
+      break;
+    case OPT_DUMP_PRIORITIES:
+      opt_dump_priorities = true;
+      break;
+    case OPT_DUPS:
+      opt_unique = false;
+      break;
+    case OPT_SEED:
+      opt_seed = to_int(arg, "--seed");
+      break;
+    case OPT_TREE_SIZE:
+      opt_tree_size = parse_range(arg);
+      if (opt_tree_size.min > opt_tree_size.max)
+        std::swap(opt_tree_size.min, opt_tree_size.max);
+      break;
+    case ARGP_KEY_ARG:
+      jobs.emplace_back(arg, job_type::LTL_FILENAME);
+      break;
+    default:
+      return ARGP_ERR_UNKNOWN;
+    }
+  END_EXCEPTION_PROTECT;
+  return 0;
+}
+
+int
+main(int argc, char* argv[])
+{
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
+                        argp_program_doc, children, nullptr, nullptr };
+
+      // This will ensure that all objects stored in this struct are
+      // destroyed before global variables.
+      opt_t o;
+      opt = &o;
+
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
+
+      check_no_formula("combine");
+
+      if (subreader.run())
+        return 2;
+
+      if (opt->sub.empty())
+        error(2, 0, "the set of subformulas to build from is empty");
+
+      spot::srand(opt_seed);
+
+      spot::randltlgenerator rg
+        (opt_ap_count,
+         [&] (){
+          spot::option_map opts;
+          opts.set("output", output);
+          opts.set("tree_size_min", opt_tree_size.min);
+          opts.set("tree_size_max", opt_tree_size.max);
+          opts.set("seed", opt_seed);
+          opts.set("simplification_level", 0);
+          opts.set("unique", opt_unique);
+          opts.set("literals", opt_literal);
+          return opts;
+         }(), opt_pL, nullptr, opt_pB, &opt->sub);
+
+      if (opt_dump_priorities)
+        {
+          switch (output)
+            {
+            case spot::randltlgenerator::LTL:
+              std::cout <<
+                "Use --ltl-priorities to set the following LTL priorities:\n";
+              rg.dump_ltl_priorities(std::cout);
+              break;
+            case spot::randltlgenerator::Bool:
+              std::cout <<
+                "Use --boolean-priorities to set the following Boolean "
+                "formula priorities:\n";
+              rg.dump_bool_priorities(std::cout);
+              break;
+            case spot::randltlgenerator::PSL:
+            case spot::randltlgenerator::SERE:
+              error(2, 0, "PSL/SERE output is unsupported");
+              break;
+            }
+          exit(0);
+        }
+
+      int count = 0;
+      while (opt_formulas < 0 || opt_formulas--)
+        {
+          spot::formula f = rg.next();
+          if (!f)
+            {
+              error(2, 0, "failed to generate a new unique formula after %d " \
+                    "trials", spot::randltlgenerator::MAX_TRIALS);
+            }
+          else
+            {
+              output_formula_checked(f, nullptr, nullptr, count + 1, count);
+              ++count;
+            }
+        };
+
+      flush_cout();
+      return 0;
+    });
+}
diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am
index 1b6319766..2ccf4b8b1 100644
--- a/bin/man/Makefile.am
+++ b/bin/man/Makefile.am
@@ -35,6 +35,7 @@ dist_man1_MANS = \
   ltldo.1 \
   ltlfilt.1 \
   ltlgrind.1 \
+  ltlmix.1 \
   ltlsynt.1 \
   randaut.1 \
   randltl.1
@@ -72,6 +73,9 @@ ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
 ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc
 	$(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@
 
+ltlmix.1: $(common_dep) $(srcdir)/ltlmix.x $(srcdir)/../ltlmix.cc
+	$(convman) ../ltlmix$(EXEEXT) $(srcdir)/ltlmix.x $@
+
 ltlsynt.1: $(common_dep) $(srcdir)/ltlsynt.x $(srcdir)/../ltlsynt.cc
 	$(convman) ../ltlsynt$(EXEEXT) $(srcdir)/ltlsynt.x $@
 
diff --git a/bin/man/genltl.x b/bin/man/genltl.x
index 6194ba8ab..db40c653b 100644
--- a/bin/man/genltl.x
+++ b/bin/man/genltl.x
@@ -80,3 +80,4 @@ Proceedings of RV'10.  LNCS 6418.
 .BR ltlfilt (1),
 .BR randaut (1),
 .BR randltl (1)
+.BR ltlmix (1)
diff --git a/bin/man/ltlmix.x b/bin/man/ltlmix.x
new file mode 100644
index 000000000..dbdc2f9f5
--- /dev/null
+++ b/bin/man/ltlmix.x
@@ -0,0 +1,7 @@
+[NAME]
+ltlmix \- combine formulas selected randomly
+[DESCRIPTION]
+.\" Add any additional description here
+[SEE ALSO]
+.BR randltl (1),
+.BR genltl (1)
diff --git a/bin/man/randltl.x b/bin/man/randltl.x
index cce4714fb..c9ab79c80 100644
--- a/bin/man/randltl.x
+++ b/bin/man/randltl.x
@@ -14,3 +14,4 @@ Proceedings of ATVA'13.  LNCS 8172.
 .BR genltl (1),
 .BR ltlfilt (1),
 .BR randaut (1)
+.BR ltlmix (1)
diff --git a/bin/man/spot.x b/bin/man/spot.x
index 037069d39..428839987 100644
--- a/bin/man/spot.x
+++ b/bin/man/spot.x
@@ -22,6 +22,7 @@ that are listed below.
 .BR ltldo (1)
 .BR ltlfilt (1)
 .BR ltlgrind (1)
+.BR ltlmix (1)
 .BR ltlsynt (1)
 .BR randaut (1)
 .BR randltl (1)
diff --git a/bin/spot.cc b/bin/spot.cc
index 75401ddbc..e8be7f42a 100644
--- a/bin/spot.cc
+++ b/bin/spot.cc
@@ -37,6 +37,8 @@ static const argp_option options[] =
     { DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but "
           "simpler ones.  Use this when looking for shorter formula to "
           "reproduce a bug.") },
+    { DOC("ltlmix",
+          "Combine LTL/PSL formulas taken randomly from some input set.") },
     { nullptr, 0, nullptr, 0, "Tools that output automata or circuits:", 0 },
     { DOC("randaut", "Generate random ω-automata.") },
     { DOC("genaut", "Generate ω-automata from scalable patterns.") },
diff --git a/doc/Makefile.am b/doc/Makefile.am
index 7abe05f9e..5b8e7edac 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -104,6 +104,7 @@ ORG_FILES = \
   org/ltldo.org \
   org/ltlfilt.org \
   org/ltlgrind.org \
+  org/ltlmix.org \
   org/ltlsynt.org \
   org/ltlsynt.tex \
   org/oaut.org \
diff --git a/doc/org/arch.tex b/doc/org/arch.tex
index 0e9e97e4a..f94df93e1 100644
--- a/doc/org/arch.tex
+++ b/doc/org/arch.tex
@@ -22,18 +22,19 @@
            usedby/.style={->,ultra thick,>={Stealth[length=5mm,round]},gray!50!black}}
   \node[cppbox=14.12cm] (libspot) {\texttt{libspot\strut}};
   \node[shbox=3cm,above right=2mm and 0mm of libspot.north west,align=center] (shcmd) {
-    \href{https://spot.lrde.epita.fr/randltl.html}{\texttt{randltl}}\\
-    \href{https://spot.lrde.epita.fr/ltlfilt.html}{\texttt{ltlfilt}}\\
-    \href{https://spot.lrde.epita.fr/randaut.html}{\texttt{randaut}}\\
-    \href{https://spot.lrde.epita.fr/autfilt.html}{\texttt{autfilt}}\\
-    \href{https://spot.lrde.epita.fr/ltl2tgba.html}{\texttt{ltl2tgba}}\\
-    \href{https://spot.lrde.epita.fr/ltl2tgta.html}{\texttt{ltl2tgta}}\\
-    \href{https://spot.lrde.epita.fr/dstar2tgba.html}{\texttt{dstar2tgba}}\\
-    \href{https://spot.lrde.epita.fr/ltlcross.html}{\texttt{ltlcross}}\\
-    \href{https://spot.lrde.epita.fr/ltlgrind.html}{\texttt{ltlgrind}}\\
-    \href{https://spot.lrde.epita.fr/ltlsynt.html}{\texttt{ltlsynt}}\\
-    \href{https://spot.lrde.epita.fr/ltldo.html}{\texttt{ltldo}}\\
-    \href{https://spot.lrde.epita.fr/autcross.html}{\texttt{autcross}}
+    \href{https://spot.lre.epita.fr/randltl.html}{\texttt{randltl}}\\
+    \href{https://spot.lre.epita.fr/ltlmix.html}{\texttt{ltlmix}}\\
+    \href{https://spot.lre.epita.fr/ltlfilt.html}{\texttt{ltlfilt}}\\
+    \href{https://spot.lre.epita.fr/randaut.html}{\texttt{randaut}}\\
+    \href{https://spot.lre.epita.fr/autfilt.html}{\texttt{autfilt}}\\
+    \href{https://spot.lre.epita.fr/ltl2tgba.html}{\texttt{ltl2tgba}}\\
+    \href{https://spot.lre.epita.fr/ltl2tgta.html}{\texttt{ltl2tgta}}\\
+    \href{https://spot.lre.epita.fr/dstar2tgba.html}{\texttt{dstar2tgba}}\\
+    \href{https://spot.lre.epita.fr/ltlcross.html}{\texttt{ltlcross}}\\
+    \href{https://spot.lre.epita.fr/ltlgrind.html}{\texttt{ltlgrind}}\\
+    \href{https://spot.lre.epita.fr/ltlsynt.html}{\texttt{ltlsynt}}\\
+    \href{https://spot.lre.epita.fr/ltldo.html}{\texttt{ltldo}}\\
+    \href{https://spot.lre.epita.fr/autcross.html}{\texttt{autcross}}
   };
   \node[cppbox=4.7cm,above right=0mm and 2mm of shcmd.south east] (libgen) {\texttt{libspotgen\strut}};
   \node[cppbox=2.5cm,above right=0mm and 2mm of libgen.south east] (buddy) {\texttt{libbddx\strut}};
@@ -41,8 +42,8 @@
   \node[cppbox=4cm,above right=0mm and 2mm of pyspot.south east] (libltsmin) {\texttt{libspotltsmin\strut}};
 
   \node[shbox=1.5cm,above right=2mm and 0mm of libgen.north west,align=center] (genaut) {
-    \href{https://www.lrde.epita.fr/genaut.html}{\texttt{genaut\strut}}\\
-    \href{https://www.lrde.epita.fr/genltl.html}{\texttt{genltl}}
+    \href{https://www.lre.epita.fr/genaut.html}{\texttt{genaut\strut}}\\
+    \href{https://www.lre.epita.fr/genltl.html}{\texttt{genltl}}
   };
 
   \node[pybox=3cm,above left=2mm and 0mm of libgen.north east] (pygen) {\texttt{import spot.gen\strut}};
diff --git a/doc/org/concepts.org b/doc/org/concepts.org
index c4de7a324..d7ce0a57e 100644
--- a/doc/org/concepts.org
+++ b/doc/org/concepts.org
@@ -158,7 +158,7 @@ $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-buchi.svg]]
+[[file:concept-buchi2.svg]]
 
 The =1= displayed on the edge that loops on state =1= should be
 read as /true/, i.e., the Boolean formula that accepts
diff --git a/doc/org/ltlmix.org b/doc/org/ltlmix.org
new file mode 100644
index 000000000..338122d41
--- /dev/null
+++ b/doc/org/ltlmix.org
@@ -0,0 +1,365 @@
+# -*- coding: utf-8 -*-
+#+TITLE: =ltlgrind=
+#+DESCRIPTION: Spot command-line tool for combining LTL formulas randomly
+#+INCLUDE: setup.org
+#+HTML_LINK_UP: tools.html
+#+PROPERTY: header-args:sh :results verbatim :exports both
+
+This tool creates new formulas by combining formulas randomly selected
+from an input set of formulas.  Some authors have argued that for some
+tasks, like [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][LTL satisfiability]], working with randomly generated
+formulas is often easy, because random formulas tend to simplify
+trivially.  =ltlmix= allows you to take a set of formulas, usually
+some handwritten, meaningful formulas, and combine those formulas to
+build larger sets that are possibly more challenging.
+
+Here is a very simple example that builds five formulas that are
+Boolean combination of formulas from taken in the set
+$\{\mathsf{GF}a,\mathsf{FG}b,\mathsf{X}c\}$:
+
+#+BEGIN_SRC sh :exports both
+ltlmix -f GFa -f FGb -f Xc -n 5
+#+END_SRC
+
+#+RESULTS:
+: !FGb xor !Xc
+: !GFa -> !FGb
+: FGb | (FGb -> Xc)
+: FGb
+: GFa & (FGb | Xc)
+
+* Shape of the generated formulas
+
+** Size of the syntax tree
+
+For each formula that it generates, =ltlmix= constructs a random
+syntax-tree of a certain size (5 by default) in which internal nodes
+represent operators selected randomly from a list of operator, and
+leaves are subformulas selected randomly from the set of input
+formulas.  As an example, the syntax tree of =!φ₁ xor !φ₂= has size 5,
+and its leaves =φ₁= and =φ₂= will be taken randomly from the set of
+input formulas.
+
+The algorithm is actually the same as for =randltl=, except
+that =randltl= use random atomic propositions as leaves when =ltlmix=
+uses random formulas.
+
+The same input formula can be picked several times to be used on
+multiple leaves of the tree.  Note that because Spot implements some
+trivial rewritings directly during the construction of any formula,
+formulas like =FGb | !!FGb= (which correspond to a tree of size 5 in
+the above example) cannot be represented: they are automatically
+simplified to =FGb=.  Similarly, something like =φ xor φ= will be
+output as =0=.
+
+The size of the tree can be changed using the =--tree-size= option.
+
+#+BEGIN_SRC sh :exports both
+  for i in 1 2 3 4 5 6 7 8 9 10 11 12; do
+      ltlmix -fXa -fGb -fFc -fXd -fGe --tree-size=$i
+  done
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Fc
+!Xd
+0
+Ge xor !Fc
+!Xd xor !Ge
+!Xd xor (Fc | Xd)
+!Ge
+Ge xor (!Ge -> Gb)
+Ge xor (!Xa -> !Fc)
+(Ge & !Fc) xor (!Gb xor !Ge)
+(Ge & !Fc) xor (!Gb xor (Gb | Fc))
+(Ge & (Gb xor Xd)) xor (!Fc -> (Gb | Fc))
+#+end_example
+
+The above shows that while the size of the syntax tree generally grows
+along with =--tree-size= there are several cases where it reduces
+trivially.
+
+** Operator priorities
+
+It is possible to control the set of operators used in the generation.
+The first step is to obtain that list of operators with =--dump-priorities=.
+For instance:
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fXa -fGb -fFc -fXd -fGe --dump-priorities
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Use --boolean-priorities to set the following Boolean formula priorities:
+sub	5
+false	0
+true	0
+not	1
+equiv	1
+implies	1
+xor	1
+and	1
+or	1
+#+end_example
+
+In the above list, =false= and =true= represent the Boolean constants
+(which are usually undesirable when building random Boolean formulas),
+and =sub= represent a random formula drawn from the list of input
+formulas.
+
+The above command shows that each operator has a weight, called
+/priority/.  When the priority is 0, the operator is never used.  When
+=ltlmix= generates a syntax tree of size N, it looks among all
+operators that can be used at the root of such a tree, and performs a
+weighted random selection.  In other words, an operator with priority
+=2= will be twice more likely to be selected than an operator with
+priority =1=.
+
+Those priorities can be changed with =--boolean-priorities= as in the
+following example, which disables =xor= and makes =<->= thrice more
+likely to appear.
+
+#+BEGIN_SRC sh :exports both
+  for i in 1 2 3 4 5 6 7 8 9 10 11 12; do
+      ltlmix -fXa -fGb -fFc -fXd -fGe --tree-size=$i --boolean-prio='xor=0,equiv=3'
+  done
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Fc
+!Xd
+1
+Ge <-> !Fc
+!Xd <-> !Ge
+!Xd <-> (Fc | Xd)
+Ge
+Ge <-> (Gb <-> !Ge)
+Ge <-> (!Fc <-> !Xa)
+(Ge & !Fc) <-> (!Ge -> !Gb)
+(Ge & !Fc) <-> ((Gb | Fc) -> !Gb)
+(Ge & (Gb <-> Xd)) <-> ((Gb | Fc) <-> !Fc)
+#+end_example
+
+** Boolean or LTL syntax tree
+
+By default, the syntax tree generated on top of the randomly selected
+input formula uses only Boolean operators.
+
+Using option =-L= will use LTL operators instead.
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fXa -fGb -fFc --tree-size=10 -L -n10
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Gb R (XFc W 0)
+!(Gb | !Xa)
+1 U !X(0)
+(Xa xor Gb) -> (GXa M Fc)
+GFc M 1
+(Fc U Gb) -> (0 R Xa)
+!Gb <-> (Gb | GFc)
+1
+GFc | (1 U Xa)
+!(Xa | GFc)
+#+end_example
+
+The following operators are used:
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fXa -fGb -fFc -fXd -fGe -L --dump-priorities
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Use --ltl-priorities to set the following LTL priorities:
+sub	5
+false	1
+true	1
+not	1
+F	1
+G	1
+X	1
+equiv	1
+implies	1
+xor	1
+R	1
+U	1
+W	1
+M	1
+and	1
+or	1
+#+end_example
+
+Note that in the LTL case, =false= and =true= can be generated by default.
+
+* Randomizing atomic propositions with =-A= or =-P=
+
+Options =-A= or =-P= can be used to change the atomic propositions
+used in the input formulas.  This works as follows: if =-A N= was
+given, every time an input formula φ is selected, its atomic
+propositions are replaced by atomic propositions randomly selected in
+a set of size $N$.  If φ uses $i$ atomic propositions and $i\ge N$,
+then those $i$ atomic proposition will be remapped to $i$ distinct
+atomic propositions chosen randomly in that set.  if $i>N$, some of
+the new atomic propositions may replace several of the original atomic
+propositions.
+
+Option =-P N= is similar to =-A N= except that the selected atomic
+propositions can possibly be negated.
+
+
+These options solve two problems:
+
+- They lessen the issue that a formula selected several times can lead
+  to syntax tree such as =φ | φ | φ= that reduces to =φ=.  Now, each
+  occurrence of =φ= as a chance to use different atomic propositions.
+  (the larger =N= is, the more likely it is that these copies of φ
+  will be different).
+
+- They allow combining formulas that had completely different sets of
+  atomic propositions, in such a way that they are now interdependent
+  (the smaller N is the more likely it is that subformulas will share
+  atomic propositions).
+
+
+Here is an example with a single formula, =GFa=, whose atomic proposition
+will be randomly replaced by one of $\{p_0,p_1,p_2,p_3,p_4\}$.
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fGFa -A5 --tree-size=8 -n10
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+(GFp2 & GFp3) xor (!GFp0 xor GFp1)
+(GFp4 -> GFp1) -> !GFp2
+!GFp4 | ((GFp2 & GFp3) -> GFp2)
+!GFp2 | (GFp3 <-> (GFp2 & GFp1))
+!GFp0 | GFp4
+!(GFp2 & GFp1) <-> (GFp3 xor GFp0)
+(GFp2 xor GFp0) | (GFp4 -> !GFp0)
+(GFp4 | !GFp3) -> GFp4
+!GFp0 -> (GFp2 | GFp1)
+!GFp1 <-> (!GFp2 xor !GFp1)
+#+end_example
+
+Here is a similar example, with polarized atomic propositions instead:
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fGFa -P5 --tree-size=8 -n10
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+(GFp2 & GF!p3) xor (GFp4 -> !GF!p1)
+(GFp4 | !GFp2) -> (GFp1 -> GF!p1)
+!GF!p2 & (GF!p0 xor (GF!p0 -> GF!p3))
+GFp1 <-> (GF!p3 | !GFp0)
+GF!p1 & GFp0 & (GF!p3 xor !GF!p4)
+(GF!p1 xor GF!p2) | (GF!p3 & !GF!p4)
+!(GFp4 xor (!GF!p2 | !GF!p3))
+GFp0 | (!GFp1 -> (GFp1 -> GF!p4))
+GF!p1 xor (!GF!p2 | (GF!p1 <-> GFp0))
+!((GF!p2 <-> GF!p4) & (GFp1 xor GF!p2))
+#+end_example
+
+
+* More serious examples
+
+** Mixing the DAC patterns
+
+The command [[file:genltl.org][=genltl --dac-pattern=]] will print a list of 55 LTL
+formulas representing various specification patterns listed by Dwyer
+et al. (FMSP'98).  Using =--stat=%x= to count the atomic propositions
+in each formula, and some standard unix tools, we can compute that
+they use at most 6 atomic propositions.
+
+#+BEGIN_SRC sh :exports both
+  genltl --dac-pattern --stat=%x | sort -n | tail -n 1
+#+END_SRC
+#+RESULTS:
+: 6
+
+Based on this, we could decide to generate Boolean combination of
+those formulas while replacing atomic propositions by literals built
+out of a set of 10 atomic propositions (chosen larger than 6 to ensure
+that each individual formula will still make sense after the change of
+atomic propositions).
+
+#+BEGIN_SRC sh :exports both
+  genltl --dac-pattern | ltlmix -n8 -P10
+#+END_SRC
+
+#+RESULTS:
+: !G((p8 & F!p7) -> (!p4 U (!p7 | (!p2 & !p4 & X(!p4 U p1))))) xor !G(!p3 -> ((p4 & !p7) U (!p4 | ((p4 & p7) U (!p4 | ((p4 & !p7) U (!p4 | ((p4 & p7) U (!p4 | (!p7 W !p4) | Gp7)))))))))
+: !G(!p3 -> Gp5) xor !G(!p7 -> G(p9 -> (!p5 & !p8 & X(!p5 U p2))))
+: G(p6 -> ((!(!p1 & p7 & X(!p1 U (!p1 & !p3))) U (p1 | !p2)) | G!(p7 & XF!p3))) & (G((!p4 & XF!p5) -> XF(!p5 & F!p0)) <-> G((p5 & !p6) -> (p5 W (p5 & p7))))
+: !G((p0 & p9) -> (!p7 W (!p0 | p4))) & !G((p1 & !p2) -> (!p8 W p2))
+: ((Fp2 -> ((!p1 -> (!p2 U (p0 & !p2))) U p2)) -> G(p1 -> G(p9 -> (!p4 & p8 & X(!p4 U !p7))))) xor G(p1 -> Gp9)
+: !G((p5 & !p9 & F!p5) -> ((!p8 -> (p5 U (!p0 & p5))) U !p5)) -> !G((p6 & p9) -> (!p7 W !p9))
+: G((!p1 & !p2) -> (p9 W p1)) <-> (G(p5 -> G(p0 -> F!p4)) -> (Fp6 -> ((!p5 & !p6) U (p6 | ((p5 & !p6) U (p6 | ((!p5 & !p6) U (p6 | ((p5 & !p6) U (p6 | (!p5 U p6)))))))))))
+: ((Fp1 -> ((p6 -> (!p1 U (!p1 & !p2 & X(!p1 U !p9)))) U p1)) <-> (F!p0 -> (p0 U (p0 & !p7 & X(p0 U !p9))))) | (Fp2 -> (p6 U (p2 | (p6 & !p7 & X(p6 U p1)))))
+
+Now we might want to clean this list a bit by relabeling each formula
+so is uses atomic propositions $\{p_0,p_1,...\}$ starting at 0 and without gap.
+
+#+BEGIN_SRC sh :exports both
+  genltl --dac-pattern | ltlmix -n8 -P10 | ltlfilt --relabel=pnn
+#+END_SRC
+
+#+RESULTS:
+: !G((p0 & F!p1) -> (!p2 U (!p1 | (!p2 & !p3 & X(!p2 U p4))))) xor !G(!p5 -> ((!p1 & p2) U (!p2 | ((p1 & p2) U (!p2 | ((!p1 & p2) U (!p2 | ((p1 & p2) U (!p2 | (!p1 W !p2) | Gp1)))))))))
+: !G(!p0 -> Gp1) xor !G(!p2 -> G(p3 -> (!p1 & !p4 & X(!p1 U p5))))
+: G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & !p3))) U (p1 | !p4)) | G!(p2 & XF!p3))) & (G((!p5 & XF!p6) -> XF(!p6 & F!p7)) <-> G((!p0 & p6) -> (p6 W (p2 & p6))))
+: !G((p0 & p1) -> (!p2 W (!p0 | p3))) & !G((p4 & !p5) -> (!p6 W p5))
+: ((Fp0 -> ((!p1 -> (!p0 U (!p0 & p2))) U p0)) -> G(p1 -> G(p3 -> (!p4 & p5 & X(!p4 U !p6))))) xor G(p1 -> Gp3)
+: !G((p0 & !p1 & F!p0) -> ((!p2 -> (p0 U (p0 & !p3))) U !p0)) -> !G((p1 & p4) -> (!p5 W !p1))
+: G((!p0 & !p1) -> (p2 W p0)) <-> (G(p3 -> G(p4 -> F!p5)) -> (Fp6 -> ((!p3 & !p6) U (p6 | ((p3 & !p6) U (p6 | ((!p3 & !p6) U (p6 | ((p3 & !p6) U (p6 | (!p3 U p6)))))))))))
+: ((Fp0 -> ((p1 -> (!p0 U (!p0 & !p2 & X(!p0 U !p3)))) U p0)) <-> (F!p4 -> (p4 U (p4 & !p5 & X(p4 U !p3))))) | (Fp2 -> (p1 U (p2 | (p1 & !p5 & X(p1 U p0)))))
+
+** Random conjunctions
+
+Some benchmark (e.g., [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][for LTL satisfiability]]) are built by conjunction
+of $L$ random formulas picked from a set of basic formulas.  Each
+picked formula has its atomic proposition mapped to random literals
+built from a subset of $m$ atomic variables.
+
+Given a value for $m$, option =-P m= will achieve the second part of
+the above description.  To build a conjunction of $L$ formulas, we
+need to ask for a tree of size $2L-1$ in which only the =and= operator
+is allowed.
+
+Here is an example with $L=10$ (hence =--tree-size=19=) and $m=50$.
+The example use a small set of three basic formulas
+$\{\mathsf{G}a,\mathsf{F}a,\mathsf{X}a\}$ for illustration, but in
+practice you should replace these =-f= options by =-F FILENAME=
+pointing to a file containing all the input formulas to select from.
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fGa -fFa -fXa -n10 -P50 \
+         --tree-size=19 --boolean-prio=not=0,or=0,xor=0,equiv=0,implies=0
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Xp27 & F!p21 & G!p19 & X!p26 & Fp4 & Gp43 & Fp39 & Fp7
+G!p28 & G!p30 & X!p34 & Fp21 & Gp3 & Fp6 & F!p18 & Xp5 & Fp8 & F!p12
+X!p32 & Xp9 & Gp4 & Xp48 & F!p48 & X!p6 & Fp5 & Xp20 & Fp28 & Fp26
+G!p46 & X!p14 & Fp29 & X!p36 & Fp12 & Xp47 & Fp42 & Gp14 & Fp19
+G!p28 & Fp21 & Fp36 & F!p0 & G!p14 & Xp21 & F!p28 & G!p21 & Gp21 & Gp40
+Gp3 & F!p48 & F!p28 & Xp7 & Gp8 & Xp42 & Gp0 & Xp36 & F!p2 & G!p0
+Xp36 & Xp46 & F!p31 & Xp11 & Xp26 & G!p9 & F!p36 & X!p12 & Fp15 & Xp18
+Xp9 & X!p33 & Fp44 & X!p13 & Gp37 & Xp19 & G!p43 & F!p34 & Gp36 & Gp10
+Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
+Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31
+#+end_example
+
+Selecting 10 random conjuncts out of 3×50×2=300 possibilities has a
+13.7% chance that at least 2 conjuncts will be identical (see [[https://en.wikipedia.org/wiki/Birthday_problem][Birthday
+paradox]]), so because of Spot's trivial rewritings, some hove the above
+formulas may have fewer than 10 conjuncts.
diff --git a/doc/org/tools.org b/doc/org/tools.org
index 46ca38ccd..e24258a19 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -41,6 +41,7 @@ corresponding commands are hidden.
 * Command-line tools
 
 - [[file:randltl.org][=randltl=]] Generate random LTL/PSL formulas.
+- [[file:ltlmix.org][=ltlmix=]] Combine LTL/PSL formulas taken randomly from some input set.
 - [[file:ltlfilt.org][=ltlfilt=]] Filter, convert, and transform LTL/PSL formulas.
 - [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns.
 - [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into various types of automata.
@@ -77,6 +78,7 @@ convenience, you can browse their HTML versions:
 [[./man/ltldo.1.html][=ltldo=]](1),
 [[./man/ltlfilt.1.html][=ltlfilt=]](1),
 [[./man/ltlgrind.1.html][=ltlgrind=]](1),
+[[./man/ltlmix.1.html][=ltlmix=]](1),
 [[./man/ltlsynt.1.html][=ltlsynt=]](1),
 [[./man/randaut.1.html][=randaut=]](1),
 [[./man/randltl.1.html][=randltl=]](1),
diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc
index e415535b2..913b60522 100644
--- a/spot/tl/randomltl.cc
+++ b/spot/tl/randomltl.cc
@@ -28,6 +28,45 @@ namespace spot
 {
   namespace
   {
+    // Rename atomic propositions in f using atomic propositions drawn
+    // randomly from \a ap.  Avoid repetition if \a ap is large
+    // enough.  If \a lit is true, change the polarity of the atomic
+    // proposition randomly.
+    static formula
+    randomize_ap(formula f, const atomic_prop_set* ap, bool lit)
+    {
+      std::vector<formula> randap(ap->begin(), ap->end());
+      unsigned current_range = randap.size();
+      std::map<formula, formula> mapping;
+
+      auto relabel = [&](formula f, auto self) -> formula
+      {
+        if (f.is(op::ap))
+          {
+            // Did we already rename this AP?
+            if (auto it = mapping.find(f); it != mapping.end())
+              return it->second;
+
+            // If we exhausted all possible AP, start again
+            if (current_range == 0)
+              current_range = randap.size();
+
+            //
+            unsigned pos = mrand(current_range--);
+            formula ap = randap[pos];
+            std::swap(randap[current_range], randap[pos]);
+
+            if (lit && drand() < 0.5)
+              ap = formula::Not(ap);
+
+            return mapping[f] = ap;
+          }
+        return f.map(self, self);
+      };
+      return relabel(f, relabel);
+    }
+
+
     static formula
     ap_builder(const random_formula* rl, int n)
     {
@@ -38,6 +77,20 @@ namespace spot
       return *i;
     }
 
+    static formula
+    pattern_builder(const random_formula* rl, int n)
+    {
+      assert(n == 1);
+      (void) n;
+      atomic_prop_set::const_iterator i = rl->patterns()->begin();
+      std::advance(i, mrand(rl->patterns()->size()));
+      formula f = *i;
+      const atomic_prop_set* ap = rl->ap();
+      if (ap && ap->size() > 0)
+        f = randomize_ap(f, ap, rl->draw_literals());
+      return f;
+    }
+
     static formula
     true_builder(const random_formula*, int n)
     {
@@ -353,13 +406,28 @@ namespace spot
   }
 
   // Boolean formulae
-  random_boolean::random_boolean(const atomic_prop_set* ap)
+  random_boolean::random_boolean(const atomic_prop_set* ap,
+                                 const atomic_prop_set* patterns)
     : random_formula(9, ap)
   {
-    proba_[0].setup("ap",      1, ap_builder);
-    proba_[0].proba = ap_->size();
+    if (patterns)
+      {
+        proba_[0].setup("sub", 1, pattern_builder);
+        patterns_ = patterns;
+        proba_[0].proba = patterns_->size();
+      }
+    else
+      {
+        proba_[0].setup("ap",  1, ap_builder);
+        proba_[0].proba = ap_->size();
+      }
     proba_[1].setup("false",   1, false_builder);
     proba_[2].setup("true",    1, true_builder);
+    if (patterns)
+      {
+        proba_[1].proba = 0.0;
+        proba_[2].proba = 0.0;
+      }
     proba_2_or_more_ = proba_2_ = proba_ + 3;
     proba_[3].setup("not",     2, unop_builder<op::Not>);
     proba_[4].setup("equiv",   3, binop_builder<op::Equiv>);
@@ -373,10 +441,19 @@ namespace spot
 
   // LTL formulae
   void
-  random_ltl::setup_proba_()
+  random_ltl::setup_proba_(const atomic_prop_set* patterns)
   {
-    proba_[0].setup("ap",      1, ap_builder);
-    proba_[0].proba = ap_->size();
+    if (patterns)
+      {
+        proba_[0].setup("sub", 1, pattern_builder);
+        patterns_ = patterns;
+        proba_[0].proba = patterns_->size();
+      }
+    else
+      {
+        proba_[0].setup("ap",  1, ap_builder);
+        proba_[0].proba = ap_->size();
+      }
     proba_[1].setup("false",   1, false_builder);
     proba_[2].setup("true",    1, true_builder);
     proba_2_or_more_ = proba_2_ = proba_ + 3;
@@ -395,17 +472,18 @@ namespace spot
     proba_[15].setup("or",     3, multop_builder<op::Or>);
   }
 
-  random_ltl::random_ltl(const atomic_prop_set* ap)
+  random_ltl::random_ltl(const atomic_prop_set* ap,
+                         const atomic_prop_set* patterns)
     : random_formula(16, ap)
   {
-    setup_proba_();
+    setup_proba_(patterns);
     update_sums();
   }
 
   random_ltl::random_ltl(int size, const atomic_prop_set* ap)
     : random_formula(size, ap)
   {
-    setup_proba_();
+    setup_proba_(nullptr);
     // No call to update_sums(), this functions is always
     // called by the random_psl constructor.
   }
@@ -428,7 +506,8 @@ namespace spot
                                      const option_map& opts,
                                      char* opt_pL,
                                      char* opt_pS,
-                                     char* opt_pB)
+                                     char* opt_pB,
+                                     const atomic_prop_set* subs)
     : opt_simpl_level_(opts.get("simplification_level", 3)),
       simpl_(tl_simplifier_options{opt_simpl_level_})
   {
@@ -439,6 +518,7 @@ namespace spot
     opt_tree_size_max_ = opts.get("tree_size_max", 15);
     opt_unique_ = opts.get("unique", 1);
     opt_wf_ = opts.get("wf", 0);
+    bool lit = opts.get("literals", 0);
 
     const char* tok_pL = nullptr;
     const char* tok_pS = nullptr;
@@ -447,23 +527,25 @@ namespace spot
     switch (output_)
       {
       case randltlgenerator::LTL:
-        rf_ = new random_ltl(&aprops_);
+        rf_ = new random_ltl(&aprops_, subs);
+        rf_->draw_literals(lit);
         if (opt_pS)
-          throw std::invalid_argument("Cannot set sere priorities with "
+          throw std::invalid_argument("Cannot set SERE priorities with "
                                       "LTL output");
         if (opt_pB)
-          throw std::invalid_argument("Cannot set boolean priorities with "
+          throw std::invalid_argument("Cannot set Boolean priorities with "
                                       "LTL output");
         tok_pL = rf_->parse_options(opt_pL);
         break;
       case randltlgenerator::Bool:
-        rf_ = new random_boolean(&aprops_);
+        rf_ = new random_boolean(&aprops_, subs);
+        rf_->draw_literals(lit);
         tok_pB = rf_->parse_options(opt_pB);
         if (opt_pL)
-          throw std::invalid_argument("Cannot set ltl priorities with "
+          throw std::invalid_argument("Cannot set LTL priorities with "
                                       "Boolean output");
         if (opt_pS)
-          throw std::invalid_argument("Cannot set sere priorities "
+          throw std::invalid_argument("Cannot set SERE priorities "
                                       "with Boolean output");
         break;
       case randltlgenerator::SERE:
@@ -471,7 +553,7 @@ namespace spot
         tok_pS = rs_->parse_options(opt_pS);
         tok_pB = rs_->rb.parse_options(opt_pB);
         if (opt_pL)
-          throw std::invalid_argument("Cannot set ltl priorities "
+          throw std::invalid_argument("Cannot set LTL priorities "
                                       "with SERE output");
         break;
       case randltlgenerator::PSL:
@@ -500,9 +582,10 @@ namespace spot
                                      const option_map& opts,
                                      char* opt_pL,
                                      char* opt_pS,
-                                     char* opt_pB)
+                                     char* opt_pB,
+                                     const atomic_prop_set* subs)
     : randltlgenerator(create_atomic_prop_set(aprops_n), opts,
-                       opt_pL, opt_pS, opt_pB)
+                       opt_pL, opt_pS, opt_pB, subs)
   {
   }
 
@@ -602,4 +685,5 @@ namespace spot
   {
     rs_->rb.dump_priorities(os);
   }
+
 }
diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh
index a7ea3561c..8c2e7e0cd 100644
--- a/spot/tl/randomltl.hh
+++ b/spot/tl/randomltl.hh
@@ -44,16 +44,33 @@ namespace spot
       delete[] proba_;
     }
 
-    /// Return the set of atomic proposition used to build formulae.
-    const atomic_prop_set*
-      ap() const
+    /// Return the set of atomic proposition used to build formulas.
+    const atomic_prop_set* ap() const
     {
       return ap_;
     }
 
+    /// Return the set of patterns (sub-formulas) used to build formulas.
+    const atomic_prop_set* patterns() const
+    {
+      return patterns_;
+    }
+
+    /// Check whether relabeling APs should use literals.
+    bool draw_literals() const
+    {
+      return draw_literals_;
+    }
+
+    /// Set whether relabeling APs should use literals.
+    void draw_literals(bool lit)
+    {
+      draw_literals_ = lit;
+    }
+
     /// \brief Generate a formula of size \a n.
     ///
-    /// It is possible to obtain formulae that are smaller than \a
+    /// It is possible to obtain formulas that are smaller than \a
     /// n, because some simple simplifications are performed by the
     /// AST.  (For instance the formula <code>a | a</code> is
     /// automatically reduced to <code>a</code> by spot::multop.)
@@ -63,7 +80,7 @@ namespace spot
     /// and atomic propositions.
     std::ostream& dump_priorities(std::ostream& os) const;
 
-    /// \brief Update the priorities used to generate the formulae.
+    /// \brief Update the priorities used to generate the formulas.
     ///
     /// \a options should be comma-separated list of KEY=VALUE
     /// assignments, using keys from the above list.
@@ -98,14 +115,16 @@ namespace spot
     op_proba* proba_2_or_more_;
     double total_2_and_more_;
     const atomic_prop_set* ap_;
+    const atomic_prop_set* patterns_ = nullptr;
+    bool draw_literals_;
   };
 
 
   /// \ingroup tl_io
-  /// \brief Generate random LTL formulae.
+  /// \brief Generate random LTL formulas.
   ///
-  /// This class recursively constructs LTL formulae of a given
-  /// size.  The formulae will use the use atomic propositions from
+  /// This class recursively constructs LTL formulas of a given
+  /// size.  The formulas will use the use atomic propositions from
   /// the set of propositions passed to the constructor, in addition
   /// to the constant and all LTL operators supported by Spot.
   ///
@@ -118,25 +137,26 @@ namespace spot
   public:
     /// Create a random LTL generator using atomic propositions from \a ap.
     ///
-    /// The default priorities are defined as follows:
+    /// The default priorities are defined as follows, depending on the
+    /// presence of \a subformulas.
     ///
     /** \verbatim
-        ap      n
-        false   1
-        true    1
-        not     1
-        F       1
-        G       1
-        X       1
-        equiv   1
-        implies 1
-        xor     1
-        R       1
-        U       1
-        W       1
-        M       1
-        and     1
-        or      1
+        ap      n              sub     n
+        false   1              false   1
+        true    1              true    1
+        not     1              not     1
+        F       1              F       1
+        G       1              G       1
+        X       1              X       1
+        equiv   1              equiv   1
+        implies 1              implies 1
+        xor     1              xor     1
+        R       1              R       1
+        U       1              U       1
+        W       1              W       1
+        M       1              M       1
+        and     1              and     1
+        or      1              or      1
         \endverbatim */
     ///
     /// Where \c n is the number of atomic propositions in the
@@ -147,18 +167,25 @@ namespace spot
     /// as each constant (i.e., true and false) to be picked.
     ///
     /// These priorities can be changed use the parse_options method.
-    random_ltl(const atomic_prop_set* ap);
+    ///
+    /// If a set of subformulas is passed to the constructor, the generator
+    /// will build a Boolean formulas using patterns as atoms.  Atomic
+    /// propositions in patterns will be rewritten randomly by drawing
+    /// some from \a ap.  The probability of false/true to be generated
+    /// default to 0 in this case.
+    random_ltl(const atomic_prop_set* ap,
+               const atomic_prop_set* subformulas = nullptr);
 
   protected:
-    void setup_proba_();
+    void setup_proba_(const atomic_prop_set* patterns);
     random_ltl(int size, const atomic_prop_set* ap);
   };
 
   /// \ingroup tl_io
-  /// \brief Generate random Boolean formulae.
+  /// \brief Generate random Boolean formulas.
   ///
-  /// This class recursively constructs Boolean formulae of a given size.
-  /// The formulae will use the use atomic propositions from the
+  /// This class recursively constructs Boolean formulas of a given size.
+  /// The formulas will use the use atomic propositions from the
   /// set of propositions passed to the constructor, in addition to the
   /// constant and all Boolean operators supported by Spot.
   ///
@@ -169,18 +196,19 @@ namespace spot
     /// Create a random Boolean formula generator using atomic
     /// propositions from \a ap.
     ///
-    /// The default priorities are defined as follows:
+    /// The default priorities are defined as follows depending on
+    /// the presence of \a subformulas.
     ///
     /** \verbatim
-        ap      n
-        false   1
-        true    1
-        not     1
-        equiv   1
-        implies 1
-        xor     1
-        and     1
-        or      1
+        ap      n         sub     n
+        false   1         false   0
+        true    1         true    0
+        not     1         not     1
+        equiv   1         equiv   1
+        implies 1         implies 1
+        xor     1         xor     1
+        and     1         and     1
+        or      1         or      1
         \endverbatim */
     ///
     /// Where \c n is the number of atomic propositions in the
@@ -191,14 +219,20 @@ namespace spot
     /// as each constant (i.e., true and false) to be picked.
     ///
     /// These priorities can be changed use the parse_options method.
-    random_boolean(const atomic_prop_set* ap);
+    ///
+    /// If a set of \a subformulas is passed to the constructor, the
+    /// generator will build a Boolean formulas using patterns as
+    /// atoms.  Atomic propositions in patterns will be rewritten
+    /// randomly by drawing some from \a ap.
+    random_boolean(const atomic_prop_set* ap,
+                   const atomic_prop_set* subformulas = nullptr);
   };
 
   /// \ingroup tl_io
   /// \brief Generate random SERE.
   ///
   /// This class recursively constructs SERE of a given size.
-  /// The formulae will use the use atomic propositions from the
+  /// The formulas will use the use atomic propositions from the
   /// set of propositions passed to the constructor, in addition to the
   /// constant and all SERE operators supported by Spot.
   ///
@@ -230,7 +264,7 @@ namespace spot
     /// These priorities can be changed use the parse_options method.
     ///
     /// In addition, you can set the properties of the Boolean
-    /// formula generator used to build Boolean subformulae using
+    /// formula generator used to build Boolean subformulas using
     /// the parse_options method of the \c rb attribute.
     random_sere(const atomic_prop_set* ap);
 
@@ -238,10 +272,10 @@ namespace spot
   };
 
   /// \ingroup tl_io
-  /// \brief Generate random PSL formulae.
+  /// \brief Generate random PSL formulas.
   ///
-  /// This class recursively constructs PSL formulae of a given size.
-  /// The formulae will use the use atomic propositions from the
+  /// This class recursively constructs PSL formulas of a given size.
+  /// The formulas will use the use atomic propositions from the
   /// set of propositions passed to the constructor, in addition to the
   /// constant and all PSL operators supported by Spot.
   class SPOT_API random_psl: public random_ltl
@@ -249,7 +283,7 @@ namespace spot
   public:
     /// Create a random PSL generator using atomic propositions from \a ap.
     ///
-    /// PSL formulae are built by combining LTL operators, plus
+    /// PSL formulas are built by combining LTL operators, plus
     /// three operators (EConcat, UConcat, Closure) taking a SERE
     /// as parameter.
     ///
@@ -287,11 +321,11 @@ namespace spot
     /// These priorities can be changed use the parse_options method.
     ///
     /// In addition, you can set the properties of the SERE generator
-    /// used to build SERE subformulae using the parse_options method
+    /// used to build SERE subformulas using the parse_options method
     /// of the \c rs attribute.
     random_psl(const atomic_prop_set* ap);
 
-    /// The SERE generator used to generate SERE subformulae.
+    /// The SERE generator used to generate SERE subformulas.
     random_sere rs;
   };
 
@@ -307,12 +341,14 @@ namespace spot
     randltlgenerator(int aprops_n, const option_map& opts,
                      char* opt_pL = nullptr,
                      char* opt_pS = nullptr,
-                     char* opt_pB = nullptr);
+                     char* opt_pB = nullptr,
+                     const atomic_prop_set* subformulas = nullptr);
 
     randltlgenerator(atomic_prop_set aprops, const option_map& opts,
                      char* opt_pL = nullptr,
                      char* opt_pS = nullptr,
-                     char* opt_pB = nullptr);
+                     char* opt_pB = nullptr,
+                     const atomic_prop_set* subformulas = nullptr);
 
     ~randltlgenerator();
 
@@ -345,4 +381,6 @@ namespace spot
     random_psl* rp_ = nullptr;
     random_sere* rs_ = nullptr;
   };
+
+
 }
diff --git a/tests/Makefile.am b/tests/Makefile.am
index bffb79ff1..54abc1a73 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -176,6 +176,7 @@ TESTS_tl = \
   core/kind.test \
   core/remove_x.test \
   core/ltlrel.test \
+  core/ltlmix.test \
   core/ltlgrind.test \
   core/ltlcrossgrind.test \
   core/ltlfilt.test \
diff --git a/tests/core/ltlmix.test b/tests/core/ltlmix.test
new file mode 100755
index 000000000..dd279e4fa
--- /dev/null
+++ b/tests/core/ltlmix.test
@@ -0,0 +1,93 @@
+#! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) by the Spot authors, see the AUTHORS file for details.
+#
+# 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 || exit 1
+
+set -e
+
+# Make sure sort isn't affected by the user's LC_COLLATE
+LC_ALL=C
+export LC_ALL
+
+ltlmix -fGa -fFb --tree-size=4 -n 50 -o out.ltl 2>stderr && exit 1
+grep 'failed to generate a new unique formula' stderr
+test 34 -eq `wc -l < out.ltl`
+
+ltlmix -fGa -fFb --tree-size=4 -n 500 -L -o out.ltl 2>stderr && exit 1
+grep 'failed to generate a new unique formula' stderr
+test 448 -eq `wc -l < out.ltl`
+
+P=--boolean-priorities=not=0,xor=0,equiv=0,implies=0
+ltlmix -fGa -fFb --tree-size=4 -n 10 $P -o out.ltl 2>stderr && exit 1
+grep 'failed to generate a new unique formula' stderr
+test 4 -eq `wc -l < out.ltl`
+
+ltlmix -fa -A9 --tree-size=1 -n9 | sort > list1
+ltlmix -fa -P9 --tree-size=1 -n18 | sort > list2
+grep -v '!' list2 > list3
+diff list1 list3
+
+# The following message appears only if run from a tty.
+if (: > /dev/tty) >/dev/null 2>&1 ; then
+   ltlmix -A9 -n10 </dev/tty 2>err && exit 2
+   grep 'No formula to combine' err
+fi
+
+
+genltl --gf-equiv-xn=1..3 | ltlmix --tree-size=1 -A2 -n6 | sort >out
+cat >expected <<EOF
+GF(p0 <-> XXXp0)
+GF(p0 <-> XXp0)
+GF(p0 <-> Xp0)
+GF(p1 <-> XXXp1)
+GF(p1 <-> XXp1)
+GF(p1 <-> Xp1)
+EOF
+diff out expected
+
+
+genltl --and-gf=4 > in.ltl
+ltlmix in.ltl --tree-size=1 -A1 --stats=%x > out.txt
+ltlmix in.ltl --tree-size=1 -A2 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -A3 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -A4 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -A5 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -A6 --stats=%x >> out.txt
+
+cat >expected <<EOF
+1
+2
+3
+4
+4
+4
+EOF
+diff out.txt expected
+
+# Using -P won't change the number of atomic propositions
+ltlmix in.ltl --tree-size=1 -P1 --stats=%x > out.txt
+ltlmix in.ltl --tree-size=1 -P2 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -P3 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -P4 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -P5 --stats=%x >> out.txt
+ltlmix in.ltl --tree-size=1 -P6 --stats=%x >> out.txt
+diff out.txt expected
+
+ltlmix -fa -A500 $P,or=0 -n10 | tee out
+test 10 -eq `grep '&.*&' < out | wc -l`