[SMT-LIB] SMT-LIB: Syntax Error in smtlib/logics/QF_UFIDL.smt

[Cesare Tinelli]

Hi Jim,

On Oct 12, 2007, at 2:30 PM, Grundy, Jim D wrote:

> Hi All
>
> There is a syntax error in the file smtlib/logics/QF_UFIDL.smt  
> hosted on
> http://combination.cs.uiowa.edu/smtlib/logics/QF_UFIDL.smt.  The close
> quote on the :language section is missing, which violates the  
> published
> SMT-LIB grammar.
>
Thanks for pointing that out. The error has now been fixed.

> We were using an old version (due to Clark), which was syntactically
> correct, that we downloaded some time back until just recently, so we
> only just noticed this error - which has presumably been there for  
> some
> time.  I'm wondering why other people haven't been complaining about
> this, do other solvers not actually parse the referenced logic files
> when running a benchmark?
>
Most solvers have those theories/logics built-in, which is the whole  
point of SMT ;)
So, no, they do not parse the theory or logic specifications.
It is good to know though that there is at least one tool that parses  
them and checks them out.

Cheers,


Cesare




> All the best
>
> Jim
>
> --
> Jim Grundy, Research Scientist. Intel Corporation, Strategic CAD Labs
> Mail Stop RA2-451, 2501 NW 229th Ave, Hillsboro, OR 97124-5503, USA
> Phone: +1 971 214-1709  Fax: +1 971 214-1771
> Key Fingerprint: 5F8B 8EEC 9355 839C D777  4D42 404A 492A AEF6 15E2
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib