support for vampire prover

[nikhedonia]

Just wanted to raise awareness of Vampire Prover

Vampire prover uses z3 and minisat internally and performs significantly better in many tasks. One of its unique features is to can discover loop invariants and compute closed form solutions.

Here is the talk about Vampire Prover at FaceTAV from last week: https://www.facebook.com/ze.jaloto/videos/10157041551887975/

[levjj]

Thanks! I just noticed that the Vampire prover supports SMTLIB 2 input, so it might not be too difficult to use it for esverify.