[SMT-LIB] Two annotations in NRA

[Christoph Wintersteiger]

Hi all,

For a while now, the current development version of Z3 has returned the "wrong" status on these files:

NRA\keymaera\ETCS-essentials-live-range2.proof-node1046.smt2
NRA\keymaera\reactivity-lemma-node2938.smt2

We think Z3 is right, but I didn't have much time to dig into the details myself yet. Could an NRA expert take a closer look at these?

Thanks!
Christoph

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

[MSFT_logo_Gray DE sized SIG1.png]
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.jpg
Type: image/jpeg
Size: 1168 bytes
Desc: image001.jpg
URL: </pipermail/smt-lib/attachments/20160606/0fd0ffb8/attachment.jpg>