Dear VST developers and everyone who is using VST,
I am working on an industrial verification project that uses Verified Software Toolchain (until now we have ~300 loc verified, but we aim at ~1800 in the near future), and compilation times for common tactics became an issue. In particular, forward
, forward_call
, entailer!
can take up to 1 min to execute. Since proofs range between 500 and 3000 loc, and these are very common tactics, the development becomes very slow and painful. Is this normal? Are there ways to speed up the process? Is there anyone from VST community who could share their expertise on this topic? It will be very much appreciated!