Merge remote-tracking branch 'origin/develop'

runtimeverification · Oct 17, 2024 · 2b3f7c8 · 2b3f7c8
2 parents 664df4c + 2d26b93
commit 2b3f7c8
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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 <Int N [simplification]
 
   // Bit-shifts
-  rule X <<Int 0 => X [simplification]
-  rule 0 <<Int _ => 0 [simplification]
-  rule X >>Int 0 => X [simplification]
-  rule 0 >>Int _ => 0 [simplification]
+  rule X <<Int 0 => X                    [simplification, preserves-definedness]
+  rule 0 <<Int Y => 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]