Sample‐Based Testing

We now have tools for randomly testing Vampire over its many options and thereby finding crashes.

To do this, you need the following points:

1. Build Vampire in a debug configuration. Release works too, but you typically want to trap assertion violations here.
2. Run Vampire over an appropriate set of problems that you care about, such as the FOF fragment of TPTP. You may find tools such as GNU Parallel useful here.
3. Sample random strategies using a sampler file with e.g. --sample_strategy samplers/samplerFOL.txt. We have some prebuilt sampler files in samplers/. (samplerSMT.txt is for theory reasoning, best run on SMT problems, samplerIND.txt covers most of the induction machinery.)

A suitable pattern for finding problems is viola|SIG|error. (error for USER_ERRORs, but careful, gives some false positives on SMTLIB.)

Hot Tips from Martin

1. Use randomised options, e.g. -si on -rtra on to further randomise Vampire's execution.
2. Use a few different random seeds with --random_seed N.
3. Try with a small resource limit such as -i 100 at first, then increment in orders of magnitude up to maybe -i 10000.