From ce19f5ef895de85e59b75cdb1df3b26f33552618 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Tue, 23 Jul 2024 11:02:09 +0200
Subject: [PATCH] Resolve non-determinism in minInt (#4544)

Fixes #4543
---
 k-distribution/include/kframework/builtin/domains.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
index 3e5e6e783e2..7426c158392 100644
--- a/k-distribution/include/kframework/builtin/domains.md
+++ b/k-distribution/include/kframework/builtin/domains.md
@@ -1432,7 +1432,7 @@ module INT
     ((I1 %Int absInt(I2)) +Int absInt(I2)) %Int absInt(I2)
   requires I2 =/=Int 0    [concrete, simplification]
 
-  rule minInt(I1:Int, I2:Int) => I1 requires I1 <=Int I2
+  rule minInt(I1:Int, I2:Int) => I1 requires I1 <Int  I2
   rule minInt(I1:Int, I2:Int) => I2 requires I1 >=Int I2
 
   rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)