[SMT-LIB] How to submit benchmarks to smtlib

Martin Brain martin.brain at cs.ox.ac.uk
Fri Apr 10 15:22:16 EDT 2015


On Fri, 2015-03-27 at 14:31 +0000, Christoph Wintersteiger wrote:
> I agree, that sounds like a good solution to the logic-naming problem, I'm in favor. 

It sounds good to me as well.  Although I will sound one note of
caution.  Logics have not just been a combination of signatures, they
have also introduced syntactic sugar and restrictions on what sorts and
terms were well defined.  The real challenge is how to handle
restrictions in a modular way.  For this to be a serious proposal,
someone would need to look at the current logics and propose how the
restrictions in them could be handled.

HTH

Cheers,
 - Martin



More information about the SMT-LIB mailing list