diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index b04af99c8e..bd6ea7716e 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1366,10 +1366,10 @@ module INT-SYMBOLIC [symbolic] rule X %Int N => X requires 0 <=Int X andBool X X [simplification] - rule 0 < 0 [simplification] - rule X >>Int 0 => X [simplification] - rule 0 >>Int _ => 0 [simplification] + rule X < X [simplification, preserves-definedness] + rule 0 < 0 requires 0 <=Int Y [simplification, preserves-definedness] + rule X >>Int 0 => X [simplification, preserves-definedness] + rule 0 >>Int Y => 0 requires 0 <=Int Y [simplification, preserves-definedness] endmodule module INT-SYMBOLIC-KORE [symbolic, haskell]