Silicon instantiates axioms when trigger terms are in the wrong state

[viper-admin]

Created by @alexanderjsummers on 2019-03-08 12:28 Last updated on 2019-03-08 13:56

In the attached example, two methods are expected not to verify, since the trigger terms are available in the wrong (old, rather than current) states. However, they go through with Silicon (the example comes from the somewhat-related Carbon issue 264).

---

Attachments:

• 0264.vpr

[viper-admin]

@alexanderjsummers on 2019-03-08 12:29:

• changed attachment from (none) to 0264.vpr
• edited the description

[viper-admin]

@alexanderjsummers on 2019-03-08 12:30:

• edited the description

[viper-admin]

@mschwerhoff commented on 2019-03-08 13:56

Could be related to https://github.com/viperproject/silicon/issues/204