diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index 37e0e5a21518..3f8427ffff13 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -135,14 +135,14 @@ macro_rules! eprint {
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! println {
-    () => { };
+    () => { $crate::print!("\n") };
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! eprintln {
-    () => { };
+    () => { $crate::eprint!("\n") };
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
diff --git a/tests/kani/Print/no_semicolon.rs b/tests/kani/Print/no_semicolon.rs
new file mode 100644
index 000000000000..bee09e628472
--- /dev/null
+++ b/tests/kani/Print/no_semicolon.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that the (e)println with no arguments do not require a trailing semicolon
+
+fn println() {
+    println!()
+}
+fn eprintln() {
+    eprintln!()
+}
+
+#[kani::proof]
+fn main() {
+    println();
+    eprintln();
+}