Is verification condition splitting implemented

Aug 19, 2010 at 3:36 PM
Hi, one quick question: Is the verification condition splitting outlined in the paper "Verification Condition Splitting" by Leino et al. implemented in the normal boogie releases? Thanks, Thorsten
Aug 19, 2010 at 7:48 PM

Yes, it is. Boogie /help gives some description of how to use it.

Aug 20, 2010 at 9:29 AM

Thanks, it worked. It reduced the maximum verification time quite a bit, but did not have much affect on the average in my set of samples.

Aug 20, 2010 at 6:29 PM

This is expected. There is more Z3 invocations, so randomness in each averages out.

Back in Z3 1.x days it used to speed up the proving process, but the current Z3 version seems to keep the context tidy and needs not “manual cleaning up”.