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.

[marcoeilers]

With current master Silicon, the warning still shows up, but Silicon is no longer slow. It takes 6.4 seconds on my laptop when started from scratch, so I'd assume like 3 seconds on a warmed up Viper server. I have no idea what may have caused the difference, but I'd say that means the performance problem no longer exists.