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 I2 requires I1 >=Int I2 rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)