diff --git a/NEWS b/NEWS
index 8b469d5fd..c1c464f92 100644
--- a/NEWS
+++ b/NEWS
@@ -16,6 +16,7 @@ New in spot 1.2.5a (not yet released)
       state labels.
     - the acceptance specification in the HOA format output have been
       adjusted to match recent changes in the format specifications.
+    - atomic propositions are correctly escaped in the HOA output.
     - the build rules for documentation have been made compatible with
       version 8.0 of Org-mode.  (This was only a problem if you build
       from the git repository, or if you want to edit the
diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc
index 152d5e506..afbe546be 100644
--- a/src/tgbaalgos/hoaf.cc
+++ b/src/tgbaalgos/hoaf.cc
@@ -32,6 +32,7 @@
 #include "misc/minato.hh"
 #include "tgba/formula2bdd.hh"
 #include "ltlvisit/tostring.hh"
+#include "ltlast/atomic_prop.hh"
 
 namespace spot
 {
@@ -265,7 +266,11 @@ namespace spot
     bdd_dict* d = aut->get_dict();
     for (metadata::vap_t::const_iterator i = md.vap.begin();
 	 i != md.vap.end(); ++i)
-      escape_str(os << " \"", to_string(d->bdd_map[*i].f)) << '"';
+      {
+	const ltl::atomic_prop* f = ltl::is_atomic_prop(d->bdd_map[*i].f);
+	assert(f);
+	escape_str(os << " \"", f->name()) << '"';
+      }
     os << nl;
     unsigned num_acc = md.acc.size();
     if (num_acc == 0)