Examples
This page presents some additional examples. Some of them are in SMTLIB syntax, others are examples in Java. Further examples can be downloaded from the SMTLIB website.
| Benchmark | Description | Download |
| usage.smt2 | Example from the usage section of the tool paper | usage.smt2 (Checksum: SHA 256 ) |
| unsat.smt2 | Example from the "Proofs and Annotations" section of the tool paper | unsat.smt2 (Checksum: SHA 256 ) |
| subannot.smt2 | Example that demonstrates sub annotations in proofs from SMTInterpol | subannot.smt2 (Checksum: SHA 256 ) |
| interpolation.smt2 | Interpolation example | interpolation.smt2 (Checksum: SHA 256 ) |
| mccarthy1.smt2 | Interpolation example from McCarthy's 91 function | mccarthy1.smt2 (Checksum: SHA 256 ) |
| mccarthy2.smt2 | Another interpolation example from McCarthy's 91 function | mccarthy2.smt2 (Checksum: SHA 256 ) |
| UsageStub.java | Small API usage example from the usage section of the tool paper | UsageStub.java (Checksum: SHA 256 ) |
| InterpolationUsageStub.java | Small API usage example from the interpolation section of the tool paper | InterpolationUsageStub.java (Checksum: SHA 256 ) |
| fmcad11.tar.bz2 | Interpolation examples from the paper Interpolants from Z3 proofs | fmcad11.tar.bz2 (Checksum: SHA 256 ) |
| interpolationtests.tar.bz2 | Small interpolation tests | interpolationtests.tar.bz2 (Checksum: SHA 256 ) |