Distinguish models by their absolute paths rather than their contents
At the moment Weaver caches results obtained for models using checksums calculated on the base of their contents. Surprisingly, contents of different models can be the same. For instance, Pavel Andrianov reported such the case: both of his models are actually empty (there is just the same copyright notice).
It seems that it will be enough to distinguish different models just by their absolute paths that are unique during the whole verification job solution.