diff --git a/NEWS b/NEWS
index 0aa3e31f0..4ff6eb53e 100644
--- a/NEWS
+++ b/NEWS
@@ -32,8 +32,7 @@ New in spot 2.5.2.dev (not yet released)
     and fg_safety_to_dca() is a specialized construction for
     translating formulas of the form FG(safety) to DCA.  These
     are slight generalizations of some constructions proposed
-    by J. Esparza, J. Křentínský, and S. Sickert in a submitted
-    paper.
+    by J. Esparza, J. Křentínský, and S. Sickert (LICS'18).
 
     These are now used by the main translation routine, and can be
     disabled by passing -x '!gf-guarantee' to ltl2tgba.  As an
diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x
index 881265282..e6c534cec 100644
--- a/bin/man/spot-x.x
+++ b/bin/man/spot-x.x
@@ -281,6 +281,16 @@ checks for ω-regular languages, Proceedings of SPIN'15.  LNCS 9232.
 Describes the stutter-invariance checks that can be selected through
 \fBSPOT_STUTTER_CHECK\fR.
 
+.TP
+5.
+Javier Esparza, Jan Křetínský and Salomon Sickert: One Theorem to Rule
+Them All: A Unified Translation of LTL into ω-Automata.  Proceedings
+of LICS'18.  To appear.
+
+Describes (among other things) the constructions used for translating
+formulas of the form GF(guarantee) or FG(safety), that can be
+disabled with \fB-x gf-guarantee=0\fR.
+
 
 [SEE ALSO]
 .BR ltl2tgba (1)
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index d5b23ffa3..b9d1a77b0 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -107,10 +107,9 @@ the determinization algorithm.") },
 the determinization algorithm.") },
     { DOC("det-stutter", "Set to 0 to disable optimizations based on \
 the stutter-invariance in the determinization algorithm.") },
-    // FIXME: Add bibliographic reference to their paper ASAP.
     { DOC("gf-guarantee", "Set to 0 to disable alternate constructions \
 for GF(guarantee)->[D]BA and FG(safety)->DCA.  Those constructions \
-are based on work by J. Esparza, J. Křentínský, and S. Sickert.  \
+are from an LICS'18 paper by J. Esparza, J. Křentínský, and S. Sickert.  \
 This is enabled by default for medium and high optimization \
 levels.  Unless we are building deterministic automata, the \
 resulting automata are compared to the automata built using the \
diff --git a/spot/twaalgos/gfguarantee.hh b/spot/twaalgos/gfguarantee.hh
index 97611dbdb..8e163dce8 100644
--- a/spot/twaalgos/gfguarantee.hh
+++ b/spot/twaalgos/gfguarantee.hh
@@ -39,8 +39,8 @@ namespace spot
   /// If \a state_based is not set, all transition going to terminal
   /// states are made accepting and redirected to the initial state.
   ///
-  /// This construction is inspired by a similar construction in a
-  /// submitted paper by J. Esparza, J. Křetínský, & S. Sickert.
+  /// This construction is inspired by a similar construction in the
+  /// LICS'18 paper by J. Esparza, J. Křetínský, and S. Sickert.
   SPOT_API twa_graph_ptr
   g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based = false);
 
@@ -56,10 +56,10 @@ namespace spot
   /// Return nullptr if the input formula is not of the supported
   /// form.
   ///
-  /// This construction generalized a similar construction in a
-  /// submitted paper by J. Esparza, J. Křetínský, & S. Sickert in the
-  /// sense that it will work if Φ represent a safety property, even
-  /// if it is not a syntactic safety.
+  /// This construction generalizes a construction in the LICS'18
+  /// paper of J. Esparza, J. Křetínský, and S. Sickert.  This version
+  /// will work if Φ represent a safety property, even if it is not a
+  /// syntactic safety.
   SPOT_API twa_graph_ptr
   gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict,
                            bool deterministic = true, bool state_based = false);