Trigger warning might cause slow and failing verification

[mschwerhoff]

For file wSolRec_rec.vpr.txt, Silicon generates a "trigger might not be usable" warning for the following loop invariant:

forall xs: Seq[Int] :: {price(n, xs, prices)} valid_cut(xs, n) && 0 < xs[0] < i ==> price(n, xs, prices) <= price(n, bestCuts, prices)

Carbon verifies the file in 2s, while Silicon fails after 30s. This might be due to triggering. I spent a bit of time trying to isolate the problem, but for (much) simpler versions, the warning didn't appear.