New official release of SMT-LIB benchmark library

27 vues
Accéder directement au premier message non lu

Clark Barrett

non lue,
20 mai 2018, 12:03:0020/05/2018
à smt...@googlegroups.com,smt-...@cs.nyu.edu
A new release of the SMT-LIB benchmark library (2018-05-20) is now available, both on the GitLab server and on StarExec. For this release we have:
  • Fixed minor errors in formatting
  • Removed duplicate benchmarks
  • Updated statuses of 18,739 previously unknown non-incremental benchmarks (based on the results from 2 or more solvers from SMT-COMP'17)
  • Updated 232,167 statuses of previously unknown incremental check-sat calls (based on the results from 2 or more solvers from SMT-COMP'17)
  • Added 3121 new benchmarks in new logics:
    • non-incremental: AUFNIA (3)
    • incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327)
  • Added 7969 new benchmarks in existing logics:
    • non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5), QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807), QF_UFBV (1193)
    • incremental: QF_BV (787), QF_LIA (1)
For details on the changes to SMT-LIB, please check the git logs at:

The SMT-LIB coordinators

Dejan Jovanovic

non lue,
21 mai 2018, 14:06:0921/05/2018
à smt...@googlegroups.com,smt-...@cs.nyu.edu
Hi Clark, 

I’m having trouble checking out the benchmarks:

Cloning into 'QF_NRA'...
fatal: unable to access 'https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git/': server certificate verification failed. CAfile: /etc/ssl/certs/ca-certificates.crt CRLfile: none

The problem is with the server certificate. I can bypass the certificate checking but it would be better to fix this on Iowa side if possible.

Best, Dejan

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To post to this group, send email to smt...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAFOm5sRRVoCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%3Ds58QeQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

Pascal Fontaine

non lue,
22 mai 2018, 04:22:2222/05/2018
à Dejan Jovanovic,smt...@googlegroups.com,smt-...@cs.nyu.edu
Hi All,

I am not an expert in https (and in particular, I do not know how to manage an https server so that certificates are handled seamlessly), but maybe this helps (for linux, under administrator user):
echo -n | openssl s_client -showcerts -connect clc-gitlab.cs.uiowa.edu:2443 2>/dev/null  | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' >> /etc/ssl/certs/ca-certificates.crt
Afaik, it downloads the necessary certificates manually.  Of course, do not do this if you suspect a man in the middle.

Best,

  Pascal



On 05/21/2018 07:49 PM, Dejan Jovanovic wrote:
Hi Clark, 

I’m having trouble checking out the benchmarks:

$ git clone https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git
Cloning into 'QF_NRA'...
fatal: unable to access 'https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git/': server certificate verification failed. CAfile: /etc/ssl/certs/ca-certificates.crt CRLfile: none

The problem is with the server certificate. I can bypass the certificate checking but it would be better to fix this on Iowa side if possible.

Best, Dejan


On May 20, 2018, at 12:02 PM, Clark Barrett <bar...@cs.stanford.edu>
 wrote:

A new release of the SMT-LIB benchmark library (2018-05-20) is now available, both on the GitLab <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2Fexplore%2Fgroups&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=UttU%2FwCFXE%2FacGwsfeQr2c98q5A0e8Qkrbr8h5tdpOY%3D&reserved=0> server and on StarExec <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.starexec.org%2Fstarexec%2Fsecure%2Fexplore%2Fspaces.jsp%3Fid%3D234826&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=HNCCS8M%2B%2F08%2Bku%2FHcpWcDrK7SCFfP8jBfX2iXdfzEBk%3D&reserved=0>. For this release we have:
Fixed minor errors in formatting
Removed duplicate benchmarks
Updated statuses of 18,739 previously unknown non-incremental benchmarks (based on the results from 2 or more solvers from SMT-COMP'17)
Updated 232,167 statuses of previously unknown incremental check-sat calls (based on the results from 2 or more solvers from SMT-COMP'17)
Added 3121 new benchmarks in new logics:
non-incremental: AUFNIA (3)
incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327)
Added 7969 new benchmarks in existing logics:
non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5), QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807), QF_UFBV (1193)
incremental: QF_BV (787), QF_LIA (1)
For details on the changes to SMT-LIB, please check the git logs at:
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=0UplFbVxxbjYDbNV%2BAx9m00rld7OGKy%2BKI41Od6hEYc%3D&reserved=0> and
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks-inc&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=ecgaj6J1yXrnZmYMVmZ08hIDzgIUAsAnxz%2BkveiYLuo%3D&reserved=0>

The SMT-LIB coordinators

-- 
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com <mailto:smt-lib+u...@googlegroups.com>.
To post to this group, send email to smt...@googlegroups.com <mailto:smt...@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAFOm5sRRVoCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%3Ds58QeQ%40mail.gmail.com <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fsmt-lib%2FCAFOm5sRRVoCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%253Ds58QeQ%2540mail.gmail.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=0U8quxNr3kbIiNs7k7%2F57SZKnBVVX3Zvk4ICdgcsBNY%3D&reserved=0>.
For more options, visit https://groups.google.com/d/optout <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Foptout&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=6XaRCUIwjHgJsVavubyb276vIm%2B%2BhcdTRlHWuKJHrkQ%3D&reserved=0>.


      

      

      

      
_______________________________________________
SMT-COMP mailing list
SMT-...@cs.nyu.edu
https://cs.nyu.edu/mailman/listinfo/smt-comp


    

    


    

  



Dejan Jovanović
non lue,
22 mai 2018, 14:07:3022/05/2018
à Pascal Fontaine,smt-...@cs.nyu.edu,smt...@googlegroups.com
A user can disable SSL certificate checking with



|git config --global http.sslVerify false|



I'm OK doing this myself, but for SMTLIB distribution it would be better if users don't have to do this.



As far as reproducing the issue, I think Iowa computers might be setup to trust the Iowa certificates so just try from outside the Iowa network.



Dejan





On 05/22/2018 04:22 AM, Pascal Fontaine wrote:

> Hi All,

>

> I am not an expert in https (and in particular, I do not know how to

> manage an https server so that certificates are handled seamlessly), but

> maybe this helps (for linux, under administrator user):

> echo -n | openssl s_client -showcerts -connect

> clc-gitlab.cs.uiowa.edu:2443 2>/dev/null  | sed -ne '/-BEGIN

> CERTIFICATE-/,/-END CERTIFICATE-/p' >> /etc/ssl/certs/ca-certificates.crt

> Afaik, it downloads the necessary certificates manually.  Of course, do

> not do this if you suspect a man in the middle.

>

> Best,

>

>    Pascal

>

>

> On 05/21/2018 07:49 PM, Dejan Jovanovic wrote:

> > Hi Clark,

> >

> > I’m having trouble checking out the benchmarks:

> >

> > $ git clonehttps://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git

> > Cloning into 'QF_NRA'...

> > fatal: unable to access 'https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git/': server certificate verification failed. CAfile: /etc/ssl/certs/ca-certificates.crt CRLfile: none

> >

> > The problem is with the server certificate. I can bypass the certificate checking but it would be better to fix this on Iowa side if possible.

> >

> > Best, Dejan

> >

> >> On May 20, 2018, at 12:02 PM, Clark Barrett<bar...@cs.stanford.edu>  wrote:

> >>

> >> A new release of the SMT-LIB benchmark library (2018-05-20) is now available, both on the GitLab<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2Fexplore%2Fgroups&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=UttU%2FwCFXE%2FacGwsfeQr2c98q5A0e8Qkrbr8h5tdpOY%3D&reserved=0>  server and on StarExec<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.starexec.org%2Fstarexec%2Fsecure%2Fexplore%2Fspaces.jsp%3Fid%3D234826&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=HNCCS8M%2B%2F08%2Bku%2FHcpWcDrK7SCFfP8jBfX2iXdfzEBk%3D&reserved=0>. For this release we have:

> >> Fixed minor errors in formatting

> >> Removed duplicate benchmarks

> >> Updated statuses of 18,739 previously unknown non-incremental benchmarks (based on the results from 2 or more solvers from SMT-COMP'17)

> >> Updated 232,167 statuses of previously unknown incremental check-sat calls (based on the results from 2 or more solvers from SMT-COMP'17)

> >> Added 3121 new benchmarks in new logics:

> >> non-incremental: AUFNIA (3)

> >> incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327)

> >> Added 7969 new benchmarks in existing logics:

> >> non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5), QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807), QF_UFBV (1193)

> >> incremental: QF_BV (787), QF_LIA (1)

> >> For details on the changes to SMT-LIB, please check the git logs at:

> >> https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks  <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=0UplFbVxxbjYDbNV%2BAx9m00rld7OGKy%2BKI41Od6hEYc%3D&reserved=0>  and

> >> https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc  <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks-inc&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=ecgaj6J1yXrnZmYMVmZ08hIDzgIUAsAnxz%2BkveiYLuo%3D&reserved=0>

> >>

> >> The SMT-LIB coordinators

> >>

> >> --

> >> You received this message because you are subscribed to the Google Groups "SMT-LIB" group.

> >> To unsubscribe from this group and stop receiving emails from it, send an email tosmt-lib+...@googlegroups.com  <mailto:smt-lib+u...@googlegroups.com>.

> >> To post to this group, send email tosm...@googlegroups.com  <mailto:smt...@googlegroups.com>.

> >> To view this discussion on the web visithttps://groups.google.com/d/msgid/smt-lib/CAFOm5sRRVoCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%3Ds58QeQ%40mail.gmail.com  <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fsmt-lib%2FCAFOm5sRRVoCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%253Ds58QeQ%2540mail.gmail.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=0U8quxNr3kbIiNs7k7%2F57SZKnBVVX3Zvk4ICdgcsBNY%3D&reserved=0>.

> >> For more options, visithttps://groups.google.com/d/optout  <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Foptout&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=6XaRCUIwjHgJsVavubyb276vIm%2B%2BhcdTRlHWuKJHrkQ%3D&reserved=0>.

Clark Barrett
non lue,
22 mai 2018, 14:23:5422/05/2018
à smt...@googlegroups.com,smt-...@cs.nyu.edu
---------- Forwarded message ----------
From: Dejan Jovanović <dejan.j...@sri.com>
Date: Tue, May 22, 2018 at 11:20 AM
Subject: Re: [SMT-COMP] [smt-lib] New official release of SMT-LIB benchmark library
To: Clark Barrett <bar...@cs.stanford.edu>
Cc: Pascal Fontaine <Pascal....@inria.fr>, Cesare Tinelli <cesare-...@uiowa.edu>


Ooops, sorry.



Turns out my computers are all running old version of Ubuntu with outdated certificates.



Disregard, sorry for the confusion!



Dejan



On 05/22/2018 02:13 PM, Clark Barrett wrote:



Removing this from the list for now while we try to get to the bottom of it.



Dejan - we are still having trouble reproducing the issue.  I tried the git clone command you sent from both Stanford computers and NYU computers and it worked fine - I don't get the error.  As far as I know, I don't have anything special configured to trust Iowa, but I'm not an expert so I might be missing something.



-Clark



On Tue, May 22, 2018 at 10:43 AM, Dejan Jovanović <dejan.j...@sri.com <mailto:dejan.j...@sri.com>> wrote:



    A user can disable SSL certificate checking with



    |git config --global http.sslVerify false|



    I'm OK doing this myself, but for SMTLIB distribution it would be

    better if users don't have to do this.



    As far as reproducing the issue, I think Iowa computers might be

    setup to trust the Iowa certificates so just try from outside the

    Iowa network.



    Dejan





    On 05/22/2018 04:22 AM, Pascal Fontaine wrote:



        Hi All,



        I am not an expert in https (and in particular, I do not know how to

        manage an https server so that certificates are handled

        seamlessly), but

        maybe this helps (for linux, under administrator user):

        echo -n | openssl s_client -showcerts -connect

        clc-gitlab.cs.uiowa.edu:2443


        2>/dev/null  | sed -ne '/-BEGIN

        CERTIFICATE-/,/-END CERTIFICATE-/p' >>

        /etc/ssl/certs/ca-certificates.crt

        Afaik, it downloads the necessary certificates manually.  Of

        course, do

        not do this if you suspect a man in the middle.



        Best,



            Pascal





        On 05/21/2018 07:49 PM, Dejan Jovanovic wrote:

        > Hi Clark,

        >

        > I’m having trouble checking out the benchmarks:

        >

         > $ git

        clonehttps://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git


        > Cloning into 'QF_NRA'...

        > fatal: unable to access 'https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_NRA.git/


        server certificate verification failed. CAfile:

        /etc/ssl/certs/ca-certificates.crt CRLfile: none

        >

        > The problem is with the server certificate. I can bypass the certificate checking but it would be better to fix this on Iowa side if possible.

        >

        > Best, Dejan

        >

        >> On May 20, 2018, at 12:02 PM, Clark Barrett<bar...@cs.stanford.edu <mailto:bar...@cs.stanford.edu>>  wrote:

        >>

        >> A new release of the SMT-LIB benchmark library (2018-05-20) is now available, both on the GitLab<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2Fexplore%2Fgroups&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=UttU%2FwCFXE%2FacGwsfeQr2c98q5A0e8Qkrbr8h5tdpOY%3D&reserved=0

        <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2Fexplore%2Fgroups&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=UttU%2FwCFXE%2FacGwsfeQr2c98q5A0e8Qkrbr8h5tdpOY%3D&reserved=0>>         server and on

        StarExec<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.starexec.org%2Fstarexec%2Fsecure%2Fexplore%2Fspaces.jsp%3Fid%3D234826&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=HNCCS8M%2B%2F08%2Bku%2FHcpWcDrK7SCFfP8jBfX2iXdfzEBk%3D&reserved=0

        <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.starexec.org%2Fstarexec%2Fsecure%2Fexplore%2Fspaces.jsp%3Fid%3D234826&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=HNCCS8M%2B%2F08%2Bku%2FHcpWcDrK7SCFfP8jBfX2iXdfzEBk%3D&reserved=0>>.

        For this release we have:

        >> Fixed minor errors in formatting

        >> Removed duplicate benchmarks

        >> Updated statuses of 18,739 previously unknown non-incremental benchmarks (based on the results from 2 or more solvers from SMT-COMP'17)

        >> Updated 232,167 statuses of previously unknown incremental check-sat calls (based on the results from 2 or more solvers from SMT-COMP'17)

        >> Added 3121 new benchmarks in new logics:

        >> non-incremental: AUFNIA (3)

        >> incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327)

        >> Added 7969 new benchmarks in existing logics:

        >> non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5), QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807), QF_UFBV (1193)

        >> incremental: QF_BV (787), QF_LIA (1)

        >> For details on the changes to SMT-LIB, please check the git logs at:

        >> https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks


        <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks-inc&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=ecgaj6J1yXrnZmYMVmZ08hIDzgIUAsAnxz%2BkveiYLuo%3D&reserved=0>>

        >>

        >> The SMT-LIB coordinators

        >>

        >> --

        >> You received this message because you are subscribed to the Google Groups "SMT-LIB" group.

         >> To unsubscribe from this group and stop receiving emails

        from it, send an email tosmt-lib+unsubscribe@googlegroups.com

        <mailto:tosmt-lib%2Bunsubscribe...@googlegroups.com>         <mailto:smt-lib+unsubscribe@googlegroups.com

        <mailto:smt-lib%2Bunsubscribe@googlegroups.com>>.


         >> To post to this group, send email tosm...@googlegroups.com

        <mailto:tosmt-lib@googlegroups.com>         <mailto:smt-lib@googlegroups.com <mailto:smt-lib@googlegroups.com>>.


         >> To view this discussion on the web

        visithttps://groups.google.com/d/msgid/smt-lib/CAFOm5sRRVoCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%3Ds58QeQ%40mail.gmail.com

        > SMT-...@cs.nyu.edu <mailto:SMT-...@cs.nyu.edu>

        > https://cs.nyu.edu/mailman/listinfo/smt-comp

        <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcs.nyu.edu%2Fmailman%2Flistinfo%2Fsmt-comp&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cc3514dacbd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=GByzlM%2Byd5MyMtCobyF55EDRjaMJykwZmQtfAwI4izM%3D&reserved=0>







    _______________________________________________

    SMT-COMP mailing list

    SMT-...@cs.nyu.edu <mailto:SMT-...@cs.nyu.edu>

    https://cs.nyu.edu/mailman/listinfo/smt-comp

    <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcs.nyu.edu%2Fmailman%2Flistinfo%2Fsmt-comp&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cc3514dacbd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=GByzlM%2Byd5MyMtCobyF55EDRjaMJykwZmQtfAwI4izM%3D&reserved=0>











Bruno Dutertre
non lue,
23 mai 2018, 15:14:1023/05/2018
à smt...@googlegroups.com,Clark Barrett,smt-...@cs.nyu.edu
On 5/20/18 9:02 AM, Clark Barrett wrote:

> A new release of the SMT-LIB benchmark library (2018-05-20) is now

> available, both on the GitLab server and on StarExec.

> For this release we have:

> 

>     - Fixed minor errors in formatting

>     - Removed duplicate benchmarks

>     - Updated statuses of 18,739 previously unknown non-incremental

>     benchmarks (based on the results from 2 or more solvers from SMT-COMP'17)

>     - Updated 232,167 statuses of previously unknown incremental check-sat

>     calls (based on the results from 2 or more solvers from SMT-COMP'17)

>     - Added 3121 new benchmarks in new logics:

>     - non-incremental: AUFNIA (3)

>        - incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327)

>     - Added 7969 new benchmarks in existing logics:

>     - non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5),

>        QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807),

>        QF_UFBV (1193)

>        - incremental: QF_BV (787), QF_LIA (1)

> 



Clark,



The following new benchmarks in QF_UF are mislabeled:



20170829-Rodin/smt2831655880469397696.smt2

20170829-Rodin/smt3232867547761696161.smt2

20170829-Rodin/smt3248576982810563470.smt2

20170829-Rodin/smt3508124013603727984.smt2

20170829-Rodin/smt3809952321495040629.smt2

20170829-Rodin/smt3910673230463462036.smt2

20170829-Rodin/smt4027072204816894856.smt2

20170829-Rodin/smt4241633917533372498.smt2

20170829-Rodin/smt4480564921249140261.smt2

20170829-Rodin/smt6109211130895037835.smt2

20170829-Rodin/smt6377531776677660648.smt2

20170829-Rodin/smt834303034702425531.smt2

20170829-Rodin/smt862177804180920815.smt2

20170829-Rodin/smt8855268942650190404.smt2



They are all marked unsat but they are all sat.

This can be easily seen by inspection or by running

CVC4, mathsat, yices, z3 on them.



Bruno

Clark Barrett
non lue,
23 mai 2018, 17:36:4223/05/2018
à Bruno Dutertre,smt...@googlegroups.com,smt-...@cs.nyu.edu
Thank you Bruno for this report.  These benchmarks have now been fixed on the GitLab server.

We also fixed three QF_FP benchmarks on GitLab:

Removed an unused declare-sort command from:
griggio/fmcad12/f23.smt2

Removed from QF_FP because they use uninterpreted functions (will look into adding again next year):
schanda/spark/O402-020_1.smt2
schanda/spark/O402-020_2.smt2

We haven't yet updated StarExec with these fixes.  We will probably wait to see if any other minor issues are reported and then make a patch to StarExec early next week.  I will be sure to report any additional updates on the SMT-LIB and SMT-COMP mailing lists.

-Clark
Clark Barrett
non lue,
29 mai 2018, 14:25:1629/05/2018
à smt...@googlegroups.com,smt-...@cs.nyu.edu
A few minor updates have been made to SMT-LIB since the release on May 20.  These updates have been committed to GitLab and the affected benchmarks have been updated on StarExec.  If you have cloned one of the affected directories, you may want to grab a new copy.  All updates are to non-incremental benchmarks and are detailed below:

1. Rename "reset" to "reset_" as reset is a reserved word in SMT-LIB.  Affected benchmarks:

UFNIA/vcc-havoc/baby.34.vamp_step.smt2
UFNIA/vcc-havoc/verisoft-baby.c.35.vamp_step.smt2
UFNIA/vcc-havoc/verisoft-vamp.c.35.vamp_step.smt2

2. Update incorrect statuses.  Affected benchmarks:

QF_UF/20170829-Rodin/smt2831655880469397696.smt2
QF_UF/20170829-Rodin/smt3232867547761696161.smt2
QF_UF/20170829-Rodin/smt3248576982810563470.smt2
QF_UF/20170829-Rodin/smt3508124013603727984.smt2
QF_UF/20170829-Rodin/smt3809952321495040629.smt2
QF_UF/20170829-Rodin/smt3910673230463462036.smt2
QF_UF/20170829-Rodin/smt4027072204816894856.smt2
QF_UF/20170829-Rodin/smt4241633917533372498.smt2
QF_UF/20170829-Rodin/smt4480564921249140261.smt2
QF_UF/20170829-Rodin/smt6109211130895037835.smt2
QF_UF/20170829-Rodin/smt6377531776677660648.smt2
QF_UF/20170829-Rodin/smt834303034702425531.smt2
QF_UF/20170829-Rodin/smt862177804180920815.smt2
QF_UF/20170829-Rodin/smt8855268942650190404.smt2

3. Remove unused "declare-sort".  Affected benchmark:

QF_FP/griggio/fmcad12/f23.smt2

4. Remove benchmarks using uninterpreted functions from QF_FP.  Affected benchmarks:

QF_FP/schanda/spark/O402-020_1.smt2
QF_FP/schanda/spark/O402-020_2.smt2



Répondre à tous
Répondre à l'auteur
Transférer
0 nouveau message