The Viper tutorial explicitly states that function applications, which contain operations in its arg(s), can't be used as triggers.
For example, f(x + 1) is not a valid trigger.
When not specifying triggers, leaving Viper to find them instead, no triggers are generated. When using the Silicon backend this does not result in any error or warning. If using Carbon this generates a warning.
Weird case still exists where keeping an invalid trigger makes functions verify and unrolls the function (#35).
The Viper tutorial explicitly states that function applications, which contain operations in its arg(s), can't be used as triggers. For example,
f(x + 1)is not a valid trigger. When not specifying triggers, leaving Viper to find them instead, no triggers are generated. When using the Silicon backend this does not result in any error or warning. If using Carbon this generates a warning.Weird case still exists where keeping an invalid trigger makes functions verify and unrolls the function (#35).