Resolve non-determinism in minInt (#4544)

Fixes #4543
runtimeverification · Jul 23, 2024 · ce19f5e · ce19f5e
1 parent 3435a3c
commit ce19f5e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)