[  download | publications | talks | license ]

ddSMT serves as an input minimizer for Sat Modulo Theories (SMT) benchmarks in SMT-LIB v2 format. It supports all SMT-LIB v2 logics and has been tested on the SMT-LIB v2 benchmark set.

Download

ddSMT is available on GitHub.

Publications

Aina Niemetz, Armin Biere. ddSMT: A Delta Debugger for the SMT-LIB v2 Format. In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), pages 36-45, aff. to SAT'13, Helsinki, Finland, 2013.
[ paper | bibtex ]

Talk Slides

ddSMT: A Delta Debugger for the SMT-LIB v2 Format, SMT Workshop 2013, Helsinki, Finland.

License

ddSMT is developed and maintained by Aina Niemetz.
It is released under the GNU GPLv3 License (see file COPYING, which is part of the distribution).