diff --git a/src/rewrite/vct/rewrite/EnumToDomain.scala b/src/rewrite/vct/rewrite/EnumToDomain.scala
index c6368addd..0c3f25860 100644
--- a/src/rewrite/vct/rewrite/EnumToDomain.scala
+++ b/src/rewrite/vct/rewrite/EnumToDomain.scala
@@ -124,12 +124,14 @@ case class EnumToDomain[Pre <: Generation]() extends CoercingRewriter[Pre] {
                 )))
 
                 // toIntRange
-                aDTDeclarations.declare(new ADTAxiom(forall[Post](
-                  T(enum),
-                  e =>
-                    (const(0) <= InlinePattern(toInt(e))) &&
-                      (toInt(e) < const(enum.constants.length)),
-                )))
+                if (enum.constants.nonEmpty) {
+                  aDTDeclarations.declare(new ADTAxiom(forall[Post](
+                    T(enum),
+                    e =>
+                      (const(0) <= InlinePattern(toInt(e))) &&
+                        (toInt(e) < const(enum.constants.length)),
+                  )))
+                }
               }._1,
               Seq(),
             ))
diff --git a/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala b/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala
index af3ea6066..850c572b6 100644
--- a/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala
+++ b/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala
@@ -45,6 +45,10 @@ class Test {
     enum AB { A, B }
   """
 
+  vercors should verify using silicon in "pvl/enum empty" pvl """
+    enum Empty { }
+  """
+
   vercors should verify using silicon in "pvl/enum return" pvl """
     enum AB { A, B }