[isabelle-dev] Status of HOL/SMT

[Jasmin Christian Blanchette]

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

    I do have an idea what might go wrong. I'll need to investigate it further before committing a patch.

Jasmin