1
Vote

Empty set membership assertion produces Boogie error

description

The code
assert forall x:int :: x !in {};
produces the following error message
stdin.dfy(2,9): Error: trigger must mention all quantified variables, but does not mention: x#1
1 name resolution errors detected in D:\local\Temp\stdin.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

D:\local\Temp\stdin.bpl(1753,31): Error: trigger must mention all quantified variables, but does not mention: x#1
1 name resolution errors detected in D:\local\Temp\stdin.bpl

comments