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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
