[SMT-COMP] SMT Benchmark from Ultimate Automizer

[Christoph Wintersteiger]

Hi Matthias,

Thanks for these benchmarks too! I've added them to our *-pending repository as well. 

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: smt-comp-bounces at cs.nyu.edu [mailto:smt-comp-bounces at cs.nyu.edu] On Behalf Of Matthias Heizmann
Sent: 02 May 2017 11:36
To: Clark Barrett <barrett at cs.stanford.edu>; Pascal Fontaine <Pascal.Fontaine at loria.fr>; Cesare Tinelli <cesare-tinelli at uiowa.edu>
Cc: smt-comp at cs.nyu.edu
Subject: [SMT-COMP] SMT Benchmark from Ultimate Automizer

Hi Cesare, Clark and Pascal,

I would like to submit the following benchmarks.
https://na01.safelinks.protection.outlook.com/?url=http:%2F%2Fwww2.informatik.uni-freiburg.de%2F~heizmann%2F20170501-UltimateSmtBenchmarks.tar.xz&data=02%7C01%7Ccwinter%40microsoft.com%7C9fc41428b09a49514a2408d491497ea9%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636293192230302654&sdata=fYHMF4RT7hRpvFNFhJgUWiJDgfXo1TiRUtbxAIv3Cu8%3D&reserved=0

The archive contains non-incremental benchmarks for
    BV, QF_BV, QF_LRA, QF_NRA
and incremental benchmarks for
    BV, QF_BV

Please note that these benchmarks reflect only some aspects of our tool's SMT usage. Most SMT scripts that our tool produces contain nested arrays which are currently not allowed in any logic.

Best,
Matthias