add simplification to mcd-structured verification module (buf ==K nullbytes) (#2828)

Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>

Author: jberthold

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