Files for "SMT Proof Checking Using a Logical Framework" by Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. Formal Methods in System Design. 42(1):91-118, February 2013.
DOI 10.1007/s10703-012-0163-3.

---

• The clsat page can be found at this address: http://sites.google.com/site/duckkioe/projects/clsat.
  • The source code of clsat contains the LFSC signatures for QF_IDL.
• The QF_IDL results can be found at: http://smt-exec.org/exec/?jobs=534.
• A read me for the IDL signature can be found here: readme-idl.txt

---

• The following are the signature files used in the QF_LRA experiments:
  • sat.plf
  • smt.plf
  • th_base.plf
  • th_real.plf
  • th_lra.plf
  • th_lra-cvc3.plf
• A read me for this signature can be found here: readme-lra-sig.txt
• The complete results can be found here: results-qf-lra.xls
• The companion report for this work can be found here: report-qf-lra.pdf

---

• The following are the signature files used in the EUF interpolant generation experiments:
  • sat.plf
  • smt.plf
  • color_base.plf
  • color_euf.plf
  • euf_interpolation.plf
• A read me for this signature can be found here: readme-eufi-sig.txt
• Detailed results can be found here: results-eufi.xls

---

• The LFSC binary used for these experiments can be downloaded here: lfsc
• Instructions for using LFSC can be found here: readme-lfsc.txt
• The source code for LFSC can be found here: lfsc_src.zip
• The license for LFSC is here.

---