This bug will be introduced by #447
There's an issue with wildcard predicates and syntax sugared predicates :(
Let's say I write this custom predicate:
MyPred(a, b) = AND(
Equal(a, 5)
b(8, 1)
)
And then I want to prove with b = Gt, so I'll create these statements
Gt is syntax sugar for Lt, so the statement I get is Lt(1, 8), and now the arguments don't match with the template (they are swapped)
I don't think we will use wildcard predicates with native predicates because the interesting case of dynamic predicates is using them with custom predicates (so that the user defines the rules arbitrarily).
A potential solutions is to forbid using native predicates as wildcards via a check in the frontend.
This bug will be introduced by #447
There's an issue with wildcard predicates and syntax sugared predicates :(
Let's say I write this custom predicate:
And then I want to prove with
b = Gt, so I'll create these statementsGtis syntax sugar forLt, so the statement I get isLt(1, 8), and now the arguments don't match with the template (they are swapped)I don't think we will use wildcard predicates with native predicates because the interesting case of dynamic predicates is using them with custom predicates (so that the user defines the rules arbitrarily).
A potential solutions is to forbid using native predicates as wildcards via a check in the frontend.