Towards Bit-Width-Independent Proofs in SMT Solvers

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli

This site provides our paper Towards Bit-Width-Independent Proofs in SMT Solvers and related material at CADE 2019.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

• Paper at CADE 2019
• README for the artifact
• Artifact [tar.xz] all materials
• Binaries:
  • CVC4 Binary [tar.xz]
    
    • configuration 1: --nl-ext-planes
    • configuration 2: --nl-ext-tplanes --full-saturate-quant --no-e-matching
  • Vampire Binary [tar.xz]
    configuration: ----ignore_missing on --mode smtcomp --cores 4
  • Z3 Binary [tar.xz]
    configuration: default