Best practices & Pitfalls for Viper, Silicon and Carbon

Best-practices & Pitfalls for Viper, Silicon and Carbon

Slow verification

Problem

A Viper program takes 190 seconds to verify in Silicon. The CFG looks reasonable, but there are a lot of statements (>1000) and a lot of local variables (>200). By removing 123 unnecessary <var> := new() statements the verification time goes from 190s to just 20s -- a big improvement, but it's still a lot. There are still 50 new(..) statements in the program.

Questions

What is the cause of the 10x reduction in verification time (from 190s to 20s)? How to speed up the verification?

Solution

Each new() statement has to ensure that the result is different from any other reference, and this adds quite some overhead. By removing the remaining 50 new() statements the verification time goes below 8 seconds.