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

[Aina Niemetz]

Hello Juergen,

ddSMT now supports named annotations. Current version is 0.92-beta.
Please let me know if you run into troubles.

Best,
Aina


On 04/05/2013 03:49 PM, Aina Niemetz wrote:
> Hello Juergen,
>
> thanks a lot for your feedback!
>
>> 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?
>
> Sounds like a reasonable feature request! I'll add this as soon as
> possible.
>
> I'll keep you updated,
> Aina
>