[isabelle-dev] Status of HOL/SMT

[Makarius]

On Tue, 4 Dec 2012, Jasmin Christian Blanchette wrote:

> Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette:
>
>> The real issue, at the end of the day, seems to be not so much Z3 4.0 
>> in itself but rather the fact that our code often can't parse them. 
>> I've looked into this and saw no quick fix [*].
>
> Oh, Tobias just reminded me that a second issue is the "rewr_conv" 
> change. See Ondra's and Sascha's emails on November 9. If there's no 
> quick resolution on that front, I would suggest simply introducing 
> "rewr_conv_old" in the SMT source code and using that.
>
> Sascha, any progress on that front? Last time you wrote

With the start of December I also started weeding through old mails from 
October/November, so that Nov. 9 breakdown was already on my radar.  So 
far I did not manage to reproduce it, but it might be due to overlay with 
other problems.

The whole rewr_conv isssue was more like a social desaster on two mailing 
lists.  Technically it should be a non-issue.  It was just bad luck that 
it caught me half-way getting on the plane, otherwise I would have sorted 
this triviality out without further notice as usual.


The question which SMT/Z3 version to ship with the release basically has 
time until the new year.


 	Makarius