Skip to content

Commit caac131

Browse files
authored
Update from master (#934)
Missing simplification for `0 <= asInt(#findVariantIdxAux(...))`
2 parents 1b9da75 + 030db09 commit caac131

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,10 @@ For symbolic enum values, the variant index remains unevaluated but the original
9494
requires isOneOf(DISCR, DISCRS)
9595
[simplification, symbolic(DISCR)]
9696
97+
rule 0 <=Int asInt(#findVariantIdxAux(DISCR, DISCRS, _)) => true
98+
requires isOneOf(DISCR, DISCRS)
99+
[simplification, symbolic(DISCR)]
100+
97101
syntax Bool ::= isOneOf ( Int , Discriminants ) [function, total]
98102
// --------------------------------------------------------------
99103
rule isOneOf( _, .Discriminants ) => false

0 commit comments

Comments
 (0)