[SMT-LIB] ddSMT - a delta debugger for SMT-LIB v2

Aina Niemetz aina.niemetz at jku.at
Wed Apr 3 07:46:54 EDT 2013


Dear all,

I'm a PhD student under the supervision of Armin Biere and I'm currently 
working on the SMT solver Boolector.

We, as many others here, have been in need of a SMT-LIB v2 delta 
debugger for quite some time, which is why I've recently been working on 
ddSMT, a delta debugger for SMT-LIB v2. A beta version of ddSMT is now 
available at http://fmv.jku.at/ddsmt.

ddSMT supports all SMT-LIB v2 logics and has been tested on the SMT-LIB 
v2 benchmark set. It is released under the GPLv3 and requires Python 3.2 
(or later). Note that due to major improvements with respect to the 
internal string representation in Python 3.3, it is strongly recommended 
to use Python version 3.3 (or later).

I hope that ddSMT is useful and I'd appreciate any comments, questions, 
suggestions and bug reports.

Thanks,
Aina


More information about the SMT-LIB mailing list