CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


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