Silicon takes long time to verify abstract function with unfolding in postconditions

[ThomasMayerl]

I have a small Gobra file that should only return an abstract data structure based on heap data structures. The function does not have a body and even if it is never called, it will take a long time for Silicon to prove. I attached the Viper file after translation from Gobra.

Some further remarks:

• If we change the function (toAbstractChain2) to be a method (and then also hand permissions back in the postcondition, so that we have access from the other postconditions), Silicon terminates within seconds.
• If we select Carbon instead of Silicon, it also terminates within seconds.
• Upon running Silicon with --printTranslatedProgram, there is a method toAbstractChain2_97009f8b_F_posts_termination_proof (see second attachment). On line 668, there is an if statement. If we comment out the last two conjuncts (i.e. the ones from lines 680-701), Silicon also terminates within seconds.

defs2.gobra.vpr.txt

defs2-translated.vpr.txt

[marcoeilers]

Silver PR viperproject/silver#879 modifies the termination plugin so that these checks, which are not actually needed for this specific example, are no longer generated. Then we still have the more general problem that verifying this code is apparently really slow. That problem should hopefully be fixed by #929 once that's merged.