In the case of loop invariants, there are two queries:
verify the loop condition holds at beginning of loop
Verify that given the invariant, the invariant still holds
I think a typical approach is to split these up into separate, perhaps parallel calls to Z3. Currently our approach is to smush them into a single query. There may be other such opportunities for query splitting. This probably would provide performance benefits although nothing is guaranteed.
In the case of loop invariants, there are two queries:
I think a typical approach is to split these up into separate, perhaps parallel calls to Z3. Currently our approach is to smush them into a single query. There may be other such opportunities for query splitting. This probably would provide performance benefits although nothing is guaranteed.