[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks
cwinter at microsoft.com
Fri Apr 28 11:25:54 EDT 2017
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 :-/
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
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
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 (
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.
More information about the SMT-COMP