Towards Satisfiability Modulo Parametric Bit-vectors

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

This site provides our paper Towards Satisfiability Modulo Parametric Bit-vectors and related material published in the Journal of Automated Reasoning (JAR).

This paper is an extended version of our paper at CADE 2019, which can be found here.

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

Downloads

• Paper as published in the Journal of Automated Reasoning (JAR)
• 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