diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 9dd803c9de9..3e5e6e783e2 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2210,14 +2210,14 @@ module BYTES imports BYTES-KORE imports private INT + rule Int2Bytes(I::Int, _::Endianness, _) => .Bytes + requires I ==Int 0 rule Int2Bytes(I::Int, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E) requires I >Int 0 [preserves-definedness] - rule Int2Bytes(0, _::Endianness, _) => .Bytes - rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E) + rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E) requires I >Int 0 [preserves-definedness] - rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E) - requires I Int2Bytes(1, -1, E) + rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E) + requires I