diff --git a/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean b/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean
index 4e082856d4..ecc238e3a0 100644
--- a/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean
+++ b/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean
@@ -75,7 +75,8 @@ private def seqEmptyTysIn (p : StrataDDM.Program) : Except String (List String)
   for d in cp.decls do
     match d with
     | .proc proc _ =>
-      for stmt in proc.body do
+      let stmts ← proc.body.getStructured
+      for stmt in stmts do
         out := out ++ (collectFromStmt stmt).map fmtSeqEmptyTy
     | _ => pure ()
   return out
@@ -128,4 +129,48 @@ spec { }
 /-- info: Except.ok ["Sequence bv32"] -/
 #guard_msgs in #eval seqEmptyTysIn nonEmptyBv32LiteralPgm
 
+/-! ## Empty literals for bv8, bv16, bv64 must also lower to typed `Sequence.empty`. -/
+
+private def emptyBv8LiteralPgm : StrataDDM.Program :=
+#strata
+program Boole;
+
+procedure p() returns (s: (Sequence bv8))
+spec { }
+{
+  s := Sequence.of_bv8[];
+};
+#end
+
+/-- info: Except.ok ["Sequence bv8"] -/
+#guard_msgs in #eval seqEmptyTysIn emptyBv8LiteralPgm
+
+private def emptyBv16LiteralPgm : StrataDDM.Program :=
+#strata
+program Boole;
+
+procedure p() returns (s: (Sequence bv16))
+spec { }
+{
+  s := Sequence.of_bv16[];
+};
+#end
+
+/-- info: Except.ok ["Sequence bv16"] -/
+#guard_msgs in #eval seqEmptyTysIn emptyBv16LiteralPgm
+
+private def emptyBv64LiteralPgm : StrataDDM.Program :=
+#strata
+program Boole;
+
+procedure p() returns (s: (Sequence bv64))
+spec { }
+{
+  s := Sequence.of_bv64[];
+};
+#end
+
+/-- info: Except.ok ["Sequence bv64"] -/
+#guard_msgs in #eval seqEmptyTysIn emptyBv64LiteralPgm
+
 end Strata