[SMT-LIB] Unknown status in Griggio's benchmark (QF_FP)

[Christoph Wintersteiger]

Hi Zhoulai,

No, we haven't updated the status of these benchmarks yet. Technically there may still be bugs in the current solvers, so it didn't feel safe to do so yet. However, as far as I remember, at least MathSAT and Z3 agree on the status, so for now it should be okay to take those as a reference.

Cheers,
Christoph


Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Zhoulai
Sent: 18 December 2015 06:20
To: smt-lib <smt-lib at cs.nyu.edu>
Subject: [SMT-LIB] Unknown status in Griggio's benchmark (QF_FP)

Hi,

I am playing Z3 with Griggio's  benchmark ( https://na01.safelinks.protection.outlook.com/?url=http:%2f%2fwww.cs.nyu.edu%2f~barrett%2fsmtlib%2fQF_FP_Hierarchy.zip%2c&data=01%7C01%7Ccwinter%40064d.mgd.microsoft.com%7C48fbad4d93ce41ff7c9c08d307738828%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=AzVOwtbKyclYJ1eLp2rlbOgBW9wn8JvSw16OFzxhTUY%3d in the QF_FP
folder)

It seems all of these benchmarks have 'unknown status'.  I wonder whether there is a link  where you have already updated the status of these benchmarks to 'sat' or 'unsat'?  Thanks for your help.

--
Zhoulai
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.cs.nyu.edu%2fmailman%2flistinfo%2fsmt-lib&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c48fbad4d93ce41ff7c9c08d307738828%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=A1d9vtkf7%2fsIVCxytYSV5zLz9iBhk7eWRIOdbaw9lao%3d