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

[Juergen Christ]

Hello Aina,

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

I'm working on the interpolating SMT solver SMTInterpol and know Armin from a 
few meetings at conferences and workshops.  It's great news to hear that there 
is a delta debugger for SMTLIBv2.

> 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.

Unfortunately, I have a bug report which is actually just a bug we encountered 
in SMTInterpol as well.  SMTLIBv2 supports the :named annotation to define a 
name for a closed sub-formula.  You don't seem to support this.  Find attached 
an example using the :named construct.  The problem here is that this new name 
can be used in further commands and terms just like the function symbol has 
been defined with define-fun.  We actually map the :named annotation to 
define-fun internally.  Since most users of SMTInterpol use the :named-
construct, it would be nice for us to have support for it in ddSMT as well.  
Could you add that?

Regards,

Juergen Christ
-------------- next part --------------
(set-logic QF_LIA)
(declare-fun x () Int)
(assert (! (>= x 0) :named bug))
(assert (not bug))
(check-sat)
(exit)