SMTInterpol
an Interpolating SMT Solver
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.
BenchmarkDescriptionDownload
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 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 )
 

Last modified: Wed Mar 22 20:25:10 CET 2017   Valid XHTML 1.0 TransitionalValid CSS!