Triggers without appropriate variables can make it to Boogie (causing internal error)

[viper-admin]

Created by @alexanderjsummers on 2017-03-26 11:01 Last updated on 2017-03-26 11:04

In the following example, a trigger is manually specified for the select_store_diff axiom which, because of a typo, does not mention all quantified variables. An internal error is encountered - we send an invalid trigger to Boogie. This sounds like a Silver issue, but Silicon does not encounter it.

---

Attachments:

• Matrices.vpr

[viper-admin]

@alexanderjsummers on 2017-03-26 11:04:

• edited the description