Skip to content

Commit ae3569a

Browse files
committed
Update src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
1 parent 017837e commit ae3569a

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ module INT-SIMPLIFICATIONS [symbolic]
3636
rule [bytes2int-and-255-noop]: Bytes2Int(X, LE, Unsigned) &Int 255 => Bytes2Int(X, LE, Unsigned)
3737
requires lengthBytes(X) <=Int 1 [simplification]
3838
rule [bytes2int-zero-prefix-or-to-concat]: Bytes2Int(b"\x00" +Bytes X, LE, Unsigned) |Int Y => Bytes2Int(Int2Bytes(Y, LE, Unsigned) +Bytes X, LE, Unsigned)
39-
requires Y <Int 256 [simplification, concrete(Y)]
39+
requires 0 <=Int Y andBool Y <Int 256 [simplification, concrete(Y)]
4040
```
4141

4242
## Equality Lemmas

0 commit comments

Comments
 (0)