Linter "expression is always true [vcg-always-true]" falsely thrown when using "exists" in checks

[christophkloeffel]

Example .rsl:

package Foo

type T {
    a Integer[0..*]
}

checks T {
    (exists item in a => item == 7), warning "there is no 7 in a"
}

Example .trlc:

package Foo

T Bar {
    a = [7]
}

T Kitten {
    a = []
}

Output:

(exists item in a => item == 7), warning "7 is not allowed in a"
 ^^^^^^ rbt-existential-quantification-semantics/foo.rsl:8: issue: expression is always true [vcg-always-true]
T Kitten {
  ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a
Processed 1 model, 0 checks and 1 requirement file and found 2 warnings

Expectation: The linter should not throw this issue

[florianschanda]

Thank you for this find. I can confirm it is a real issue.

[florianschanda]

I think I am mis-translating existential quantifiers.

While (forall bounds => expr) is the correct for, for exists it needs to be (exists bounds and expr).