diff --git a/NEWS b/NEWS
index 098a4948b..5bc21f22d 100644
--- a/NEWS
+++ b/NEWS
@@ -82,6 +82,11 @@ New in spot 2.10.5.dev  (not yet released)
     averted in the parser by delaying the construction of such n-ary
     nodes until all children are known.
 
+  - make_twa_graph() will now preserve state number when copying a
+    kripke_graph object.  As a consequence, print_dot() and
+    print_hoa() will now use state numbers matching those of the
+    kripke_graph (issue #505).
+
 New in spot 2.10.5  (2022-05-03)
 
   Bugs fixed:
diff --git a/THANKS b/THANKS
index b49b3eb95..4a7259d46 100644
--- a/THANKS
+++ b/THANKS
@@ -11,6 +11,7 @@ Christian Dax
 Christopher Ziegler
 Clément Tamines
 David Müller
+Edmond Irani Liu
 Ernesto Posse
 Étienne Renault
 Fabrice Kordon
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index b11ca12c5..c2bdd5650 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -23,6 +23,7 @@
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/timer.hh>
 #include <spot/twa/bddprint.hh>
+#include <spot/kripke/kripkegraph.hh>
 #include <spot/misc/escape.hh>
 #include <spot/priv/robin_hood.hh>
 #include <vector>
@@ -1600,6 +1601,17 @@ namespace spot
           return p.first->second;
         };
 
+      // If the input is a kripke_graph and the number of states is
+      // not restricted, predeclare all states to keep their
+      // numbering, and also copy unreachable states.
+      if (max_states == -1U)
+        if (auto kg = std::dynamic_pointer_cast<const kripke_graph>(aut))
+          {
+            unsigned ns = kg->num_states();
+            for (unsigned s = 0; s < ns; ++s)
+              new_state(kg->state_from_number(s));
+          }
+
       out->set_init_state(new_state(aut->get_init_state()));
       while (!todo.empty())
         {
@@ -1638,7 +1650,6 @@ namespace spot
             }
         }
 
-
       auto s = seen.begin();
       while (s != seen.end())
         {
diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc
index 1865a6d49..0e03b07f5 100644
--- a/spot/twaalgos/hoa.cc
+++ b/spot/twaalgos/hoa.cc
@@ -31,6 +31,7 @@
 #include <spot/twa/formula2bdd.hh>
 #include <spot/tl/formula.hh>
 #include <spot/kripke/fairkripke.hh>
+#include <spot/kripke/kripkegraph.hh>
 
 using namespace std::string_literals;
 
@@ -973,7 +974,11 @@ namespace spot
           strcpy(tmpopt, opt);
         tmpopt[n] = 'k';
         tmpopt[n + 1] = 0;
-        preserve_names = true;
+        // Preserve names if we have some state names, or if we are
+        // not a kripke_graph.
+        auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
+        preserve_names =
+          !!sn || !std::dynamic_pointer_cast<const kripke_graph>(aut);
       }
 
     auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
diff --git a/tests/python/kripke.py b/tests/python/kripke.py
index fa92b3fa9..b1669bb78 100644
--- a/tests/python/kripke.py
+++ b/tests/python/kripke.py
@@ -29,35 +29,53 @@ p2 = buddy.bdd_ithvar(k.register_ap("p2"))
 cond1 = p1 & p2
 cond2 = p1 & -p2
 cond3 = -p1 & -p2
-s2 = k.new_state(cond1)
+s0 = k.new_state(cond1)
 s1 = k.new_state(cond2)
-s3 = k.new_state(cond3)
+s2 = k.new_state(cond3)
+k.new_edge(s1, s0)
+k.new_edge(s0, s0)
 k.new_edge(s1, s2)
 k.new_edge(s2, s2)
-k.new_edge(s1, s3)
-k.new_edge(s3, s3)
-k.new_edge(s3, s2)
+k.new_edge(s2, s0)
 k.set_init_state(s1)
 
 hoa = """HOA: v1
 States: 3
-Start: 0
+Start: 1
 AP: 2 "p1" "p2"
 acc-name: all
 Acceptance: 0 t
 properties: state-labels explicit-labels state-acc
 --BODY--
-State: [0&!1] 0 "1"
-1 2
-State: [0&1] 1 "0"
-1
-State: [!0&!1] 2 "2"
-2 1
+State: [0&1] 0
+0
+State: [0&!1] 1
+0 2
+State: [!0&!1] 2
+2 0
 --END--"""
 tc.assertEqual(hoa, k.to_str('HOA'))
 tc.assertEqual(k.num_states(), 3)
 tc.assertEqual(k.num_edges(), 5)
 
+k.set_state_names(["s0", "s1", "s2"])
+hoa = """HOA: v1
+States: 3
+Start: 1
+AP: 2 "p1" "p2"
+acc-name: all
+Acceptance: 0 t
+properties: state-labels explicit-labels state-acc
+--BODY--
+State: [0&1] 0 "s0"
+0
+State: [0&!1] 1 "s1"
+0 2
+State: [!0&!1] 2 "s2"
+2 0
+--END--"""
+tc.assertEqual(hoa, k.to_str('HOA'))
+
 res = []
 for e in k.out(s1):
     res.append((e.src, e.dst))