From 62252934ad0a77be7a410c4d730f75866d5cf114 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Fri, 19 Jul 2024 13:29:27 +1000
Subject: [PATCH] Further fine-tune equations for Int2Bytes(Int, Endianness,
 Signedness)

* Use `0 ==Int I` instead of a syntactic _match_ of the argument with `0`.
  This enables evaluating terms with `I ==Int 0` in the path condition.
* Remove case with literal `-1` and widen requires in equation for negative
  arguments (previously `I <Int -1`, now `I <Int 0`).
---
 k-distribution/include/kframework/builtin/domains.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

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 <Int -1 [preserves-definedness]
-  rule Int2Bytes(-1, E::Endianness, Signed) => Int2Bytes(1, -1, E)
+  rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
+    requires I <Int 0 [preserves-definedness]
 endmodule
 ```