[SMT-LIB] submitting SMTLIB2 benchmarks?

[Pascal Fontaine]

Dear Ranjit,

we are always looking for benchmarks; and your benchmarks having an 
incremental flavor, I believe they can be valuable for people working on 
incremental solvers.  The sets operation you mention may classify your 
benchmarks outside QF_UFLIA, but they may be recast to UFLIA, or they 
may trigger some interest in new logics. Anyway they are valuable.

SMT-LIB is currently reorganizing itself, and for various reasons the 
process is a bit slow.  The benchmarks will thus not be available 
immediately on the web site.  In order not to forget them, just send 
them to Cesare, Clark or myself (if you want to have an account on a 
system for transferring large files, let me know).

Cesare and Clark may want to add information or correct this message.  I 
am just stepping in the organization.

Thank you for helping us to provide a comprehensive library of problems!

Best,

   Pascal

On 07/20/2013 06:59 AM, Ranjit Jhala wrote:
> Hi all,
>
> I have a bunch of SMTLIB2 benchmarks of the form
>
>    (push . assert* . checksat . pop)*
>
> the queries are QF_UFLIA formulas (though there
> are some which require SET operations like union,
> intersection, subset etc.)
>
> Is there any interest in adding these to the SMTLIB benchmark set? If so,
> could you point me in the right direction?
>
> Many thanks (and apologies if this was the wrong
> place to ask!)
>
> Ranjit Jhala.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib