Triggers in SMT output
See this cvc5 issue, where we reported some regressions to cvc5 team. According to Andrew Reynolds it was due to this:
Just for more information, the quantified formulas that are confusing are of this form:
(forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y))))
Technically this is say "instantiate x with no guidance, afterwards instantiate y based on the pattern (f x y) for which x you chose. > The clearer definition is:
(forall ((x Int) (y Int)) (! P :pattern ((f x y))))
Which says "instantiate x and y based on the pattern (f x y)".
It seems they are fixing cvc5 to accept both forms, but do we want to change why3 to emit the second form?