From 1c8b7b85a3a3c2b22ea93a1b585dc6169a165fdc Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 23 Jul 2024 10:20:24 +0200 Subject: [PATCH] Resolve non-determinism in minInt --- 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 I2 requires I1 >=Int I2 rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)