Skip to content

Sequence containment does not work in triggers #349

@marcoeilers

Description

@marcoeilers

The following trivial program does not verify:

method wow(s: Seq[Int])
  requires forall i: Int :: {i in s} i in s == i > 5
{
    assert 7 in s
}

The problem is that the trigger is translated using the function Seq#ContainsTrigger, but the assertion uses the function Seq#Contains, and the two are not connected anywhere in the sequence axiomatization.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions