[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Christoph Wintersteiger]

The 2.5 standard says:

SMT-LIB source files are not limited to the US-ASCII format anymore and can now
consist of Unicode characters. The concrete encoding is currently left unspecified, but
should be a compatible 8-bit extension of the 7-bit US-ASCII set, such as UTF-8.

So, we can keep it as is, as the benchmarks use version 2.5. I guess that means I'll have to figure out why my Emacs doesn't do UTF-8 then :-/

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/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: Delcypher [mailto:delcypher at gmail.com] 
Sent: 28 April 2017 16:08
To: Christoph Wintersteiger <cwinter at microsoft.com>
Cc: Clark Barrett <barrett at cs.stanford.edu>; smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

Hi,

On 28 April 2017 at 14:54, Christoph Wintersteiger <cwinter at microsoft.com> wrote:
> Yes, I downloaded them (old and new) but haven't committed them to the repository yet. I'll run the latest Z3 over them as well, just to make sure everything's in order.
>
> Just a minor point: Rafael Z?hl's name doesn't render right (when I open the file in emacs). Should I change it to Zaehl?

It renders okay for me in both vim and emacs. The ä is UTF-8 (
https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.fileformat.info%2Finfo%2Funicode%2Fchar%2F00E4%2Findex.htm&data=02%7C01%7Ccwinter%40microsoft.com%7Cca045ce0f89746b5609408d48e48588d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636289888753172206&sdata=L5xqgUWdbKZD40DYyI9pgJ2ZVSHqOnrsCFsSATkRd4Y%3D&reserved=0 ).

I'm not sure what encoding is required for SMT-LIBv2.5 files. I'm happy to produce a new version with `ä` replaced with `ae` if you would prefer that. That might help with solvers that don't parse UTF-8 properly.

Thanks,
Dan.