[isabelle-dev] Status of HOL/SMT
makarius at sketis.net
Tue Dec 4 15:29:50 CET 2012
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
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.
More information about the isabelle-dev