Trigger warning might cause slow and failing verification
Opened this issue · 0 comments
mschwerhoff commented
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.