Incompleteness when unrolling a loop too many times

[viper-admin]

Created by bitbucket user robinsierra on 2019-06-04 17:44 Last updated on 2019-07-29 14:18

When doing loop unrolling both Silicon and Carbon hit a limit after which they can’t prove the postcondition anymore.

• 99 iterations: ok for both Silicon and Carbon (SyCy.vpr)
• 100 iterations: ok for Silicon, but not Carbon (SyCn.vpr)
• 101 iterations: neither Silicon nor Carbon (SnCn.vpr)

---

Attachments:

• SyCy.vpr
• SyCn.vpr
• SnCn.vpr

[viper-admin]

Bitbucket user robinsierra commented on 2019-06-04 17:48

See also Silicon issue 386.

[viper-admin]

@marcoeilers commented on 2019-07-29 12:53

A workaround is calling Carbon with

--boogieOpt="/z3opt:smt.qi.lazy_threshold=N" 

where N is the desired maximum number of instantiations for any given quantifier (default seems to be 100).

[viper-admin]

@alexanderjsummers commented on 2019-07-29 14:18

This is a “nice” issue. I guess we should remove the threshold entirely. It has bitten us in the past, too (and then we increased it…)