From d00b4e7bc6e747df21a705d516fce0c9242ae0dd Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Fri, 12 Dec 2025 17:45:37 +1100
Subject: [PATCH] add simplification to mcd-structured verification module (buf
 ==K nullbytes)

---
 tests/specs/mcd-structured/verification.k | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tests/specs/mcd-structured/verification.k b/tests/specs/mcd-structured/verification.k
index 8078d1654c..aaec5beecb 100644
--- a/tests/specs/mcd-structured/verification.k
+++ b/tests/specs/mcd-structured/verification.k
@@ -401,4 +401,11 @@ module LEMMAS-MCD [symbolic]
     rule #if B #then C #else D #fi => C requires         B [simplification]
     rule #if B #then C #else D #fi => C requires notBool B [simplification]
 
+  // #buf simplification comparing to null-bytes: compare as Int
+  rule #buf(N, X:Int) ==K NULLBYTES => X ==Int 0
+    requires 0 <=Int X
+     andBool X <=Int 2 ^Int ( 8 *Int N)
+     andBool #asInteger(NULLBYTES) ==Int 0
+    [simplification, concrete(NULLBYTES)]
+
 endmodule