From 11b77e8d333aa49c9f7aa8d7216b4dcf1e9361ca Mon Sep 17 00:00:00 2001
From: GrigorenkoPV <grigorenkopv@ya.ru>
Date: Tue, 28 May 2024 16:17:55 +0300
Subject: [PATCH 1/2] Fix `{,e}println!()`

---
 library/std/src/lib.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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)*); }};
 }
 

From a609bb89f47d22bdecb8ddfddd6e6dfa37c9bbec Mon Sep 17 00:00:00 2001
From: Pavel Grigorenko <GrigorenkoPV@ya.ru>
Date: Wed, 29 May 2024 14:09:33 +0300
Subject: [PATCH 2/2] Add a test for `{,e}println!()`

---
 tests/kani/Print/no_semicolon.rs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 tests/kani/Print/no_semicolon.rs

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();
+}