Fix side condition in new simplification for mcd-structured (#2830)

* Adjust side condition (X <Int 2^numbits not X <=Int)

* add length condition and preserves-definedness

* remove accidentally-committed json file

Author: jberthold

tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json

@@ -404,8 +404,9 @@ module LEMMAS-MCD [symbolic]
   // #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 X <Int 2 ^Int ( 8 *Int N)
      andBool #asInteger(NULLBYTES) ==Int 0
-    [simplification, concrete(NULLBYTES)]
+     andBool lengthBytes(NULLBYTES) ==Int N
+    [simplification, concrete(NULLBYTES), preserves-definedness]
 
 endmodule