assume writable to save verification time

Oct 28, 2010 at 2:07 AM


I observed in Z3Inspector that proving 'writable' takes time for some variable. Once it is verified, I know that it is writable. Now next time I want to verify the same program with only slight change(which I am sure does not effect the writ-ability of same variable), I want the verifier to skip this step, to same time.

How can I do so?

e.g. something like assume(writable(variable_name));

I did the similar thing for assume(typed(var)); and assume(thread_local(var)); to save time.



Oct 28, 2010 at 6:57 AM

Unfortunately, this is not so easy as there is no C-level name for writable. If you think it would helpful, file an issue on the issue tracker and we will have a look at it.