[SMT-COMP] Fwd: [smt-lib] New official release of SMT-LIB benchmark library

Clark Barrett barrett at cs.stanford.edu
Tue May 22 14:23:18 EDT 2018


---------- Forwarded message ----------
From: Dejan Jovanović <dejan.jovanovic at 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 <barrett at cs.stanford.edu>
Cc: Pascal Fontaine <Pascal.Fontaine at inria.fr>, Cesare Tinelli <
cesare-tinelli at 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.jovanovic at sri.com
> <mailto:dejan.jovanovic at 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
>         <https://na01.safelinks.protection.outlook.com/?url=http%3A%
> 2F%2Fclc-gitlab.cs.uiowa.edu%3A2443&data=01%7C01%7Cdejan.
> jovanovic%40sri.com%7Cc3514dacbd974d4fd8a808d5c00fd6d1%7C407
> 79d3379c44626b8bf140c4d5e9075%7C1&sdata=4r0s9O47dO2%2BxWukJU
> gXdNBwr%2F9hQi%2FQcmMyou8sPhQ%3D&reserved=0>
>         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
>         <https://na01.safelinks.protection.outlook.com/?url=http%3A%
> 2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks%
> 2FQF_NRA.git&data=01%7C01%7Cdejan.jovanovic%40sri.com%7C
> c3514dacbd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8bf140c4
> d5e9075%7C1&sdata=RAK3HkkztFaf1975rSYaQxj1wEuB07Feze0tMjCzyB
> w%3D&reserved=0>
>         > Cloning into 'QF_NRA'...
>         > fatal: unable to access 'https://clc-gitlab.cs.uiowa.e
> du:2443/SMT-LIB-benchmarks/QF_NRA.git/
>         <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmark
> s%2FQF_NRA.git%2F&data=01%7C01%7Cdejan.jovanovic%40sri.
> com%7Cc3514dacbd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8b
> f140c4d5e9075%7C1&sdata=fpkfuPYT7oafR3YmgPYEptkMMF9CwmcTmmxz
> cmUM%2B0A%3D&reserved=0>':
>         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<
> barrett at cs.stanford.edu <mailto:barrett at 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.uiow
> a.edu%3A2443%2Fexplore%2Fgroups&data=01%7C01%7Cdejan.jovanov
> ic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C40779d3379
> c44626b8bf140c4d5e9075%7C1&sdata=UttU%2FwCFXE%2FacGwsfeQr
> 2c98q5A0e8Qkrbr8h5tdpOY%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%7Cab65c259f67e47565
> 38208d5be6b29db%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%7C407
> 79d3379c44626b8bf140c4d5e9075%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%7C40779d3379c4
> 4626b8bf140c4d5e9075%7C1&sdata=HNCCS8M%2B%2F08%2Bku%2FH
> cpWcDrK7SCFfP8jBfX2iXdfzEBk%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-benchmark
> s&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cc3514dac
> bd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8bf140c4d5e9075%
> 7C1&sdata=LKA4uiFHeZrgDgN3y1qvAuUsQnutT%2BZGJHFKyX1oy0M%3D&reserved=0>
>      <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmark
> s&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259
> f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%
> 7C1&sdata=0UplFbVxxbjYDbNV%2BAx9m00rld7OGKy%2BKI41Od6hEYc%3D&reserved=0
>         <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmark
> s&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259
> f67e4756538208d5be6b29db%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-benchmark
> s-inc&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cc3514dac
> bd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8bf140c4d5e9075%
> 7C1&sdata=Z2U4hTzvuvSbcD7N4Pkg6aikE1IyD1BETQR1rfmOvHI%3D&reserved=0>
>    <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmark
> s-inc&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259
> f67e4756538208d5be6b29db%7C40779d3379c44626b8bf140c4d5e9075%
> 7C1&sdata=ecgaj6J1yXrnZmYMVmZ08hIDzgIUAsAnxz%2BkveiYLuo%3D&reserved=0
>         <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fclc-gitlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmark
> s-inc&data=01%7C01%7Cdejan.jovanovic%40sri.com%7Cab65c259
> f67e4756538208d5be6b29db%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 at googlegroups.com
>         <mailto:tosmt-lib%2Bunsubscribe at googlegroups.com>         <mailto:
> smt-lib+unsubscribe at googlegroups.com
>         <mailto:smt-lib%2Bunsubscribe at googlegroups.com>>.
>          >> To post to this group, send email tosmt-lib at googlegroups.com
>         <mailto:tosmt-lib at googlegroups.com>         <mailto:
> smt-lib at googlegroups.com <mailto:smt-lib at googlegroups.com>>.
>          >> To view this discussion on the web
>         visithttps://groups.google.com/d/msgid/smt-lib/CAFOm5sRRVoCk
> dh9WNnFy7N-m9OTUKkncru-a56AWvfq%3Ds58QeQ%40mail.gmail.com
>         <https://na01.safelinks.protection.outlook.com/?url=http%3A%
> 2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fsmt-lib%2FCAFOm5sRRV
> oCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%253Ds58QeQ%2540mail.
> gmail.com&data=01%7C01%7Cdejan.jovanovic%40sri.com%7C
> c3514dacbd974d4fd8a808d5c00fd6d1%7C40779d3379c44626b8bf140c4
> d5e9075%7C1&sdata=SycQV3iIUAl2yGvdl%2B9sJXrv3KDSNNdH0mGDm8mL
> EhQ%3D&reserved=0>         <https://na01.safelinks.prote
> ction.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%7C407
> 79d3379c44626b8bf140c4d5e9075%7C1&sdata=0U8quxNr3kbIiNs7k7%2
> F57SZKnBVVX3Zvk4ICdgcsBNY%3D&reserved=0
>         <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fsmt-lib%2FCAFOm5sRRV
> oCkdh9WNnFy7N-m9OTUKkncru-a56AWvfq%253Ds58QeQ%2540mail.
> gmail.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=01%7C01%7Cdejan.
> jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C407
> 79d3379c44626b8bf140c4d5e9075%7C1&sdata=0U8quxNr3kbIiNs7k7%2
> F57SZKnBVVX3Zvk4ICdgcsBNY%3D&reserved=0>>.
>          >> For more options, visithttps://groups.google.com/d/optout
>         <https://na01.safelinks.protection.outlook.com/?url=http%3A%
> 2F%2Fgroups.google.com%2Fd%2Foptout&data=01%7C01%7Cdejan.
> jovanovic%40sri.com%7Cc3514dacbd974d4fd8a808d5c00fd6d1%7C407
> 79d3379c44626b8bf140c4d5e9075%7C1&sdata=COuJPVdDYHY2rW08cfLa
> WrcId4SYYDUDPKCN8Ru2l2M%3D&reserved=0>         <
> https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fgroups.google.com%2Fd%2Foptout&data=01%7C01%7Cdejan.
> jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C407
> 79d3379c44626b8bf140c4d5e9075%7C1&sdata=6XaRCUIwjHgJsVavubyb
> 276vIm%2B%2BhcdTRlHWuKJHrkQ%3D&reserved=0
>         <https://na01.safelinks.protection.outlook.com/?url=https%
> 3A%2F%2Fgroups.google.com%2Fd%2Foptout&data=01%7C01%7Cdejan.
> jovanovic%40sri.com%7Cab65c259f67e4756538208d5be6b29db%7C407
> 79d3379c44626b8bf140c4d5e9075%7C1&sdata=6XaRCUIwjHgJsVavubyb
> 276vIm%2B%2BhcdTRlHWuKJHrkQ%3D&reserved=0>>.
>         >
>         >
>         > _______________________________________________
>         > SMT-COMP mailing list
>         > SMT-COMP at cs.nyu.edu <mailto:SMT-COMP at 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%7Cc3514dacbd974d4fd8a808d5
> c00fd6d1%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=
> GByzlM%2Byd5MyMtCobyF55EDRjaMJykwZmQtfAwI4izM%3D&reserved=0>
>
>
>
>     _______________________________________________
>     SMT-COMP mailing list
>     SMT-COMP at cs.nyu.edu <mailto:SMT-COMP at 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%7Cc3514dacbd974d4fd8a808d5
> c00fd6d1%7C40779d3379c44626b8bf140c4d5e9075%7C1&sdata=
> GByzlM%2Byd5MyMtCobyF55EDRjaMJykwZmQtfAwI4izM%3D&reserved=0>
>
>
>


More information about the SMT-COMP mailing list