[isabelle-dev] Status of HOL/SMT

[Sascha Boehme]

Hi,

I spent a couple of hours on this issue. Some odd things are going on during normalization of goals in the smt method. I have the feeling that normalization somehow (accidentally?) worked before Tobias' change on rewr_conv, but that it should really be implemented in a different, more stable way. I'll need a bit more time. Everything should be fixed by the end of the year.

Cheers,
Sascha

----- Urspr�ngliche Nachricht -----
Von: Jasmin Christian Blanchette
Gesendet: 04.12.2012 15:07
An: Makarius
Cc: isabelle-dev Mailinglist; Sascha Boehme
Betreff: Re: [isabelle-dev] Status of HOL/SMT

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121204/c190d13d/attachment-0002.html>